theory Watched_Literals_Algorithm_Enumeration
imports Watched_Literals.Watched_Literals_Algorithm Watched_Literals_Transition_System_Enumeration
begin
definition cdcl_twl_enum_inv :: ‹'v twl_st ⇒ bool› where
‹cdcl_twl_enum_inv S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧ final_twl_state S ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)›
definition mod_restriction :: ‹'v clauses ⇒ 'v clauses ⇒ bool› where
‹mod_restriction N N' ⟷
(∀M. M ⊨sm N ⟶ M ⊨sm N') ∧
(∀M. total_over_m M (set_mset N') ⟶ consistent_interp M ⟶ M ⊨sm N' ⟶ M ⊨sm N)›
lemma mod_restriction_satisfiable_iff:
‹mod_restriction N N' ⟹ satisfiable (set_mset N) ⟷ satisfiable (set_mset N')›
apply (auto simp: mod_restriction_def satisfiable_carac[symmetric])
by (meson satisfiable_carac satisfiable_def true_clss_set_mset)
definition enum_mod_restriction_st_clss :: ‹('v twl_st × ('v literal list option × 'v clauses)) set› where
‹enum_mod_restriction_st_clss = {(S, (M, N)). mod_restriction (get_all_init_clss S) N ∧
twl_struct_invs S ∧ twl_stgy_invs S ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S) ∧
atms_of_mm (get_all_init_clss S) = atms_of_mm N}›
definition enum_model_st_direct :: ‹('v twl_st × ('v literal list option × 'v clauses)) set› where
‹enum_model_st_direct = {(S, (M, N)).
mod_restriction (get_all_init_clss S) N ∧
(get_conflict S = None ⟶ M ≠ None ∧ lit_of `# mset (get_trail S) = mset (the M)) ∧
(get_conflict S ≠ None ⟶ M = None) ∧
atms_of_mm (get_all_init_clss S) = atms_of_mm N ∧
(get_conflict S = None ⟶ next_model (map lit_of (get_trail S)) N) ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S) ∧
cdcl_twl_enum_inv S}›
definition enum_model_st :: ‹((bool × 'v twl_st) × ('v literal list option × 'v clauses)) set› where
‹enum_model_st = {((b, S), (M, N)).
mod_restriction (get_all_init_clss S) N ∧
(b ⟶ get_conflict S = None ∧ M ≠ None ∧ lits_of_l (get_trail S) = set (the M)) ∧
(get_conflict S ≠ None ⟶ ¬b ∧ M = None)}›
fun add_to_init_cls :: ‹'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st› where
‹add_to_init_cls C (M, N, U, D, NE, UE, WS, Q) = (M, add_mset C N, U, D, NE, UE, WS, Q)›
lemma cdcl_twl_stgy_final_twl_stateE:
assumes
‹cdcl_twl_stgy⇧*⇧* S T› and
final: ‹final_twl_state T› and
‹twl_struct_invs S› and
‹twl_stgy_invs S› and
ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)› and
Hunsat: ‹get_conflict T ≠ None ⟹ unsatisfiable (set_mset (get_all_init_clss S)) ⟹ P› and
Hsat: ‹get_conflict T = None ⟹ consistent_interp (lits_of_l (get_trail T)) ⟹
no_dup (get_trail T) ⟹ atm_of ` (lits_of_l (get_trail T)) ⊆ atms_of_mm (get_all_init_clss T) ⟹
get_trail T ⊨asm get_all_init_clss S ⟹ satisfiable (set_mset (get_all_init_clss S)) ⟹ P›
shows P
proof -
have ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* (state⇩W_of S) (state⇩W_of T)›
by (simp add: assms(1) assms(3) rtranclp_cdcl_twl_stgy_cdcl⇩W_stgy)
have all_struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of T)›
using assms(1) assms(3) rtranclp_cdcl_twl_stgy_twl_struct_invs twl_struct_invs_def by blast
then have
M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
have ent': ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of T)›
by (meson ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* (state⇩W_of S) (state⇩W_of T)› assms(3)
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 ent twl_struct_invs_def)
have [simp]: ‹get_all_init_clss T = get_all_init_clss S›
by (metis assms(1) rtranclp_cdcl_twl_stgy_all_learned_diff_learned)
have stgy_T: ‹twl_stgy_invs T›
using assms(1) assms(3) assms(4) rtranclp_cdcl_twl_stgy_twl_stgy_invs by blast
consider
(confl) ‹count_decided (get_trail T) = 0› and ‹get_conflict T ≠ None› |
(sat) ‹no_step cdcl_twl_stgy T› and ‹get_conflict T = None› |
(unsat) ‹no_step cdcl_twl_stgy T› and ‹get_conflict T ≠ None›
using final unfolding final_twl_state_def
by fast
then show ?thesis
proof cases
case confl
then show ?thesis
using conflict_of_level_unsatisfiable[OF all_struct_T] ent'
by (auto simp: twl_st intro!: Hunsat)
next
case sat
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy (state⇩W_of T)›
using assms(1) assms(3) no_step_cdcl_twl_stgy_no_step_cdcl⇩W_stgy
rtranclp_cdcl_twl_stgy_twl_struct_invs sat(1) by blast
from cdcl⇩W_restart_mset.cdcl⇩W_stgy_final_state_conclusive2[OF this]
have ‹get_trail T ⊨asm cdcl⇩W_restart_mset.clauses (state⇩W_of T)›
using sat all_struct_T
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by (auto simp: twl_st)
then have tr_T: ‹get_trail T ⊨asm get_all_init_clss T›
by (cases T) (auto simp: clauses_def)
show ?thesis
apply (rule Hsat)
subgoal using sat by auto
subgoal using M_lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st)
subgoal
using tr_T M_lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by (auto simp: twl_st)
subgoal using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def by (auto simp: twl_st)
subgoal using tr_T by auto
subgoal using tr_T M_lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: satisfiable_carac[symmetric] twl_st true_annots_true_cls)
done
next
case unsat
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy (state⇩W_of T)›
using assms(1) assms(3) no_step_cdcl_twl_stgy_no_step_cdcl⇩W_stgy
rtranclp_cdcl_twl_stgy_twl_struct_invs unsat(1) by blast
from cdcl⇩W_restart_mset.cdcl⇩W_stgy_final_state_conclusive2[OF this]
have unsat': ‹unsatisfiable (set_mset (cdcl⇩W_restart_mset.clauses (state⇩W_of T)))›
using unsat all_struct_T stgy_T
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def twl_stgy_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by (auto simp: twl_st)
have unsat': ‹unsatisfiable (set_mset (get_all_init_clss T))›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain I where
cons: ‹consistent_interp I› and
I: ‹I ⊨sm get_all_init_clss T› and
tot: ‹total_over_m I (set_mset (get_all_init_clss T))›
unfolding satisfiable_def by blast
have [simp]: ‹cdcl⇩W_restart_mset.clauses (state⇩W_of T) = get_all_init_clss T + get_all_learned_clss T›
by (cases T) (auto simp: clauses_def)
moreover have ‹total_over_m I (set_mset (cdcl⇩W_restart_mset.clauses (state⇩W_of T)))›
using alien tot unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: cdcl⇩W_restart_mset_state total_over_m_alt_def twl_st)
ultimately have ‹I ⊨sm cdcl⇩W_restart_mset.clauses (state⇩W_of T)›
using ent' I cons unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
true_clss_clss_def total_over_m_def
by (auto simp: clauses_def cdcl⇩W_restart_mset_state satisfiable_carac[symmetric] twl_st)
then show False
using unsat' cons I by auto
qed
show ?thesis
apply (rule Hunsat)
subgoal using unsat by auto
subgoal using unsat' by auto
done
qed
qed
context
fixes P :: ‹'v literal set ⇒ bool›
begin
fun negate_model_and_add :: ‹'v literal list option × 'v clauses ⇒ _ × 'v clauses› where
‹negate_model_and_add (Some M, N) =
(if P (set M) then (Some M, N)
else (None, add_mset (uminus `# mset M) N))› |
‹negate_model_and_add (None, N) = (None, N)›
text ‹
The code below is a little tricky to get right (in a way that can be easily refined later).
There are three cases:
▸ the considered clauses are not satisfiable. Then we can conclude that there is no model.
▸ the considered clauses are satisfiable and there is at least one decision. Then, we can simply
apply \<^term>‹negate_model_and_add_twl›.
▸ the considered clauses are satisfiable and there are no decisions. Then we cannot apply
\<^term>‹negate_model_and_add_twl›, because that would produce the empty clause that cannot
be part of our state (because of our invariants). Therefore, as we know that the model is
the last possible model, we break out of the loop and handle test if the model is acceptable
outside of the loop.
›
definition cdcl_twl_enum :: ‹'v twl_st ⇒ bool nres› where
‹cdcl_twl_enum S = do {
S ← conclusive_TWL_run S;
S ← WHILE⇩T⇗cdcl_twl_enum_inv⇖
(λS. get_conflict S = None ∧ count_decided(get_trail S) > 0 ∧ ¬P (lits_of_l (get_trail S)))
(λS. do {
S ← SPEC (negate_model_and_add_twl S);
conclusive_TWL_run S
})
S;
if get_conflict S = None
then RETURN (if count_decided(get_trail S) = 0 then P (lits_of_l (get_trail S)) else True)
else RETURN (False)
}›
definition next_model_filtered_nres where
‹next_model_filtered_nres N =
SPEC (λb. ∃M. full (next_model_filtered P) N M ∧ b = (fst M ≠ None))›
lemma mod_restriction_next_modelD:
‹mod_restriction N N' ⟹ atms_of_mm N ⊆ atms_of_mm N' ⟹ next_model M N ⟹ next_model M N'›
by (auto simp: mod_restriction_def next_model.simps)
definition enum_mod_restriction_st_clss_after :: ‹('v twl_st × ('v literal list option × 'v clauses)) set› where
‹enum_mod_restriction_st_clss_after = {(S, (M, N)).
(get_conflict S = None ⟶ count_decided (get_trail S) = 0 ⟶
mod_restriction (add_mset {#} (get_all_init_clss S))
(add_mset (uminus `# lit_of `# mset (get_trail S)) N)) ∧
(mod_restriction (get_all_init_clss S) N) ∧
twl_struct_invs S ∧ twl_stgy_invs S ∧
(get_conflict S = None ⟶ M ≠ None ⟶ P (set(the M)) ∧ lit_of `# mset (get_trail S) = mset (the M)) ∧
(get_conflict S ≠ None ⟶ M = None) ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S) ∧
atms_of_mm (get_all_init_clss S) = atms_of_mm N}›
lemma atms_of_uminus_lit_of[simp]: ‹atms_of {#- lit_of x. x ∈# A#} = atms_of (lit_of `# A)›
by (auto simp: atms_of_def image_image)
lemma lit_of_mset_eq_mset_setD[dest]:
‹lit_of `# mset M = mset aa ⟹ set aa = lit_of ` set M›
by (metis set_image_mset set_mset_mset)
lemma mod_restriction_add_twice[simp]:
‹mod_restriction A (add_mset C (add_mset C N)) ⟷ mod_restriction A (add_mset C N)›
by (auto simp: mod_restriction_def)
lemma
assumes
confl: ‹get_conflict W = None› and
count_dec: ‹count_decided (get_trail W) = 0› and
enum_inv: ‹cdcl_twl_enum_inv W› and
mod_rest_U: ‹mod_restriction (get_all_init_clss W) N› and
atms_U_U': ‹atms_of_mm (get_all_init_clss W) = atms_of_mm N›
shows
final_level0_add_empty_clause:
‹mod_restriction (add_mset {#} (get_all_init_clss W))
(add_mset {#- lit_of x. x ∈# mset (get_trail W)#} N)› (is ?A) and
final_level0_add_empty_clause_unsat:
‹unsatisfiable (set_mset (add_mset {#- lit_of x. x ∈# mset (get_trail W)#} N))› (is ?B)
proof -
have [simp]: ‹DECO_clause (get_trail W) = {#}› and
[simp]: ‹{unmark L |L. is_decided L ∧ L ∈ set (trail (state⇩W_of W))} = {}›
using count_dec by (auto simp: count_decided_0_iff DECO_clause_def
filter_mset_empty_conv twl_st)
have struct_W: ‹twl_struct_invs W› and
ent_W: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of W)›
using enum_inv
unfolding cdcl_twl_enum_inv_def by blast+
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of W)› and
decomp: ‹all_decomposition_implies_m (cdcl⇩W_restart_mset.clauses (state⇩W_of W))
(get_all_ann_decomposition (trail (state⇩W_of W)))›
using struct_W unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have alien_W: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of W)›
using struct_W
unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
have 1: ‹set_mset (cdcl⇩W_restart_mset.clauses (state⇩W_of W))⊨ps
unmark_l (trail (state⇩W_of W))›
using all_decomposition_implies_propagated_lits_are_implied[OF decomp]
by simp
then have 2: ‹set_mset (get_all_init_clss W) ⊨ps
unmark_l (trail (state⇩W_of W))›
using ent_W unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
cdcl⇩W_restart_mset.clauses_def
by (fastforce simp: clauses_def twl_st dest: true_clss_clss_generalise_true_clss_clss)
have H: False
if M_tr_W: ‹M ⊨ {#- lit_of x. x ∈# mset (get_trail W)#}› and
M_U': ‹M ⊨m N› and
tot: ‹total_over_m M (set_mset N)› and
cons: ‹consistent_interp M›
for M
proof -
have ‹M ⊨sm get_all_init_clss W›
using mod_rest_U M_U' cons
unfolding mod_restriction_def
apply auto
using tot apply blast+
done
moreover have ‹total_over_m M (set_mset (get_all_init_clss W) ∪
unmark_l (trail (state⇩W_of W)))›
using alien_W atms_U_U' tot
unfolding total_over_m_alt_def total_over_set_alt_def
cdcl⇩W_restart_mset.no_strange_atm_def
by (auto 5 5 dest: atms_of_DECO_clauseD simp: lits_of_def twl_st)
ultimately have ‹M ⊨s unmark_l (trail (state⇩W_of W))›
using 2 cons unfolding true_clss_clss_def
by auto
then show False
using cons M_tr_W
by (auto simp: true_clss_def twl_st true_cls_def consistent_interp_def)
qed
then show ?A
unfolding mod_restriction_def
by auto
from mod_restriction_satisfiable_iff[OF this]
show ?B
by (auto simp: satisfiable_def)
qed
lemma cdcl_twl_enum_next_model_filtered_nres:
‹(cdcl_twl_enum, next_model_filtered_nres) ∈
[λ(M, N). M = None]⇩f enum_mod_restriction_st_clss → ⟨bool_rel⟩nres_rel›
proof -
define model_if_exists where
‹model_if_exists S ≡ λM.
(if ∃M. next_model M (snd S)
then (fst M ≠ None ∧ next_model (the (fst M)) (snd S) ∧ snd M = snd S)
else (fst M = None ∧ M = S))›
for S :: ‹_ × 'v clauses›
have ‹full (next_model_filtered P) S U ⟷
(∃T. model_if_exists S T ∧ full (next_model_filtered P) (None, snd T) U)›
(is ‹?A ⟷ ?B›)
if ‹fst S = None›
for S U
proof
assume ?A
then consider
(nss) ‹no_step (next_model_filtered P) S› |
(s1) T where ‹(next_model_filtered P) S T› and ‹full (next_model_filtered P) T U›
unfolding full_def
by (metis converse_rtranclpE)
then show ?B
proof cases
case nss
then have SU: ‹S = U›
using ‹?A›
apply (subst (asm) no_step_full_iff_eq)
apply assumption by simp
have ‹model_if_exists S S› and ‹fst S = None›
using nss no_step_next_model_filtered_next_model_iff[of ‹(_, snd S)›] that
unfolding model_if_exists_def
by (cases S; auto; fail)+
moreover {
have ‹no_step (next_model_filtered P) (None, snd S)›
using nss
apply (subst no_step_next_model_filtered_next_model_iff)
subgoal using that by (cases S) auto
apply (subst (asm) no_step_next_model_filtered_next_model_iff)
subgoal using that by (cases S) auto
unfolding Ex_next_model_iff_statisfiable
apply (rule unsatisfiable_mono)
defer
apply assumption
by (cases S; cases ‹fst S›) (auto intro: unsatisfiable_mono)
then have ‹full (next_model_filtered P) (None, snd S) U›
apply (subst no_step_full_iff_eq)
apply assumption
using SU ‹fst S = None›
by (cases S) auto
}
ultimately show ?B
by fast
next
case (s1 T)
obtain M where
M: ‹next_model M (snd S)› and
T: ‹T = (if P (set M) then (Some M, snd S)
else (None, add_mset (image_mset uminus (mset M)) (snd S)))›
using s1
unfolding model_if_exists_def
apply (cases T)
apply (auto simp: next_model_filtered.simps)
done
let ?T = ‹((Some M, snd S))›
have nm: ‹model_if_exists S ?T›
using M T that unfolding model_if_exists_def
by (cases S) auto
moreover have ‹full (next_model_filtered P) (negate_model_and_add ?T) U›
using s1(2) T
by (auto split: if_splits)
moreover have ‹next_model_filtered P (None, snd ?T) (negate_model_and_add (Some M, snd S))›
using nm that by (cases S) (auto simp: next_model_filtered.simps model_if_exists_def
split: if_splits)
ultimately show ?B
proof -
have "(None, snd (Some M, snd S)) = S"
by (metis (no_types) sndI surjective_pairing that)
then have "full (next_model_filtered P) (None, snd (Some M, snd S)) U"
by (metis ‹full (next_model_filtered P) S U›)
then show ?thesis
using ‹model_if_exists S (Some M, snd S)› by blast
qed
qed
next
assume ?B
then show ?A
apply (auto simp: model_if_exists_def full1_is_full full_fullI split: if_splits)
by (metis prod.exhaust_sel that)
qed
note H = this
have next_model_filtered_nres_alt_def: ‹next_model_filtered_nres S = do {
S ← SPEC (model_if_exists S);
T ← SPEC (λT. full (next_model_filtered P) (None, snd S) T);
RETURN (fst T ≠ None)
}› if ‹fst S = None› for S
using that
unfolding next_model_filtered_nres_def RES_RES_RETURN_RES RES_RETURN_RES
H[OF that]
by blast+
have conclusive_run: ‹conclusive_TWL_run S
≤ ⇓ {(S, T). (S, T) ∈ enum_model_st_direct ∧ final_twl_state S ∧
(get_conflict S = None ⟶ next_model (map lit_of (get_trail S)) (snd T)) ∧
(get_conflict S ≠ None ⟶ unsatisfiable (set_mset (snd T)))}
(SPEC (model_if_exists MN))›
(is ‹_ ≤ ⇓ ?spec_twl _›)
if
S_MN: ‹(S, MN) ∈ enum_mod_restriction_st_clss› and
M: ‹case MN of (M, N) ⇒ M = None›
for S MN
proof -
have H: ‹∃s'∈Collect (model_if_exists MN). (s, s') ∈ enum_model_st_direct ∧ final_twl_state s ∧
(get_conflict s = None ⟶ next_model (map lit_of (get_trail s)) (snd s')) ∧
(get_conflict s ≠ None ⟶ unsatisfiable (set_mset (snd s')))›
if
star: ‹cdcl_twl_stgy⇧*⇧* S s› and
final: ‹final_twl_state s›
for s :: ‹'v twl_st›
proof -
obtain N where
[simp]: ‹MN = (None, N)›
using M by auto
have [simp]: ‹get_all_init_clss s = get_all_init_clss S›
by (metis rtranclp_cdcl_twl_stgy_all_learned_diff_learned that(1))
have struct_S: ‹twl_struct_invs S›
using S_MN unfolding enum_mod_restriction_st_clss_def by blast
moreover have stgy_S: ‹twl_stgy_invs S›
using S_MN unfolding enum_mod_restriction_st_clss_def by blast
moreover have ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)›
using S_MN unfolding enum_mod_restriction_st_clss_def by blast
then have ent_s: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of s)›
using rtranclp_cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init star struct_S by blast
then have enum_inv: ‹cdcl_twl_enum_inv s›
using star S_MN final unfolding enum_mod_restriction_st_clss_def cdcl_twl_enum_inv_def
by (auto intro: rtranclp_cdcl_twl_stgy_twl_struct_invs
rtranclp_cdcl_twl_stgy_twl_stgy_invs)
show ?thesis
using struct_S stgy_S ent
proof (rule cdcl_twl_stgy_final_twl_stateE[OF star final])
assume
confl: ‹get_conflict s ≠ None› and
unsat: ‹unsatisfiable (set_mset (get_all_init_clss S))›
let ?s = ‹(None, snd MN)›
have s: ‹(s, ?s) ∈ enum_model_st_direct›
using S_MN confl unsat enum_inv ent star unfolding enum_model_st_def
by (auto simp: enum_model_st_direct_def enum_mod_restriction_st_clss_def
intro: rtranclp_cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init)
moreover have ‹model_if_exists MN ?s›
using unsat S_MN unsat_no_step_next_model_filtered[of N P] Ex_next_model_iff_statisfiable[of N]
unfolding model_if_exists_def
by (auto simp: enum_mod_restriction_st_clss_def
mod_restriction_satisfiable_iff)
moreover have ‹unsatisfiable (set_mset N)›
using unsat
using s unfolding enum_model_st_direct_def
by (auto simp: mod_restriction_satisfiable_iff)
ultimately show ?thesis
apply -
by (rule bexI[of _ ‹?s›]) (use confl final in auto)
next
let ?s = ‹(Some (map lit_of (get_trail s)), N)›
assume
confl: ‹get_conflict s = None› and
cons: ‹consistent_interp (lits_of_l (get_trail s))› and
ent: ‹get_trail s ⊨asm get_all_init_clss S› and
sat: ‹satisfiable (set_mset (get_all_init_clss S))› and
n_d: ‹no_dup (get_trail s)› and
alien: ‹atm_of ` (lits_of_l (get_trail s)) ⊆ atms_of_mm (get_all_init_clss s)›
moreover have nm: ‹next_model (map lit_of (get_trail s)) N›
‹next_model (map lit_of (get_trail s)) (get_all_init_clss s)›
using ent cons n_d S_MN alien
by (auto simp: next_model.simps true_annots_true_cls lits_of_def
no_dup_map_lit_of enum_mod_restriction_st_clss_def mod_restriction_def)
ultimately have s: ‹(s, ?s) ∈ enum_model_st_direct›
using S_MN enum_inv star ent unfolding enum_model_st_direct_def
by (auto simp: mod_restriction_satisfiable_iff next_model.simps
enum_mod_restriction_st_clss_def lits_of_def
rtranclp_cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init)
moreover have ‹model_if_exists (None, N) (Some (map lit_of (get_trail s)), N)›
using nm by (auto simp: model_if_exists_def
enum_mod_restriction_st_clss_def
mod_restriction_satisfiable_iff)
moreover have ‹satisfiable (set_mset N)›
using sat
using s unfolding enum_model_st_direct_def
by (auto simp: Ex_next_model_iff_statisfiable[symmetric])
ultimately show ?thesis
using nm
apply -
by (rule bexI[of _ ‹(Some (map lit_of (get_trail s)), snd MN)›])
(use final confl in auto)
qed
qed
show ?thesis
unfolding conclusive_TWL_run_def
apply (rule RES_refine)
unfolding mem_Collect_eq prod.simps
apply (rule H)
apply fast+
done
qed
have loop: ‹WHILE⇩T⇗cdcl_twl_enum_inv⇖
(λS. get_conflict S = None ∧ count_decided (get_trail S) > 0 ∧
¬P (lits_of_l (get_trail S)))
(λS. SPEC (negate_model_and_add_twl S) ⤜
conclusive_TWL_run) T
≤ SPEC
(λy. ∃x. (y, x) ∈ {(y, x).
(( (get_conflict y ≠ None ∧ fst x = None) ∨
(fst x ≠ None ∧ P (lits_of_l (get_trail y))) ∧
(y, x) ∈ enum_mod_restriction_st_clss_after) ∨
(get_conflict y = None ∧ count_decided (get_trail y) = 0 ∧
¬P (lits_of_l (get_trail y)) ∧ fst x = None ∧
(y, (None, remove1_mset (uminus `# lit_of `# mset (get_trail y)) (snd x)))
∈ enum_mod_restriction_st_clss_after))
} ∧
full (next_model_filtered P) (None, snd M) x)›
(is ‹WHILE⇩T⇗_ ⇖ ?Cond _ _ ≤ SPEC ?Spec›
is ‹_ ≤ SPEC (λy. ∃x. (y, x) ∈ ?Res ∧ ?Full x)›)
if
MN: ‹case MN of (M, N) ⇒ M = None› and
S: ‹(S, MN) ∈ enum_mod_restriction_st_clss› and
T: ‹(T, M) ∈ ?spec_twl› and
M: ‹M ∈ Collect (model_if_exists MN)›
for S T :: ‹'v twl_st› and MN M
proof -
define R where
‹R = {(T :: 'v twl_st, S :: 'v twl_st).
get_conflict S = None ∧ ¬P (lits_of_l (get_trail S)) ∧ get_conflict T = None ∧
¬P (lits_of_l (get_trail T)) ∧
(get_all_init_clss T, get_all_init_clss S) ∈ measure (λN. card (all_models N))} ∪
{(T :: 'v twl_st, S :: 'v twl_st).
get_conflict S = None ∧ ¬P (lits_of_l (get_trail S)) ∧
(get_conflict T ≠ None ∨ P (lits_of_l (get_trail T)))}›
have wf: ‹wf R›
unfolding R_def
apply (subst Un_commute)
apply (rule wf_Un)
subgoal
by (rule wf_no_loop)
auto
subgoal
by (rule wf_if_measure_in_wf[of ‹measure (λN. card (all_models N))› _ ‹get_all_init_clss›])
auto
subgoal
by auto
done
define I where ‹I s = (∃x. (s, x) ∈ enum_mod_restriction_st_clss_after ∧
(next_model_filtered P)⇧*⇧* (None, snd M) (negate_model_and_add x) ∧
(next_model_filtered P)⇧*⇧* (None, snd M) (None, snd (negate_model_and_add x)) ∧
(get_conflict s = None ⟶ next_model (map lit_of (get_trail s)) (snd x)) ∧
(get_conflict s ≠ None ⟶ unsatisfiable (set_mset (snd x))) ∧
final_twl_state s)› for s
let ?Q = ‹λU V s'. cdcl_twl_enum_inv s' ∧ final_twl_state s' ∧ cdcl_twl_stgy⇧*⇧* V s' ∧ (s', U) ∈ R›
have
conc_run: ‹conclusive_TWL_run V ≤ SPEC (?Q U V)›
(is ?conc_run is ‹_ ≤ SPEC ?Q›) and
inv_I: ‹?Q U V W ⟹ I W› (is ‹_ ⟹ ?I›)
if
U: ‹cdcl_twl_enum_inv U› and
confl: ‹?Cond U› and
neg: ‹negate_model_and_add_twl U V› and
I_U: ‹I U›
for U V W
proof -
{
have ‹clauses_to_update V = {#}›
using neg by (auto simp: negate_model_and_add_twl.simps)
have
ent_V: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of V)› and
struct_U: ‹twl_struct_invs U› and
ent_U: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of U)›
using U unfolding cdcl_twl_enum_inv_def
using neg negate_model_and_add_twl_cdcl⇩W_learned_clauses_entailed_by_init by blast+
have invs_V: ‹twl_struct_invs V› ‹twl_stgy_invs V›
using U neg unfolding cdcl_twl_enum_inv_def
using negate_model_and_add_twl_twl_struct_invs negate_model_and_add_twl_twl_stgy_invs
by blast+
have [simp]: ‹get_all_init_clss V = add_mset (DECO_clause (get_trail U))(get_all_init_clss U)›
using neg by (auto simp: negate_model_and_add_twl.simps)
have next_mod_U: ‹next_model (map lit_of (get_trail U)) (get_all_init_clss U)›
if None: ‹get_conflict U = None›
proof (rule cdcl_twl_stgy_final_twl_stateE[of U U])
show ‹cdcl_twl_stgy⇧*⇧* U U›
by simp
show ‹final_twl_state U› ‹twl_struct_invs U› ‹twl_stgy_invs U›
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of U)›
using U unfolding cdcl_twl_enum_inv_def by blast+
show ?thesis
if ‹get_conflict U ≠ None›
using that None by blast
show ?thesis
if
‹get_conflict U = None› and
‹consistent_interp (lits_of_l (get_trail U))› and
‹no_dup (get_trail U)› and
incl: ‹atm_of ` lits_of_l (get_trail U) ⊆ atms_of_mm (get_all_init_clss U)› and
‹get_trail U ⊨asm get_all_init_clss U› and
‹satisfiable (set_mset (get_all_init_clss U))›
using that that(5) unfolding next_model.simps
by (auto simp: lits_of_def true_annots_true_cls no_dup_map_lit_of)
qed
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› and
decomp: ‹all_decomposition_implies_m (cdcl⇩W_restart_mset.clauses (state⇩W_of U))
(get_all_ann_decomposition (trail (state⇩W_of U)))›
using struct_U unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have ‹all_models (add_mset ((uminus o lit_of) `# mset (get_trail U)) (get_all_init_clss U)) ⊇
all_models (add_mset (DECO_clause (get_trail U)) (get_all_init_clss U))›
if None: ‹get_conflict U = None›
proof (rule cdcl_twl_stgy_final_twl_stateE[of U U])
show ‹cdcl_twl_stgy⇧*⇧* U U›
by simp
show ‹final_twl_state U› ‹twl_struct_invs U› ‹twl_stgy_invs U›
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of U)›
using U unfolding cdcl_twl_enum_inv_def by blast+
show ?thesis
if ‹get_conflict U ≠ None›
using that None by blast
show ?thesis
if
‹get_conflict U = None› and
‹consistent_interp (lits_of_l (get_trail U))› and
‹no_dup (get_trail U)› and
incl: ‹atm_of ` lits_of_l (get_trail U) ⊆ atms_of_mm (get_all_init_clss U)› and
‹get_trail U ⊨asm get_all_init_clss U› and
‹satisfiable (set_mset (get_all_init_clss U))›
proof -
have 1: ‹I ⊨ {#- lit_of x. x ∈# mset (get_trail U)#}›
if
I_U: ‹I ⊨ DECO_clause (get_trail U)›
for I
by (rule true_cls_mono_set_mset[OF _ I_U]) (auto simp: DECO_clause_def)
have ‹atms_of (DECO_clause (get_trail U)) ∪ atms_of_mm (get_all_init_clss U) =
atms_of_mm (get_all_init_clss U)›
using incl by (auto simp: DECO_clause_def lits_of_def atms_of_def)
then show ?thesis
by (auto simp: all_models_def 1)
qed
qed
from card_mono[OF _ this]
have card_decr: ‹card (all_models (add_mset (DECO_clause (get_trail U)) (get_all_init_clss U))) <
card (all_models (get_all_init_clss U))›
if ‹get_conflict U = None›
using next_model_decreasing[OF next_mod_U] that by (auto simp: finite_all_models)
{
fix WW
assume star: ‹cdcl_twl_stgy⇧*⇧* V WW› and final: ‹final_twl_state WW›
have ent_W: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of WW)›
using U ent_V neg invs_V rtranclp_cdcl_twl_stgy_cdcl⇩W_learned_clauses_entailed_by_init
star
unfolding cdcl_twl_enum_inv_def by blast
then have H1: ‹cdcl_twl_enum_inv WW›
using star final invs_V unfolding cdcl_twl_enum_inv_def
using rtranclp_cdcl_twl_stgy_twl_stgy_invs rtranclp_cdcl_twl_stgy_twl_struct_invs by blast
have init_clss_WW_V[simp]: ‹get_all_init_clss WW = get_all_init_clss V›
by (metis rtranclp_cdcl_twl_stgy_all_learned_diff_learned star)
have next_mod: ‹next_model (map lit_of (get_trail WW)) (get_all_init_clss WW)›
if None: ‹get_conflict WW = None›
using invs_V ent_V
proof (rule cdcl_twl_stgy_final_twl_stateE[OF star final])
show ?thesis
if ‹get_conflict WW ≠ None›
using that None by blast
show ?thesis
if
‹get_conflict WW = None› and
‹consistent_interp (lits_of_l (get_trail WW))› and
‹no_dup (get_trail WW)› and
‹atm_of ` lits_of_l (get_trail WW) ⊆ atms_of_mm (get_all_init_clss WW)› and
‹get_trail WW ⊨asm get_all_init_clss V› and
‹satisfiable (set_mset (get_all_init_clss V))›
using that that(5) unfolding next_model.simps
by (auto simp: lits_of_def true_annots_true_cls no_dup_map_lit_of)
qed
have not_none_unsat: ‹unsatisfiable (set_mset (get_all_init_clss V))›
if None: ‹get_conflict WW ≠ None›
using invs_V ent_V
proof (rule cdcl_twl_stgy_final_twl_stateE[OF star final])
show ?thesis
if ‹unsatisfiable (set_mset (get_all_init_clss V))›
using that None by blast
show ?thesis
if
‹get_conflict WW = None›
using that None unfolding next_model.simps
by (auto simp: lits_of_def true_annots_true_cls no_dup_map_lit_of)
qed
have H2: ‹(WW, U) ∈ R›
using confl card_decr unfolding R_def by (auto)
note H1 H2 next_mod init_clss_WW_V not_none_unsat
} note H = this(1,2) and next_mod = this(3) and init_clss_WW_V = this(4) and
not_none_unsat = this(5)
{
assume ‹?Q W›
then have
twl_enum: ‹cdcl_twl_enum_inv W› and
final: ‹final_twl_state W› and
st: ‹cdcl_twl_stgy⇧*⇧* V W› and
W_U: ‹(W, U) ∈ R›
by blast+
obtain U' where
U_U': ‹(U, U') ∈ enum_mod_restriction_st_clss_after› and
st_M_U': ‹(next_model_filtered P)⇧*⇧* (None, snd M) (negate_model_and_add U')›
using I_U unfolding I_def by blast
have 1: ‹{unmark L |L. is_decided L ∧ L ∈ set (trail (state⇩W_of U))} =
CNot (DECO_clause (get_trail U))›
by (force simp: DECO_clause_def twl_st CNot_def)
have ent3_gnerealise: ‹A ∪ B ∪ C ⊨ps D ⟹ A ⊨ps B ⟹ A ∪ C ⊨ps D› for A B C D
by (metis Un_absorb inf_sup_aci(5) true_clss_clss_def
true_clss_clss_generalise_true_clss_clss)
have ‹set_mset (cdcl⇩W_restart_mset.clauses (state⇩W_of U)) ∪
CNot (DECO_clause (get_trail U)) ⊨ps unmark_l (trail (state⇩W_of U))›
using all_decomposition_implies_propagated_lits_are_implied[OF decomp]
unfolding 1 .
then have 2: ‹set_mset (get_all_init_clss U) ∪ CNot (DECO_clause (get_trail U)) ⊨ps
unmark_l (trail (state⇩W_of U))›
using ent_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
cdcl⇩W_restart_mset.clauses_def
by (auto simp: clauses_def twl_st intro: ent3_gnerealise)
have [simp]: ‹unmark_l (get_trail U) = CNot {#- lit_of x. x ∈# mset (get_trail U)#}›
by (force simp: CNot_def)
have mod_U: ‹mod_restriction (get_all_init_clss U) (snd U')› and
atms_U_U': ‹atms_of_mm (get_all_init_clss U) = atms_of_mm (snd U')›
using U_U' confl unfolding enum_mod_restriction_st_clss_after_def by (cases U'; auto; fail)+
have alien_U: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)›
using ‹twl_struct_invs U›
unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
have mod_restriction_H: ‹M ⊨ DECO_clause (get_trail U)›
if
total: ‹total_over_m M (set_mset (snd U'))› and
consistent: ‹consistent_interp M› and
M_tr: ‹M ⊨ {#- lit_of x. x ∈# mset (get_trail U)#}› and
M_U': ‹M ⊨m snd U'›
for M
proof (rule ccontr)
assume ‹¬?thesis›
moreover have tot_tr: ‹total_over_m M {DECO_clause (get_trail U)}›
using alien_U total atms_U_U' unfolding cdcl⇩W_restart_mset.no_strange_atm_def
apply (auto simp: twl_st image_iff total_over_m_alt_def lits_of_def
dest!: atms_of_DECO_clauseD(1))
apply (metis atms_of_s_def contra_subsetD image_iff in_atms_of_s_decomp)+
done
ultimately have ‹M ⊨s CNot (DECO_clause (get_trail U))›
by (simp add: total_not_true_cls_true_clss_CNot)
moreover have ‹M ⊨sm get_all_init_clss U›
using mod_U total consistent M_U' unfolding mod_restriction_def
by blast
moreover have ‹total_over_m M (set_mset (get_all_init_clss U))›
using total atms_U_U' by (simp add: total_over_m_def)
moreover have ‹total_over_m M (unmark_l (trail (state⇩W_of U)))›
using alien_U tot_tr total atms_U_U' unfolding cdcl⇩W_restart_mset.no_strange_atm_def
apply (auto simp: total_over_m_alt_def
twl_st dest: atms_of_DECO_clauseD)
by (metis atms_of_uminus_lit_atm_of_lit_of atms_of_uminus_lit_of lits_of_def
set_mset_mset subsetCE total total_over_m_def total_over_set_def)
ultimately have ‹M ⊨s unmark_l (trail (state⇩W_of U))›
using 2 total consistent tot_tr unfolding true_clss_clss_def
by auto
then show False
using M_tr tot_tr consistent
by (auto simp: true_clss_def twl_st true_cls_def consistent_interp_def)
qed
have ‹mod_restriction (get_all_init_clss U) (snd U')›
using U_U' confl unfolding enum_mod_restriction_st_clss_after_def
by auto
moreover have ‹M ⊨ {#- lit_of x. x ∈# mset (get_trail U)#}›
if ‹M ⊨ DECO_clause (get_trail U)› for M
by (rule true_cls_mono_set_mset[OF _ that]) (auto simp: DECO_clause_def)
ultimately have mod_rest_U:
‹mod_restriction (add_mset (DECO_clause (get_trail U)) (get_all_init_clss U))
(add_mset {#- lit_of x. x ∈# mset (get_trail U)#} (snd U'))›
using 2
by (auto simp: mod_restriction_def twl_st mod_restriction_H)
have ‹(next_model_filtered P) (negate_model_and_add U')
((negate_model_and_add (Some (map lit_of (get_trail U)), snd U')))›
using confl U_U'
apply (cases U'; cases ‹fst U'›)
apply (auto simp: enum_mod_restriction_st_clss_after_def lits_of_def
eq_commute[of _ ‹mset _›] next_model_filtered.simps
intro!: exI[of _ ‹map lit_of (get_trail U)›]
dest: mset_eq_setD)
defer
apply (metis list.set_map mset_eq_setD mset_map)
using next_mod_U by (auto dest: mod_restriction_next_modelD)
then have ‹(next_model_filtered P)⇧*⇧* (None, snd M)
((negate_model_and_add (Some (map lit_of (get_trail U)), snd U')))›
using st_M_U' by simp
moreover {
have ‹mod_restriction (add_mset {#} (get_all_init_clss W))
(add_mset {#- lit_of x. x ∈# mset (get_trail W)#}
(add_mset {#- lit_of x. x ∈# mset (get_trail U)#} (snd U')))›
if
confl: ‹get_conflict W = None› and
count_dec: ‹count_decided (get_trail W) = 0›
apply (rule final_level0_add_empty_clause[OF that])
using ‹cdcl_twl_enum_inv W ∧ final_twl_state W ∧ cdcl_twl_stgy⇧*⇧* V W ∧
(W, U) ∈ R› mod_rest_U init_clss_WW_V[OF st final] U_U' atms_U_U' alien_U
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto dest: atms_of_DECO_clauseD(2) simp: twl_st lits_of_def)
(auto simp: image_image atms_of_def)
then have W: ‹(W, (negate_model_and_add (Some (map lit_of (get_trail U)), snd U')))
∈ enum_mod_restriction_st_clss_after›
using confl init_clss_WW_V[OF st final] twl_enum alien_U atms_U_U' confl
apply (auto simp: enum_mod_restriction_st_clss_after_def lits_of_def
cdcl_twl_enum_inv_def mod_rest_U
dest: atms_of_DECO_clauseD)
defer
apply (smt U atms_of_def cdcl_twl_enum_inv_def cdcl_twl_stgy_final_twl_stateE contra_subsetD
lits_of_def rtranclp.intros(1) set_image_mset set_mset_mset)
done
} note W = this
moreover have ‹get_conflict W = None ⟹ 0 < count_decided (get_trail W) ⟹
next_model (map lit_of (get_trail W))
(add_mset {#- lit_of x. x ∈# mset (get_trail U)#} (snd U'))›
using W next_mod[OF st] final confl unfolding enum_mod_restriction_st_clss_after_def
by (auto simp: mod_restriction_def next_model.simps lits_of_def)
moreover have ‹get_conflict W = None ⟹ count_decided (get_trail W) = 0 ⟹
next_model (map lit_of (get_trail W))
(add_mset {#- lit_of x. x ∈# mset (get_trail U)#} (snd U'))›
using W next_mod[OF st] final confl unfolding enum_mod_restriction_st_clss_after_def
apply (subst (asm)(2) mod_restriction_def)
by (auto simp: mod_restriction_def next_model.simps lits_of_def)
moreover have ‹get_conflict W ≠ None ⟹
unsatisfiable (set_mset (add_mset {#- lit_of x. x ∈# mset (get_trail U)#} (snd U')))›
using W not_none_unsat[OF st] final confl mod_rest_U unfolding enum_mod_restriction_st_clss_after_def
by (auto simp: lits_of_def dest: mod_restriction_satisfiable_iff
split: if_splits)
ultimately have ?I
using final next_mod[OF st]
unfolding I_def
apply -
apply (rule exI[of _ ‹(negate_model_and_add (Some (map lit_of (get_trail U)), snd U'))›])
using confl
by (auto simp: lits_of_def)
} note I = this
note H and I
} note H = this(1,2) and I = this(3)
then show ?conc_run
by (auto simp add: conclusive_TWL_run_def)
show ?I if ‹?Q W›
using I that
by (auto simp: I_def)
qed
have neg_neg[simp]: ‹negate_model_and_add (negate_model_and_add M) = negate_model_and_add M›
by (cases M; cases ‹fst M›; auto)
have [simp]: ‹(T, a, b) ∈ enum_model_st_direct ⟹ (T, None, b) ∈ enum_mod_restriction_st_clss_after›
for a b
unfolding enum_model_st_direct_def enum_mod_restriction_st_clss_after_def
cdcl_twl_enum_inv_def
by (auto intro!: final_level0_add_empty_clause simp: cdcl_twl_enum_inv_def)
have I_T: ‹I T›
unfolding I_def
apply (rule exI[of _ ‹(None, snd M)›])
unfolding neg_neg
apply (intro conjI)
subgoal
using T by (cases M) auto
subgoal by (auto simp: enum_mod_restriction_st_clss_after_def cdcl_twl_enum_inv_def
enum_model_st_def enum_model_st_direct_def)
subgoal by (auto simp: enum_mod_restriction_st_clss_after_def cdcl_twl_enum_inv_def
enum_model_st_def enum_model_st_direct_def)
subgoal using T by (auto simp: enum_mod_restriction_st_clss_after_def cdcl_twl_enum_inv_def
enum_model_st_def enum_model_st_direct_def)
subgoal using T by (auto simp: enum_mod_restriction_st_clss_after_def cdcl_twl_enum_inv_def
enum_model_st_def enum_model_st_direct_def)
subgoal using T by (auto simp: enum_mod_restriction_st_clss_after_def cdcl_twl_enum_inv_def
enum_model_st_def enum_model_st_direct_def)
done
have final: ‹?Spec s›
if
I: ‹I s› and
cond: ‹¬ (?Cond s)› and
enum: ‹cdcl_twl_enum_inv s›
for s
proof -
obtain x where
sx: ‹(s, x) ∈ enum_mod_restriction_st_clss_after› and
st': ‹(next_model_filtered P)⇧*⇧* (None, snd M) (None, snd (negate_model_and_add x))› and
st: ‹(next_model_filtered P)⇧*⇧* (None, snd M) (negate_model_and_add x)› and
final: ‹final_twl_state s› and
nm: ‹get_conflict s = None ⟹ next_model (map lit_of (get_trail s)) (snd x)› and
unsat: ‹get_conflict s ≠ None ⟹ unsatisfiable (set_mset (snd x))›
using I unfolding I_def by meson
let ?x = ‹if get_conflict s = None
then (Some (map lit_of (get_trail s)), snd x)
else (None, snd x)›
let ?y = ‹negate_model_and_add ?x›
have step: ‹(next_model_filtered P) (None, snd (negate_model_and_add x)) ?y›
if ‹get_conflict s = None› and ‹P (lits_of_l (get_trail s))›
using cond that sx final nm unfolding enum_mod_restriction_st_clss_after_def
enum_model_st_def
by (cases x; cases ‹fst x›)
(auto simp: next_model_filtered.simps lits_of_def
conclusive_TWL_run_def conc_fun_RES
intro!: exI[of _ ‹map lit_of (get_trail s)›])
moreover have step: ‹(next_model_filtered P)⇧*⇧* (negate_model_and_add x) ?y›
if ‹get_conflict s ≠ None›
using cond that sx unfolding enum_mod_restriction_st_clss_after_def
enum_model_st_def
by (cases x; cases ‹fst x›)
(auto simp: next_model_filtered.simps lits_of_def)
moreover have step: ‹(next_model_filtered P) (negate_model_and_add x) ?y ∨
(negate_model_and_add x) = ?y›
if ‹get_conflict s = None› and ‹¬P (lits_of_l (get_trail s))›
using cond that sx nm unfolding enum_mod_restriction_st_clss_after_def
enum_model_st_def
apply (cases x; cases ‹fst x›)
by (auto simp: next_model_filtered.simps lits_of_def
conclusive_TWL_run_def conc_fun_RES
intro!: exI[of _ ‹map lit_of (get_trail s)›])
ultimately have st: ‹(next_model_filtered P)⇧*⇧* (None, snd M) ?y›
using st st' by force
have 1: ‹(s, ?x) ∈ enum_mod_restriction_st_clss_after›
if ‹count_decided (get_trail s) ≠ 0 ∨ get_conflict s ≠ None ∨ P (lit_of ` set (get_trail s))›
using sx cond nm that unfolding enum_mod_restriction_st_clss_after_def
enum_model_st_def
by (cases x; cases ‹fst x›) (auto simp: lits_of_def)
have unsat': ‹unsatisfiable (set_mset (add_mset {#- lit_of x. x ∈# mset (get_trail s)#} (snd x)))›
if ‹get_conflict s = None› and ‹count_decided (get_trail s) = 0› and
‹¬P (lit_of ` set (get_trail s))›
apply (rule final_level0_add_empty_clause_unsat)
using cond that sx nm enum unfolding enum_mod_restriction_st_clss_after_def
enum_model_st_def apply -
by (cases x; cases ‹fst x›)
(force simp: next_model_filtered.simps lits_of_def)+
have ‹no_step (next_model_filtered P) ?y›
apply (rule unsat_no_step_next_model_filtered')
apply (cases x; cases ‹fst x›)
using cond unsat nm unsat' that
by (auto simp: lits_of_def)
then have 2: ‹full (next_model_filtered P) (None, snd M) ?y›
using st that unfolding full_def by blast
have "1b": ‹count_decided (get_trail s) = 0 ⟹
¬ P (lit_of ` set (get_trail s)) ⟹
get_conflict s = None ⟹
(s, None, snd x) ∈ enum_mod_restriction_st_clss_after›
using that cond unsat nm unsat' sx
unfolding enum_mod_restriction_st_clss_after_def
by (cases x; cases ‹fst x›) auto
show ?thesis
apply (rule exI[of _ ‹?y›])
using 1 "1b" 2 cond by (auto simp: lits_of_def)
qed
show ?thesis
apply (refine_vcg WHILEIT_rule_stronger_inv[where R=‹R› and I' = I] conc_run)
subgoal by (rule wf)
subgoal
using T S unfolding enum_model_st_direct_def enum_mod_restriction_st_clss_def
cdcl_twl_enum_inv_def
by auto
subgoal by (rule I_T)
apply assumption
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal for U V W by (rule inv_I)
subgoal by fast
subgoal by (rule final)
done
qed
have H1: ‹(if get_conflict Sb = None
then RETURN
(if count_decided (get_trail Sb) = 0
then P (lits_of_l (get_trail Sb)) else True)
else RETURN False)
≤ ⇓ bool_rel (RETURN (fst x' ≠ None))›
if
‹case y of (M, N) ⇒ M = None› and
‹(Sb, x') ∈ ?Res› and
‹x' ∈ Collect (full (next_model_filtered P) (None, snd Sa))›
for x x' Sa Sb S y
using that
by (auto simp: enum_mod_restriction_st_clss_after_def enum_model_st_def
enum_mod_restriction_st_clss_def lits_of_def split: if_splits)
show ?thesis
supply if_splits[split]
unfolding cdcl_twl_enum_def
apply (intro frefI nres_relI)
apply (subst next_model_filtered_nres_alt_def)
subgoal by auto
apply (refine_vcg conclusive_run)
unfolding conc_fun_SPEC
apply (rule loop; assumption)
apply (rule H1; assumption)
done
qed
end
end