Theory IsaSAT_Backtrack

theory IsaSAT_Backtrack_Defs imports IsaSAT_Setup IsaSAT_VMTF IsaSAT_Rephase_State IsaSAT_LBD IsaSAT_Proofs IsaSAT_Bump_Heuristics (*TODO: should be _State*) begin hide_const (open) NEMonad.ASSERT NEMonad.RETURN chapter ‹Backtrack› text ‹ The backtrack function is highly complicated and tricky to maintain. › section ‹Backtrack with direct extraction of literal if highest level› paragraph ‹Empty conflict› definition empty_conflict_and_extract_clause_heur_inv where ‹empty_conflict_and_extract_clause_heur_inv M outl = (λ(E, C, i). mset (take i C) = mset (take i outl) ∧ length C = length outl ∧ C ! 0 = outl ! 0 ∧ i ≥ 1 ∧ i ≤ length outl ∧ (1 < length (take i C) ⟶ highest_lit M (mset (tl (take i C))) (Some (C ! 1, get_level M (C ! 1)))))› definition isa_empty_conflict_and_extract_clause_heur :: ‹trail_pol ⇒ lookup_clause_rel ⇒ nat literal list ⇒ (_ × nat literal list × nat) nres› where ‹isa_empty_conflict_and_extract_clause_heur M D outl = do { let C = replicate (length outl) (outl!0); (D, C, _) ← WHILE_T (λ(D, C, i). i < length_uint32_nat outl) (λ(D, C, i). do { ASSERT(i < length outl); ASSERT(i < length C); ASSERT(lookup_conflict_remove1_pre (outl ! i, D)); let D = lookup_conflict_remove1 (outl ! i) D; let C = C[i := outl ! i]; ASSERT(get_level_pol_pre (M, C!i)); ASSERT(get_level_pol_pre (M, C!1)); ASSERT(1 < length C); let C = (if get_level_pol M (C!i) > get_level_pol M (C!1) then swap C 1 i else C); ASSERT(i+1 ≤ unat32_max); RETURN (D, C, i+1) }) (D, C, 1); ASSERT(length outl ≠ 1 ⟶ length C > 1); ASSERT(length outl ≠ 1 ⟶ get_level_pol_pre (M, C!1)); RETURN ((True, D), C, if length outl = 1 then 0 else get_level_pol M (C!1)) }› definition empty_cach_ref_set_inv where ‹empty_cach_ref_set_inv cach0 support = (λ(i, cach). length cach = length cach0 ∧ (∀L ∈ set (drop i support). L < length cach) ∧ (∀L ∈ set (take i support). cach ! L = SEEN_UNKNOWN) ∧ (∀L < length cach. cach ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set (drop i support)))› definition empty_cach_ref_set where ‹empty_cach_ref_set = (λ(cach0, support). do { let n = length support; ASSERT(n ≤ Suc (unat32_max div 2)); (_, cach) ← WHILE_T⇗empty_cach_ref_set_inv cach0 support⇖ (λ(i, cach). i < length support) (λ(i, cach). do { ASSERT(i < length support); ASSERT(support ! i < length cach); RETURN(i+1, cach[support ! i := SEEN_UNKNOWN]) }) (0, cach0); RETURN (cach, emptied_list support) })› paragraph ‹Minimisation of the conflict› definition empty_cach_ref_pre where ‹empty_cach_ref_pre = (λ(cach :: minimize_status list, supp :: nat list). (∀L∈set supp. L < length cach) ∧ length supp ≤ Suc (unat32_max div 2) ∧ (∀L<length cach. cach ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set supp))› definition (in -) empty_cach_ref where ‹empty_cach_ref = (λ(cach, support). (replicate (length cach) SEEN_UNKNOWN, []))› definition extract_shorter_conflict_list_heur_st :: ‹isasat ⇒ (isasat × _ × _) nres› where ‹extract_shorter_conflict_list_heur_st = (λS. do { let M = get_trail_wl_heur S; let N = get_clauses_wl_heur S; let outl = get_outlearned_heur S; let vm = get_vmtf_heur S; let lbd = get_lbd S; let cach = get_conflict_cach S; let (_, D) = get_conflict_wl_heur S; lbd ← mark_lbd_from_list_heur M outl lbd; ASSERT(fst M ≠ []); let K = lit_of_last_trail_pol M; ASSERT(0 < length outl); ASSERT(lookup_conflict_remove1_pre (-K, D)); let D = lookup_conflict_remove1 (-K) D; let outl = outl[0 := -K]; vm ← isa_vmtf_mark_to_rescore_also_reasons M N outl (-K) vm; (D, cach, outl) ← isa_minimize_and_extract_highest_lookup_conflict M N D cach lbd outl; ASSERT(empty_cach_ref_pre cach); let cach = empty_cach_ref cach; ASSERT(outl ≠ [] ∧ length outl ≤ unat32_max); (D, C, n) ← isa_empty_conflict_and_extract_clause_heur M D outl; let S = set_outl_wl_heur (take 1 outl) S; let S = set_conflict_wl_heur D S; let S = set_vmtf_wl_heur vm S; let S = set_ccach_max_wl_heur cach S; let S = set_lbd_wl_heur lbd S; RETURN (S, n, C) })› definition update_propagation_heuristics_stats where ‹update_propagation_heuristics_stats = (λglue (fema, sema, res_info, wasted, phasing, reluctant, fullyproped, s). (ema_update glue fema, ema_update glue sema, incr_conflict_count_since_last_restart res_info, wasted,phasing, reluctant, False, s))› definition update_propagation_heuristics where ‹update_propagation_heuristics glue = Restart_Heuristics o update_propagation_heuristics_stats glue o get_content› definition propagate_bt_wl_D_heur :: ‹nat literal ⇒ nat clause_l ⇒ isasat ⇒ isasat nres› where ‹propagate_bt_wl_D_heur = (λL C S₀. do { let M = get_trail_wl_heur S₀; let vdom = get_aivdom S₀; let N0 = get_clauses_wl_heur S₀; let W0 = get_watched_wl_heur S₀; let lcount = get_learned_count S₀; let heur = get_heur S₀; let stats = get_stats_heur S₀; let lbd = get_lbd S₀; let vm0 = get_vmtf_heur S₀; ASSERT(length (get_vdom_aivdom vdom) ≤ length N0); ASSERT(length (get_avdom_aivdom vdom) ≤ length N0); ASSERT(nat_of_lit (C!1) < length W0 ∧ nat_of_lit (-L) < length W0); ASSERT(length C > 1); let L' = C!1; ASSERT(length C ≤ unat32_max div 2 + 1); vm ← isa_bump_rescore C M vm0; glue ← get_LBD lbd; let b = False; let b' = (length C = 2); ASSERT(isasat_fast S₀ ⟶ append_and_length_fast_code_pre ((b, C), N0)); ASSERT(isasat_fast S₀ ⟶ clss_size_lcount lcount < snat64_max); (N, i) ← fm_add_new b C N0; ASSERT(update_lbd_pre ((i, glue), N)); let N = update_lbd_and_mark_used i glue N; ASSERT(isasat_fast S₀ ⟶ length_ll W0 (nat_of_lit (-L)) < snat64_max); let W = W0[nat_of_lit (- L) := W0 ! nat_of_lit (- L) @ [(i, L', b')]]; ASSERT(isasat_fast S₀ ⟶ length_ll W (nat_of_lit L') < snat64_max); let W = W[nat_of_lit L' := W!nat_of_lit L' @ [(i, -L, b')]]; lbd ← lbd_empty lbd; j ← mop_isa_length_trail M; ASSERT(i ≠ DECISION_REASON); ASSERT(cons_trail_Propagated_tr_pre ((-L, i), M)); M ← cons_trail_Propagated_tr (- L) i M; vm ← isa_bump_heur_flush M vm; heur ← mop_save_phase_heur (atm_of L') (is_neg L') heur; let S = set_watched_wl_heur W S₀; let S = set_learned_count_wl_heur (clss_size_incr_lcount lcount) S; let S = set_aivdom_wl_heur (add_learned_clause_aivdom i vdom) S; let S = set_heur_wl_heur (unset_fully_propagated_heur (heuristic_reluctant_tick (update_propagation_heuristics glue heur))) S; let S = set_stats_wl_heur (add_lbd (of_nat glue) stats) S; let S = set_trail_wl_heur M S; let S = set_clauses_wl_heur N S; let S = set_literals_to_update_wl_heur j S; let S = set_count_max_wl_heur 0 S; let S = set_vmtf_wl_heur vm S; let S = set_lbd_wl_heur lbd S; _ ← log_new_clause_heur S i; S ← maybe_mark_added_clause_heur2 S i; RETURN (S) })› definition propagate_unit_bt_wl_D_int :: ‹nat literal ⇒ isasat ⇒ isasat nres› where ‹propagate_unit_bt_wl_D_int = (λL S. do { let M = get_trail_wl_heur S; let vdom = get_aivdom S; let N = get_clauses_wl_heur S; let W0 = get_watched_wl_heur S; let lcount = get_learned_count S; let heur = get_heur S; let stats = get_stats_heur S; let lbd = get_lbd S; let vm0 = get_vmtf_heur S; vm ← isa_bump_heur_flush M vm0; glue ← get_LBD lbd; lbd ← lbd_empty lbd; j ← mop_isa_length_trail M; ASSERT(0 ≠ DECISION_REASON); ASSERT(cons_trail_Propagated_tr_pre ((- L, 0::nat), M)); M ← cons_trail_Propagated_tr (- L) 0 M; let stats = incr_units_since_last_GC (incr_uset stats); let S = set_stats_wl_heur stats S; let S = set_trail_wl_heur M S; let S = set_vmtf_wl_heur vm S; let S = set_lbd_wl_heur lbd S; let S = set_literals_to_update_wl_heur j S; let S = set_heur_wl_heur (unset_fully_propagated_heur (heuristic_reluctant_tick (update_propagation_heuristics glue heur))) S; let S = set_learned_count_wl_heur (clss_size_incr_lcountUEk lcount) S; RETURN S})› paragraph ‹Full function› definition backtrack_wl_D_heur_inv where ‹backtrack_wl_D_heur_inv S ⟷ (∃S'. (S, S') ∈ twl_st_heur_conflict_ana ∧ backtrack_wl_inv S')› definition backtrack_wl_D_nlit_heur :: ‹isasat ⇒ isasat nres› where ‹backtrack_wl_D_nlit_heur S₀ = do { ASSERT(backtrack_wl_D_heur_inv S₀); ASSERT(fst (get_trail_wl_heur S₀) ≠ []); L ← lit_of_hd_trail_st_heur S₀; (S, n, C) ← extract_shorter_conflict_list_heur_st S₀; ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S₀ ∧ get_learned_count S = get_learned_count S₀); S ← find_decomp_wl_st_int n S; ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S₀ ∧ get_learned_count S = get_learned_count S₀); if size C > 1 then do { S ← propagate_bt_wl_D_heur L C S; save_phase_st S } else do { propagate_unit_bt_wl_D_int L S } }› lemma empty_cach_ref_set_empty_cach_ref: ‹(empty_cach_ref_set, RETURN o empty_cach_ref) ∈ [λ(cach, supp). (∀L ∈ set supp. L < length cach) ∧ length supp ≤ Suc (unat32_max div 2) ∧ (∀L < length cach. cach ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set supp)]_f Id → ⟨Id⟩ nres_rel› proof - have H: ‹WHILE_T⇗empty_cach_ref_set_inv cach0 support'⇖ (λ(i, cach). i < length support') (λ(i, cach). ASSERT (i < length support') ⤜ (λ_. ASSERT (support' ! i < length cach) ⤜ (λ_. RETURN (i + 1, cach[support' ! i := SEEN_UNKNOWN])))) (0, cach0) ⤜ (λ(_, cach). RETURN (cach, emptied_list support')) ≤ ⇓ Id (RETURN (replicate (length cach0) SEEN_UNKNOWN, []))› if ‹∀L∈set support'. L < length cach0› and ‹∀L<length cach0. cach0 ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set support'› for cach support cach0 support' proof - have init: ‹empty_cach_ref_set_inv cach0 support' (0, cach0)› using that unfolding empty_cach_ref_set_inv_def by auto have valid_length: ‹empty_cach_ref_set_inv cach0 support' s ⟹ case s of (i, cach) ⇒ i < length support' ⟹ s = (cach', sup') ⟹ support' ! cach' < length sup'› for s cach' sup' using that unfolding empty_cach_ref_set_inv_def by auto have set_next: ‹empty_cach_ref_set_inv cach0 support' (i + 1, cach'[support' ! i := SEEN_UNKNOWN])› if inv: ‹empty_cach_ref_set_inv cach0 support' s› and cond: ‹case s of (i, cach) ⇒ i < length support'› and s: ‹s = (i, cach')› and valid[simp]: ‹support' ! i < length cach'› for s i cach' proof - have le_cach_cach0: ‹length cach' = length cach0› and le_length: ‹∀L∈set (drop i support'). L < length cach'› and UNKNOWN: ‹∀L∈set (take i support'). cach' ! L = SEEN_UNKNOWN› and support: ‹∀L<length cach'. cach' ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set (drop i support')› and [simp]: ‹i < length support'› using inv cond unfolding empty_cach_ref_set_inv_def s prod.case by auto show ?thesis unfolding empty_cach_ref_set_inv_def unfolding prod.case apply (intro conjI) subgoal by (simp add: le_cach_cach0) subgoal using le_length by (simp add: Cons_nth_drop_Suc[symmetric]) subgoal using UNKNOWN by (auto simp add: take_Suc_conv_app_nth) subgoal using support by (auto simp add: Cons_nth_drop_Suc[symmetric]) done qed have final: ‹((cach', emptied_list support'), replicate (length cach0) SEEN_UNKNOWN, []) ∈ Id› if inv: ‹empty_cach_ref_set_inv cach0 support' s› and cond: ‹¬ (case s of (i, cach) ⇒ i < length support')› and s: ‹s = (i, cach')› for s cach' i proof - have le_cach_cach0: ‹length cach' = length cach0› and le_length: ‹∀L∈set (drop i support'). L < length cach'› and UNKNOWN: ‹∀L∈set (take i support'). cach' ! L = SEEN_UNKNOWN› and support: ‹∀L<length cach'. cach' ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set (drop i support')› and i: ‹¬i < length support'› using inv cond unfolding empty_cach_ref_set_inv_def s prod.case by auto have ‹∀L<length cach'. cach' ! L = SEEN_UNKNOWN› using support i by auto then have [dest]: ‹L ∈ set cach' ⟹ L = SEEN_UNKNOWN› for L by (metis in_set_conv_nth) then have [dest]: ‹SEEN_UNKNOWN ∉ set cach' ⟹ cach0 = [] ∧ cach' = []› using le_cach_cach0 by (cases cach') auto show ?thesis by (auto simp: emptied_list_def list_eq_replicate_iff le_cach_cach0) qed show ?thesis unfolding conc_Id id_def apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i, _). length support' - i)›]) subgoal by auto subgoal by (rule init) subgoal by auto subgoal by (rule valid_length) subgoal by (rule set_next) subgoal by auto subgoal using final by simp done qed show ?thesis unfolding empty_cach_ref_set_def empty_cach_ref_def Let_def comp_def by (intro frefI nres_relI ASSERT_leI) (clarify intro!: H ASSERT_leI) qed end

Theory IsaSAT_Backtrack_Defs