Theory IsaSAT_Inner_Propagation

theory IsaSAT_Inner_Propagation_Defs imports IsaSAT_Setup IsaSAT_Bump_Heuristics IsaSAT_Clauses IsaSAT_VMTF IsaSAT_LBD begin definition find_non_false_literal_between where ‹find_non_false_literal_between M a b C = find_in_list_between (λL. polarity M L ≠ Some False) a b C› (* TODO change to return the iterator (i) instead of the position in the clause *) definition isa_find_unwatched_between :: ‹_ ⇒ trail_pol ⇒ arena ⇒ nat ⇒ nat ⇒ nat ⇒ (nat option) nres› where ‹isa_find_unwatched_between P M' NU a b C = do { ASSERT(C+a ≤ length NU); ASSERT(C+b ≤ length NU); (x, _) ← WHILE_T⇗λ(found, i). True⇖ (λ(found, i). found = None ∧ i < C + b) (λ(_, i). do { ASSERT(i < C + (arena_length NU C)); ASSERT(i ≥ C); ASSERT(i < C + b); ASSERT(arena_lit_pre NU i); L ← mop_arena_lit NU i; ASSERT(polarity_pol_pre M' L); if P L then RETURN (Some (i - C), i) else RETURN (None, i+1) }) (None, C+a); RETURN x } › definition isa_find_unwatched :: ‹(nat literal ⇒ bool) ⇒ trail_pol ⇒ arena ⇒ nat ⇒ (nat option) nres› where ‹isa_find_unwatched P M' arena C = do { l ← mop_arena_length arena C; b ← RETURN(l ≤ MAX_LENGTH_SHORT_CLAUSE); if b then isa_find_unwatched_between P M' arena 2 l C else do { ASSERT(get_saved_pos_pre arena C); pos ← mop_arena_pos arena C; n ← isa_find_unwatched_between P M' arena pos l C; if n = None then isa_find_unwatched_between P M' arena 2 pos C else RETURN n } } › definition isa_save_pos :: ‹nat ⇒ nat ⇒ isasat ⇒ isasat nres› where ‹isa_save_pos C i = (λS. do { ASSERT(arena_is_valid_clause_idx (get_clauses_wl_heur S) C); if arena_length (get_clauses_wl_heur S) C > MAX_LENGTH_SHORT_CLAUSE then do { ASSERT(isa_update_pos_pre ((C, i), get_clauses_wl_heur S)); let N = arena_update_pos C i (get_clauses_wl_heur S); RETURN (set_clauses_wl_heur N S) } else RETURN S }) › definition mark_conflict_to_rescore :: ‹nat ⇒ isasat ⇒ isasat nres› where ‹mark_conflict_to_rescore C S = do { let M = get_trail_wl_heur S; let N = get_clauses_wl_heur S; let D = get_conflict_wl_heur S; let vm = get_vmtf_heur S; n ← mop_arena_length N C; ASSERT (n ≤ length N); (_, vm) ← WHILE_T (λ(i, vm). i < n) (λ(i, vm). do{ ASSERT (i < n); L ← mop_arena_lit2 N C i; vm ← isa_vmtf_bump_to_rescore_also_reasons_cl M N C (-L) vm; RETURN (i+1, vm) }) (0, vm); let lbd = get_lbd S; (N, lbd) ← calculate_LBD_heur_st M N lbd C; let S = set_vmtf_wl_heur vm S; let S = set_clauses_wl_heur N S; let S = set_lbd_wl_heur lbd S; RETURN S }› definition set_conflict_wl_heur :: ‹nat ⇒ isasat ⇒ isasat nres› where ‹set_conflict_wl_heur = (λC S. do { let n = 0; let M = get_trail_wl_heur S; let N = get_clauses_wl_heur S; let D = get_conflict_wl_heur S; let outl = get_outlearned_heur S; ASSERT(curry5 isa_set_lookup_conflict_aa_pre M N C D n outl); (D, clvls, outl) ← isa_set_lookup_conflict_aa M N C D n outl; j ← mop_isa_length_trail M; let S = IsaSAT_Setup.set_conflict_wl_heur D S; let S = set_outl_wl_heur outl S; let S = set_count_max_wl_heur clvls S; let S = set_literals_to_update_wl_heur j S; RETURN S})› definition update_clause_wl_code_pre where ‹update_clause_wl_code_pre = (λ((((((((L, L'), C), b), j), w), i), f), S). w < length (get_watched_wl_heur S ! nat_of_lit L) )› definition update_clause_wl_heur :: ‹nat literal ⇒ nat literal ⇒ nat ⇒ bool ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ isasat ⇒ (nat × nat × isasat) nres› where ‹update_clause_wl_heur = (λ(L::nat literal) L' C b j w i f S. do { let N = get_clauses_wl_heur S; let W = get_watched_wl_heur S; K' ← mop_arena_lit2' (set (get_vdom S)) N C f; ASSERT(w < length N); N' ← mop_arena_swap C i f N; ASSERT(nat_of_lit K' < length W); ASSERT(length (W ! (nat_of_lit K')) < length N); let W = W[nat_of_lit K':= W ! (nat_of_lit K') @ [(C, L, b)]]; let S = set_watched_wl_heur W S; let S = set_clauses_wl_heur N' S; RETURN (j, w+1, S) })› definition propagate_lit_wl_heur :: ‹nat literal ⇒ nat ⇒ nat ⇒ isasat ⇒ isasat nres› where ‹propagate_lit_wl_heur = (λL' C i S. do { let M = get_trail_wl_heur S; let N = get_clauses_wl_heur S; let heur = get_heur S; ASSERT(i ≤ 1); M ← cons_trail_Propagated_tr L' C M; N' ← mop_arena_swap C 0 (1 - i) N; heur ← mop_save_phase_heur (atm_of L') (is_pos L') heur; let S = set_trail_wl_heur M S; let S = set_clauses_wl_heur N' S; let S = set_heur_wl_heur heur S; RETURN S })› definition propagate_lit_wl_bin_heur :: ‹nat literal ⇒ nat ⇒ isasat ⇒ isasat nres› where ‹propagate_lit_wl_bin_heur = (λL' C S. do { let M = get_trail_wl_heur S; let heur = get_heur S; M ← cons_trail_Propagated_tr L' C M; heur ← mop_save_phase_heur (atm_of L') (is_pos L') heur; let S = set_trail_wl_heur M S; let S = set_heur_wl_heur heur S; RETURN S })› definition unit_prop_body_wl_heur_inv where ‹unit_prop_body_wl_heur_inv S j w L ⟷ (∃S'. (S, S') ∈ twl_st_heur ∧ unit_prop_body_wl_inv S' j w L)› definition unit_prop_body_wl_D_find_unwatched_heur_inv where ‹unit_prop_body_wl_D_find_unwatched_heur_inv f C S ⟷ (∃S'. (S, S') ∈ twl_st_heur ∧ unit_prop_body_wl_find_unwatched_inv f C S')› definition keep_watch_heur where ‹keep_watch_heur = (λL i j S. do { let W = get_watched_wl_heur S; ASSERT(nat_of_lit L < length W); ASSERT(i < length (W ! nat_of_lit L)); ASSERT(j < length (W ! nat_of_lit L)); let W = W[nat_of_lit L := (W!(nat_of_lit L))[i := W ! (nat_of_lit L) ! j]]; RETURN (set_watched_wl_heur W S) })› definition update_blit_wl_heur :: ‹nat literal ⇒ nat ⇒ bool ⇒ nat ⇒ nat ⇒ nat literal ⇒ isasat ⇒ (nat × nat × isasat) nres› where ‹update_blit_wl_heur = (λ(L::nat literal) C b j w K S. do { let W = get_watched_wl_heur S; ASSERT(nat_of_lit L < length W); ASSERT(j < length (W ! nat_of_lit L)); ASSERT(j < length (get_clauses_wl_heur S)); ASSERT(w < length (get_clauses_wl_heur S)); let W = W[nat_of_lit L := (W!nat_of_lit L)[j:= (C, K, b)]]; RETURN (j+1, w+1, set_watched_wl_heur W S) })› definition pos_of_watched_heur :: ‹isasat⇒ nat ⇒ nat literal ⇒ nat nres› where ‹pos_of_watched_heur S C L = do { L' ← mop_access_lit_in_clauses_heur S C 0; RETURN (if L = L' then 0 else 1) }› definition unit_propagation_inner_loop_wl_loop_D_heur_inv0 where ‹unit_propagation_inner_loop_wl_loop_D_heur_inv0 L = (λ(j, w, S'). ∃S. (S', S) ∈ twl_st_heur ∧ unit_propagation_inner_loop_wl_loop_inv L (j, w, S) ∧ length (watched_by S L) ≤ length (get_clauses_wl_heur S') - MIN_HEADER_SIZE)› definition other_watched_wl_heur :: ‹isasat ⇒ nat literal ⇒ nat ⇒ nat ⇒ nat literal nres› where ‹other_watched_wl_heur S L C i = do { ASSERT(i < 2 ∧ arena_lit_pre2 (get_clauses_wl_heur S) C i ∧ arena_lit (get_clauses_wl_heur S) (C + i) = L ∧ arena_lit_pre2 (get_clauses_wl_heur S) C (1 - i)); mop_access_lit_in_clauses_heur S C (1 - i) }› definition isa_find_unwatched_wl_st_heur :: ‹isasat ⇒ nat ⇒ nat option nres› where ‹isa_find_unwatched_wl_st_heur = (λS i. do { isa_find_unwatched (λL. polarity_pol (get_trail_wl_heur S) L ≠ Some False) (get_trail_wl_heur S) (get_clauses_wl_heur S) i })› definition unit_propagation_inner_loop_body_wl_heur :: ‹nat literal ⇒ nat ⇒ nat ⇒ isasat ⇒ (nat × nat × isasat) nres› where ‹unit_propagation_inner_loop_body_wl_heur L j w S0 = do { ASSERT(unit_propagation_inner_loop_wl_loop_D_heur_inv0 L (j, w, S0)); (C, K, b) ← mop_watched_by_app_heur S0 L w; S ← keep_watch_heur L j w S0; ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0)); val_K ← mop_polarity_st_heur S K; if val_K = Some True then RETURN (j+1, w+1, S) else do { if b then do { if val_K = Some False then do { S ← set_conflict_wl_heur C S; RETURN (j+1, w+1, S)} else do { S ← propagate_lit_wl_bin_heur K C S; RETURN (j+1, w+1, S)} } else do { ―‹Now the costly operations:› ASSERT(clause_not_marked_to_delete_heur_pre (S, C)); if ¬clause_not_marked_to_delete_heur S C then RETURN (j, w+1, S) else do { i ← pos_of_watched_heur S C L; ASSERT(i ≤ 1); L' ← other_watched_wl_heur S L C i; val_L' ← mop_polarity_st_heur S L'; if val_L' = Some True then update_blit_wl_heur L C b j w L' S else do { f ← isa_find_unwatched_wl_st_heur S C; case f of None ⇒ do { if val_L' = Some False then do { S ← set_conflict_wl_heur C S; RETURN (j+1, w+1, S)} else do { S ← propagate_lit_wl_heur L' C i S; RETURN (j+1, w+1, S)} } | Some f ⇒ do { S ← isa_save_pos C f S; ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0)); K ← mop_access_lit_in_clauses_heur S C f; val_L' ← mop_polarity_st_heur S K; if val_L' = Some True then update_blit_wl_heur L C b j w K S else do { update_clause_wl_heur L L' C b j w i f S } } } } } } }› definition unit_propagation_inner_loop_wl_loop_D_heur_inv where ‹unit_propagation_inner_loop_wl_loop_D_heur_inv S₀ L = (λ(j, w, S'). ∃S₀' S. (S₀, S₀') ∈ twl_st_heur ∧ (S', S) ∈ twl_st_heur ∧ unit_propagation_inner_loop_wl_loop_inv L (j, w, S) ∧ L ∈# ℒ_a_l_l (all_atms_st S) ∧ dom_m (get_clauses_wl S) = dom_m (get_clauses_wl S₀') ∧ length (get_clauses_wl_heur S₀) = length (get_clauses_wl_heur S'))› definition unit_propagation_inner_loop_wl_loop_D_heur :: ‹nat literal ⇒ isasat ⇒ (nat × nat × isasat) nres› where ‹unit_propagation_inner_loop_wl_loop_D_heur L S₀ = do { ASSERT(length (watched_by_int S₀ L) ≤ length (get_clauses_wl_heur S₀)); n ← mop_length_watched_by_int S₀ L; WHILE_T⇗unit_propagation_inner_loop_wl_loop_D_heur_inv S₀ L⇖ (λ(j, w, S). w < n ∧ get_conflict_wl_is_None_heur S) (λ(j, w, S). do { unit_propagation_inner_loop_body_wl_heur L j w S }) (0, 0, S₀) }› definition cut_watch_list_heur :: ‹nat ⇒ nat ⇒ nat literal ⇒ isasat ⇒ isasat nres› where ‹cut_watch_list_heur j w L =(λS. do { let W = get_watched_wl_heur S; ASSERT(j ≤ length (W!nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length W ∧ w ≤ length (W ! (nat_of_lit L))); let W = W[nat_of_lit L := take j (W!(nat_of_lit L)) @ drop w (W!(nat_of_lit L))]; RETURN (set_watched_wl_heur W S) })› definition cut_watch_list_heur2 :: ‹nat ⇒ nat ⇒ nat literal ⇒ isasat ⇒ isasat nres› where ‹cut_watch_list_heur2 = (λj w L S. do { let W = get_watched_wl_heur S; ASSERT(j ≤ length (W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length W ∧ w ≤ length (W ! (nat_of_lit L))); let n = length (W!(nat_of_lit L)); (j, w, W) ← WHILE_T⇗λ(j, w, W). j ≤ w ∧ w ≤ n ∧ nat_of_lit L < length W⇖ (λ(j, w, W). w < n) (λ(j, w, W). do { ASSERT(w < length (W!(nat_of_lit L))); RETURN (j+1, w+1, W[nat_of_lit L := (W!(nat_of_lit L))[j := W!(nat_of_lit L)!w]]) }) (j, w, W); ASSERT(j ≤ length (W ! nat_of_lit L) ∧ nat_of_lit L < length W); let W = W[nat_of_lit L := take j (W ! nat_of_lit L)]; RETURN (set_watched_wl_heur W S) })› definition unit_propagation_inner_loop_wl_D_heur :: ‹nat literal ⇒ isasat ⇒ isasat nres› where ‹unit_propagation_inner_loop_wl_D_heur L S₀ = do { (j, w, S) ← unit_propagation_inner_loop_wl_loop_D_heur L S₀; ASSERT(length (watched_by_int S L) ≤ length (get_clauses_wl_heur S₀) - MIN_HEADER_SIZE); cut_watch_list_heur2 j w L S }› definition select_and_remove_from_literals_to_update_wl_heur :: ‹isasat ⇒ (isasat × nat literal) nres› where ‹select_and_remove_from_literals_to_update_wl_heur S = do { ASSERT(literals_to_update_wl_heur S < length (fst (get_trail_wl_heur S))); ASSERT(literals_to_update_wl_heur S + 1 ≤ unat32_max); L ← isa_trail_nth (get_trail_wl_heur S) (literals_to_update_wl_heur S); RETURN (set_literals_to_update_wl_heur (literals_to_update_wl_heur S + 1) S, -L) }› definition unit_propagation_outer_loop_wl_D_heur_inv :: ‹isasat ⇒ isasat ⇒ bool› where ‹unit_propagation_outer_loop_wl_D_heur_inv S₀ S' ⟷ (∃S₀' S. (S₀, S₀') ∈ twl_st_heur ∧ (S', S) ∈ twl_st_heur ∧ unit_propagation_outer_loop_wl_inv S ∧ dom_m (get_clauses_wl S) = dom_m (get_clauses_wl S₀') ∧ length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S₀) ∧ isa_length_trail_pre (get_trail_wl_heur S'))› definition unit_propagation_update_statistics :: ‹64 word ⇒ 64 word ⇒ isasat ⇒ isasat nres› where ‹unit_propagation_update_statistics p q S = do { let stats = get_stats_heur S; let pq = q - p; let stats = incr_propagation_by pq stats; let stats = (if get_conflict_wl_is_None_heur S then stats else incr_conflict stats); let stats = (if count_decided_pol (get_trail_wl_heur S) = 0 then incr_units_since_last_GC_by pq (incr_uset_by pq stats) else stats); height ← (if get_conflict_wl_is_None_heur S then RETURN q else do {j ← trail_height_before_conflict (get_trail_wl_heur S); RETURN (of_nat j)}); let stats = set_no_conflict_until q stats; RETURN (set_stats_wl_heur stats S)}› definition unit_propagation_outer_loop_wl_D_heur :: ‹isasat ⇒ isasat nres› where ‹unit_propagation_outer_loop_wl_D_heur S₀ = do { let j1 = isa_length_trail (get_trail_wl_heur S₀); _ ← RETURN (IsaSAT_Profile.start_propagate); S ← WHILE_T⇗unit_propagation_outer_loop_wl_D_heur_inv S₀⇖ (λS. literals_to_update_wl_heur S < isa_length_trail (get_trail_wl_heur S)) (λS. do { ASSERT(literals_to_update_wl_heur S < isa_length_trail (get_trail_wl_heur S)); (S', L) ← select_and_remove_from_literals_to_update_wl_heur S; ASSERT(length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S)); unit_propagation_inner_loop_wl_D_heur L S' }) S₀; let j2 = isa_length_trail (get_trail_wl_heur S); S ← unit_propagation_update_statistics (of_nat j1) (of_nat j2) S; _ ← RETURN (IsaSAT_Profile.stop_propagate); RETURN S} › definition isa_find_unset_lit :: ‹trail_pol ⇒ arena ⇒ nat ⇒ nat ⇒ nat ⇒ nat option nres› where ‹isa_find_unset_lit M = isa_find_unwatched_between (λL. polarity_pol M L ≠ Some False) M› end

Theory IsaSAT_Inner_Propagation_Defs