Theory IsaSAT_Conflict_Analysis

theory IsaSAT_Conflict_Analysis_Defs imports IsaSAT_Setup IsaSAT_Bump_Heuristics (*TODO _State *) IsaSAT_VMTF IsaSAT_LBD begin definition lit_and_ann_of_propagated_st :: ‹nat twl_st_wl ⇒ nat literal × nat› where ‹lit_and_ann_of_propagated_st S = lit_and_ann_of_propagated (hd (get_trail_wl S))› definition lit_and_ann_of_propagated_st_heur :: ‹isasat ⇒ (nat literal × nat) nres› where ‹lit_and_ann_of_propagated_st_heur = (λS. do { let (M, _, _, reasons, _, _) = get_trail_wl_heur S; ASSERT(M ≠ [] ∧ atm_of (last M) < length reasons); RETURN (last M, reasons ! (atm_of (last M)))})› definition tl_state_wl_heur_pre :: ‹isasat ⇒ bool› where ‹tl_state_wl_heur_pre = (λS. let M = get_trail_wl_heur S in let x = get_vmtf_heur S in fst M ≠ [] ∧ tl_trailt_tr_pre M)› definition tl_state_wl_heur :: ‹isasat ⇒ (bool × isasat) nres› where ‹tl_state_wl_heur = (λS. do { ASSERT(tl_state_wl_heur_pre S); let M = get_trail_wl_heur S; let vm = get_vmtf_heur S; let S = set_trail_wl_heur (tl_trailt_tr M) S; ASSERT (isa_bump_unset_pre (atm_of (lit_of_last_trail_pol M)) vm); vm ← isa_bump_unset (atm_of (lit_of_last_trail_pol M)) vm; let S = set_vmtf_wl_heur vm S; RETURN (False, S) })› definition update_confl_tl_wl_heur :: ‹nat literal ⇒ nat ⇒ isasat ⇒ (bool × isasat) nres› where ‹update_confl_tl_wl_heur = (λL C S. do { let M = get_trail_wl_heur S; let N = get_clauses_wl_heur S; let lbd = get_lbd S; let outl = get_outlearned_heur S; let clvls = get_count_max_lvls_heur S; let vm = get_vmtf_heur S; let (b, (n, xs)) = get_conflict_wl_heur S; (N, lbd) ← calculate_LBD_heur_st M N lbd C; ASSERT (clvls ≥ 1); let L' = atm_of L; ASSERT(arena_is_valid_clause_idx N C); ((b, (n, xs)), clvls, outl) ← if arena_length N C = 2 then isasat_lookup_merge_eq2 L M N C (b, (n, xs)) clvls outl else isa_resolve_merge_conflict_gt2 M N C (b, (n, xs)) clvls outl; ASSERT(curry lookup_conflict_remove1_pre L (n, xs) ∧ clvls ≥ 1); let (n, xs) = lookup_conflict_remove1 L (n, xs); ASSERT(arena_act_pre N C); vm ← isa_vmtf_bump_to_rescore_also_reasons_cl M N C (-L) vm; ASSERT(isa_bump_unset_pre L' vm); ASSERT(tl_trailt_tr_pre M); vm ← isa_bump_unset L' vm; let S = set_trail_wl_heur (tl_trailt_tr M) S; let S = set_conflict_wl_heur (b, (n, xs)) S; let S = set_vmtf_wl_heur vm S; let S = set_count_max_wl_heur (clvls - 1) S; let S = set_outl_wl_heur outl S; let S = set_clauses_wl_heur N S; let S = set_lbd_wl_heur lbd S; RETURN (False, S) })› definition is_decided_hd_trail_wl_heur :: ‹isasat ⇒ bool› where ‹is_decided_hd_trail_wl_heur = (λS. is_None (snd (last_trail_pol (get_trail_wl_heur S))))› definition skip_and_resolve_loop_wl_D_heur_inv where ‹skip_and_resolve_loop_wl_D_heur_inv S₀' = (λ(brk, S'). ∃S S₀. (S', S) ∈ twl_st_heur_conflict_ana ∧ (S₀', S₀) ∈ twl_st_heur_conflict_ana ∧ skip_and_resolve_loop_wl_inv S₀ brk S ∧ length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S₀') ∧ get_learned_count S' = get_learned_count S₀')› definition update_confl_tl_wl_heur_pre :: ‹(nat × nat literal) × isasat ⇒ bool› where ‹update_confl_tl_wl_heur_pre = (λ((i, L), S). let M = get_trail_wl_heur S; x = get_vmtf_heur S in i > 0 ∧ (fst M) ≠ [] ∧ isa_bump_unset_pre (atm_of L) x ∧ L = (last (fst M)) )› definition lit_and_ann_of_propagated_st_heur_pre where ‹lit_and_ann_of_propagated_st_heur_pre = (λ((M, _, _, reasons, _), _). atm_of (last M) < length reasons ∧ M ≠ [])› definition atm_is_in_conflict_st_heur_pre :: ‹nat literal × isasat ⇒ bool› where ‹atm_is_in_conflict_st_heur_pre = (λ(L, S). atm_of L < length (snd (snd (get_conflict_wl_heur S))))› definition maximum_level_removed_eq_count_dec_heur where ‹maximum_level_removed_eq_count_dec_heur L S = RETURN (get_count_max_lvls_heur S > 1)› definition is_decided_hd_trail_wl_heur_pre where ‹is_decided_hd_trail_wl_heur_pre = (λS. fst (get_trail_wl_heur S) ≠ [] ∧ last_trail_pol_pre (get_trail_wl_heur S))› definition skip_and_resolve_loop_wl_D_heur :: ‹isasat ⇒ isasat nres› where ‹skip_and_resolve_loop_wl_D_heur S₀ = do { _ ← RETURN (IsaSAT_Profile.start_analyze); (_, S) ← WHILE_T⇗skip_and_resolve_loop_wl_D_heur_inv S₀⇖ (λ(brk, S). ¬brk ∧ ¬is_decided_hd_trail_wl_heur S) (λ(brk, S). do { ASSERT(¬brk ∧ ¬is_decided_hd_trail_wl_heur S); (L, C) ← lit_and_ann_of_propagated_st_heur S; b ← atm_is_in_conflict_st_heur (-L) S; if b then tl_state_wl_heur S else do { b ← maximum_level_removed_eq_count_dec_heur L S; if b then do { update_confl_tl_wl_heur L C S } else RETURN (True, S) } } ) (False, S₀); _ ← RETURN (IsaSAT_Profile.stop_analyze); RETURN S } › lemma twl_st_heur_conflict_ana_trail_empty: ‹(T, x) ∈ twl_st_heur_conflict_ana ⟹ fst (get_trail_wl_heur T) = [] ⟷ get_trail_wl x = []› by (clarsimp simp: twl_st_heur_def state_wl_l_def twl_st_l_def twl_st_heur_conflict_ana_def trail_pol_alt_def last_trail_pol_pre_def last_rev hd_map literals_are_in_ℒ_i_n_trail_def simp flip: rev_map dest: multi_member_split) lemma twl_st_heur_conflict_ana_last_trail_pol_pre: ‹(T, x) ∈ twl_st_heur_conflict_ana ⟹ fst (get_trail_wl_heur T) ≠ [] ⟹ last_trail_pol_pre (get_trail_wl_heur T)› apply (cases ‹get_trail_wl x›) by (clarsimp_all simp: twl_st_heur_def state_wl_l_def twl_st_l_def twl_st_heur_conflict_ana_def trail_pol_alt_def last_trail_pol_pre_def last_rev hd_map literals_are_in_ℒ_i_n_trail_def simp flip: rev_map dest: multi_member_split) (clarsimp_all dest!: multi_member_split simp: ann_lits_split_reasons_def) lemma skip_and_resolve_loop_wl_DI: assumes ‹skip_and_resolve_loop_wl_D_heur_inv S (b, T)› shows ‹is_decided_hd_trail_wl_heur_pre T› using assms apply - unfolding skip_and_resolve_loop_wl_inv_def skip_and_resolve_loop_inv_l_def skip_and_resolve_loop_inv_def skip_and_resolve_loop_wl_D_heur_inv_def is_decided_hd_trail_wl_heur_pre_def apply (subst (asm) case_prod_beta)+ unfolding prod.case apply normalize_goal+ by (simp add: twl_st_heur_conflict_ana_trail_empty twl_st_heur_conflict_ana_last_trail_pol_pre) lemma isasat_fast_after_skip_and_resolve_loop_wl_D_heur_inv: ‹isasat_fast x ⟹ skip_and_resolve_loop_wl_D_heur_inv x (False, a2') ⟹ isasat_fast a2'› unfolding skip_and_resolve_loop_wl_D_heur_inv_def isasat_fast_def by (auto dest: get_learned_count_learned_clss_countD2) end

Theory IsaSAT_Conflict_Analysis_Defs