theory IsaSAT_Conflict_Analysis
imports IsaSAT_Setup IsaSAT_VMTF
begin
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)›
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)›
lemma get_maximum_level_eq_count_decided_iff:
‹ya ≠ {#} ⟹ get_maximum_level xa ya = count_decided xa ⟷ (∃L ∈# ya. get_level xa L = count_decided xa)›
apply (rule iffI)
defer
subgoal
using count_decided_ge_get_maximum_level[of xa]
apply (auto dest!: multi_member_split dest: le_antisym simp: get_maximum_level_add_mset max_def)
using le_antisym by blast
subgoal
using get_maximum_level_exists_lit_of_max_level[of ya xa]
by auto
done
lemma get_maximum_level_card_max_lvl_ge1:
‹count_decided xa > 0 ⟹ get_maximum_level xa ya = count_decided xa ⟷ card_max_lvl xa ya > 0›
apply (cases ‹ya = {#}›)
subgoal by auto
subgoal
by (auto simp: card_max_lvl_def get_maximum_level_eq_count_decided_iff dest: multi_member_split
dest!: multi_nonempty_split[of ‹filter_mset _ _›] filter_mset_eq_add_msetD
simp flip: nonempty_has_size)
done
lemma card_max_lvl_remove_hd_trail_iff:
‹xa ≠ [] ⟹ - lit_of (hd xa) ∈# ya ⟹ 0 < card_max_lvl xa (remove1_mset (- lit_of (hd xa)) ya) ⟷ Suc 0 < card_max_lvl xa ya›
by (cases xa)
(auto dest!: multi_member_split simp: card_max_lvl_add_mset)
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 get_trail_wl_heur_def: ‹get_trail_wl_heur = (λ(M, S). M)›
by (intro ext, rename_tac S, case_tac S) auto
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
:: ‹twl_st_wl_heur ⇒ (nat literal × nat) nres›
where
‹lit_and_ann_of_propagated_st_heur = (λ((M, _, _, reasons, _), _). do {
ASSERT(M ≠ [] ∧ atm_of (last M) < length reasons);
RETURN (last M, reasons ! (atm_of (last M)))})›
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 (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_heur_pre :: ‹twl_st_wl_heur ⇒ bool› where
‹tl_state_wl_heur_pre =
(λ(M, N, D, WS, Q, ((A, m, fst_As, lst_As, next_search), to_remove), _). fst M ≠ [] ∧
tl_trailt_tr_pre M ∧
vmtf_unset_pre (atm_of (last (fst M))) ((A, m, fst_As, lst_As, next_search), to_remove) ∧
atm_of (last (fst M)) < length A ∧
(next_search ≠ None ⟶ the next_search < length A))›
definition tl_state_wl_heur :: ‹twl_st_wl_heur ⇒ (bool × twl_st_wl_heur) nres› where
‹tl_state_wl_heur = (λ(M, N, D, WS, Q, vmtf, clvls). do {
ASSERT(tl_state_wl_heur_pre (M, N, D, WS, Q, vmtf, clvls));
RETURN (False, (tl_trailt_tr M, N, D, WS, Q, isa_vmtf_unset (atm_of (lit_of_last_trail_pol M)) vmtf, clvls))
})›
lemma tl_state_wl_heur_alt_def:
‹tl_state_wl_heur = (λ(M, N, D, WS, Q, vmtf, clvls). do {
ASSERT(tl_state_wl_heur_pre (M, N, D, WS, Q, vmtf, clvls));
let L = lit_of_last_trail_pol M;
RETURN (False, (tl_trailt_tr M, N, D, WS, Q, isa_vmtf_unset (atm_of L) vmtf, clvls))
})›
by (auto simp: tl_state_wl_heur_def Let_def intro!: ext)
lemma card_max_lvl_Cons:
assumes ‹no_dup (L # a)› ‹distinct_mset y›‹¬tautology y› ‹¬is_decided L›
shows ‹card_max_lvl (L # a) y =
(if (lit_of L ∈# y ∨ -lit_of L ∈# y) ∧ count_decided a ≠ 0 then card_max_lvl a y + 1
else card_max_lvl a y)›
proof -
have [simp]: ‹count_decided a = 0 ⟹ get_level a L = 0› for L
by (simp add: count_decided_0_iff)
have [simp]: ‹lit_of L ∉# A ⟹
- lit_of L ∉# A ⟹
{#La ∈# A. La ≠ lit_of L ∧ La ≠ - lit_of L ⟶ get_level a La = b#} =
{#La ∈# A. get_level a La = b#}› for A b
apply (rule filter_mset_cong)
apply (rule refl)
by auto
show ?thesis
using assms by (auto simp: card_max_lvl_def get_level_cons_if tautology_add_mset
atm_of_eq_atm_of
dest!: multi_member_split)
qed
lemma card_max_lvl_tl:
assumes ‹a ≠ []› ‹distinct_mset y›‹¬tautology y› ‹¬is_decided (hd a)› ‹no_dup a›
‹count_decided a ≠ 0›
shows ‹card_max_lvl (tl a) y =
(if (lit_of(hd a) ∈# y ∨ -lit_of(hd a) ∈# y)
then card_max_lvl a y - 1 else card_max_lvl a y)›
using assms by (cases a) (auto simp: card_max_lvl_Cons)
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›
using tl_trailt_tr_pre[of ‹get_trail_wl y› ‹get_trail_wl_heur x› ‹all_atms_st y›]
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
intro!: vmtf_unset_pre'[where M = ‹get_trail_wl y›])
apply (auto simp: neq_Nil_conv literals_are_in_ℒ⇩i⇩n_trail_Cons phase_saving_def isa_vmtf_def
vmtf_def
dest!: multi_member_split)
done
lemma mop_tl_state_wl_pre_simps:
‹mop_tl_state_wl_pre ([], ax, ay, az, bga, NS, US, bh, bi) ⟷ False›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NS, US, bh, bi) ⟹
lit_of (hd xa) ∈# ℒ⇩a⇩l⇩l (all_atms ax (az + bga + NS + US))›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NS, US, bh, bi) ⟹ lit_of (hd xa) ∉# the ay›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NS, US, bh, bi) ⟹ -lit_of (hd xa) ∉# the ay›
‹mop_tl_state_wl_pre (xa, ax, Some ay', az, bga, NS, US, bh, bi) ⟹ lit_of (hd xa) ∉# ay'›
‹mop_tl_state_wl_pre (xa, ax, Some ay', az, bga, NS, US, bh, bi) ⟹ -lit_of (hd xa) ∉# ay'›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NS, US, bh, bi) ⟹ is_proped (hd xa)›
‹mop_tl_state_wl_pre (xa, ax, ay, az, bga, NS, US, 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_alt_def2)
done
abbreviation twl_st_heur_conflict_ana' :: ‹nat ⇒ (twl_st_wl_heur × nat twl_st_wl) set› where
‹twl_st_heur_conflict_ana' r ≡ {(S, T). (S, T) ∈ twl_st_heur_conflict_ana ∧
length (get_clauses_wl_heur S) = r}›
lemma tl_state_wl_heur_tl_state_wl:
‹(tl_state_wl_heur, mop_tl_state_wl) ∈
[λ_. True]⇩f twl_st_heur_conflict_ana' r → ⟨bool_rel ×⇩f twl_st_heur_conflict_ana' r⟩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 a b aa ba ab bb ac bc ad bd ae be
using mop_tl_state_wl_pre_tl_state_wl_heur_pre[of x y] by simp
subgoal
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
intro!: tl_trail_tr[THEN fref_to_Down_unRET] isa_vmtf_tl_isa_vmtf)
apply (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id])
apply (auto simp: lit_of_hd_trail_def mop_tl_state_wl_pre_simps counts_maximum_level_def)
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›
definition update_confl_tl_wl_heur
:: ‹nat literal ⇒ nat ⇒ twl_st_wl_heur ⇒ (bool × twl_st_wl_heur) nres›
where
‹update_confl_tl_wl_heur = (λL C (M, N, (b, (n, xs)), Q, W, vm, clvls, cach, lbd, outl, stats). do {
ASSERT (clvls ≥ 1);
let L' = atm_of L;
ASSERT(arena_is_valid_clause_idx N C);
((b, (n, xs)), clvls, lbd, outl) ←
if arena_length N C = 2 then isasat_lookup_merge_eq2 L M N C (b, (n, xs)) clvls lbd outl
else isa_resolve_merge_conflict_gt2 M N C (b, (n, xs)) clvls lbd 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);
let N = mark_used N C;
ASSERT(arena_act_pre N C);
let N = arena_incr_act N C;
ASSERT(vmtf_unset_pre L' vm);
ASSERT(tl_trailt_tr_pre M);
RETURN (False, (tl_trailt_tr M, N, (b, (n, xs)), Q, W, isa_vmtf_unset L' vm,
clvls - 1, cach, lbd, outl, stats))
})›
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 ∈# ℒ⇩a⇩l⇩l (all_atms_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
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›
apply (subst (2) subset_mset.sup.commute)
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, hide_lams) ‹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 dest!: 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 remove1_mset_union_distrib2)
by (simp add: distinct_mset_remove1_All[of ‹mset (get_clauses_wl S ∝ C)›])
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 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 mset_as_position_remove3:
‹mset_as_position xs (D - {#L#}) ⟹ atm_of L < length xs ⟹ distinct_mset D ⟹
mset_as_position (xs[atm_of L := None]) (D - {#L, -L#})›
using mset_as_position_remove2[of xs ‹D - {#L#}› ‹L›] mset_as_position_tautology[of xs ‹remove1_mset L D›]
mset_as_position_distinct_mset[of xs ‹remove1_mset L D›]
by (cases ‹L ∈# D›; cases ‹-L ∈# D›)
(auto dest!: multi_member_split simp: minus_notin_trivial ac_simps add_mset_eq_add_mset tautology_add_mset)
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 → ⟨bool_rel ×⇩f twl_st_heur_conflict_ana' r⟩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));
D ← RETURN (resolve_cls_wl' (M, N, D, NE, UE, WS, Q) C L);
N ← RETURN N;
N ← RETURN N;
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 intro!: ext)
define rr where
‹rr L M N C b n xs clvls lbd outl = do {
((b, (n, xs)), clvls, lbd, outl) ←
if arena_length N C = 2 then isasat_lookup_merge_eq2 L M N C (b, (n, xs)) clvls lbd outl
else isa_resolve_merge_conflict_gt2 M N C (b, (n, xs)) clvls lbd outl;
ASSERT(curry lookup_conflict_remove1_pre L (n, xs) ∧ clvls ≥ 1);
let (nxs) = lookup_conflict_remove1 L (n, xs);
RETURN ((b, (nxs)), clvls, lbd, 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 (M, N, (b, (n, xs)), Q, W, vm, clvls, cach, lbd, outl, stats). do {
ASSERT (clvls ≥ 1);
let L' = atm_of L;
ASSERT(arena_is_valid_clause_idx N C);
((b, (n, xs)), clvls, lbd, outl) ← rr L M N C b n xs clvls lbd outl;
ASSERT(arena_act_pre N C);
let N = mark_used N C;
ASSERT(arena_act_pre N C);
let N = arena_incr_act N C;
ASSERT(vmtf_unset_pre L' vm);
ASSERT(tl_trailt_tr_pre M);
RETURN (False, (tl_trailt_tr M, N, (b, (n, xs)), Q, W, isa_vmtf_unset L' vm,
clvls - 1, cach, lbd, outl, stats))
})›
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), x1h, x1i, (x1k, x1l, x2k), x1m, x1n, x1p, x1q, x1r,
x1s, x1t, m, n, p, q, ra, s, t),
(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 ⟹
CLS = ((x1, x2), x1a, x1b, x1c, x1d, x1e, NS, US, x1f, x2f) ⟹
CLS' =
((x1g, x2g), x1h, x1i, (x1k, x1l, x2k), x1m, x1n, x1p, x1q, x1r,
x1s, x1t, m, n, p, q, ra, 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 ⟹
rr x1g x1h x1i x2g x1k x1l x2k x1q x1s x1t
≤ ⇓ {((C, clvls, lbd, 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 x1s x1t CLS CLS' NS US
unfolding rr_def
apply (refine_vcg lhs_step_If)
apply (rule isasat_lookup_merge_eq2_lookup_merge_eq2[where
vdom = ‹set (get_vdom (x1h, x1i, (x1k, x1l, x2k), x1m, x1n, x1p, x1q, x1r,
x1s, x1t, m, n, p, q, ra, s, t))› 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
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 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 (_ ∝ _)›]
intro!: mset_as_position_remove3
intro!: ASSERT_leI)
done
subgoal
apply (subst (asm) arena_lifting(4)[where vdom = ‹set p› 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 p›,
THEN fref_to_Down_curry6, of x1a x1b x2g x1c x1q x1s x1t,
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
intro!: ASSERT_leI)
done
done
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; 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)
apply (rule rr; assumption)
subgoal by (simp add: arena_act_pre_def)
subgoal using arena_act_pre_mark_used by blast
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
intro!: vmtf_unset_pre')
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 x1s x1t D x1v x1w x2v x1x x1y
by (rule tl_trailt_tr_pre[of x1a _ ‹all_atms_st (x1a, x1b, x1c, x1d, x1e, x1f, ha, ia, ja)›])
(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
intro!: tl_trailt_tr_pre)
subgoal by (clarsimp simp: twl_st_heur_conflict_ana_def update_confl_tl_wl_pre'_def
valid_arena_arena_incr_act valid_arena_mark_used subset_mset.sup.commute[of _ ‹remove1_mset _ _›]
tl_trail_tr[THEN fref_to_Down_unRET] resolve_cls_wl'_def isa_vmtf_tl_isa_vmtf no_dup_tlD
counts_maximum_level_def)
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 isa_vmtf_le:
‹((a, b), M) ∈ isa_vmtf 𝒜 M' ⟹ A ∈# 𝒜 ⟹ A < length a›
‹((a, b), M) ∈ isa_vmtf 𝒜 M' ⟹ B ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ atm_of B < length a›
by (auto simp: isa_vmtf_def vmtf_def vmtf_ℒ⇩a⇩l⇩l_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
lemma isa_vmtf_next_search_le:
‹((a, b, c, c', Some d), M) ∈ isa_vmtf 𝒜 M' ⟹ d < length a›
by (auto simp: isa_vmtf_def vmtf_def vmtf_ℒ⇩a⇩l⇩l_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)
definition is_decided_hd_trail_wl_heur :: ‹twl_st_wl_heur ⇒ bool› where
‹is_decided_hd_trail_wl_heur = (λS. is_None (snd (last_trail_pol (get_trail_wl_heur S))))›
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 → ⟨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)
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_inv where
‹skip_and_resolve_loop_wl_D_heur_inv S⇩0' =
(λ(brk, S'). ∃S S⇩0. (S', S) ∈ twl_st_heur_conflict_ana ∧ (S⇩0', S⇩0) ∈ twl_st_heur_conflict_ana ∧
skip_and_resolve_loop_wl_inv S⇩0 brk S ∧
length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S⇩0'))›
definition update_confl_tl_wl_heur_pre
:: ‹(nat × nat literal) × twl_st_wl_heur ⇒ bool›
where
‹update_confl_tl_wl_heur_pre =
(λ((i, L), (M, N, D, W, Q, ((A, m, fst_As, lst_As, next_search), _), clvls, cach, lbd,
outl, _)).
i > 0 ∧
(fst M) ≠ [] ∧
atm_of ((last (fst M))) < length A ∧ (next_search ≠ None ⟶ the next_search < length A) ∧
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 × twl_st_wl_heur ⇒ bool›
where
‹atm_is_in_conflict_st_heur_pre = (λ(L, (M,N,(_, (_, D)), _)). atm_of L < length D)›
definition skip_and_resolve_loop_wl_D_heur
:: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹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
}
›
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)
unfolding ℒ⇩a⇩l⇩l_all_atms_all_lits[symmetric]
apply assumption+
done
subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x1e x2d x2e
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)[]
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_iff)
done
done
qed
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 →⇩f ⟨twl_st_heur_conflict_ana' r⟩nres_rel›
proof -
have H[refine0]: ‹(x, y) ∈ twl_st_heur_conflict_ana ⟹
((False, x), False, y)
∈ bool_rel ×⇩f
twl_st_heur_conflict_ana' (length (get_clauses_wl_heur x))› for x y
by auto
show ?thesis
supply [[goals_limit=1]]
unfolding skip_and_resolve_loop_wl_D_heur_def skip_and_resolve_loop_wl_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 by fast
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: )
subgoal by auto
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
definition (in -) get_count_max_lvls_code where
‹get_count_max_lvls_code = (λ(_, _, _, _, _, _, _, clvls, _). clvls)›
lemma is_decided_hd_trail_wl_heur_alt_def:
‹is_decided_hd_trail_wl_heur = (λ(M, _). is_None (snd (last_trail_pol M)))›
by (auto intro!: ext simp: is_decided_hd_trail_wl_heur_def)
lemma atm_of_in_atms_of: ‹atm_of x ∈ atms_of C ⟷ x ∈# C ∨ -x ∈# C›
using atm_of_notin_atms_of_iff by blast
definition atm_is_in_conflict where
‹atm_is_in_conflict L D ⟷ atm_of L ∈ atms_of (the D)›
fun is_in_option_lookup_conflict where
is_in_option_lookup_conflict_def[simp del]:
‹is_in_option_lookup_conflict L (a, n, xs) ⟷ is_in_lookup_conflict (n, xs) L›
lemma is_in_option_lookup_conflict_atm_is_in_conflict_iff:
assumes
‹ba ≠ None› and aa: ‹aa ∈# ℒ⇩a⇩l⇩l 𝒜› and uaa: ‹- aa ∉# the ba› and
‹((b, c, d), ba) ∈ option_lookup_clause_rel 𝒜›
shows ‹is_in_option_lookup_conflict aa (b, c, d) =
atm_is_in_conflict aa ba›
proof -
obtain yb where ba[simp]: ‹ba = Some yb›
using assms by auto
have map: ‹mset_as_position d yb› and le: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length d› and [simp]: ‹¬b›
using assms by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def)
have aa_d: ‹atm_of aa < length d› and uaa_d: ‹atm_of (-aa) < length d›
using le aa by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
from mset_as_position_in_iff_nth[OF map aa_d]
have 1: ‹(aa ∈# yb) = (d ! atm_of aa = Some (is_pos aa))›
.
from mset_as_position_in_iff_nth[OF map uaa_d] have 2: ‹(d ! atm_of aa ≠ Some (is_pos (-aa)))›
using uaa by simp
then show ?thesis
using uaa 1 2
by (auto simp: is_in_lookup_conflict_def is_in_option_lookup_conflict_def atm_is_in_conflict_def
atm_of_in_atms_of is_neg_neg_not_is_neg
split: option.splits)
qed
lemma is_in_option_lookup_conflict_atm_is_in_conflict:
‹(uncurry (RETURN oo is_in_option_lookup_conflict), uncurry (RETURN oo atm_is_in_conflict))
∈ [λ(L, D). D ≠ None ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ -L ∉# the D]⇩f
Id ×⇩f option_lookup_clause_rel 𝒜 → ⟨bool_rel⟩nres_rel›
apply (intro frefI nres_relI)
apply (case_tac x, case_tac y)
by (simp add: is_in_option_lookup_conflict_atm_is_in_conflict_iff[of _ _ 𝒜])
lemma is_in_option_lookup_conflict_alt_def:
‹RETURN oo is_in_option_lookup_conflict =
RETURN oo (λL (_, n, xs). is_in_lookup_conflict (n, xs) L)›
by (auto intro!: ext simp: is_in_option_lookup_conflict_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+
apply (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)
apply (case_tac x)
apply (clarsimp_all dest!: multi_member_split simp: ann_lits_split_reasons_def)
done
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
end