Theory IsaSAT_Conflict_Analysis
theory IsaSAT_Conflict_Analysis
imports IsaSAT_Conflict_Analysis_Defs
begin
lemma literals_are_in_ℒ⇩i⇩n_mm_all_atms_self[simp]:
‹literals_are_in_ℒ⇩i⇩n_mm (all_atms ca NUE) {#mset (fst x). x ∈# ran_m ca#}›
by (auto simp: literals_are_in_ℒ⇩i⇩n_mm_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
all_atms_def all_lits_def in_all_lits_of_mm_ain_atms_of_iff)
lemma literals_are_in_ℒ⇩i⇩n_mm_ran_m[simp]:
‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st (x1a, x1b, y))
{#mset (fst x). x ∈# ran_m x1b#}›
by (cases y; auto simp: literals_are_in_ℒ⇩i⇩n_mm_def all_lits_st_def all_lits_def all_lits_of_mm_union
simp flip: all_lits_st_alt_def)
paragraph ‹Skip and resolve›
definition maximum_level_removed_eq_count_dec where
‹maximum_level_removed_eq_count_dec L S ⟷
get_maximum_level_remove (get_trail_wl S) (the (get_conflict_wl S)) L =
count_decided (get_trail_wl S)›
definition maximum_level_removed_eq_count_dec_pre where
‹maximum_level_removed_eq_count_dec_pre =
(λ(L, S). L = -lit_of (hd (get_trail_wl S)) ∧ L ∈# the (get_conflict_wl S) ∧
get_conflict_wl S ≠ None ∧ get_trail_wl S ≠ [] ∧ count_decided (get_trail_wl S) ≥ 1)›
lemma maximum_level_removed_eq_count_dec_heur_maximum_level_removed_eq_count_dec:
‹(uncurry maximum_level_removed_eq_count_dec_heur,
uncurry mop_maximum_level_removed_wl) ∈
[λ_. True]⇩f
Id ×⇩r twl_st_heur_conflict_ana → ⟨bool_rel⟩nres_rel›
unfolding maximum_level_removed_eq_count_dec_heur_def mop_maximum_level_removed_wl_def
uncurry_def
apply (intro frefI nres_relI)
subgoal for x y
apply refine_rcg
apply (cases x)
apply (auto simp: count_decided_st_def counts_maximum_level_def twl_st_heur_conflict_ana_def
maximum_level_removed_eq_count_dec_heur_def maximum_level_removed_eq_count_dec_def
maximum_level_removed_eq_count_dec_pre_def mop_maximum_level_removed_wl_pre_def
mop_maximum_level_removed_l_pre_def mop_maximum_level_removed_pre_def state_wl_l_def
twl_st_l_def get_maximum_level_card_max_lvl_ge1 card_max_lvl_remove_hd_trail_iff)
done
done
lemma lit_and_ann_of_propagated_st_heur_lit_and_ann_of_propagated_st:
‹(lit_and_ann_of_propagated_st_heur, mop_hd_trail_wl) ∈
[λS. True]⇩f twl_st_heur_conflict_ana → ⟨Id ×⇩f Id⟩nres_rel›
apply (intro frefI nres_relI)
unfolding lit_and_ann_of_propagated_st_heur_def mop_hd_trail_wl_def
apply refine_rcg
apply (case_tac ‹get_trail_wl_heur x›)
apply (auto simp: twl_st_heur_conflict_ana_def mop_hd_trail_wl_def mop_hd_trail_wl_pre_def
mop_hd_trail_l_pre_def twl_st_l_def state_wl_l_def mop_hd_trail_pre_def last_rev hd_map
lit_and_ann_of_propagated_st_def trail_pol_alt_def ann_lits_split_reasons_def
intro!: ASSERT_leI ASSERT_refine_right simp flip: rev_map elim: is_propedE)
apply (auto elim!: is_propedE)
done
definition tl_state_wl_pre where
‹tl_state_wl_pre S ⟷ get_trail_wl S ≠ [] ∧
literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) (get_trail_wl S) ∧
(lit_of (hd (get_trail_wl S))) ∉# the (get_conflict_wl S) ∧
-(lit_of (hd (get_trail_wl S))) ∉# the (get_conflict_wl S) ∧
¬tautology (the (get_conflict_wl S)) ∧
distinct_mset (the (get_conflict_wl S)) ∧
¬is_decided (hd (get_trail_wl S)) ∧
count_decided (get_trail_wl S) > 0›
lemma tl_state_out_learned:
‹lit_of (hd a) ∉# the at' ⟹
- lit_of (hd a) ∉# the at' ⟹
¬ is_decided (hd a) ⟹
out_learned (tl a) at' an ⟷ out_learned a at' an›
by (cases a) (auto simp: out_learned_def get_level_cons_if atm_of_eq_atm_of
intro!: filter_mset_cong)
lemma mop_tl_state_wl_pre_tl_state_wl_heur_pre:
‹(x, y) ∈ twl_st_heur_conflict_ana ⟹ mop_tl_state_wl_pre y ⟹ tl_state_wl_heur_pre x›
‹(x, y) ∈ twl_st_heur_conflict_ana ⟹ mop_tl_state_wl_pre y ⟹
isa_bump_unset_pre (atm_of (lit_of_last_trail_pol (get_trail_wl_heur x)))
(get_vmtf_heur x)
›
using tl_trailt_tr_pre[of ‹get_trail_wl y› ‹get_trail_wl_heur x› ‹all_atms_st y›]
subgoal
unfolding mop_tl_state_wl_pre_def tl_state_wl_heur_pre_def mop_tl_state_l_pre_def
mop_tl_state_pre_def tl_state_wl_heur_pre_def
by (cases ‹get_trail_wl_heur x›; cases y)
(clarsimp_all simp: twl_st_heur_conflict_ana_def state_wl_l_def twl_st_l_def trail_pol_alt_def
rev_map[symmetric] last_rev hd_map simp flip: all_lits_st_alt_def
intro!: isa_bump_unset_pre[where M = ‹get_trail_wl y›])
subgoal
unfolding mop_tl_state_wl_pre_def tl_state_wl_heur_pre_def mop_tl_state_l_pre_def
mop_tl_state_pre_def tl_state_wl_heur_pre_def
apply normalize_goal+
apply (cases ‹get_trail_wl y›)
apply (solves simp)
apply (rule isa_bump_unset_pre[of _ ‹all_atms_st y› ‹get_trail_wl y›])
apply (simp add: twl_st_heur_conflict_ana_def)
apply (simp add: twl_st_heur_conflict_ana_def lit_of_last_trail_pol_def)
apply (clarsimp_all simp: twl_st_heur_conflict_ana_def state_wl_l_def twl_st_l_def trail_pol_alt_def
rev_map[symmetric] last_rev hd_map lit_of_last_trail_pol_def
simp flip: all_lits_st_alt_def IsaSAT_Setup.all_lits_st_alt_def
intro!: isa_bump_unset_pre[where M = ‹get_trail_wl y›])
using IsaSAT_Setup.all_lits_st_alt_def by blast
done
lemma mop_tl_state_wl_pre_simps:
‹mop_tl_state_wl_pre ([], ax, ay, az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟷ False›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹
lit_of (hd xa) ∈# all_lits_st (xa', ax, ay'', az, bga, NEk, UEk, NS, US, N0, U0, bh'', bi'')›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹ lit_of (hd xa) ∉# the ay›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹ -lit_of (hd xa) ∉# the ay›
‹mop_tl_state_wl_pre (xa, ax, Some ay', az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹ lit_of (hd xa) ∉# ay'›
‹mop_tl_state_wl_pre (xa, ax, Some ay', az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹ -lit_of (hd xa) ∉# ay'›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹ is_proped (hd xa)›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NEk, UEk, NS, US, N0, U0, bh, bi) ⟹ count_decided xa > 0›
unfolding mop_tl_state_wl_pre_def tl_state_wl_heur_pre_def mop_tl_state_l_pre_def
mop_tl_state_pre_def tl_state_wl_heur_pre_def
apply (auto simp: twl_st_heur_conflict_ana_def state_wl_l_def twl_st_l_def trail_pol_alt_def
rev_map[symmetric] last_rev hd_map mset_take_mset_drop_mset' ℒ⇩a⇩l⇩l_all_atms_all_lits
simp flip: image_mset_union all_lits_def all_lits_st_alt_def; fail)[]
apply (normalize_goal+; simp add: all_lits_st_def; fail)+
done
lemma all_atms_st_st_simps2[simp]:
‹all_atms_st (tl xaa, bu, bv, bw, bx, by, NEk, UEk, bz, ca, cb, cc, cd) =
all_atms_st (xaa, bu, bv, bw, bx, by, NEk, UEk, bz, ca, cb, cc, cd)›
‹all_atms_st (xaa, bu, Some (bv' ∪# tt - uu), bw, bx, by, NEk, UEk, bz, ca, cb, cc, cd) =
all_atms_st (xaa, bu, Some bv', bw, bx, by, NEk, UEk, bz, ca, cb, cc, cd)›
by (auto simp: all_atms_st_def)
declare isasat_input_bounded_def[simp del]
lemma tl_state_wl_heur_tl_state_wl:
‹(tl_state_wl_heur, mop_tl_state_wl) ∈
[λ_. True]⇩f twl_st_heur_conflict_ana' r lcount →
⟨bool_rel ×⇩f twl_st_heur_conflict_ana' r lcount⟩nres_rel›
supply [[goals_limit=1]]
unfolding tl_state_wl_heur_def mop_tl_state_wl_def
apply (intro frefI nres_relI)
apply refine_vcg
subgoal for x y
using mop_tl_state_wl_pre_tl_state_wl_heur_pre[of x y] by simp
subgoal for x y
using mop_tl_state_wl_pre_tl_state_wl_heur_pre[of x y] by simp
subgoal for x y
apply (cases y)
apply (auto simp: twl_st_heur_conflict_ana_def tl_state_wl_heur_def tl_state_wl_def vmtf_unset_vmtf_tl
mop_tl_state_wl_pre_simps lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id]
card_max_lvl_tl tl_state_out_learned
dest: no_dup_tlD simp flip: all_lits_st_alt_def
intro!: tl_trail_tr[THEN fref_to_Down_unRET] isa_bump_unset_vmtf_tl)
apply (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id])
apply (auto simp: mop_tl_state_wl_pre_simps lit_of_hd_trail_def mop_tl_state_wl_pre_simps counts_maximum_level_def
intro!: isa_bump_unset_vmtf_tl[THEN order_trans] IsaSAT_Trail.tl_trail_tr[THEN fref_to_Down_unRET]
intro: no_dup_tlD)
apply (metis (no_types, lifting) IsaSAT_Setup.all_lits_st_alt_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff mop_tl_state_wl_pre_simps(2))
apply (metis (no_types, lifting) IsaSAT_Setup.all_lits_st_alt_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff mop_tl_state_wl_pre_simps(2))
apply (rule no_dup_tlD, assumption)
apply (subst card_max_lvl_tl)
apply (auto simp: mop_tl_state_wl_pre_simps lookup_clause_rel_not_tautolgy lookup_clause_rel_distinct_mset
option_lookup_clause_rel_def)
apply (subst tl_state_out_learned)
apply (auto simp: mop_tl_state_wl_pre_simps lookup_clause_rel_not_tautolgy lookup_clause_rel_distinct_mset
option_lookup_clause_rel_def)
apply (subst tl_state_out_learned)
apply (auto simp: mop_tl_state_wl_pre_simps lookup_clause_rel_not_tautolgy lookup_clause_rel_distinct_mset
option_lookup_clause_rel_def)
done
done
lemma arena_act_pre_mark_used:
‹arena_act_pre arena C ⟹
arena_act_pre (mark_used arena C) C›
unfolding arena_act_pre_def arena_is_valid_clause_idx_def
apply clarify
apply (rule_tac x=N in exI)
apply (rule_tac x=vdom in exI)
by (auto simp: arena_act_pre_def
simp: valid_arena_mark_used)
definition (in -) get_max_lvl_st :: ‹nat twl_st_wl ⇒ nat literal ⇒ nat› where
‹get_max_lvl_st S L = get_maximum_level_remove (get_trail_wl S) (the (get_conflict_wl S)) L›
lemma card_max_lvl_remove1_mset_hd:
‹-lit_of (hd M) ∈# y ⟹ is_proped (hd M) ⟹
card_max_lvl M (remove1_mset (-lit_of (hd M)) y) = card_max_lvl M y - 1›
by (cases M) (auto dest!: multi_member_split simp: card_max_lvl_add_mset)
lemma update_confl_tl_wl_heur_state_helper:
‹(L, C) = lit_and_ann_of_propagated (hd (get_trail_wl S)) ⟹ get_trail_wl S ≠ [] ⟹
is_proped (hd (get_trail_wl S)) ⟹ L = lit_of (hd (get_trail_wl S))›
by (cases S; cases ‹hd (get_trail_wl S)›) auto
lemma (in -) not_ge_Suc0: ‹¬Suc 0 ≤ n ⟷ n = 0›
by auto
definition update_confl_tl_wl_pre' :: ‹((nat literal × nat) × nat twl_st_wl) ⇒ bool› where
‹update_confl_tl_wl_pre' = (λ((L, C), S).
C ∈# dom_m (get_clauses_wl S) ∧
get_conflict_wl S ≠ None ∧ get_trail_wl S ≠ [] ∧
- L ∈# the (get_conflict_wl S) ∧
L ∉# the (get_conflict_wl S) ∧
(L, C) = lit_and_ann_of_propagated (hd (get_trail_wl S)) ∧
L ∈# all_lits_st S ∧
is_proped (hd (get_trail_wl S)) ∧
C > 0 ∧
card_max_lvl (get_trail_wl S) (the (get_conflict_wl S)) ≥ 1 ∧
distinct_mset (the (get_conflict_wl S)) ∧
- L ∉ set (get_clauses_wl S ∝ C) ∧
(length (get_clauses_wl S ∝ C) ≠ 2 ⟶
L ∉ set (tl (get_clauses_wl S ∝ C)) ∧
get_clauses_wl S ∝ C ! 0 = L ∧
mset (tl (get_clauses_wl S ∝ C)) = remove1_mset L (mset (get_clauses_wl S ∝ C)) ∧
(∀L∈set (tl(get_clauses_wl S ∝ C)). - L ∉# the (get_conflict_wl S)) ∧
card_max_lvl (get_trail_wl S) (mset (tl (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) =
card_max_lvl (get_trail_wl S) (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S))) ∧
L ∈ set (watched_l (get_clauses_wl S ∝ C)) ∧
distinct (get_clauses_wl S ∝ C) ∧
¬tautology (the (get_conflict_wl S)) ∧
¬tautology (mset (get_clauses_wl S ∝ C)) ∧
¬tautology (remove1_mset L (remove1_mset (- L)
((the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C))))) ∧
count_decided (get_trail_wl S) > 0 ∧
literals_are_in_ℒ⇩i⇩n (all_atms_st S) (the (get_conflict_wl S)) ∧
literals_are_ℒ⇩i⇩n (all_atms_st S) S ∧
literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) (get_trail_wl S) ∧
(∀K. K ∈# remove1_mset L (mset (get_clauses_wl S ∝ C)) ⟶ - K ∉# the (get_conflict_wl S)) ∧
size (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) > 0 ∧
Suc 0 ≤ card_max_lvl (get_trail_wl S) (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) ∧
size (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) =
size (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#}) + Suc 0 ∧
lit_of (hd (get_trail_wl S)) = L ∧
card_max_lvl (get_trail_wl S) ((mset (get_clauses_wl S ∝ C) - unmark (hd (get_trail_wl S))) ∪# the (get_conflict_wl S)) =
card_max_lvl (tl (get_trail_wl S)) (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#}) + Suc 0 ∧
out_learned (tl (get_trail_wl S)) (Some (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#})) =
out_learned (get_trail_wl S) (Some ((mset (get_clauses_wl S ∝ C) - unmark (hd (get_trail_wl S))) ∪# the (get_conflict_wl S)))
)›
lemma remove1_mset_union_distrib1:
‹L ∉# B ⟹ remove1_mset L (A ∪# B) = remove1_mset L A ∪# B› and
remove1_mset_union_distrib2:
‹L ∉# A ⟹ remove1_mset L (A ∪# B) = A ∪# remove1_mset L B›
by (auto simp: remove1_mset_union_distrib)
lemma update_confl_tl_wl_pre_update_confl_tl_wl_pre':
assumes ‹update_confl_tl_wl_pre L C S›
shows ‹update_confl_tl_wl_pre' ((L, C), S)›
proof -
obtain x xa where
Sx: ‹(S, x) ∈ state_wl_l None› and
‹correct_watching S› and
x_xa: ‹(x, xa) ∈ twl_st_l None› and
st_invs: ‹twl_struct_invs xa› and
list_invs: ‹twl_list_invs x› and
‹twl_stgy_invs xa› and
C: ‹C ∈# dom_m (get_clauses_wl S)› and
nempty: ‹get_trail_wl S ≠ []› and
‹literals_to_update_wl S = {#}› and
hd: ‹hd (get_trail_wl S) = Propagated L C› and
C_0: ‹0 < C› and
confl: ‹get_conflict_wl S ≠ None› and
‹0 < count_decided (get_trail_wl S)› and
‹get_conflict_wl S ≠ Some {#}› and
‹L ∈ set (get_clauses_wl S ∝ C)› and
uL_D: ‹- L ∈# the (get_conflict_wl S)› and
xa: ‹hd (get_trail xa) = Propagated L (mset (get_clauses_wl S ∝ C))› and
L: ‹L ∈# all_lits_st S› and
blits: ‹blits_in_ℒ⇩i⇩n S›
using assms
unfolding update_confl_tl_wl_pre_def
update_confl_tl_l_pre_def update_confl_tl_pre_def
prod.case apply -
by normalize_goal+
(simp flip: all_lits_def all_lits_alt_def2
add: mset_take_mset_drop_mset' ℒ⇩a⇩l⇩l_all_atms_all_lits)
have
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of xa)› and
M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of xa)› and
confl': ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of xa)› and
st_inv: ‹twl_st_inv xa›
using st_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
pcdcl_all_struct_invs_def state⇩W_of_def[symmetric]
by fast+
have eq: ‹lits_of_l (tl (get_trail_wl S)) = lits_of_l (tl (get_trail xa))›
using Sx x_xa unfolding list.set_map[symmetric] lits_of_def
by (cases S; cases x; cases xa;
auto simp: state_wl_l_def twl_st_l_def map_tl list_of_l_convert_map_lit_of simp del: list.set_map)
have card_max: ‹card_max_lvl (get_trail_wl S) (the (get_conflict_wl S)) ≥ 1›
using hd uL_D nempty by (cases ‹get_trail_wl S›; auto dest!: multi_member_split simp: card_max_lvl_def)
have dist_C: ‹distinct_mset (the (get_conflict_wl S))›
using dist Sx x_xa confl C unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto simp: twl_st)
have dist: ‹distinct (get_clauses_wl S ∝ C)›
using dist Sx x_xa confl C unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_alt_def
by (auto simp: image_image ran_m_def dest!: multi_member_split)
have n_d: ‹no_dup (get_trail_wl S)›
using Sx x_xa M_lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st)
have CNot_D: ‹get_trail_wl S ⊨as CNot (the (get_conflict_wl S))›
using confl' confl Sx x_xa unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: twl_st)
then have ‹tl (get_trail_wl S) ⊨as CNot (the (get_conflict_wl S) - {#-L#})›
using dist_C uL_D n_d hd nempty by (cases ‹get_trail_wl S›)
(auto dest!: multi_member_split simp: true_annots_true_cls_def_iff_negation_in_model)
moreover have CNot_C': ‹tl (get_trail_wl S) ⊨as CNot (mset (get_clauses_wl S ∝ C) - {#L#})› and
L_C: ‹L ∈# mset (get_clauses_wl S ∝ C)›
using confl' nempty x_xa xa hd Sx nempty eq
unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (cases ‹get_trail xa›; fastforce simp: twl_st twl_st_l true_annots_true_cls_def_iff_negation_in_model
dest: spec[of _ ‹[]›])+
ultimately have tl: ‹tl (get_trail_wl S) ⊨as CNot ((the (get_conflict_wl S) - {#-L#}) ∪# (mset (get_clauses_wl S ∝ C) - {#L#}))›
by (auto simp: true_annots_true_cls_def_iff_negation_in_model)
then have ‹(the (get_conflict_wl S) - {#-L#}) ∪# (mset (get_clauses_wl S ∝ C) - {#L#}) =
(the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) -
{#L, - L#})›
using multi_member_split[OF L_C] uL_D dist dist_C n_d hd nempty
apply (cases ‹get_trail_wl S›; auto dest!: multi_member_split
simp: true_annots_true_cls_def_iff_negation_in_model)
apply (subst sup_union_left1)
apply (auto dest!: multi_member_split dest: in_lits_of_l_defined_litD)
done
with tl have ‹tl (get_trail_wl S) ⊨as CNot (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) -
{#L, - L#})› by simp
with distinct_consistent_interp[OF no_dup_tlD[OF n_d]] have 1: ‹¬tautology
(the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) -
{#L, - L#})›
unfolding true_annots_true_cls
by (rule consistent_CNot_not_tautology)
have False if ‹- L ∈# mset (get_clauses_wl S ∝ C)›
using multi_member_split[OF L_C] hd nempty n_d CNot_C' multi_member_split[OF that]
by (cases ‹get_trail_wl S›; auto dest!: multi_member_split
simp: add_mset_eq_add_mset true_annots_true_cls_def_iff_negation_in_model
dest!: in_lits_of_l_defined_litD)
then have 2: ‹-L ∉ set (get_clauses_wl S ∝ C)›
by auto
have ‹length (get_clauses_wl S ∝ C) ≥ 2›
using st_inv C Sx x_xa by (cases xa; cases x; cases S; cases ‹irred (get_clauses_wl S) C›;
auto simp: twl_st_inv.simps state_wl_l_def twl_st_l_def conj_disj_distribR Collect_disj_eq image_Un
ran_m_def Collect_conv_if dest!: multi_member_split)
then have [simp]: ‹length (get_clauses_wl S ∝ C) ≠ 2 ⟷ length (get_clauses_wl S ∝ C) > 2›
by (cases ‹get_clauses_wl S ∝ C›; cases ‹tl (get_clauses_wl S ∝ C)›;
auto simp: twl_list_invs_def all_conj_distrib dest: in_set_takeD)
have CNot_C: ‹¬tautology (mset (get_clauses_wl S ∝ C))›
using CNot_C' Sx hd nempty C_0 dist multi_member_split[OF L_C] dist
consistent_CNot_not_tautology[OF distinct_consistent_interp[OF no_dup_tlD[OF n_d]]
CNot_C'[unfolded true_annots_true_cls]] 2
unfolding true_annots_true_cls_def_iff_negation_in_model
apply (auto simp: tautology_add_mset dest: arg_cong[of ‹mset _› _ set_mset])
by (metis member_add_mset set_mset_mset)
have stupid: ‹K ∈# removeAll_mset L D ⟷ K ≠ L ∧ K ∈# D› for K L D
by auto
have K: ‹K ∈# remove1_mset L (mset (get_clauses_wl S ∝ C)) ⟹ - K ∉# the (get_conflict_wl S)› and
uL_C: ‹-L ∉# (mset (get_clauses_wl S ∝ C))› for K
apply (subst (asm) distinct_mset_remove1_All)
subgoal using dist by auto
apply (subst (asm)stupid)
apply (rule conjE, assumption)
apply (drule multi_member_split)
using 1 uL_D CNot_C dist 2[unfolded in_multiset_in_set[symmetric]] dist_C
consistent_CNot_not_tautology[OF distinct_consistent_interp[OF n_d]
CNot_D[unfolded true_annots_true_cls]] ‹L ∈# mset (get_clauses_wl S ∝ C)›
by (auto dest!: multi_member_split[of ‹-L›] multi_member_split in_set_takeD
simp: tautology_add_mset add_mset_eq_add_mset uminus_lit_swap diff_union_swap2
simp del: set_mset_mset in_multiset_in_set
distinct_mset_mset_distinct simp flip: distinct_mset_mset_distinct)
have size: ‹size (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) > 0›
using uL_D uL_C by (auto dest!: multi_member_split)
have max_lvl: ‹Suc 0 ≤ card_max_lvl (get_trail_wl S) (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S))›
using uL_D hd nempty uL_C by (cases ‹get_trail_wl S›; auto simp: card_max_lvl_def dest!: multi_member_split)
have s: ‹size (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) =
size (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#}) + 1›
using uL_D hd nempty uL_C dist_C apply (cases ‹get_trail_wl S›; auto simp: dest!: multi_member_split)
by (metis (no_types, opaque_lifting) ‹remove1_mset (- L) (the (get_conflict_wl S)) ∪# remove1_mset L (mset (get_clauses_wl S ∝ C)) = the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#}› add_mset_commute add_mset_diff_bothsides add_mset_remove_trivial set_mset_mset subset_mset.sup_commute sup_union_left1)
have SC_0: ‹length (get_clauses_wl S ∝ C) > 2 ⟹ L ∉ set (tl (get_clauses_wl S ∝ C)) ∧ get_clauses_wl S ∝ C ! 0 = L ∧
mset (tl (get_clauses_wl S ∝ C)) = remove1_mset L (mset (get_clauses_wl S ∝ C)) ∧
(∀L∈set (tl(get_clauses_wl S ∝ C)). - L ∉# the (get_conflict_wl S)) ∧
card_max_lvl (get_trail_wl S) (mset (tl (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S)) =
card_max_lvl (get_trail_wl S) (remove1_mset L (mset (get_clauses_wl S ∝ C)) ∪# the (get_conflict_wl S))›
‹L ∈ set (watched_l (get_clauses_wl S ∝ C))›
‹L ∈# mset (get_clauses_wl S ∝ C)›
using list_invs Sx hd nempty C_0 dist L_C K
by (cases ‹get_trail_wl S›; cases ‹get_clauses_wl S ∝ C›;
auto simp: twl_list_invs_def all_conj_distrib dest: in_set_takeD; fail)+
have max: ‹card_max_lvl (get_trail_wl S) ((mset (get_clauses_wl S ∝ C) - unmark (hd (get_trail_wl S))) ∪# the (get_conflict_wl S)) =
card_max_lvl (tl (get_trail_wl S)) (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#}) + Suc 0›
using multi_member_split[OF uL_D] L_C hd nempty n_d dist dist_C 1 ‹0 < count_decided (get_trail_wl S)› uL_C n_d
consistent_CNot_not_tautology[OF distinct_consistent_interp[OF n_d]
CNot_D[unfolded true_annots_true_cls]] CNot_C apply (cases ‹get_trail_wl S›;
auto simp: card_max_lvl_Cons card_max_lvl_add_mset subset_mset.sup_commute[of _ ‹remove1_mset _ _› ]
subset_mset.sup_commute[of _ ‹mset _›] tautology_add_mset)
apply (subst card_max_lvl_Cons)
apply (auto simp: card_max_lvl_Cons card_max_lvl_add_mset subset_mset.sup_commute[of _ ‹remove1_mset _ _› ]
subset_mset.sup_commute[of _ ‹mset _›] tautology_add_mset remove1_mset_union_distrib1)
using K uL_D apply presburger
done
have xx: ‹out_learned (tl (get_trail_wl S)) (Some (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#})) outl ⟷
out_learned (get_trail_wl S) (Some (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#})) outl› for outl
apply (subst tl_state_out_learned)
apply (cases ‹get_trail_wl S›; use L_C hd nempty dist dist_C in auto)
apply (meson distinct_mem_diff_mset distinct_mset_mset_distinct distinct_mset_union_mset union_single_eq_member)
apply (cases ‹get_trail_wl S›; use L_C hd nempty dist dist_C in auto)
apply (metis add_mset_commute distinct_mem_diff_mset distinct_mset_mset_distinct distinct_mset_union_mset union_single_eq_member)
apply (cases ‹get_trail_wl S›; use L_C hd nempty dist dist_C in auto)
..
have [simp]: ‹get_level (get_trail_wl S) L = count_decided (get_trail_wl S)›
by (cases ‹get_trail_wl S›; use L_C hd nempty dist dist_C in auto)
have yy: ‹out_learned (get_trail_wl S) (Some ((the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C)) - {#L, - L#})) outl ⟷
out_learned (get_trail_wl S) (Some ((mset (get_clauses_wl S ∝ C) - unmark (hd (get_trail_wl S))) ∪# the (get_conflict_wl S))) outl› for outl
by (use L_C hd nempty dist dist_C in ‹auto simp add: out_learned_def ac_simps›)
have xx: ‹out_learned (tl (get_trail_wl S)) (Some (the (get_conflict_wl S) ∪# mset (get_clauses_wl S ∝ C) - {#L, - L#})) =
out_learned (get_trail_wl S) (Some ((mset (get_clauses_wl S ∝ C) - unmark (hd (get_trail_wl S))) ∪# the (get_conflict_wl S)))›
using xx yy by (auto intro!: ext)
show ?thesis
using Sx x_xa C C_0 confl nempty uL_D L blits 1 2 card_max dist_C dist SC_0 max
consistent_CNot_not_tautology[OF distinct_consistent_interp[OF n_d]
CNot_D[unfolded true_annots_true_cls]] CNot_C K xx
‹0 < count_decided (get_trail_wl S)› size max_lvl s
literals_are_ℒ⇩i⇩n_literals_are_in_ℒ⇩i⇩n_conflict[OF Sx st_invs x_xa _ , of ‹all_atms_st S›]
literals_are_ℒ⇩i⇩n_literals_are_ℒ⇩i⇩n_trail[OF Sx st_invs x_xa _ , of ‹all_atms_st S›]
unfolding update_confl_tl_wl_pre'_def
by (clarsimp simp flip: all_lits_def simp add: hd mset_take_mset_drop_mset' ℒ⇩a⇩l⇩l_all_atms_all_lits)
qed
lemma (in -)out_learned_add_mset_highest_level:
‹L = lit_of (hd M) ⟹ out_learned M (Some (add_mset (- L) A)) outl ⟷
out_learned M (Some A) outl›
by (cases M)
(auto simp: out_learned_def get_level_cons_if atm_of_eq_atm_of count_decided_ge_get_level
uminus_lit_swap cong: if_cong
intro!: filter_mset_cong2)
lemma (in -)out_learned_tl_Some_notin:
‹is_proped (hd M) ⟹ lit_of (hd M) ∉# C ⟹ -lit_of (hd M) ∉# C ⟹
out_learned M (Some C) outl ⟷ out_learned (tl M) (Some C) outl›
by (cases M) (auto simp: out_learned_def get_level_cons_if atm_of_eq_atm_of
intro!: filter_mset_cong2)
lemma update_confl_tl_wl_heur_update_confl_tl_wl:
‹(uncurry2 (update_confl_tl_wl_heur), uncurry2 mop_update_confl_tl_wl) ∈
[λ_. True]⇩f
Id ×⇩f nat_rel ×⇩f twl_st_heur_conflict_ana' r lcount →
⟨bool_rel ×⇩f twl_st_heur_conflict_ana' r lcount⟩nres_rel›
proof -
have mop_update_confl_tl_wl_alt_def: ‹mop_update_confl_tl_wl = (λL C (M, N, D, NE, UE, WS, Q). do {
ASSERT(update_confl_tl_wl_pre L C (M, N, D, NE, UE, WS, Q));
N ← calculate_LBD_st M N C;
D ← RETURN (resolve_cls_wl' (M, N, D, NE, UE, WS, Q) C L);
N ← RETURN N;
_ ← RETURN ();
N ← RETURN N;
_ ← RETURN ();
RETURN (False, (tl M, N, Some D, NE, UE, WS, Q))
})›
by (auto simp: mop_update_confl_tl_wl_def update_confl_tl_wl_def calculate_LBD_st_def
intro!: ext)
define rr where
‹rr L M N C b n xs clvls outl = do {
((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 (nxs) = lookup_conflict_remove1 L (n, xs);
RETURN ((b, (nxs)), clvls, outl) }›
for L M N C b n xs clvls lbd outl
have update_confl_tl_wl_heur_alt_def:
‹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) ← rr L M N C b n xs clvls outl;
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)
})›
by (auto simp: update_confl_tl_wl_heur_def Let_def rr_def intro!: ext bind_cong[OF refl])
note [[goals_limit=1]]
have rr: ‹(((x1g, x2g), S),
(x1, x2), x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f)
∈ nat_lit_lit_rel ×⇩f nat_rel ×⇩f twl_st_heur_conflict_ana' r lcount ⟹
CLS = ((x1, x2), x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f) ⟹
CLS' = ((x1g, x2g), S, s, t) ⟹
update_confl_tl_wl_pre x1 x2 (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f) ⟹
1 ≤ x1q ⟹
arena_is_valid_clause_idx x1i x2g ⟹
(x1k, (x1l, x2k)) = get_conflict_wl_heur S ⟹
rr x1g (get_trail_wl_heur S) (get_clauses_wl_heur S) x2g x1k x1l x2k (get_count_max_lvls_heur S)
(get_outlearned_heur S)
≤ ⇓ {((C, clvls, outl), D). (C, Some D) ∈ option_lookup_clause_rel (all_atms_st (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f)) ∧
clvls = card_max_lvl x1a (remove1_mset x1 (mset (x1b ∝ x2)) ∪# the x1c) ∧
out_learned x1a (Some (remove1_mset x1 (mset (x1b ∝ x2)) ∪# the x1c)) (outl) ∧
size (remove1_mset x1 (mset (x1b ∝ x2)) ∪# the x1c) =
size ((mset (x1b ∝ x2)) ∪# the x1c - {#x1, -x1#}) + Suc 0 ∧
D = resolve_cls_wl' (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f) x2 x1}
(RETURN (resolve_cls_wl' (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f) x2 x1))›
for m n p q ra s t x1 x2 x1a x1b x1c x1d x1e x1f x2f x1g x2g x1h x1i x1k
x1l x2k x1m x1n x1p x1q x1r x1t CLS CLS' NS US x1s S
unfolding rr_def
apply (refine_vcg lhs_step_If)
apply (rule isasat_lookup_merge_eq2_lookup_merge_eq2[where
vdom = ‹set (get_vdom S)› and M = x1a and N = x1b and C = x1c and
𝒜 = ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f) ›, THEN order_trans])
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre' simp: update_confl_tl_wl_pre'_def)
subgoal by (auto simp: literals_are_in_ℒ⇩i⇩n_mm_def all_lits_st_def all_lits_of_mm_union
all_lits_def
simp flip: all_lits_st_alt_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal unfolding Down_id_eq
apply (rule lookup_merge_eq2_spec[where M = x1a and C = ‹the x1c› and
𝒜 = ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f)›, THEN order_trans])
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def literals_are_in_ℒ⇩i⇩n_mm_def all_lits_st_def all_lits_of_mm_union
all_lits_def simp flip: all_lits_st_alt_def
intro!: literals_are_in_ℒ⇩i⇩n_mm_literals_are_in_ℒ⇩i⇩n)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def counts_maximum_level_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_lifting twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_lifting twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def merge_conflict_m_eq2_def conc_fun_SPEC lookup_conflict_remove1_pre_def
atms_of_def
option_lookup_clause_rel_def lookup_clause_rel_def resolve_cls_wl'_def lookup_conflict_remove1_def
remove1_mset_union_distrib1 remove1_mset_union_distrib2 subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
subset_mset.sup_commute[of _ ‹mset (_ ∝ _)›]
simp flip: all_lits_st_alt_def[symmetric]
intro!: mset_as_position_remove3
intro!: ASSERT_leI)
done
subgoal
apply (subst (asm) arena_lifting(4)[where vdom = ‹set (get_vdom_aivdom (get_aivdom S))› and N = x1b, symmetric])
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def)
apply (rule isa_resolve_merge_conflict_gt2[where
𝒜 = ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f)› and vdom = ‹set (get_vdom_aivdom (get_aivdom S))›,
THEN fref_to_Down_curry5, of x1a x1b x2g x1c ‹get_count_max_lvls_heur S› ‹get_outlearned_heur S›,
THEN order_trans])
subgoal unfolding merge_conflict_m_pre_def
by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def counts_maximum_level_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal
by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def conc_fun_SPEC lookup_conflict_remove1_pre_def atms_of_def
option_lookup_clause_rel_def lookup_clause_rel_def resolve_cls_wl'_def
merge_conflict_m_def lookup_conflict_remove1_def subset_mset.sup_commute[of _ ‹mset (_ ∝ _)›]
remove1_mset_union_distrib1 remove1_mset_union_distrib2
simp flip: all_lits_st_alt_def[symmetric]
intro!: mset_as_position_remove3
intro!: ASSERT_leI)
done
done
have rr: ‹(((x1g, x2g), S),
(x1, x2), x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja)
∈ nat_lit_lit_rel ×⇩f nat_rel ×⇩f twl_st_heur_conflict_ana' r lcount ⟹
CLS = ((x1, x2), x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja) ⟹
CLS' = ((x1g, x2g), S) ⟹
get_conflict_wl_heur S = (x1k, (x1l, x2k)) ⟹
update_confl_tl_wl_pre x1 x2
(x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja) ⟹
((x1t, x2t :: bool list), x1b)
∈ {((arena', lbd), N').
valid_arena arena' N'
(set (get_vdom
(snd ((x1g, x2g), S)))) ∧
N = N' ∧ length x1i = length arena'} ⟹
1 ≤ x1p ⟹
arena_is_valid_clause_idx x1t x2g ⟹
rr x1g (get_trail_wl_heur S) x1t x2g x1k x1l x2k (get_count_max_lvls_heur S)
(get_outlearned_heur S)
≤ ⇓ {((C, clvls, outl), D). (C, Some D) ∈ option_lookup_clause_rel (all_atms_st (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja)) ∧
clvls = card_max_lvl x1a (remove1_mset x1 (mset (x1b ∝ x2)) ∪# the x1c) ∧
out_learned x1a (Some (remove1_mset x1 (mset (x1b ∝ x2)) ∪# the x1c)) (outl) ∧
size (remove1_mset x1 (mset (x1b ∝ x2)) ∪# the x1c) =
size ((mset (x1b ∝ x2)) ∪# the x1c - {#x1, -x1#}) + Suc 0 ∧
D = resolve_cls_wl' (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja) x2 x1}
(RETURN (resolve_cls_wl' (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja) x2 x1))›
for l m n p q ra s ha ia ja x1 x2 x1a x1b x1c x1d x1e x1f x1g x2g x1h x1i
x1k x1l x2k x1m x1n x1o x1p x1q x1r x1s N x1t x2t CLS CLS' S
unfolding rr_def
apply (refine_vcg lhs_step_If)
apply (rule isasat_lookup_merge_eq2_lookup_merge_eq2[where
vdom = ‹set (get_vdom S)› and M = x1a and N = x1b and C = x1c and
𝒜 = ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja)›, THEN order_trans])
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre' simp: update_confl_tl_wl_pre'_def)
subgoal by auto
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal unfolding Down_id_eq
apply (rule lookup_merge_eq2_spec[where M = x1a and C = ‹the x1c› and
𝒜 = ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja)›, THEN order_trans])
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def intro!: literals_are_in_ℒ⇩i⇩n_mm_literals_are_in_ℒ⇩i⇩n)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def counts_maximum_level_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_lifting twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_lifting twl_st_heur_conflict_ana_def
dest: in_set_takeD)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def merge_conflict_m_eq2_def conc_fun_SPEC lookup_conflict_remove1_pre_def
atms_of_def
option_lookup_clause_rel_def lookup_clause_rel_def resolve_cls_wl'_def lookup_conflict_remove1_def
remove1_mset_union_distrib1 remove1_mset_union_distrib2 subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
subset_mset.sup_commute[of _ ‹mset (_ ∝ _)›]
simp flip: all_lits_st_alt_def
intro!: mset_as_position_remove3
intro!: ASSERT_leI)
done
subgoal
apply (subst (asm) arena_lifting(4)[where vdom = ‹set (get_vdom_aivdom (get_aivdom S))› and N = x1b, symmetric])
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def)
apply (rule isa_resolve_merge_conflict_gt2[where
𝒜 = ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja)› and vdom = ‹set (get_vdom_aivdom (get_aivdom S))›,
THEN fref_to_Down_curry5, of x1a x1b x2g x1c ‹get_count_max_lvls_heur S› ‹get_outlearned_heur S›,
THEN order_trans])
subgoal unfolding merge_conflict_m_pre_def
by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def twl_st_heur_conflict_ana_def counts_maximum_level_def)
subgoal by (auto simp: twl_st_heur_conflict_ana_def)
subgoal
by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def conc_fun_SPEC lookup_conflict_remove1_pre_def atms_of_def
option_lookup_clause_rel_def lookup_clause_rel_def resolve_cls_wl'_def
merge_conflict_m_def lookup_conflict_remove1_def subset_mset.sup_commute[of _ ‹mset (_ ∝ _)›]
remove1_mset_union_distrib1 remove1_mset_union_distrib2
intro!: mset_as_position_remove3
simp flip: all_lits_st_alt_def
intro!: ASSERT_leI)
done
done
have all_in_dom: ‹∀C∈set (N ∝ x2).
C ∈# ℒ⇩a⇩l⇩l (all_atms_st (x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la))› if
‹valid_arena x1t N vdom›
‹x2 ∈# dom_m N›
for x2 x1t C x1a N x1c x2d x1e x1f ha ia ja ka la x1d vdom
apply (intro ballI)
subgoal for C
using that(2)
by (auto intro!: literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l in_clause_in_all_lits_of_m
simp: literals_are_in_ℒ⇩i⇩n_def all_atms_st_def all_atms_def all_lits_def
all_lits_of_mm_add_mset ℒ⇩a⇩l⇩l_union ran_m_def ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm
dest!: multi_member_split[of _ ‹dom_m _›])
done
have all_in_do: ‹C∈set [x2..<x2 + arena_length x1t x2] ⟹
arena_lit x1t C ∈# ℒ⇩a⇩l⇩l (all_atms_st (x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la))› if
‹valid_arena x1t N vdom›
‹x2 ∈# dom_m N›
for x2 x1t C x1a N x1c x2d x1e x1f ha ia ja ka la x1d vdom
apply (subst (asm) arena_lifting(4)[OF that, symmetric])
using that(2) arena_lifting(5)[OF that, of ‹C - x2›, symmetric]
by (auto intro!: literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l in_clause_in_all_lits_of_m
simp: literals_are_in_ℒ⇩i⇩n_def all_atms_st_def all_atms_def all_lits_def
all_lits_of_mm_add_mset ℒ⇩a⇩l⇩l_union ran_m_def ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm
dest!: multi_member_split[of _ ‹dom_m _›])
have isa_vmtf_mark_to_rescore_clause: ‹
(((x1g, x2g), S), (x1, x2), x1a, x1b, x1c, x1d,
x1e, x1f, ha, ia, ja, ka, la)
∈ nat_lit_lit_rel ×⇩f nat_rel ×⇩f twl_st_heur_conflict_ana' r lcount ⟹
CLS = ((x1, x2), x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la) ⟹
CLS' = ((x1g, x2g), S) ⟹
update_confl_tl_wl_pre x1 x2 (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la) ⟹
((x1t, x2t), N)
∈ {((arena', lbd), N').
valid_arena arena' N'
(set (get_vdom (snd ((x1g, x2g), S)))) ∧
x1b = N' ∧ length x1i = length arena'} ⟹
1 ≤ x1p ⟹
arena_is_valid_clause_idx x1t x2g ⟹
(((x1v, x1w, x2v), x1x, x2x), D)
∈ {a. case a of
(a, b) ⇒
(case a of
(C, a) ⇒
case a of
(clvls, outl) ⇒
λD. (C, Some D) ∈ option_lookup_clause_rel (all_atms_st (x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la)) ∧
clvls = card_max_lvl x1a (remove1_mset x1 (mset (N ∝ x2)) ∪# the x1c) ∧
out_learned x1a (Some (remove1_mset x1 (mset (N ∝ x2)) ∪# the x1c)) outl ∧
size (remove1_mset x1 (mset (N ∝ x2)) ∪# the x1c) = size (mset (N ∝ x2) ∪# the x1c - {#x1, - x1#}) + Suc 0 ∧
D = resolve_cls_wl' (x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la) x2 x1)
b} ⟹
arena_act_pre x1t x2g ⟹
isa_vmtf_bump_to_rescore_also_reasons_cl (get_trail_wl_heur S) x1t x2g (-x1g) (get_vmtf_heur S)
≤ ⇓ {(vm, N'). N = N' ∧ vm ∈ bump_heur (all_atms_st (x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la)) x1a}
(RETURN N)›
for l m n p q ra s ha ia ja ka la x1 x2 x1a x1b x1c x1d x1e x1f x1g x2g x1h x1i x1k x1l x2k
x1m x1n x1o x1p x1q x1r x1s N x1t x2t D x1v x1w x2v x1x x2x CLS CLS' S
unfolding twl_st_heur_conflict_ana_def apply (clarsimp simp only: prod_rel_iff)
subgoal
apply (rule isa_vmtf_bump_to_rescore_also_reasons_cl_vmtf_mark_to_rescore_also_reasons_cl[
where 𝒜 = ‹all_atms_st (x1a, N, x1c, x1d, x1e, x1f, ha, ia, ja, ka, la)›,
THEN fref_to_Down_curry4,
of _ _ _ _ _ x1a x1t x2 ‹-x1› ‹get_vmtf_heur S›,
THEN order_trans])
subgoal by (simp add: twl_st_heur_conflict_ana_def)
subgoal by (auto simp add: twl_st_heur_conflict_ana_def)
subgoal
apply (rule ref_two_step'[THEN order_trans, OF vmtf_mark_to_rescore_also_reasons_cl_spec,
of _ _ x1a _
N ‹set (get_vdom_aivdom (get_aivdom S))›])
subgoal by (auto simp: )
subgoal by (auto simp: update_confl_tl_wl_pre_def update_confl_tl_l_pre_def
twl_st_l_def state_wl_l_def)
subgoal by (auto simp: update_confl_tl_wl_pre_def update_confl_tl_l_pre_def
twl_st_l_def state_wl_l_def)
subgoal by auto
subgoal
by (rule all_in_dom)
(auto simp: update_confl_tl_wl_pre_def update_confl_tl_l_pre_def ran_m_def
twl_st_l_def state_wl_l_def)
subgoal
by (intro conjI impI ballI allI,
(auto simp: update_confl_tl_wl_pre_def update_confl_tl_l_pre_def ran_m_def
twl_st_l_def state_wl_l_def twl_list_invs_def)[])
(rule all_in_do,
auto simp: update_confl_tl_wl_pre_def update_confl_tl_l_pre_def ran_m_def
twl_st_l_def state_wl_l_def twl_list_invs_def)
subgoal by (auto simp: RETURN_def conc_fun_RES)
done
done
done
have isa_bump_unset: ‹isa_bump_unset L x ≤ ⇓{(a, _). a ∈ bump_heur 𝒜 (tl M)} (RETURN ())›
if
vmtf: ‹x∈ bump_heur 𝒜 M› and
L_N: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and [simp]: ‹M ≠ []› and
nz: ‹count_decided M > 0› and
L: ‹L = atm_of (lit_of (hd M))› for L x M 𝒜
unfolding L
by (rule isa_bump_unset_vmtf_tl[OF that(1-4)[unfolded L], THEN order_trans])
(auto simp: conc_fun_RES RETURN_def)
have mset_tl_nth_0: ‹length Na > 0 ⟹ mset (tl (Na)) = mset Na - {#(Na ! 0)#}› for Na
by (cases Na) auto
show ?thesis
supply [[goals_limit = 1]]
supply RETURN_as_SPEC_refine[refine2 del]
update_confl_tl_wl_pre_update_confl_tl_wl_pre'[dest!]
apply (intro frefI nres_relI)
subgoal for CLS' CLS
apply (cases CLS'; cases CLS; hypsubst+)
unfolding uncurry_def update_confl_tl_wl_heur_alt_def comp_def Let_def
update_confl_tl_wl_def mop_update_confl_tl_wl_alt_def prod.case
apply (refine_rcg calculate_LBD_heur_st_calculate_LBD_st[where
vdom = ‹set (get_vdom (snd CLS'))› and
𝒜 = ‹all_atms_st (snd CLS)›]
isa_bump_unset[where 𝒜3 = ‹all_atms_st (snd CLS)› and M3 = ‹get_trail_wl (snd CLS)›];
remove_dummy_vars)
subgoal
by (auto simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
RES_RETURN_RES RETURN_def counts_maximum_level_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_is_valid_clause_idx_def twl_st_heur_conflict_ana_def)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_is_valid_clause_idx_def twl_st_heur_conflict_ana_def)
subgoal
using literals_are_in_ℒ⇩i⇩n_nth[of ‹snd (fst CLS)› ‹snd CLS›
‹all_atms_st (snd CLS)›, simplified]
by (auto
simp: update_confl_tl_wl_pre'_def arena_is_valid_clause_idx_def twl_st_heur_conflict_ana_def)
subgoal by auto
subgoal
by (auto simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
RES_RETURN_RES RETURN_def counts_maximum_level_def)
subgoal by (auto intro!: exI[of _ ‹get_clauses_wl (snd CLS)›] exI[of _ ‹set (get_vdom (snd CLS'))›]
simp: update_confl_tl_wl_pre'_def arena_is_valid_clause_idx_def twl_st_heur_conflict_ana_def)
apply (rule rr; assumption)
subgoal by (simp add: arena_act_pre_def)
apply (rule isa_vmtf_mark_to_rescore_clause; assumption)
subgoal by (auto dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_is_valid_clause_idx_def twl_st_heur_conflict_ana_def
simp flip: all_lits_st_alt_def
intro!: isa_bump_unset_pre
dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of _ M ‹lit_of (hd M)› for M])
subgoal for m n p q ra s t ha ia ja x1 x2 x1a x1b x1c x1d x1e x1f x1g x2g x1h x1i
x1k x1l x2k x1m x1n x1o x1p x1q x1r x1t
by (rule tl_trailt_tr_pre[of x1 _ ‹all_atms_st (x1, x1i, x1a, x1b, x1c, x1d, n, p, q, ra, s, t, ha)›])
(clarsimp_all dest!: update_confl_tl_wl_pre_update_confl_tl_wl_pre'
simp: update_confl_tl_wl_pre'_def arena_is_valid_clause_idx_def twl_st_heur_conflict_ana_def
simp flip: all_lits_st_alt_def
intro!: tl_trailt_tr_pre)
subgoal by auto
subgoal apply (clarsimp simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
valid_arena_mark_used subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
tl_trail_tr[THEN fref_to_Down_unRET] resolve_cls_wl'_def isa_bump_unset_vmtf_tl no_dup_tlD
counts_maximum_level_def
simp flip: all_lits_st_alt_def
dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of _ M ‹lit_of (hd M)› for M])
apply (meson all_in_dom atm_of_lit_in_atms_of)
by (meson atm_of_in_atms_of literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l)+
subgoal by (clarsimp simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
valid_arena_mark_used subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
tl_trail_tr[THEN fref_to_Down_unRET] resolve_cls_wl'_def isa_bump_unset_vmtf_tl no_dup_tlD
counts_maximum_level_def
simp flip: all_lits_st_alt_def
dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of _ M ‹lit_of (hd M)› for M])
subgoal by (clarsimp simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
valid_arena_mark_used subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
tl_trail_tr[THEN fref_to_Down_unRET] resolve_cls_wl'_def isa_bump_unset_vmtf_tl no_dup_tlD
counts_maximum_level_def
simp flip: all_lits_st_alt_def
dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of _ M ‹lit_of (hd M)› for M])
subgoal by (clarsimp simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
valid_arena_mark_used subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
tl_trail_tr[THEN fref_to_Down_unRET] resolve_cls_wl'_def isa_bump_unset_vmtf_tl no_dup_tlD
counts_maximum_level_def
simp flip: all_lits_st_alt_def
dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of _ M ‹lit_of (hd M)› for M])
subgoal by (clarsimp simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
valid_arena_mark_used subset_mset.sup_commute[of _ ‹remove1_mset _ _›]
tl_trail_tr[THEN fref_to_Down_unRET] resolve_cls_wl'_def isa_bump_unset_vmtf_tl no_dup_tlD
counts_maximum_level_def
simp flip: all_lits_st_alt_def
dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of _ M ‹lit_of (hd M)› for M])
done
done
qed
lemma phase_saving_le: ‹phase_saving 𝒜 φ ⟹ A ∈# 𝒜 ⟹ A < length φ›
‹phase_saving 𝒜 φ ⟹ B ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ atm_of B < length φ›
by (auto simp: phase_saving_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
lemma trail_pol_nempty: ‹¬(([], aa, ab, ac, ad, b), L # ys) ∈ trail_pol 𝒜›
by (auto simp: trail_pol_def ann_lits_split_reasons_def)
lemma is_decided_hd_trail_wl_heur_hd_get_trail:
‹(RETURN o is_decided_hd_trail_wl_heur, RETURN o (λM. is_decided (hd (get_trail_wl M))))
∈ [λM. get_trail_wl M ≠ []]⇩f twl_st_heur_conflict_ana' r lcount → ⟨bool_rel⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: is_decided_hd_trail_wl_heur_def twl_st_heur_conflict_ana_def neq_Nil_conv
trail_pol_def ann_lits_split_reasons_def is_decided_no_proped_iff last_trail_pol_def
split: option.splits)
lemma skip_and_resolve_loop_wl_D_heur_alt_def:
‹skip_and_resolve_loop_wl_D_heur S⇩0 =
do {
(_, S) ←
WHILE⇩T⇗skip_and_resolve_loop_wl_D_heur_inv S⇩0⇖
(λ(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⇩0);
RETURN S
}
›
unfolding IsaSAT_Profile.start_def IsaSAT_Profile.stop_def nres_monad1
skip_and_resolve_loop_wl_D_heur_def ..
lemma atm_is_in_conflict_st_heur_is_in_conflict_st:
‹(uncurry (atm_is_in_conflict_st_heur), uncurry (mop_lit_notin_conflict_wl)) ∈
[λ(L, S). True]⇩f
Id ×⇩r twl_st_heur_conflict_ana → ⟨Id⟩ nres_rel›
proof -
have 1: ‹aaa ∈# ℒ⇩a⇩l⇩l A ⟹ atm_of aaa ∈ atms_of (ℒ⇩a⇩l⇩l A)› for aaa A
by (auto simp: atms_of_def)
show ?thesis
unfolding atm_is_in_conflict_st_heur_def twl_st_heur_def option_lookup_clause_rel_def uncurry_def comp_def
mop_lit_notin_conflict_wl_def twl_st_heur_conflict_ana_def
apply (intro frefI nres_relI)
apply refine_rcg
apply clarsimp
subgoal
apply (rule atm_in_conflict_lookup_pre[of _ ‹all_atms_st _›])
unfolding ℒ⇩a⇩l⇩l_all_atms_all_lits[symmetric] all_lits_st_alt_def[symmetric]
apply auto
done
subgoal for x y x1 x2 x1a x2a x1b x2b
apply (subst atm_in_conflict_lookup_atm_in_conflict[THEN fref_to_Down_unRET_uncurry_Id, of ‹all_atms_st x2› ‹atm_of x1› ‹the (get_conflict_wl (snd y))›])
apply (simp add: ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def all_lits_st_alt_def[symmetric])[]
apply (auto simp add: ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def option_lookup_clause_rel_def)[]
apply (simp add: atm_in_conflict_def atm_of_in_atms_of)
done
done
qed
lemma skip_and_resolve_loop_wl_alt_def:
‹skip_and_resolve_loop_wl S⇩0 =
do {
ASSERT(get_conflict_wl S⇩0 ≠ None);
(_, S) ←
WHILE⇩T⇗λ(brk, S). skip_and_resolve_loop_wl_inv S⇩0 brk S⇖
(λ(brk, S). ¬brk ∧ ¬is_decided (hd (get_trail_wl S)))
(λ(_, S).
do {
(L, C) ← mop_hd_trail_wl S;
b ← mop_lit_notin_conflict_wl (-L) S;
if b then
mop_tl_state_wl S
else do {
b ← mop_maximum_level_removed_wl L S;
if b
then do {
mop_update_confl_tl_wl L C S
}
else
do {RETURN (True, S)}
}
}
)
(False, S⇩0);
RETURN S
}›
unfolding skip_and_resolve_loop_wl_def calculate_LBD_st_def IsaSAT_Profile.start_def
IsaSAT_Profile.stop_def
by (auto cong: if_cong)
lemma skip_and_resolve_loop_wl_D_heur_skip_and_resolve_loop_wl_D:
‹(skip_and_resolve_loop_wl_D_heur, skip_and_resolve_loop_wl)
∈ twl_st_heur_conflict_ana' r lcount →⇩f ⟨twl_st_heur_conflict_ana' r lcount⟩nres_rel›
proof -
have H[refine0]: ‹(x, y) ∈ twl_st_heur_conflict_ana' r lcount ⟹
((False, x), False, y)
∈ bool_rel ×⇩f
twl_st_heur_conflict_ana' r lcount› for x y
by auto
have H1: ‹(xa, x')
∈ bool_rel ×⇩f
twl_st_heur_conflict_ana' r lcount ⟹
case x' of (x, xa) ⇒ skip_and_resolve_loop_wl_inv y x xa ⟹
xa = (x1, x2) ⟹
x' = (x1a, x2a) ⟹ (x2, x2a) ∈ twl_st_heur_conflict_ana' r lcount› for xa x' x1 x2 x1a x2a y
by auto
show ?thesis
supply [[goals_limit=1]]
unfolding skip_and_resolve_loop_wl_D_heur_alt_def skip_and_resolve_loop_wl_alt_def
apply (intro frefI nres_relI)
apply (refine_vcg
update_confl_tl_wl_heur_update_confl_tl_wl[THEN fref_to_Down_curry2, unfolded comp_def]
maximum_level_removed_eq_count_dec_heur_maximum_level_removed_eq_count_dec
[THEN fref_to_Down_curry] lit_and_ann_of_propagated_st_heur_lit_and_ann_of_propagated_st[THEN fref_to_Down]
tl_state_wl_heur_tl_state_wl[THEN fref_to_Down]
atm_is_in_conflict_st_heur_is_in_conflict_st[THEN fref_to_Down_curry])
subgoal for S T brkS brkT
unfolding skip_and_resolve_loop_wl_D_heur_inv_def
apply (subst case_prod_beta)
apply (rule exI[of _ ‹snd brkT›])
apply (rule exI[of _ ‹T›])
apply (subst (asm) (1) surjective_pairing[of brkS])
apply (subst (asm) surjective_pairing[of brkT])
unfolding prod_rel_iff
by auto
subgoal for x y xa x' x1 x2 x1a x2a
apply (subst is_decided_hd_trail_wl_heur_hd_get_trail[of r, THEN fref_to_Down_unRET_Id, of x2a])
subgoal
unfolding skip_and_resolve_loop_wl_inv_def skip_and_resolve_loop_inv_l_def skip_and_resolve_loop_inv_def
apply (subst (asm) case_prod_beta)+
unfolding prod.case
apply normalize_goal+
by (auto simp: )
apply (rule H1; assumption)
subgoal by auto
done
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemmas get_learned_count_learned_clss_countD =
get_learned_count_learned_clss_countD2
end