theory Watched_Literals_Transition_System_Enumeration
imports Watched_Literals.Watched_Literals_Transition_System Model_Enumeration
begin
text ‹
Design decision: we favour shorter clauses to (potentially) better models.
More precisely, we take the clause composed of decisions, instead of taking the full trail. This
creates shorter clauses. However, this makes satisfying the initial clauses ∗‹harder› since fewer
literals can be left undefined or be defined with the wrong sign.
For now there is no difference, since TWL produces only full models anyway. Remark that this is
the clause that is produced by the minimization of the conflict of the full trail (except that
this clauses would be learned and not added to the initial set of clauses, meaning that that the
set of initial clauses is not harder to satisfy).
It is not clear if that would really make a huge performance difference.
The name DECO (e.g., \<^term>‹DECO_clause›) comes from Armin Biere's "decision only clauses"
(DECO) optimisation (see Armin Biere's "Lingeling, Plingeling and Treengeling Entering the SAT
Competition 2013"). If the learned clause becomes much larger that the clause normally learned by
backjump, then the clause composed of the negation of the decision is learned instead
(effectively doing a backtrack instead of a backjump).
Unless we get more information from the filtering function, we are in the special case where the
1st-UIP is exactly the last decision.
An important property of the transition rules is that they violate the invariant that propagations
are fully done before each decision. This means that we handle the transitions as a fast restart
and not as a backjump as one would expect, since we cannot reuse any theorem about backjump.
›
definition DECO_clause :: ‹('v, 'a) ann_lits ⇒ 'v clause›where
‹DECO_clause M = (uminus o lit_of) `# (filter_mset is_decided (mset M))›
lemma distinct_mset_DECO:
‹distinct_mset (DECO_clause M) ⟷ distinct_mset (lit_of `# filter_mset is_decided (mset M))›
(is ‹?A ⟷ ?B›)
proof -
have ‹?A ⟷ distinct_mset (uminus `# lit_of `# (filter_mset is_decided (mset M)))›
by (auto simp: DECO_clause_def)
also have ‹… ⟷ distinct_mset (lit_of `# (filter_mset is_decided (mset M)))›
apply (subst distinct_image_mset_inj)
subgoal by (auto simp: inj_on_def)
subgoal by auto
done
finally show ?thesis
.
qed
lemma [twl_st]:
‹init_clss (state⇩W_of T) = get_all_init_clss T›
‹learned_clss (state⇩W_of T) = get_all_learned_clss T›
by (cases T; auto simp: cdcl⇩W_restart_mset_state; fail)+
lemma atms_of_DECO_clauseD:
‹x ∈ atms_of (DECO_clause U) ⟹ x ∈ atms_of_s (lits_of_l U)›
‹x ∈ atms_of (DECO_clause U) ⟹ x ∈ atms_of (lit_of `# mset U)›
by (auto simp: DECO_clause_def atms_of_s_def atms_of_def lits_of_def)
definition TWL_DECO_clause where
‹TWL_DECO_clause M =
TWL_Clause
((uminus o lit_of) `# mset (take 2 (filter is_decided M)))
((uminus o lit_of) `# mset (drop 2 (filter is_decided M)))›
lemma clause_TWL_Deco_clause[simp]: ‹clause (TWL_DECO_clause M) = DECO_clause M›
by (auto simp: TWL_DECO_clause_def DECO_clause_def
simp del: image_mset_union mset_append
simp add: image_mset_union[symmetric] mset_append[symmetric] mset_filter)
inductive negate_model_and_add_twl :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
bj_unit:
‹negate_model_and_add_twl (M, N, U, None, NP, UP, WS, Q)
(Propagated (-K) (DECO_clause M) # M1, N, U, None, add_mset (DECO_clause M) NP, UP, {#}, {#K#})›
if
‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and
‹get_level M K = count_decided M› and
‹count_decided M = 1› |
bj_nonunit:
‹negate_model_and_add_twl (M, N, U, None, NP, UP, WS, Q)
(Propagated (-K) (DECO_clause M) # M1, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#},
{#K#})›
if
‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and
‹get_level M K = count_decided M› and
‹count_decided M ≥ 2› |
restart_nonunit:
‹negate_model_and_add_twl (M, N, U, None, NP, UP, WS, Q)
(M1, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#}, {#})›
if
‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and
‹get_level M K < count_decided M› and
‹count_decided M > 1›
text ‹Some remarks:
▪ Because of the invariants (unit clauses have to be propagated), a rule restart\_unit would be
the same as the bj\_unit.
▪ The rules cleans the components about updates and do not assume that they are empty.
›
lemma after_fast_restart_replay:
assumes
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M', N, U, None)› and
stgy_invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (M', N, U, None)› and
smaller_propa: ‹cdcl⇩W_restart_mset.no_smaller_propa (M', N, U, None)› and
kept: ‹∀L E. Propagated L E ∈ set (drop (length M' - n) M') ⟶ E ∈# N + U'› and
U'_U: ‹U' ⊆# U› and
no_confl: ‹∀C∈#N'. ∀M1 K M2. M' = M2 @ Decided K # M1 ⟶ ¬M1 ⊨as CNot C› and
no_propa: ‹∀C∈#N'. ∀M1 K M2 L. M' = M2 @ Decided K # M1 ⟶ L ∈# C ⟶
¬M1 ⊨as CNot (remove1_mset L C)›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* ([], N+N', U', None) (drop (length M' - n) M', N+ N', U', None)›
proof -
let ?S = ‹λn. (drop (length M' - n) M', N+N', U', None)›
note cdcl⇩W_restart_mset_state[simp]
have
M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (M', N, U, None)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (M', N, U, None)› and
confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (M', N, U, None)› and
learned: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (M', N, U, None)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
have smaller_confl: ‹cdcl⇩W_restart_mset.no_smaller_confl (M', N, U, None)›
using stgy_invs unfolding cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def by blast
have n_d: ‹no_dup M'›
using M_lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by simp
let ?L = ‹λm. M' ! (length M' - Suc m)›
have undef_nth_Suc:
‹undefined_lit (drop (length M' - m) M') (lit_of (?L m))›
if ‹m < length M'›
for m
proof -
define k where
‹k = length M' - Suc m›
then have Sk: ‹length M' - m = Suc k›
using that by linarith
have k_le_M': ‹k < length M'›
using that unfolding k_def by linarith
have n_d': ‹no_dup (take k M' @ ?L m # drop (Suc k) M')›
using n_d
apply (subst (asm) append_take_drop_id[symmetric, of _ ‹Suc k›])
apply (subst (asm) take_Suc_conv_app_nth)
apply (rule k_le_M')
apply (subst k_def[symmetric])
by simp
show ?thesis
using n_d'
apply (subst (asm) no_dup_append_cons)
apply (subst (asm) k_def[symmetric])+
apply (subst k_def[symmetric])+
apply (subst Sk)+
by blast
qed
have atm_in:
‹atm_of (lit_of (M' ! m)) ∈ atms_of_mm N›
if ‹m < length M'›
for m
using alien that
by (auto simp: cdcl⇩W_restart_mset.no_strange_atm_def lits_of_def)
then have atm_in':
‹atm_of (lit_of (M' ! m)) ∈ atms_of_mm (N + N')›
if ‹m < length M'›
for m
using alien that
by (auto simp: cdcl⇩W_restart_mset.no_strange_atm_def lits_of_def)
show ?thesis
using kept
proof (induction n)
case 0
then show ?case by simp
next
case (Suc m) note IH = this(1) and kept = this(2)
consider
(le) ‹m < length M'› |
(ge) ‹m ≥ length M'›
by linarith
then show ?case
proof (cases)
case ge
then show ?thesis
using Suc by auto
next
case le
define k where
‹k = length M' - Suc m›
then have Sk: ‹length M' - m = Suc k›
using le by linarith
have k_le_M': ‹k < length M'›
using le unfolding k_def by linarith
have kept': ‹∀L E. Propagated L E ∈ set (drop (length M' - m) M') ⟶ E ∈# N + U'›
using kept k_le_M' unfolding k_def[symmetric] Sk
by (subst (asm) Cons_nth_drop_Suc[symmetric]) auto
have M': ‹M' = take (length M' - Suc m) M' @ ?L m # trail (?S m)›
apply (subst append_take_drop_id[symmetric, of _ ‹Suc k›])
apply (subst take_Suc_conv_app_nth)
apply (rule k_le_M')
apply (subst k_def[symmetric])
unfolding k_def[symmetric] Sk
by auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy (?S m) (?S (Suc m))›
proof (cases ‹?L (m)›)
case (Decided K) note K = this
have dec: ‹cdcl⇩W_restart_mset.decide (?S m) (?S (Suc m))›
apply (rule cdcl⇩W_restart_mset.decide_rule[of _ ‹lit_of (?L m)›])
subgoal by simp
subgoal using undef_nth_Suc[of m] le by simp
subgoal using le by (auto simp: atm_in)
subgoal using le k_le_M' K unfolding k_def[symmetric] Sk
by (auto simp: state_eq_def state_def Cons_nth_drop_Suc[symmetric])
done
have Dec: ‹M' ! k = Decided K›
using K unfolding k_def[symmetric] Sk .
have H: ‹D + {#L#} ∈# N + U ⟶ undefined_lit (trail (?S m)) L ⟶
¬ (trail (?S m)) ⊨as CNot D› for D L
using smaller_propa unfolding cdcl⇩W_restart_mset.no_smaller_propa_def
trail.simps clauses_def
cdcl⇩W_restart_mset_state
apply (subst (asm) M')
unfolding Dec Sk k_def[symmetric]
by (auto simp: clauses_def state_eq_def)
have no_new_propa: ‹False›
if
‹drop (Suc k) M' ⊨as CNot (remove1_mset L E)› and
‹L ∈# E› and
‹undefined_lit (drop (Suc k) M') L› and
‹E ∈# N'› for L E
using that no_propa Sk[symmetric]
apply (subst (asm)(3) M')
apply (subst (asm)(2) M')
apply (subst (asm) M')
unfolding k_def[symmetric] Dec
apply (auto simp: k_def dest!: multi_member_split[of _ N'])
by (metis Sk that(1))
have ‹D ∈# N ⟶ undefined_lit (trail (?S m)) L ⟶ L ∈# D ⟶
¬ (trail (?S m)) ⊨as CNot (remove1_mset L D)› and
‹D ∈# U' ⟶ undefined_lit (trail (?S m)) L ⟶ L ∈# D ⟶
¬ (trail (?S m)) ⊨as CNot (remove1_mset L D)›for D L
using H[of ‹remove1_mset L D› L] U'_U by auto
then have nss: ‹no_step cdcl⇩W_restart_mset.propagate (?S m)›
using no_propa no_new_propa
by (auto simp: cdcl⇩W_restart_mset.propagate.simps clauses_def
state_eq_def k_def[symmetric] Sk)
have no_new_confl: ‹drop (Suc k) M' ⊨as CNot D ⟹ D ∈# N' ⟹ False› for D
using no_confl
apply (subst (asm)(2) M')
apply (subst (asm) M')
unfolding k_def[symmetric] Dec
by (auto simp: k_def dest!: multi_member_split)
(metis K M' Sk cdcl⇩W_restart_mset_state(1) drop_append
k_def length_take true_annots_append_l)
have H: ‹D ∈# N + U' ⟶ ¬ (trail (?S m)) ⊨as CNot D› for D
using smaller_confl U'_U unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
trail.simps clauses_def cdcl⇩W_restart_mset_state
apply (subst (asm) M')
unfolding Dec Sk k_def[symmetric]
by (auto simp: clauses_def state_eq_def)
then have nsc: ‹no_step cdcl⇩W_restart_mset.conflict (?S m)›
using no_new_confl
by (auto simp: cdcl⇩W_restart_mset.conflict.simps clauses_def state_eq_def
k_def[symmetric] Sk)
show ?thesis
apply (rule cdcl⇩W_restart_mset.cdcl⇩W_stgy.other')
apply (rule nsc)
apply (rule nss)
apply (rule cdcl⇩W_restart_mset.cdcl⇩W_o.decide)
apply (rule dec)
done
next
case K: (Propagated K C)
have Propa: ‹M' ! k = Propagated K C›
using K unfolding k_def[symmetric] Sk .
have
M_C: ‹trail (?S m) ⊨as CNot (remove1_mset K C)› and
K_C: ‹K ∈# C›
using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def trail.simps
by (subst (asm)(3) M'; auto simp: k_def[symmetric] Sk Propa)+
have [simp]: ‹k - min (length M') k = 0›
unfolding k_def by auto
have C_N_U: ‹C ∈# N + U'›
using learned kept unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def Sk
k_def[symmetric]
apply (subst (asm)(4)M')
apply (subst (asm)(10)M')
unfolding K
by (auto simp: K k_def[symmetric] Sk Propa clauses_def)
have ‹cdcl⇩W_restart_mset.propagate (?S m) (?S (Suc m))›
apply (rule cdcl⇩W_restart_mset.propagate_rule[of _ C K])
subgoal by simp
subgoal using C_N_U by (auto simp add: clauses_def)
subgoal using K_C .
subgoal using M_C .
subgoal using undef_nth_Suc[of m] le K by (simp add: k_def[symmetric] Sk)
subgoal
using le k_le_M' K unfolding k_def[symmetric] Sk
by (auto simp: state_eq_def
state_def Cons_nth_drop_Suc[symmetric])
done
then show ?thesis
by (rule cdcl⇩W_restart_mset.cdcl⇩W_stgy.propagate')
qed
then show ?thesis
using IH[OF kept'] by simp
qed
qed
qed
lemma after_fast_restart_replay':
assumes
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M', N, U, None)› and
stgy_invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (M', N, U, None)› and
smaller_propa: ‹cdcl⇩W_restart_mset.no_smaller_propa (M', N, U, None)› and
kept: ‹∀L E. Propagated L E ∈ set (drop (length M' - n) M') ⟶ E ∈# N + U'› and
U'_U: ‹U' ⊆# U› and
N_N': ‹N ⊆# N'› and
no_confl: ‹∀C∈#N'-N. ∀M1 K M2. M' = M2 @ Decided K # M1 ⟶ ¬M1 ⊨as CNot C› and
no_propa: ‹∀C∈#N'-N. ∀M1 K M2 L. M' = M2 @ Decided K # M1 ⟶ L ∈# C ⟶
¬M1 ⊨as CNot (remove1_mset L C)›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* ([], N', U', None) (drop (length M' - n) M', N', U', None)›
using after_fast_restart_replay[OF inv stgy_invs smaller_propa kept U'_U, of ‹N' - N›]
no_confl no_propa N_N'
by auto
lemma after_fast_restart_replay_no_stgy:
assumes
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M', N, U, None)› and
kept: ‹∀L E. Propagated L E ∈ set (drop (length M' - n) M') ⟶ E ∈# N+N' + U'› and
U'_U: ‹U' ⊆# U›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* ([], N+N', U', None) (drop (length M' - n) M', N+N', U', None)›
proof -
let ?S = ‹λn. (drop (length M' - n) M', N + N', U', None)›
note cdcl⇩W_restart_mset_state[simp]
have
M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (M', N, U, None)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (M', N, U, None)› and
confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (M', N, U, None)› and
learned: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (M', N, U, None)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
have n_d: ‹no_dup M'›
using M_lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by simp
let ?L = ‹λm. M' ! (length M' - Suc m)›
have undef_nth_Suc:
‹undefined_lit (drop (length M' - m) M') (lit_of (?L m))›
if ‹m < length M'›
for m
proof -
define k where
‹k = length M' - Suc m›
then have Sk: ‹length M' - m = Suc k›
using that by linarith
have k_le_M': ‹k < length M'›
using that unfolding k_def by linarith
have n_d': ‹no_dup (take k M' @ ?L m # drop (Suc k) M')›
using n_d
apply (subst (asm) append_take_drop_id[symmetric, of _ ‹Suc k›])
apply (subst (asm) take_Suc_conv_app_nth)
apply (rule k_le_M')
apply (subst k_def[symmetric])
by simp
show ?thesis
using n_d'
apply (subst (asm) no_dup_append_cons)
apply (subst (asm) k_def[symmetric])+
apply (subst k_def[symmetric])+
apply (subst Sk)+
by blast
qed
have atm_in:
‹atm_of (lit_of (M' ! m)) ∈ atms_of_mm (N+N')›
if ‹m < length M'›
for m
using alien that
by (auto simp: cdcl⇩W_restart_mset.no_strange_atm_def lits_of_def)
show ?thesis
using kept
proof (induction n)
case 0
then show ?case by simp
next
case (Suc m) note IH = this(1) and kept = this(2)
consider
(le) ‹m < length M'› |
(ge) ‹m ≥ length M'›
by linarith
then show ?case
proof cases
case ge
then show ?thesis
using Suc by auto
next
case le
define k where
‹k = length M' - Suc m›
then have Sk: ‹length M' - m = Suc k›
using le by linarith
have k_le_M': ‹k < length M'›
using le unfolding k_def by linarith
have kept': ‹∀L E. Propagated L E ∈ set (drop (length M' - m) M') ⟶ E ∈# N+N' + U'›
using kept k_le_M' unfolding k_def[symmetric] Sk
by (subst (asm) Cons_nth_drop_Suc[symmetric]) auto
have M': ‹M' = take (length M' - Suc m) M' @ ?L m # trail (?S m)›
apply (subst append_take_drop_id[symmetric, of _ ‹Suc k›])
apply (subst take_Suc_conv_app_nth)
apply (rule k_le_M')
apply (subst k_def[symmetric])
unfolding k_def[symmetric] Sk
by auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W (?S m) (?S (Suc m))›
proof (cases ‹?L (m)›)
case (Decided K) note K = this
have dec: ‹cdcl⇩W_restart_mset.decide (?S m) (?S (Suc m))›
apply (rule cdcl⇩W_restart_mset.decide_rule[of _ ‹lit_of (?L m)›])
subgoal by simp
subgoal using undef_nth_Suc[of m] le by simp
subgoal using le atm_in by auto
subgoal using le k_le_M' K unfolding k_def[symmetric] Sk
by (auto simp: state_eq_def state_def Cons_nth_drop_Suc[symmetric])
done
have Dec: ‹M' ! k = Decided K›
using K unfolding k_def[symmetric] Sk .
show ?thesis
apply (rule cdcl⇩W_restart_mset.cdcl⇩W.intros(3))
apply (rule cdcl⇩W_restart_mset.cdcl⇩W_o.decide)
apply (rule dec)
done
next
case K: (Propagated K C)
have Propa: ‹M' ! k = Propagated K C›
using K unfolding k_def[symmetric] Sk .
have
M_C: ‹trail (?S m) ⊨as CNot (remove1_mset K C)› and
K_C: ‹K ∈# C›
using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def trail.simps
by (subst (asm)(3) M'; auto simp: k_def[symmetric] Sk Propa)+
have [simp]: ‹k - min (length M') k = 0›
unfolding k_def by auto
have C_N_U: ‹C ∈# N+N' + U'›
using learned kept unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def Sk
k_def[symmetric]
apply (subst (asm)(4)M')
apply (subst (asm)(10)M')
unfolding K
by (auto simp: K k_def[symmetric] Sk Propa clauses_def)
have ‹cdcl⇩W_restart_mset.propagate (?S m) (?S (Suc m))›
apply (rule cdcl⇩W_restart_mset.propagate_rule[of _ C K])
subgoal by simp
subgoal using C_N_U by (simp add: clauses_def)
subgoal using K_C .
subgoal using M_C .
subgoal using undef_nth_Suc[of m] le K by (simp add: k_def[symmetric] Sk)
subgoal
using le k_le_M' K unfolding k_def[symmetric] Sk
by (auto simp: state_eq_def
state_def Cons_nth_drop_Suc[symmetric])
done
then show ?thesis
by (rule cdcl⇩W_restart_mset.cdcl⇩W.intros)
qed
then show ?thesis
using IH[OF kept'] by simp
qed
qed
qed
lemma after_fast_restart_replay_no_stgy':
assumes
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M', N, U, None)› and
kept: ‹∀L E. Propagated L E ∈ set (drop (length M' - n) M') ⟶ E ∈# N' + U'› and
U'_U: ‹U' ⊆# U› and
‹N ⊆# N'›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* ([], N', U', None) (drop (length M' - n) M', N', U', None)›
using after_fast_restart_replay_no_stgy[OF inv, of n ‹N'-N› U'] assms by auto
lemma cdcl⇩W_all_struct_inv_move_to_init:
assumes inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N, U + U', D)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N + U', U, D)›
using assms
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state clauses_def
assms
apply (intro conjI impI)
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
subgoal by auto
subgoal by auto
subgoal by (auto simp: ac_simps)
subgoal by (auto simp: ac_simps)
subgoal by auto
done
lemma twl_struct_invs_move_to_init:
assumes ‹twl_struct_invs (M, N, U + U', D, NP, UP, WS, Q)›
shows ‹twl_struct_invs (M, N + U', U, D, NP, UP, WS, Q)›
proof -
have H: ‹N + (U + U') = N + U' + U›
by simp
have struct_invs:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NP, clauses (U + U') + UP, D')⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses (N + U') + NP, clauses U + UP, D')›
for D'
using cdcl⇩W_all_struct_inv_move_to_init[of M ‹clauses N + NP› ‹clauses U + UP›
‹clauses U'› D']
by (auto simp: ac_simps)
have smaller: ‹clauses N + NP + (clauses (U + U') + UP) = clauses (N + U') + NP + (clauses U + UP)›
by auto
show ?thesis
using assms
apply (cases D; clarify)
unfolding twl_struct_invs_def twl_st_inv.simps valid_enqueued.simps
twl_st_exception_inv.simps no_duplicate_queued.simps
confl_cands_enqueued.simps distinct_queued.simps propa_cands_enqueued.simps
assms entailed_clss_inv.simps past_invs.simps H state⇩W_of.simps
cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state clauses_def
twl_exception_inv.simps get_conflict.simps literals_to_update.simps clauses_to_update.simps
clauses_to_update_inv.simps
apply (intro conjI)
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by (rule struct_invs) fast
subgoal unfolding smaller by argo
subgoal by argo
subgoal by argo
subgoal by argo
subgoal by fast
subgoal by fast
subgoal by argo
subgoal by fast
subgoal by argo
subgoal by blast
subgoal by fast
subgoal by argo
subgoal by argo
subgoal by argo
subgoal by argo
apply (intro conjI)
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by (rule struct_invs) fast
subgoal unfolding smaller by argo
subgoal by argo
subgoal by argo
subgoal by argo
subgoal by fast
subgoal by fast
subgoal by argo
subgoal by fast
subgoal by argo
subgoal by argo
subgoal by fast
subgoal by argo
subgoal by argo
done
qed
lemma negate_model_and_add_twl_twl_struct_invs:
fixes S T :: ‹'v twl_st›
assumes
‹negate_model_and_add_twl S T› and
‹twl_struct_invs S›
shows ‹twl_struct_invs T›
using assms
proof (induction rule: negate_model_and_add_twl.induct)
fix K :: ‹'v literal› and M1 M2 M N U NP UP WS Q
assume
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and
inv: ‹twl_struct_invs (M, N, U, None, NP, UP, WS, Q)›
let ?S = ‹(M, N, U, None, NP, UP, WS, Q)›
let ?T = ‹(Propagated K (DECO_clause M) # M1, add_mset (TWL_DECO_clause M) N, U, None,
NP, UP, {#}, {#- K#})›
have
st_invs: ‹twl_st_inv ?S› and
‹valid_enqueued ?S› and
struct_invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of ?S)› and
no_smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)› and
‹twl_st_exception_inv ?S› and
‹no_duplicate_queued ?S› and
‹distinct_queued ?S› and
‹confl_cands_enqueued ?S› and
‹propa_cands_enqueued ?S› and
‹get_conflict ?S ≠ None ⟶ clauses_to_update ?S = {#} ∧ literals_to_update ?S = {#}› and
entailed: ‹entailed_clss_inv ?S› and
‹clauses_to_update_inv ?S› and
past: ‹past_invs ?S›
using inv unfolding twl_struct_invs_def
by fast+
obtain M3 where
M: ‹M = M3 @ M2 @ Decided K # M1›
using decomp by blast
define M2' where
‹M2' = M3 @ M2›
then have M': ‹M = M2' @ Decided K # M1›
using M by auto
then have
st_invs_M1': ‹∀C∈#N + U. twl_lazy_update M1 C ∧
watched_literals_false_of_max_level M1 C ∧
twl_exception_inv (M1, N, U, None, NP, UP, {#}, {#}) C› and
confl_enqueued_M1: ‹confl_cands_enqueued (M1, N, U, None, NP, UP, {#}, {#})› and
propa_enqueued_M1: ‹propa_cands_enqueued (M1, N, U, None, NP, UP, {#}, {#})› and
clss_upd: ‹clauses_to_update_inv (M1, N, U, None, NP, UP, {#}, {#})› and
past_M1: ‹past_invs (M1, N, U, None, NP, UP, {#}, {#})›
using past
unfolding past_invs.simps
by auto
have no_dup: ‹no_dup M›
using struct_invs unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (simp add: trail.simps)
hence undef_K: ‹undefined_lit M1 K› and n_d1: ‹no_dup M1›
unfolding M' by (auto dest: no_dup_appendD)
have dist: ‹distinct (map atm_of (map lit_of M))›
using no_dup by (auto simp: no_dup_def comp_def)
have dist_filtered: ‹distinct_mset (lit_of `# mset (filter is_decided M))›
apply (rule distinct_mset_mono[of _ ‹lit_of `# mset M›])
subgoal by (auto intro!: image_mset_subseteq_mono simp: mset_filter)
subgoal using dist by (auto simp: mset_map[symmetric] simp del: mset_map
intro: distinct_mapI)
done
then have dist_filtered': ‹distinct_mset (uminus `# lit_of `# mset (filter is_decided M))›
apply (subst distinct_image_mset_inj)
subgoal by (auto simp: inj_on_def)
subgoal .
done
have cdcl_W: ‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* ([], clauses (add_mset (TWL_DECO_clause M) N) + NP,
clauses U + UP, None)
(drop (length M - length M1) M, clauses (add_mset (TWL_DECO_clause M) N) + NP, clauses U + UP,
None)›
apply (rule after_fast_restart_replay_no_stgy'[OF struct_invs[unfolded state⇩W_of.simps]])
subgoal
apply (intro allI impI conjI)
subgoal for L E
by (use M' struct_invs cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail[of E M]
in ‹auto simp add: cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset_state clauses_def›)
done
subgoal by simp
subgoal by simp
done
have ‹distinct_mset (DECO_clause M)›
using dist_filtered' unfolding DECO_clause_def
by (simp add: mset_filter)
then have struct_invs_S':
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ([], clauses (add_mset (TWL_DECO_clause M) N) + NP,
clauses U + UP, None)›
using struct_invs
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state)
with cdcl_W have struct_invs_add: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv
(M1, clauses (add_mset (TWL_DECO_clause M) N) + NP, clauses U + UP, None)›
by (auto intro: cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_all_struct_inv_inv simp: M'
dest!: cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_cdcl⇩W_restart)
have no_smaller_M1:
‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of (M1, N, U, None, NP, UP, WS, Q))›
using no_smaller by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def
cdcl⇩W_restart_mset_state clauses_def M')
have no_smaller_add:
‹cdcl⇩W_restart_mset.no_smaller_propa
(M1, clauses (add_mset (TWL_DECO_clause M) N) + NP, clauses U + UP, None)›
unfolding state⇩W_of.simps cdcl⇩W_restart_mset.no_smaller_propa_def
cdcl⇩W_restart_mset_state clauses_def
proof (intro conjI impI allI)
fix M1a M2 K' D L
assume
M1a: ‹M1 = M2 @ Decided K' # M1a› and
DL: ‹D + {#L#} ∈# clauses (add_mset (TWL_DECO_clause M) N) + NP + (clauses U + UP)› and
undef: ‹undefined_lit M1a L›
consider
‹D+{#L#} ∈# clauses N + NP + (clauses U + UP)› |
‹D+{#L#} = clause (TWL_DECO_clause M)›
using DL by auto
then show ‹¬ M1a ⊨as CNot D›
proof cases
case 1
then show ?thesis
using DL M1a undef no_smaller_M1
by (auto 5 5 simp: cdcl⇩W_restart_mset.no_smaller_propa_def
cdcl⇩W_restart_mset_state clauses_def
add_mset_eq_add_mset)
next
case 2
moreover have ‹K' ∉ lits_of_l M1a› ‹-K ∉ lits_of_l M1a› ‹K ∉ lits_of_l M1a›
using no_dup unfolding M' M1a
by (auto simp: add_mset_eq_add_mset
dest: in_lits_of_l_defined_litD
elim!: list_match_lel_lel)
ultimately show ?thesis
using undef by (auto simp: add_mset_eq_add_mset DECO_clause_def M' M1a
dest!: multi_member_split)
qed
qed
have wf_N_U: ‹C ∈# N + U ⟹ struct_wf_twl_cls C› for C
using st_invs unfolding twl_st_inv.simps by auto
{
assume
lev: ‹get_level M K = count_decided M› and
count_dec: ‹count_decided M ≥ 2›
have [simp]: ‹filter is_decided M2' = []›
using count_dec lev no_dup unfolding M'
by (auto simp: TWL_DECO_clause_def count_decided_def add_mset_eq_add_mset M')
obtain L' C where
filter_M: ‹filter is_decided M = Decided K # Decided L' # C›
using count_dec lev unfolding M'
by (cases ‹filter is_decided M›; cases ‹tl (filter is_decided M)›;
cases ‹hd (filter is_decided M)›; cases ‹hd (tl (filter is_decided M))›)
(auto simp: TWL_DECO_clause_def count_decided_def add_mset_eq_add_mset M'
filter_eq_Cons_iff tl_append)
then have deco_M: ‹TWL_DECO_clause M = TWL_Clause {#-K, -L'#} (uminus `# lit_of `# mset C)›
by (auto simp: TWL_DECO_clause_def)
have C_M1: ‹C = tl (filter is_decided M1)›
using filter_M unfolding M'
by auto
then obtain M1'' M1' where
M1: ‹M1 = M1'' @ Decided L' # M1'›
by (metis (no_types, lifting) M' ‹filter is_decided M2' = []› append_self_conv2
filter.simps(2) filter_M filter_append filter_eq_Cons_iff list.sel(3))
then have [simp]: ‹count_decided M1'' = 0› and filter_M1'': ‹filter is_decided M1'' = []›
using filter_M no_dup unfolding C_M1 M1 M'
by (auto simp: tl_append count_decided_def dest: filter_eq_ConsD split: list.splits)
have C_in_M1: ‹lits_of_l C ⊆ lits_of_l M1›
unfolding C_M1 by (auto simp: lits_of_def dest: in_set_tlD)
let ?S' = ‹(M1, add_mset (TWL_DECO_clause M) N, U, None, NP, UP,
add_mset (-L', (TWL_DECO_clause M)) {#}, {#})›
let ?T' = ‹(Propagated (-K) (DECO_clause M) # M1, add_mset (TWL_DECO_clause M) N, U, None,
NP, UP, {#}, {#- (-K)#})›
have propa: ‹cdcl_twl_cp ?S' ?T'›
unfolding clause_TWL_Deco_clause[symmetric]
apply (rule cdcl_twl_cp.propagate)
subgoal by (auto simp: deco_M)
subgoal using no_dup unfolding M by auto
subgoal using C_in_M1 unfolding deco_M by (auto simp: lits_of_def)
done
have struct_invs_S': ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of ?S')›
using struct_invs_add by auto
have no_smaller_S': ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S')›
using no_smaller_add by simp
have [simp]: ‹get_level M1 L' = count_decided M1›
using no_dup unfolding M' M1 by auto
have ‹watched_literals_false_of_max_level M1 (TWL_DECO_clause M)›
using no_dup apply (subst (asm) M')
by (auto simp: deco_M add_mset_eq_add_mset dest: in_lits_of_l_defined_litD)
moreover have ‹struct_wf_twl_cls (TWL_DECO_clause M)›
using dist_filtered' unfolding deco_M filter_M
by (auto simp: simp del: clause_TWL_Deco_clause)
ultimately have ‹twl_st_inv ?S'›
using wf_N_U st_invs_M1' unfolding twl_st_inv.simps
by (auto simp: twl_is_an_exception_def)
moreover have ‹valid_enqueued ?S'›
by (auto simp: deco_M) (auto simp: M1)
moreover have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of ?S')›
using struct_invs_S' .
moreover have ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S')›
using no_smaller_S' .
moreover have ‹twl_st_exception_inv ?S'›
using st_invs_M1' C_in_M1
by (auto simp: twl_exception_inv.simps deco_M add_mset_eq_add_mset)
(auto simp: lits_of_def)
moreover have ‹no_duplicate_queued ?S'›
by (auto simp: M1)
moreover have ‹distinct_queued ?S'›
by auto
moreover have ‹confl_cands_enqueued ?S'›
using confl_enqueued_M1 by auto
moreover have ‹propa_cands_enqueued ?S'›
using propa_enqueued_M1 by auto
moreover {
have ‹get_level M L = 0 ⟹ get_level M1 L = 0› for L
using no_dup defined_lit_no_dupD(1)[of M1 L M2']
by (cases ‹defined_lit M L›)
(auto simp: M' defined_lit_append defined_lit_cons atm_of_eq_atm_of
get_level_cons_if split: if_splits)
moreover have ‹get_level M L = 0 ⟹ L ∈ lits_of_l M ⟹ L ∈ lits_of_l M1› for L
using no_dup defined_lit_no_dupD(1)[of M1 L M2']
by (cases ‹defined_lit M L›)
(auto simp: M' defined_lit_append defined_lit_cons atm_of_eq_atm_of
get_level_cons_if split: if_splits dest: in_lits_of_l_defined_litD)
ultimately have ‹entailed_clss_inv ?S'›
using entailed unfolding entailed_clss_inv.simps by meson
}
moreover have ‹clauses_to_update_inv ?S'›
using clss_upd no_dup unfolding deco_M by (auto simp: deco_M add_mset_eq_add_mset M'
dest: in_lits_of_l_defined_litD)
moreover have ‹past_invs ?S'›
unfolding past_invs.simps
proof (intro conjI impI allI)
fix M1a M2 K'
assume M1a: ‹M1 = M2 @ Decided K' # M1a›
let ?SM1a = ‹(M1a, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#}, {#})›
have
struct:
‹C∈#N + U ⟹ twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv (M1a, N, U, None, NP, UP, {#}, {#}) C›
for C
using past_M1 unfolding past_invs.simps unfolding M1a
by fast+
have
confl: ‹confl_cands_enqueued (M1a, N, U, None, NP, UP, {#}, {#})› and
propa: ‹propa_cands_enqueued (M1a, N, U, None, NP, UP, {#}, {#})› and
clss_to_upd: ‹clauses_to_update_inv (M1a, N, U, None, NP, UP, {#}, {#})›
using past_M1 unfolding past_invs.simps unfolding M1a
by fast+
have [iff]: ‹L' ∉ lits_of_l M1a› ‹K ∉ lits_of_l M1a›
using no_dup M1 filter_M1'' unfolding deco_M unfolding M' M1a
by (auto simp: deco_M add_mset_eq_add_mset
dest: in_lits_of_l_defined_litD
simp del: ‹filter is_decided M2' = []›
elim!: list_match_lel_lel)
have ‹twl_lazy_update M1a (TWL_DECO_clause M)›
using no_dup M1 unfolding deco_M unfolding M' M1a
by (auto simp: deco_M add_mset_eq_add_mset
dest: in_lits_of_l_defined_litD)
moreover have ‹watched_literals_false_of_max_level M1a (TWL_DECO_clause M)›
unfolding deco_M by (auto simp: add_mset_eq_add_mset)
moreover have ‹twl_exception_inv ?SM1a (TWL_DECO_clause M)›
unfolding deco_M by (auto simp: add_mset_eq_add_mset twl_exception_inv.simps)
ultimately have ‹C∈#add_mset (TWL_DECO_clause M) N + U ⟹ twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv ?SM1a C› for C
using struct[of C]
by (auto simp: twl_exception_inv.simps)
then show ‹∀C∈#add_mset (TWL_DECO_clause M) N + U. twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv ?SM1a C›
by blast
show ‹confl_cands_enqueued ?SM1a›
using confl by (auto simp: deco_M)
show ‹propa_cands_enqueued ?SM1a›
using propa by (auto simp: deco_M)
show ‹clauses_to_update_inv ?SM1a›
using clss_to_upd
by (auto simp: deco_M clauses_to_update_prop.simps add_mset_eq_add_mset)
qed
moreover have ‹get_conflict ?S' = None›
by simp
ultimately have ‹twl_struct_invs ?S'›
unfolding twl_struct_invs_def
by meson
then have ‹twl_struct_invs ?T'›
by (rule cdcl_twl_cp_twl_struct_invs[OF propa])
then show ‹twl_struct_invs (Propagated (-K) (DECO_clause M) # M1, add_mset (TWL_DECO_clause M) N,
U, None, NP, UP, {#}, {#K#})›
by simp
}
{
let ?S = ‹(Propagated (- K) (DECO_clause M) # M1, N, U, None, add_mset (DECO_clause M) NP, UP,
{#}, {#K#})›
assume ‹count_decided M = 1›
then have [simp]: ‹DECO_clause M = {#-K#}›
using decomp by (auto simp: DECO_clause_def filter_mset_empty_conv count_decided_0_iff
dest!: get_all_ann_decomposition_exists_prepend)
have [simp]: ‹get_level M1 L = 0› ‹count_decided M1 = 0› for L
using count_decided_ge_get_level[of M1 L] ‹count_decided M = 1›
unfolding M by auto
have K_M: ‹K ∈ lits_of_l M›
using M' by simp
have propa: ‹cdcl⇩W_restart_mset.propagate (M1, clauses (add_mset (TWL_DECO_clause M) N) + NP, clauses U + UP, None)
(state⇩W_of ?S)›
unfolding state⇩W_of.simps
apply (rule cdcl⇩W_restart_mset.propagate_rule[of _ ‹DECO_clause M› ‹-K›])
subgoal by (simp add: cdcl⇩W_restart_mset_state)
subgoal by (simp add: clauses_def)
subgoal by simp
subgoal by (simp add: cdcl⇩W_restart_mset_state)
subgoal using no_dup by (simp add: cdcl⇩W_restart_mset_state M')
subgoal by (simp add: cdcl⇩W_restart_mset_state)
done
have lazy: ‹twl_lazy_update M1 C› if ‹C∈#N + U› for C
using that st_invs_M1' by blast
have excep: ‹twl_exception_inv (M1, N, U, None, NP, UP, {#}, {#}) C› if ‹C∈#N + U› for C
using that st_invs_M1' by blast
have ‹¬twl_is_an_exception C {#K#} {#} ⟹ twl_lazy_update (Propagated (- K) {#- K#} # M1) C› if ‹C∈#N + U› for C
using lazy[OF that] no_dup undef_K n_d1 excep[OF that]
by (cases C)
(auto simp: get_level_cons_if all_conj_distrib twl_exception_inv.simps
twl_is_an_exception_def
dest!: no_has_blit_propagate multi_member_split)
moreover have ‹watched_literals_false_of_max_level (Propagated (- K) {#- K#} # M1) C› for C
by (cases C) (auto simp: get_level_cons_if)
ultimately have ‹twl_st_inv ?S›
using st_invs_M1' wf_N_U by (auto simp: twl_st_inv.simps
simp del: set_mset_union)
moreover have ‹valid_enqueued ?S›
by auto
moreover have struct_invs_S: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of ?S)›
using struct_invs_add propa
by (auto dest!: cdcl⇩W_restart_mset.propagate cdcl⇩W_restart_mset.cdcl⇩W_cdcl⇩W_restart
simp: intro: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_inv)
moreover have ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)›
using no_smaller_add propa struct_invs_add
by (auto 5 5 simp: dest!: cdcl⇩W_restart_mset.propagate cdcl⇩W_restart_mset.cdcl⇩W_stgy.propagate'
intro: cdcl⇩W_restart_mset.cdcl⇩W_stgy_no_smaller_propa)
moreover have ‹twl_st_exception_inv ?S›
using st_invs_M1' no_dup undef_K n_d1
by (auto simp add: twl_exception_inv.simps
dest!: no_has_blit_propagate')
moreover have ‹no_duplicate_queued ?S›
by auto
moreover have ‹distinct_queued ?S›
by auto
moreover have ‹confl_cands_enqueued ?S›
unfolding confl_cands_enqueued.simps Ball_def
proof (intro impI allI)
fix C
assume
C: ‹C ∈# N + U› and
H: ‹Propagated (- K) (DECO_clause M) # M1 ⊨as CNot (clause C)›
obtain L1 L2 UW where
C': ‹C = TWL_Clause {#L1, L2#} UW› and dist_C: ‹distinct_mset (clause C)›
using wf_N_U[OF C]
apply (cases C)
by (auto simp: twl_exception_inv.simps size_2_iff cdcl⇩W_restart_mset_state)
have M1_C: ‹¬M1 ⊨as CNot (clause C)›
using confl_enqueued_M1 C by auto
define C' where ‹C' = remove1_mset K (clause C)›
then have C_K_C': ‹clause C = add_mset K C'› and ‹K ∉# C'› and
M1_C': ‹M1 ⊨as CNot C'› and K_C'_C: ‹add_mset K C' = clause C›
using dist_C M1_C H by (auto simp: true_annots_true_cls_def_iff_negation_in_model
dest: in_diffD dest!: multi_member_split)
have ‹C' + {#K#} ∈# clauses (N+U)›
using C M1_C'
by (auto simp: K_C'_C M')
then have ‹undefined_lit M1 K ⟹ ¬ M1 ⊨as CNot C'›
using no_smaller
unfolding cdcl⇩W_restart_mset.no_smaller_propa_def state⇩W_of.simps cdcl⇩W_restart_mset_state
clauses_def image_mset_union M' union_iff
by blast
then have False
using no_dup M1_C' unfolding M'
by (auto simp: cdcl⇩W_restart_mset_state clauses_def M')
then show ‹(∃L'. L' ∈# watched C ∧ L' ∈# {#K#}) ∨ (∃L. (L, C) ∈# {#})›
by fast
qed
moreover have ‹propa_cands_enqueued ?S›
unfolding propa_cands_enqueued.simps Ball_def
proof (intro impI allI)
fix C L
assume
C: ‹C ∈# N + U› and
L: ‹L ∈# clause C› and
H: ‹Propagated (- K) (DECO_clause M) # M1 ⊨as CNot (remove1_mset L (clause C))› and
undef: ‹undefined_lit (Propagated (- K) (DECO_clause M) # M1) L›
obtain L1 L2 UW where
C': ‹C = TWL_Clause {#L1, L2#} UW› and dist_C: ‹distinct_mset (clause C)›
using wf_N_U[OF C]
apply (cases C)
by (auto simp: twl_exception_inv.simps size_2_iff cdcl⇩W_restart_mset_state)
have M1_C: ‹¬M1 ⊨as CNot (remove1_mset L (clause C))›
using propa_enqueued_M1 C undef L by auto
define C' where ‹C' = remove1_mset K (remove1_mset L (clause C))›
then have C_K_C': ‹clause C = add_mset K (add_mset L C')› and ‹K ∉# C'› and
M1_C': ‹M1 ⊨as CNot C'› and K_C'_C: ‹add_mset K (add_mset L C') = clause C› and
K_C'_C': ‹add_mset K C' = remove1_mset L (clause C)›
using dist_C M1_C H L by (auto simp: true_annots_true_cls_def_iff_negation_in_model
dest: in_diffD dest!: multi_member_split)
have eq2: ‹{#L1, L2#} = {#L, L'#} ⟷ L = L1 ∧ L' = L2 ∨ L = L2 ∧ L' = L1› for L L'
by (auto simp: add_mset_eq_add_mset)
have ‹twl_exception_inv (M1, N, U, None, NP, UP, {#}, {#}) C›
using past C unfolding past_invs.simps M'
by fast
moreover have ‹L2 ∉ lits_of_l M1›
using H no_dup undef dist_C
unfolding true_annots_true_cls_def_iff_negation_in_model M' C' Ball_def
by (cases ‹L = L1›; cases ‹L = L2›;
auto dest: in_lits_of_l_defined_litD no_dup_appendD no_dup_consistentD
simp: all_conj_distrib)+
moreover have ‹L1 ∉ lits_of_l M1›
using H no_dup undef dist_C
unfolding true_annots_true_cls_def_iff_negation_in_model M' C' Ball_def
apply (cases ‹L = L1›; cases ‹L = L2›)
by (auto dest: in_lits_of_l_defined_litD no_dup_appendD no_dup_consistentD
simp: all_conj_distrib)
moreover {
have ‹L' ∈ lits_of_l M1 ⟹ L' ∈# UW ⟹ False› for L'
using H no_dup undef dist_C ‹L1 ∉ lits_of_l M1› ‹L2 ∉ lits_of_l M1› n_d1
unfolding true_annots_true_cls_def_iff_negation_in_model M' C' Ball_def
apply (cases ‹L = L1›; cases ‹L = L2›)
apply (auto dest: in_lits_of_l_defined_litD no_dup_appendD no_dup_consistentD
simp: all_conj_distrib)
by (metis diff_single_trivial in_lits_of_l_defined_litD insert_DiffM
insert_noteq_member n_d1 no_dup_consistentD)+
then have ‹¬ has_blit M1 (clause (TWL_Clause {#L1, L2#} UW)) L1› and
‹¬ has_blit M1 (clause (TWL_Clause {#L1, L2#} UW)) L2›
using ‹L1 ∉ lits_of_l M1› ‹L2 ∉ lits_of_l M1›
unfolding has_blit_def
by auto
}
ultimately have
‹- L1 ∈ lits_of_l M1 ⟹ (∀K∈#UW. - K ∈ lits_of_l M1)›
‹- L2 ∈ lits_of_l M1 ⟹ (∀K∈#UW. - K ∈ lits_of_l M1)›
unfolding C' twl_exception_inv.simps twl_clause.sel eq2
by fastforce+
moreover have ‹L1 ≠ L2›
using dist_C by (auto simp: C')
ultimately have ‹K ≠ L1 ⟹ K ≠ L2 ⟹ False›
using M1_C' L undef K_C'_C no_dup[unfolded M']
by (cases ‹- L1 ∈ lits_of_l M1›; cases ‹- L2 ∈ lits_of_l M1›;
auto simp add: C' true_annots_true_cls_def_iff_negation_in_model
add_mset_eq_add_mset
dest!: multi_member_split[of _ UW] dest: in_lits_of_l_defined_litD)
then show ‹(∃L'. L' ∈# watched C ∧ L' ∈# {#K#}) ∨ (∃L. (L, C) ∈# {#})›
by (auto simp: C')
qed
moreover have ‹get_conflict ?S = None›
by simp
moreover {
have ‹get_level M L = 0 ⟹ L ∈ lits_of_l M ⟹ L ∈ lits_of_l M1› for L
using no_dup defined_lit_no_dupD(1)[of M1 L M2']
by (cases ‹defined_lit M L›)
(auto simp: M' defined_lit_append defined_lit_cons atm_of_eq_atm_of
get_level_cons_if split: if_splits dest: in_lits_of_l_defined_litD)
then have ‹entailed_clss_inv ?S›
using entailed unfolding entailed_clss_inv.simps by (auto 5 5 simp: get_level_cons_if)
}
moreover {
have ‹¬clauses_to_update_prop {#} (M1) (L, La) ⟹
clauses_to_update_prop {#K#} (Propagated (- K) {#- K#} # M1) (L, La) ⟹ False› for L La
using no_dup n_d1 undef_K
by (auto simp: clauses_to_update_prop.simps M'
dest: in_lits_of_l_defined_litD)
then have ‹clauses_to_update_inv ?S›
using clss_upd no_dup n_d1 undef_K by (force simp: filter_mset_empty_conv
dest: in_lits_of_l_defined_litD dest!: no_has_blit_propagate')
}
moreover have ‹past_invs ?S›
unfolding past_invs.simps
proof (intro conjI impI allI)
fix M1a M2 K'
assume M1a': ‹Propagated (- K) (DECO_clause M) # M1 = M2 @ Decided K' # M1a›
then have M1a: ‹M1 = tl M2 @ Decided K' # M1a›
by (cases M2) auto
let ?SM1a = ‹(M1a, N, U, None, add_mset (DECO_clause M) NP, UP, {#}, {#})›
have
struct:
‹C∈#N + U ⟹ twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv (M1a, N, U, None, NP, UP, {#}, {#}) C›
for C
using past_M1 unfolding past_invs.simps M1a
by fast+
have
confl: ‹confl_cands_enqueued (M1a, N, U, None, NP, UP, {#}, {#})› and
propa: ‹propa_cands_enqueued (M1a, N, U, None, NP, UP, {#}, {#})› and
clss_to_upd: ‹clauses_to_update_inv (M1a, N, U, None, NP, UP, {#}, {#})›
using past_M1 unfolding past_invs.simps unfolding M1a
by fast+
show ‹∀C∈#N + U. twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv ?SM1a C›
using struct by (simp add: twl_exception_inv.simps)
show ‹confl_cands_enqueued ?SM1a›
using confl by auto
show ‹propa_cands_enqueued ?SM1a›
using propa by auto
show ‹clauses_to_update_inv ?SM1a›
using clss_to_upd by auto
qed
ultimately show ‹twl_struct_invs ?S›
unfolding twl_struct_invs_def
by meson
}
{
assume
lev_K: ‹get_level M K < count_decided M› and
count_dec: ‹count_decided M > 1›
obtain K1 K2 C where
filter_M: ‹filter is_decided M = Decided K1 # Decided K2 # C›
using count_dec
by (cases ‹filter is_decided M›; cases ‹tl (filter is_decided M)›;
cases ‹hd (filter is_decided M)›; cases ‹hd (tl (filter is_decided M))›)
(auto simp: TWL_DECO_clause_def count_decided_def add_mset_eq_add_mset
filter_eq_Cons_iff tl_append)
then have deco_M: ‹TWL_DECO_clause M = TWL_Clause {#-K1, -K2#} (uminus `# lit_of `# mset C)›
by (auto simp: TWL_DECO_clause_def)
let ?S = ‹(M1, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#}, {#})›
have struct_invs_S: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of ?S)›
using struct_invs_add by auto
have no_smaller_S: ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)›
using no_smaller_add by simp
obtain MM3 MM2 MM1 where MM: ‹M = MM3 @ Decided K1 # MM2 @ Decided K2 # MM1› and
[simp]: ‹filter is_decided MM3 = []› and
[simp]: ‹filter is_decided MM2 = []›
using filter_M
by (auto simp: filter_eq_Cons_iff filter_empty_conv
eq_commute[of _ ‹filter is_decided _›])
then have [simp]: ‹count_decided MM3 = 0› ‹count_decided MM2 = 0›
by (auto simp: count_decided_0_iff filter_empty_conv
simp del: ‹filter is_decided MM3 = []› ‹filter is_decided MM2 = []›)
have [simp]: ‹get_level M K = Suc (count_decided M1)›
using no_dup unfolding M'
by (auto simp: get_level_skip)
then have [iff]: ‹K1≠K›
using lev_K no_dup by (auto simp: MM simp del: ‹get_level M K = Suc (count_decided M1)›)
have ‹set M1 ⊆ set MM1›
using refl[of M] lev_K no_dup[unfolded MM] no_dup[unfolded M'] ‹count_decided MM2 = 0›
‹count_decided MM3 = 0›
apply (subst (asm) M')
apply (subst (asm) MM)
by (auto simp: simp del: ‹count_decided MM2 = 0› ‹count_decided MM3 = 0›
elim!: list_match_lel_lel)
then have ‹undefined_lit MM1 L ⟹ undefined_lit M1 L› for L
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
then have [iff]: ‹K1 ∉ lits_of_l M1› ‹K2 ∉ lits_of_l M1›
using no_dup unfolding MM
by (auto dest: in_lits_of_l_defined_litD)
have ‹struct_wf_twl_cls (TWL_DECO_clause M)›
using dist_filtered' unfolding deco_M filter_M
by (auto simp: simp del: clause_TWL_Deco_clause)
moreover have ‹twl_lazy_update M1 (TWL_DECO_clause M)›
by (auto simp: deco_M add_mset_eq_add_mset)
moreover have ‹watched_literals_false_of_max_level M1 (TWL_DECO_clause M)›
by (auto simp: deco_M add_mset_eq_add_mset)
ultimately have ‹twl_st_inv ?S›
using wf_N_U st_invs_M1' unfolding twl_st_inv.simps
by (auto simp: twl_is_an_exception_def)
moreover have ‹valid_enqueued ?S›
by auto
moreover have struct_invs_S: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of ?S)›
using struct_invs_add by simp
moreover have ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)›
using no_smaller_add by simp
moreover have ‹twl_st_exception_inv ?S›
using st_invs_M1' by (auto simp: twl_exception_inv.simps deco_M add_mset_eq_add_mset)
moreover have ‹no_duplicate_queued ?S›
by auto
moreover have ‹distinct_queued ?S›
by auto
moreover have ‹confl_cands_enqueued ?S›
using confl_enqueued_M1 by (auto simp: deco_M)
moreover have ‹propa_cands_enqueued ?S›
using propa_enqueued_M1
by (auto simp: deco_M true_annots_true_cls_def_iff_negation_in_model Ball_def
dest: in_lits_of_l_defined_litD in_diffD)
moreover have ‹get_conflict ?S = None›
by simp
moreover {
have ‹get_level M L = 0 ⟹ get_level M1 L = 0› for L
using no_dup defined_lit_no_dupD(1)[of M1 L M2']
by (cases ‹defined_lit M L›)
(auto simp: M' defined_lit_append defined_lit_cons atm_of_eq_atm_of
get_level_cons_if split: if_splits)
moreover have ‹get_level M L = 0 ⟹ L ∈ lits_of_l M ⟹ L ∈ lits_of_l M1› for L
using no_dup defined_lit_no_dupD(1)[of M1 L M2']
by (cases ‹defined_lit M L›)
(auto simp: M' defined_lit_append defined_lit_cons atm_of_eq_atm_of
get_level_cons_if split: if_splits dest: in_lits_of_l_defined_litD)
ultimately have ‹entailed_clss_inv ?S›
using entailed unfolding entailed_clss_inv.simps by meson
}
moreover {
have ‹¬clauses_to_update_prop {#} M1 (L, TWL_DECO_clause M)› for L
by (auto simp: deco_M clauses_to_update_prop.simps add_mset_eq_add_mset)
moreover have ‹ watched (TWL_DECO_clause M) = {#L, L'#} ⟹
- L ∈ lits_of_l M1 ⟹ False› for L L'
by (auto simp: deco_M add_mset_eq_add_mset)
ultimately have ‹clauses_to_update_inv ?S›
using clss_upd no_dup by (auto simp: filter_mset_empty_conv clauses_to_update_prop.simps
dest: in_lits_of_l_defined_litD)
}
moreover have ‹past_invs ?S›
unfolding past_invs.simps
proof (intro conjI impI allI)
fix M1a M2 K'
assume M1a: ‹M1 = M2 @ Decided K' # M1a›
let ?SM1a = ‹(M1a, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#}, {#})›
have
struct:
‹C∈#N + U ⟹ twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv (M1a, N, U, None, NP, UP, {#}, {#}) C›
for C
using past_M1 unfolding past_invs.simps M1a
by fast+
then have [iff]: ‹K1 ∉ lits_of_l M1a› ‹K2 ∉ lits_of_l M1a›
using ‹K1 ∉ lits_of_l M1› ‹K2 ∉ lits_of_l M1› unfolding M1a
by (auto dest: in_lits_of_l_defined_litD)
have
confl: ‹confl_cands_enqueued (M1a, N, U, None, NP, UP, {#}, {#})› and
propa: ‹propa_cands_enqueued (M1a, N, U, None, NP, UP, {#}, {#})› and
clss_to_upd: ‹clauses_to_update_inv (M1a, N, U, None, NP, UP, {#}, {#})›
using past_M1 unfolding past_invs.simps unfolding M1a
by fast+
show ‹∀C∈#add_mset (TWL_DECO_clause M) N + U. twl_lazy_update M1a C ∧
watched_literals_false_of_max_level M1a C ∧
twl_exception_inv ?SM1a C›
using struct by (auto simp add: twl_exception_inv.simps deco_M add_mset_eq_add_mset)
show ‹confl_cands_enqueued ?SM1a›
using confl by (auto simp: deco_M)
show ‹propa_cands_enqueued ?SM1a›
using propa by (auto simp: deco_M)
have [iff]: ‹¬ clauses_to_update_prop {#} M1a
(L, TWL_Clause {#- K1, - K2#}
{#- lit_of x. x ∈# mset C#})› for L
by (auto simp: clauses_to_update_prop.simps add_mset_eq_add_mset)
show ‹clauses_to_update_inv ?SM1a›
using clss_to_upd by (auto simp: deco_M add_mset_eq_add_mset)
qed
ultimately show ‹twl_struct_invs (M1, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#}, {#})›
unfolding twl_struct_invs_def
by meson
}
qed
lemma get_all_ann_decomposition_count_decided_1:
assumes
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and
count_dec: ‹count_decided M = 1›
shows ‹M = M2 @ Decided K # M1›
proof -
obtain M3 where
M: ‹M = M3 @ M2 @ Decided K # M1›
using decomp by blast
then have M': ‹M = (M3 @ M2) @ Decided K # M1›
by simp
have count_dec_M1: ‹count_decided M1 = 0›
using count_dec unfolding M'
by (auto simp: count_decided_0_iff)
have [simp]: ‹length (get_all_ann_decomposition (M3 @ M2)) = Suc 0›
‹length (get_all_ann_decomposition M1) = Suc 0›
using count_dec unfolding M'
by (subst no_decision_get_all_ann_decomposition; auto simp: count_decided_0_iff; fail)+
have ‹length (get_all_ann_decomposition M) = 2›
using count_dec
unfolding M' cdcl⇩W_restart_mset.length_get_all_ann_decomposition_append_Decided
by auto
moreover have ‹get_all_ann_decomposition M = [(a, b), (Decided K # M1, M2)] ⟹ False› for a b
using decomp get_all_ann_decomposition_hd_hd[of M ‹fst (hd (get_all_ann_decomposition M))›
‹snd (hd (get_all_ann_decomposition M))› ‹fst ((hd o tl) (get_all_ann_decomposition M))›
‹snd ((hd o tl) (get_all_ann_decomposition M))› Nil] count_dec
get_all_ann_decomposition_exists_prepend[of a b M]
by (cases ‹get_all_ann_decomposition M›; cases ‹tl (get_all_ann_decomposition M)›;
cases ‹fst ((hd o tl) (get_all_ann_decomposition M))›; cases a)
(auto simp: count_decided_0_iff)
ultimately have ‹get_all_ann_decomposition M = [(Decided K # M1, M2), ([], M1)]›
using decomp get_all_ann_decomposition_hd_hd[of M ‹fst (hd (get_all_ann_decomposition M))›
‹snd (hd (get_all_ann_decomposition M))› ‹fst ((hd o tl) (get_all_ann_decomposition M))›
‹snd ((hd o tl) (get_all_ann_decomposition M))› Nil]
in_get_all_ann_decomposition_decided_or_empty[of ‹fst ((hd o tl) (get_all_ann_decomposition M))›
‹snd ((hd o tl) (get_all_ann_decomposition M))› M] count_dec_M1
by (cases ‹get_all_ann_decomposition M›; cases ‹tl (get_all_ann_decomposition M)›;
cases ‹fst ((hd o tl) (get_all_ann_decomposition M))›)
(auto simp: count_decided_0_iff)
show ‹?thesis›
by (simp add: ‹get_all_ann_decomposition M = [(Decided K # M1, M2), ([], M1)]›
get_all_ann_decomposition_decomp)
qed
lemma negate_model_and_add_twl_twl_stgy_invs:
assumes
‹negate_model_and_add_twl S T› and
‹twl_struct_invs S› and
‹twl_stgy_invs S›
shows ‹twl_stgy_invs T›
using assms
proof (induction rule: negate_model_and_add_twl.induct)
case (bj_unit K M1 M2 M N U NP UP WS Q) note decomp = this(1) and lev_K = this(2) and
count_dec = this(3) and struct = this(4) and stgy = this(5)
let ?S = ‹(M, N, U, None, NP, UP, WS, Q)›
let ?T = ‹(Propagated (- K) (DECO_clause M) # M1, N, U, None, add_mset (DECO_clause M) NP, UP,
{#}, {#K#})›
have
false_with_lev: ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (state⇩W_of ?S)› and
no_smaller_confl: ‹cdcl⇩W_restart_mset.no_smaller_confl (state⇩W_of ?S)› and
confl0: ‹cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0 (state⇩W_of ?S)›
using stgy unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by fast+
have M: ‹M = M2 @ Decided K # M1›
using decomp count_dec by(simp add: get_all_ann_decomposition_count_decided_1)
have [iff]: ‹M = M' @ Decided K' # Ma ⟷ M' = M2 ∧ K' = K ∧ Ma = M1› for M' K' Ma
using count_dec unfolding M
by (auto elim!: list_match_lel_lel)
have [iff]: ‹M1 = M' @ Decided K' # Ma ⟷ False› for M' K' Ma
using count_dec unfolding M
by (auto elim!: list_match_lel_lel)
have
false_with_lev: ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (state⇩W_of ?T)›
using false_with_lev unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def)
moreover have ‹cdcl⇩W_restart_mset.no_smaller_confl (state⇩W_of ?T)›
using no_smaller_confl unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dest!: multi_member_split)
moreover have ‹cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0 (state⇩W_of ?T)›
using no_smaller_confl unfolding cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dest!: multi_member_split)
ultimately show ?case
unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def)
next
case (bj_nonunit K M1 M2 M N U NP UP WS Q) note decomp = this(1) and lev_K = this(2) and
count_dec = this(3) and struct = this(4) and stgy = this(5)
let ?S = ‹(M, N, U, None, NP, UP, WS, Q)›
let ?T = ‹(Propagated (- K) (DECO_clause M) # M1, add_mset (TWL_DECO_clause M) N, U,
None, NP, UP, {#}, {#K#})›
have
false_with_lev: ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (state⇩W_of ?S)› and
no_smaller_confl: ‹cdcl⇩W_restart_mset.no_smaller_confl (state⇩W_of ?S)› and
confl0: ‹cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0 (state⇩W_of ?S)›
using stgy unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by fast+
obtain M3 where M: ‹M = M3 @ M2 @ Decided K # M1›
using decomp by auto
have ‹no_dup M›
using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def trail.simps state⇩W_of.simps
by fast
then have H: ‹M1 = M' @ Decided Ka # M2 ⟹ ¬M2 ⊨as CNot (DECO_clause M)› for M' Ka M2
by (auto simp: M DECO_clause_def
dest: in_lits_of_l_defined_litD in_diffD)
have
false_with_lev: ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (state⇩W_of ?T)›
using false_with_lev unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def)
moreover have ‹cdcl⇩W_restart_mset.no_smaller_confl (state⇩W_of ?T)›
using no_smaller_confl H unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def M
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dest!: multi_member_split)
moreover have ‹cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0 (state⇩W_of ?T)›
using no_smaller_confl unfolding cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dest!: multi_member_split)
ultimately show ?case
unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def by fast
next
case (restart_nonunit K M1 M2 M N U NP UP WS Q) note decomp = this(1) and lev_K = this(2) and
count_dec = this(3) and struct = this(4) and stgy = this(5)
let ?S = ‹(M, N, U, None, NP, UP, WS, Q)›
let ?T = ‹(M1, add_mset (TWL_DECO_clause M) N, U, None, NP, UP, {#}, {#})›
have
false_with_lev: ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (state⇩W_of ?S)› and
no_smaller_confl: ‹cdcl⇩W_restart_mset.no_smaller_confl (state⇩W_of ?S)› and
confl0: ‹cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0 (state⇩W_of ?S)›
using stgy unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by fast+
obtain M3 where M: ‹M = M3 @ M2 @ Decided K # M1›
using decomp by auto
have ‹no_dup M›
using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def trail.simps state⇩W_of.simps
by fast
then have H: ‹M1 = M' @ Decided Ka # M2 ⟹ ¬M2 ⊨as CNot (DECO_clause M)› for M' Ka M2
by (auto simp: M DECO_clause_def
dest: in_lits_of_l_defined_litD in_diffD)
have
false_with_lev: ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (state⇩W_of ?T)›
using false_with_lev unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def)
moreover have ‹cdcl⇩W_restart_mset.no_smaller_confl (state⇩W_of ?T)›
using no_smaller_confl H unfolding cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def M
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dest!: multi_member_split)
moreover have ‹cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0 (state⇩W_of ?T)›
using no_smaller_confl unfolding cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def
by (auto simp: cdcl⇩W_restart_mset_state clauses_def
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dest!: multi_member_split)
ultimately show ?case
unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def by fast
qed
lemma cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init:
assumes
‹cdcl_twl_stgy S s› and
‹twl_struct_invs S› and
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of s)›
by (meson assms cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_learned_clauses_entailed
cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart
cdcl_twl_stgy_cdcl⇩W_stgy twl_struct_invs_def)
lemma rtranclp_cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init:
assumes
‹cdcl_twl_stgy⇧*⇧* S s› and
‹twl_struct_invs S› and
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of s)›
using assms
by (induction rule: rtranclp_induct)
(auto intro: cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init
rtranclp_cdcl_twl_stgy_twl_struct_invs)
lemma negate_model_and_add_twl_cdcl⇩W_learned_clauses_entailed_by_init:
assumes
‹negate_model_and_add_twl S s› and
‹twl_struct_invs S› and
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)›
shows
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of s)›
using assms
by (induction rule: negate_model_and_add_twl.induct)
(auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
cdcl⇩W_restart_mset_state)
end