theory Watched_Literals_Algorithm
imports
WB_More_Refinement
Watched_Literals_Transition_System
begin
section ‹First Refinement: Deterministic Rule Application›
subsection ‹Unit Propagation Loops›
definition set_conflicting :: ‹'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st› where
‹set_conflicting = (λC (M, N, U, D, NE, UE, WS, Q). (M, N, U, Some (clause C), NE, UE, {#}, {#}))›
definition propagate_lit :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st› where
‹propagate_lit = (λL' C (M, N, U, D, NE, UE, WS, Q).
(Propagated L' (clause C) # M, N, U, D, NE, UE, WS, add_mset (-L') Q))›
definition update_clauseS :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st nres› where
‹update_clauseS = (λL C (M, N, U, D, NE, UE, WS, Q). do {
K ← SPEC (λL. L ∈# unwatched C ∧ -L ∉ lits_of_l M);
if K ∈ lits_of_l M
then RETURN (M, N, U, D, NE, UE, WS, Q)
else do {
(N', U') ← SPEC (λ(N', U'). update_clauses (N, U) C L K (N', U'));
RETURN (M, N', U', D, NE, UE, WS, Q)
}
})›
definition unit_propagation_inner_loop_body :: ‹'v literal ⇒ 'v twl_cls ⇒
'v twl_st ⇒ 'v twl_st nres› where
‹unit_propagation_inner_loop_body = (λL C S. do {
do {
bL' ← SPEC (λK. K ∈# clause C);
if bL' ∈ lits_of_l (get_trail S)
then RETURN S
else do {
L' ← SPEC (λK. K ∈# watched C - {#L#});
ASSERT (watched C = {#L, L'#});
if L' ∈ lits_of_l (get_trail S)
then RETURN S
else
if ∀L ∈# unwatched C. -L ∈ lits_of_l (get_trail S)
then
if -L' ∈ lits_of_l (get_trail S)
then do {RETURN (set_conflicting C S)}
else do {RETURN (propagate_lit L' C S)}
else do {
update_clauseS L C S
}
}
}
})
›
definition unit_propagation_inner_loop :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹unit_propagation_inner_loop S⇩0 = do {
n ← SPEC(λ_::nat. True);
(S, _) ← WHILE⇩T⇗λ(S, n). twl_struct_invs S ∧ twl_stgy_invs S ∧ cdcl_twl_cp⇧*⇧* S⇩0 S ∧
(clauses_to_update S ≠ {#} ∨ n > 0 ⟶ get_conflict S = None)⇖
(λ(S, n). clauses_to_update S ≠ {#} ∨ n > 0)
(λ(S, n). do {
b ← SPEC(λb. (b ⟶ n > 0) ∧ (¬b ⟶ clauses_to_update S ≠ {#}));
if ¬b then do {
ASSERT(clauses_to_update S ≠ {#});
(L, C) ← SPEC (λC. C ∈# clauses_to_update S);
let S' = set_clauses_to_update (clauses_to_update S - {#(L, C)#}) S;
T ← unit_propagation_inner_loop_body L C S';
RETURN (T, if get_conflict T = None then n else 0)
} else do { ⌦‹This branch allows us to do skip some clauses.›
RETURN (S, n - 1)
}
})
(S⇩0, n);
RETURN S
}
›
lemma unit_propagation_inner_loop_body:
fixes S :: ‹'v twl_st›
assumes
‹clauses_to_update S ≠ {#}› and
x_WS: ‹(L, C) ∈# clauses_to_update S› and
inv: ‹twl_struct_invs S› and
inv_s: ‹twl_stgy_invs S› and
confl: ‹get_conflict S = None›
shows
‹unit_propagation_inner_loop_body L C
(set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)
≤ (SPEC (λT'. twl_struct_invs T' ∧ twl_stgy_invs T' ∧ cdcl_twl_cp⇧*⇧* S T' ∧
(T', S) ∈ measure (size ∘ clauses_to_update)))› (is ?spec) and
‹nofail (unit_propagation_inner_loop_body L C
(set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S))› (is ?fail)
proof -
obtain M N U D NE UE WS Q where
S: ‹S = (M, N, U, D, NE, UE, WS, Q)›
by (cases S) auto
have ‹C ∈# N + U› and struct: ‹struct_wf_twl_cls C› and L_C: ‹L ∈# watched C›
using inv multi_member_split[OF x_WS]
unfolding twl_struct_invs_def twl_st_inv.simps S
by force+
show ?fail
unfolding unit_propagation_inner_loop_body_def Let_def S
by (cases C) (use struct L_C in ‹auto simp: refine_pw_simps S size_2_iff update_clauseS_def›)
note [[goals_limit=15]]
show ?spec
using assms unfolding unit_propagation_inner_loop_body_def update_clause.simps
proof (refine_vcg; (unfold prod.inject clauses_to_update.simps set_clauses_to_update.simps
ball_simps)?; clarify?; (unfold triv_forall_equality)?)
fix L' :: ‹'v literal›
assume
‹clauses_to_update S ≠ {#}› and
WS: ‹(L, C) ∈# clauses_to_update S› and
twl_inv: ‹twl_struct_invs S›
have ‹C ∈# N + U› and struct: ‹struct_wf_twl_cls C› and L_C: ‹L ∈# watched C›
using twl_inv WS unfolding twl_struct_invs_def twl_st_inv.simps S by (auto; fail)+
define WS' where ‹WS' = WS - {#(L, C)#}›
have WS_WS': ‹WS = add_mset (L, C) WS'›
using WS unfolding WS'_def S by auto
have D: ‹D = None›
using confl S by auto
let ?S' = ‹(M, N, U, None, NE, UE, add_mset (L, C) WS', Q)›
let ?T = ‹(set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)›
let ?T' = ‹(M, N, U, None, NE, UE, WS', Q)›
{
fix K'
assume
K': ‹K' ∈# clause C› and
L': ‹K' ∈ lits_of_l (get_trail ?T)›
have ‹cdcl_twl_cp ?S' ?T'›
by (rule cdcl_twl_cp.delete_from_working) (use L' K' S in simp_all)
then have cdcl: ‹cdcl_twl_cp S ?T›
using L' D by (simp add: S WS_WS')
show ‹twl_struct_invs ?T›
using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)
show ‹twl_stgy_invs ?T›
using cdcl inv_s inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
show ‹cdcl_twl_cp⇧*⇧* S ?T›
using D WS_WS' cdcl by auto
show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
by (simp add: WS'_def[symmetric] WS_WS' S)
}
assume L': ‹L' ∈# remove1_mset L (watched C)›
show watched: ‹watched C = {#L, L'#}›
by (cases C) (use struct L_C L' in ‹auto simp: size_2_iff›)
then have L_C': ‹L ∈# clause C› and L'_C': ‹L' ∈# clause C›
by (cases C; auto; fail)+
{
assume L': ‹L' ∈ lits_of_l (get_trail ?T)›
have ‹cdcl_twl_cp ?S' ?T'›
by (rule cdcl_twl_cp.delete_from_working) (use L' L'_C' watched S in simp_all)
then have cdcl: ‹cdcl_twl_cp S ?T›
using L' watched D by (simp add: S WS_WS')
show ‹twl_struct_invs ?T›
using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)
show ‹twl_stgy_invs ?T›
using cdcl inv_s inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
show ‹cdcl_twl_cp⇧*⇧* S ?T›
using D WS_WS' cdcl by auto
show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
by (simp add: WS'_def[symmetric] WS_WS' S)
}
let ?M = ‹get_trail ?T›
assume L': ‹L' ∉ lits_of_l ?M›
{
{
assume unwatched: ‹∀L∈#unwatched C. - L ∈ lits_of_l ?M›
{
let ?T' = ‹(M, N, U, Some (clause C), NE, UE, {#}, {#})›
let ?T = ‹set_conflicting C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)›
assume uL': ‹-L' ∈ lits_of_l ?M›
have cdcl: ‹cdcl_twl_cp ?S' ?T'›
by (rule cdcl_twl_cp.conflict) (use uL' L' watched unwatched S in simp_all)
then have cdcl: ‹cdcl_twl_cp S ?T›
using uL' L' watched unwatched by (simp add: set_conflicting_def WS_WS' S D)
show ‹twl_struct_invs ?T›
using cdcl inv D unfolding WS_WS'
by (force intro: cdcl_twl_cp_twl_struct_invs)
show ‹twl_stgy_invs ?T›
using cdcl inv inv_s D unfolding WS_WS'
by (force intro: cdcl_twl_cp_twl_stgy_invs)
show ‹cdcl_twl_cp⇧*⇧* S ?T›
using D WS_WS' cdcl S by auto
show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
by (simp add: S WS'_def[symmetric] WS_WS' set_conflicting_def)
}
{
let ?S = ‹(M, N, U, D, NE, UE, WS, Q)›
let ?T' = ‹(Propagated L' (clause C) # M, N, U, None, NE, UE, WS', add_mset (- L') Q)›
let ?S' = ‹(M, N, U, None, NE, UE, add_mset (L, C) WS', Q)›
let ?T = ‹propagate_lit L' C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)›
assume uL': ‹- L' ∉ lits_of_l ?M›
have undef: ‹undefined_lit M L'›
using uL' L' by (auto simp: S defined_lit_map lits_of_def atm_of_eq_atm_of)
have cdcl: ‹cdcl_twl_cp ?S' ?T'›
by (rule cdcl_twl_cp.propagate) (use uL' L' undef watched unwatched D S in simp_all)
then have cdcl: ‹cdcl_twl_cp S ?T›
using uL' L' undef watched unwatched D S WS_WS' by (simp add: propagate_lit_def)
show ‹twl_struct_invs ?T›
using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)
show ‹cdcl_twl_cp⇧*⇧* S ?T›
using cdcl D WS_WS' by force
show ‹twl_stgy_invs ?T›
using cdcl inv inv_s D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
by (simp add: WS'_def[symmetric] WS_WS' S propagate_lit_def)
}
}
fix La
{
let ?S = ‹(M, N, U, D, NE, UE, WS, Q)›
let ?S' = ‹(M, N, U, None, NE, UE, add_mset (L, C) WS', Q)›
let ?T = ‹set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S›
fix K M' N' U' D' WS'' NE' UE' Q' N'' U''
have ‹update_clauseS L C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)
≤ SPEC (λS'. twl_struct_invs S' ∧ twl_stgy_invs S' ∧ cdcl_twl_cp⇧*⇧* S S' ∧
(S', S) ∈ measure (size ∘ clauses_to_update))› (is ?upd)
apply (rewrite at ‹set_clauses_to_update _ ⌑› S)
apply (rewrite at ‹clauses_to_update ⌑› S)
unfolding update_clauseS_def clauses_to_update.simps set_clauses_to_update.simps
apply clarify
proof refine_vcg
fix x xa a b
assume K: ‹x ∈# unwatched C ∧ - x ∉ lits_of_l M›
have uL: ‹- L ∈ lits_of_l M›
using inv unfolding twl_struct_invs_def S WS_WS' by auto
{
let ?T = ‹(M, N, U, D, NE, UE, remove1_mset (L, C) WS, Q)›
let ?T' = ‹(M, N, U, None, NE, UE, WS', Q)›
assume ‹x ∈ lits_of_l M›
have uL: ‹- L ∈ lits_of_l M›
using inv unfolding twl_struct_invs_def S WS_WS' by auto
have ‹L ∈# clause C› ‹x ∈# clause C›
using watched K by (cases C; simp; fail)+
have ‹cdcl_twl_cp ?S' ?T'›
by (rule cdcl_twl_cp.delete_from_working[OF ‹x ∈# clause C› ‹x ∈ lits_of_l M›])
then have cdcl: ‹cdcl_twl_cp S ?T›
by (auto simp: S D WS_WS')
show ‹twl_struct_invs ?T›
using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)
have uL: ‹- L ∈ lits_of_l M›
using inv unfolding twl_struct_invs_def S WS_WS' by auto
show ‹twl_stgy_invs ?T›
using cdcl inv inv_s D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
show ‹cdcl_twl_cp⇧*⇧* S ?T›
using D WS_WS' cdcl by auto
show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
by (simp add: WS'_def[symmetric] WS_WS' S)
}
assume
update: ‹case xa of (N', U') ⇒ update_clauses (N, U) C L x (N', U')› and
[simp]: ‹xa = (a, b)›
let ?T' = ‹(M, a, b, None, NE, UE, WS', Q)›
let ?T = ‹(M, a, b, D, NE, UE, remove1_mset (L, C) WS, Q)›
have ‹cdcl_twl_cp ?S' ?T'›
by (rule cdcl_twl_cp.update_clause)
(use uL L' K update watched S in ‹simp_all add: true_annot_iff_decided_or_true_lit›)
then have cdcl: ‹cdcl_twl_cp S ?T›
by (auto simp: S D WS_WS')
show ‹twl_struct_invs ?T›
using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)
have uL: ‹- L ∈ lits_of_l M›
using inv unfolding twl_struct_invs_def S WS_WS' by auto
show ‹twl_stgy_invs ?T›
using cdcl inv inv_s D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
show ‹cdcl_twl_cp⇧*⇧* S ?T›
using D WS_WS' cdcl by auto
show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
by (simp add: WS'_def[symmetric] WS_WS' S)
qed
moreover assume ‹¬?upd›
ultimately show ‹- La ∈
lits_of_l (get_trail (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S))›
by fast
}
}
qed
qed
declare unit_propagation_inner_loop_body(1)[THEN order_trans, refine_vcg]
lemma unit_propagation_inner_loop:
assumes ‹twl_struct_invs S› and inv: ‹twl_stgy_invs S› and ‹get_conflict S = None›
shows ‹unit_propagation_inner_loop S ≤ SPEC (λS'. twl_struct_invs S' ∧ twl_stgy_invs S' ∧
cdcl_twl_cp⇧*⇧* S S' ∧ clauses_to_update S' = {#})›
unfolding unit_propagation_inner_loop_def
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(S, n). (size o clauses_to_update) S + n)›])
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms 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 add: twl_struct_invs_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
declare unit_propagation_inner_loop[THEN order_trans, refine_vcg]
definition unit_propagation_outer_loop :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹unit_propagation_outer_loop S⇩0 =
WHILE⇩T⇗λS. twl_struct_invs S ∧ twl_stgy_invs S ∧ cdcl_twl_cp⇧*⇧* S⇩0 S ∧ clauses_to_update S = {#}⇖
(λS. literals_to_update S ≠ {#})
(λS. do {
L ← SPEC (λL. L ∈# literals_to_update S);
let S' = set_clauses_to_update {#(L, C)|C ∈# get_clauses S. L ∈# watched C#}
(set_literals_to_update (literals_to_update S - {#L#}) S);
ASSERT(cdcl_twl_cp S S');
unit_propagation_inner_loop S'
})
S⇩0
›
abbreviation unit_propagation_outer_loop_spec where
‹unit_propagation_outer_loop_spec S S' ≡ twl_struct_invs S' ∧ cdcl_twl_cp⇧*⇧* S S' ∧
literals_to_update S' = {#} ∧ (∀S'a. ¬ cdcl_twl_cp S' S'a) ∧ twl_stgy_invs S'›
lemma unit_propagation_outer_loop:
assumes ‹twl_struct_invs S› and ‹clauses_to_update S = {#}› and confl: ‹get_conflict S = None› and
‹twl_stgy_invs S›
shows ‹unit_propagation_outer_loop S ≤ SPEC (λS'. twl_struct_invs S' ∧ cdcl_twl_cp⇧*⇧* S S' ∧
literals_to_update S' = {#} ∧ no_step cdcl_twl_cp S' ∧ twl_stgy_invs S')›
proof -
have assert_twl_cp: ‹cdcl_twl_cp T
(set_clauses_to_update (Pair L `# {#Ca ∈# get_clauses T. L ∈# watched Ca#})
(set_literals_to_update (remove1_mset L (literals_to_update T)) T))› (is ?twl) and
assert_twl_struct_invs:
‹twl_struct_invs (set_clauses_to_update (Pair L `# {#Ca ∈# get_clauses T. L ∈# watched Ca#})
(set_literals_to_update (remove1_mset L (literals_to_update T)) T))›
(is ‹twl_struct_invs ?T'›) and
assert_stgy_invs:
‹twl_stgy_invs (set_clauses_to_update (Pair L `# {#Ca ∈# get_clauses T. L ∈# watched Ca#})
(set_literals_to_update (remove1_mset L (literals_to_update T)) T))› (is ?stgy)
if
p: ‹literals_to_update T ≠ {#}› and
L_T: ‹L ∈# literals_to_update T› and
invs: ‹twl_struct_invs T ∧ twl_stgy_invs T ∧cdcl_twl_cp⇧*⇧* S T ∧ clauses_to_update T = {#}›
for L T
proof -
from that have
p: ‹literals_to_update T ≠ {#}› and
L_T: ‹L ∈# literals_to_update T› and
struct_invs: ‹twl_struct_invs T› and
‹cdcl_twl_cp⇧*⇧* S T› and
w_q: ‹clauses_to_update T = {#}›
by fast+
have ‹get_conflict T = None›
using w_q p invs unfolding twl_struct_invs_def by auto
then obtain M N U NE UE Q where
T: ‹T = (M, N, U, None, NE, UE, {#}, Q)›
using w_q p by (cases T) auto
define Q' where ‹Q' = remove1_mset L Q›
have Q: ‹Q = add_mset L Q'›
using L_T unfolding Q'_def T by auto
show twl: ?twl
unfolding T set_clauses_to_update.simps set_literals_to_update.simps literals_to_update.simps Q'_def[symmetric]
unfolding Q get_clauses.simps
by (rule cdcl_twl_cp.pop)
then show ‹twl_struct_invs ?T'›
using cdcl_twl_cp_twl_struct_invs struct_invs by blast
then show ?stgy
using twl cdcl_twl_cp_twl_stgy_invs[OF twl] invs by blast
qed
show ?thesis
unfolding unit_propagation_outer_loop_def
apply (refine_vcg WHILEIT_rule[where R = ‹{(T, S). twl_struct_invs S ∧ cdcl_twl_cp⇧+⇧+ S T}›])
apply ((simp_all add: assms tranclp_wf_cdcl_twl_cp; fail)+)[6]
subgoal by (rule assert_twl_cp)
subgoal by (rule assert_twl_struct_invs)
subgoal by (rule assert_stgy_invs)
subgoal for S L
by (cases S)
(auto simp: twl_st twl_struct_invs_def)
subgoal by (simp; fail)
subgoal by auto
subgoal by auto
subgoal by simp
subgoal by auto
subgoal
by simp
subgoal by simp
subgoal by auto
subgoal by (auto simp: cdcl_twl_cp.simps)
subgoal by simp
done
qed
declare unit_propagation_outer_loop[THEN order_trans, refine_vcg]
subsection ‹Other Rules›
subsubsection ‹Decide›
definition find_unassigned_lit :: ‹'v twl_st ⇒ 'v literal option nres› where
‹find_unassigned_lit = (λS.
SPEC (λL.
(L ≠ None ⟶ undefined_lit (get_trail S) (the L) ∧
atm_of (the L) ∈ atms_of_mm (get_all_init_clss S)) ∧
(L = None ⟶ (∄L. undefined_lit (get_trail S) L ∧
atm_of L ∈ atms_of_mm (get_all_init_clss S)))))›
definition propagate_dec where
‹propagate_dec = (λL (M, N, U, D, NE, UE, WS, Q). (Decided L # M, N, U, D, NE, UE, WS, {#-L#}))›
definition decide_or_skip :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
‹decide_or_skip S = do {
L ← find_unassigned_lit S;
case L of
None ⇒ RETURN (True, S)
| Some L ⇒ RETURN (False, propagate_dec L S)
}
›
lemma decide_or_skip_spec:
assumes ‹clauses_to_update S = {#}› and ‹literals_to_update S = {#}› and ‹get_conflict S = None› and
twl: ‹twl_struct_invs S› and twl_s: ‹twl_stgy_invs S›
shows ‹decide_or_skip S ≤ SPEC(λ(brk, T). cdcl_twl_o⇧*⇧* S T ∧
get_conflict T = None ∧
no_step cdcl_twl_o T ∧ (brk ⟶ no_step cdcl_twl_stgy T) ∧ twl_struct_invs T ∧
twl_stgy_invs T ∧ clauses_to_update T = {#} ∧
(¬brk ⟶ literals_to_update T ≠ {#}) ∧
(¬no_step cdcl_twl_o S ⟶ cdcl_twl_o⇧+⇧+ S T))›
proof -
obtain M N U NE UE where S: ‹S = (M, N, U, None, NE, UE, {#}, {#})›
using assms by (cases S) auto
have atm_N_U:
‹atm_of L ∈ atms_of_mm (clauses N + NE)›
if U: ‹atm_of L ∈ atms_of_ms (clause ` set_mset U)› and
undef: ‹undefined_lit M L›
for L
proof -
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of S)› and unit: ‹entailed_clss_inv S›
using twl unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then show ?thesis
using that
by (auto simp: cdcl⇩W_restart_mset.no_strange_atm_def S cdcl⇩W_restart_mset_state image_Un)
qed
{
fix L
assume undef: ‹undefined_lit M L› and L: ‹atm_of L ∈ atms_of_mm (clauses N + NE)›
let ?T = ‹(Decided L # M, N, U, None, NE, UE, {#}, {#- L#})›
have o: ‹cdcl_twl_o (M, N, U, None, NE, UE, {#}, {#}) ?T›
by (rule cdcl_twl_o.decide) (use undef L in auto)
have twl': ‹twl_struct_invs ?T›
using S cdcl_twl_o_twl_struct_invs o twl by blast
have twl_s': ‹twl_stgy_invs ?T›
using S cdcl_twl_o_twl_stgy_invs o twl twl_s by blast
note o twl' twl_s'
} note H = this
show ?thesis
using assms unfolding S find_unassigned_lit_def propagate_dec_def decide_or_skip_def
apply (refine_vcg)
subgoal by fast
subgoal by blast
subgoal by (force simp: H elim!: cdcl_twl_oE cdcl_twl_stgyE cdcl_twl_cpE dest!: atm_N_U)
subgoal by (force elim!: cdcl_twl_oE cdcl_twl_stgyE cdcl_twl_cpE)
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by (auto elim!: cdcl_twl_oE)
subgoal using atm_N_U by (auto simp: cdcl_twl_o.simps decide)
subgoal by auto
subgoal by (auto elim!: cdcl_twl_oE)
subgoal by auto
subgoal using atm_N_U H by auto
subgoal using H atm_N_U by auto
subgoal by auto
subgoal by auto
subgoal using H atm_N_U by auto
done
qed
declare decide_or_skip_spec[THEN order_trans, refine_vcg]
subsubsection ‹Skip and Resolve Loop›
definition skip_and_resolve_loop_inv where
‹skip_and_resolve_loop_inv S⇩0 =
(λ(brk, S). cdcl_twl_o⇧*⇧* S⇩0 S ∧ twl_struct_invs S ∧ twl_stgy_invs S ∧
clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
get_conflict S ≠ None ∧
count_decided (get_trail S) ≠ 0 ∧
get_trail S ≠ [] ∧
get_conflict S ≠ Some {#} ∧
(brk ⟶ no_step cdcl⇩W_restart_mset.skip (state⇩W_of S) ∧
no_step cdcl⇩W_restart_mset.resolve (state⇩W_of S)))›
definition tl_state :: ‹'v twl_st ⇒ 'v twl_st› where
‹tl_state = (λ(M, N, U, D, NE, UE, WS, Q). (tl M, N, U, D, NE, UE, WS, Q))›
definition update_confl_tl :: ‹'v clause option ⇒ 'v twl_st ⇒ 'v twl_st› where
‹update_confl_tl = (λD (M, N, U, _, NE, UE, WS, Q). (tl M, N, U, D, NE, UE, WS, Q))›
definition skip_and_resolve_loop :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹skip_and_resolve_loop S⇩0 =
do {
(_, S) ←
WHILE⇩T⇗skip_and_resolve_loop_inv S⇩0⇖
(λ(uip, S). ¬uip ∧ ¬is_decided (hd (get_trail S)))
(λ(_, S).
do {
ASSERT(get_trail S ≠ []);
let D' = the (get_conflict S);
(L, C) ← SPEC(λ(L, C). Propagated L C = hd (get_trail S));
if -L ∉# D' then
do {RETURN (False, tl_state S)}
else
if get_maximum_level (get_trail S) (remove1_mset (-L) D') = count_decided (get_trail S)
then
do {RETURN (False, update_confl_tl (Some (cdcl⇩W_restart_mset.resolve_cls L D' C)) S)}
else
do {RETURN (True, S)}
}
)
(False, S⇩0);
RETURN S
}
›
lemma skip_and_resolve_loop_spec:
assumes struct_S: ‹twl_struct_invs S› and stgy_S: ‹twl_stgy_invs S› and
‹clauses_to_update S = {#}› and ‹literals_to_update S = {#}› and
‹get_conflict S ≠ None› and count_dec: ‹count_decided (get_trail S) > 0›
shows ‹skip_and_resolve_loop S ≤ SPEC(λT. cdcl_twl_o⇧*⇧* S T ∧ twl_struct_invs T ∧ twl_stgy_invs T ∧
no_step cdcl⇩W_restart_mset.skip (state⇩W_of T) ∧
no_step cdcl⇩W_restart_mset.resolve (state⇩W_of T) ∧
get_conflict T ≠ None ∧ clauses_to_update T = {#} ∧ literals_to_update T = {#})›
unfolding skip_and_resolve_loop_def
proof (refine_vcg WHILEIT_rule[where R = ‹measure (λ(brk, S). Suc (length (get_trail S) - If brk 1 0))›];
remove_dummy_vars)
show ‹wf (measure (λ(brk, S). Suc (length (get_trail S) - (if brk then 1 else 0))))›
by auto
have ‹get_trail S ⊨as CNot (the (get_conflict S))› if ‹get_conflict S ≠ None›
using assms that unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def by (cases S, auto simp add: cdcl⇩W_restart_mset_state)
then have ‹get_trail S ≠ []› if ‹get_conflict S ≠ Some {#}›
using that assms by auto
then show ‹skip_and_resolve_loop_inv S (False, S)›
using assms by (cases S) (auto simp: skip_and_resolve_loop_inv_def cdcl⇩W_restart_mset.skip.simps
cdcl⇩W_restart_mset.resolve.simps cdcl⇩W_restart_mset_state
twl_stgy_invs_def cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)
fix brk :: bool and T :: ‹'a twl_st›
assume
inv: ‹skip_and_resolve_loop_inv S (brk, T)› and
brk: ‹case (brk, T) of (brk, S) ⇒ ¬ brk ∧ ¬ is_decided (hd (get_trail S))›
have [simp]: ‹brk = False›
using brk by auto
show M_not_empty: ‹get_trail T ≠ []›
using brk inv unfolding skip_and_resolve_loop_inv_def by auto
fix L :: ‹'a literal› and C
assume
LC: ‹case (L, C) of (L, C) ⇒ Propagated L C = hd (get_trail T)›
obtain M N U D NE UE WS Q where
T: ‹T = (M, N, U, D, NE, UE, WS, Q)›
by (cases T)
obtain M' :: ‹('a, 'a clause) ann_lits› and D' where
M: ‹get_trail T = Propagated L C # M'› and WS: ‹WS = {#}› and Q: ‹Q = {#}› and D: ‹D = Some D'› and
st: ‹cdcl_twl_o⇧*⇧* S T› and twl: ‹twl_struct_invs T› and D': ‹D' ≠ {#}› and
twl_stgy_S: ‹twl_stgy_invs T› and
[simp]: ‹count_decided (tl M) > 0› ‹count_decided (tl M) ≠ 0›
using brk inv LC unfolding skip_and_resolve_loop_inv_def
by (cases ‹get_trail T›; cases ‹hd (get_trail T)›) (auto simp: T)
{
assume LD: ‹- L ∉# the (get_conflict T)›
let ?T = ‹tl_state T›
have o_S_T: ‹cdcl_twl_o T ?T›
using cdcl_twl_o.skip[of L ‹the D› C M' N U NE UE]
using LD D inv M unfolding skip_and_resolve_loop_inv_def T WS Q D by (auto simp: tl_state_def)
have st_T: ‹cdcl_twl_o⇧*⇧* S ?T›
using st o_S_T by auto
moreover have twl_T: ‹twl_struct_invs ?T›
using struct_S twl o_S_T cdcl_twl_o_twl_struct_invs by blast
moreover have twl_stgy_T: ‹twl_stgy_invs ?T›
using twl o_S_T stgy_S twl_stgy_S cdcl_twl_o_twl_stgy_invs by blast
moreover have ‹tl M ≠ []›
using twl_T D D' unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: cdcl⇩W_restart_mset_state T tl_state_def)
ultimately show ‹skip_and_resolve_loop_inv S (False, tl_state T)›
using WS Q D D' unfolding skip_and_resolve_loop_inv_def tl_state_def T
by simp
show ‹((False, ?T), (brk, T))
∈ measure (λ(brk, S). Suc (length (get_trail S) - (if brk then 1 else 0)))›
using M_not_empty by (simp add: tl_state_def T M)
}
{
assume
LD: ‹¬- L ∉# the (get_conflict T)› and
max: ‹get_maximum_level (get_trail T) (remove1_mset (- L) (the (get_conflict T)))
= count_decided (get_trail T)›
let ?D = ‹remove1_mset (- L) (the (get_conflict T)) ∪# remove1_mset L C›
let ?T = ‹update_confl_tl (Some ?D) T›
have count_dec: ‹count_decided M' = count_decided M›
using M unfolding T by auto
then have o_S_T: ‹cdcl_twl_o T ?T›
using cdcl_twl_o.resolve[of L ‹the D› C M' N U NE UE] LD D max M WS Q D
by (auto simp: T D update_confl_tl_def)
then have st_T: ‹cdcl_twl_o⇧*⇧* S ?T›
using st by auto
moreover have twl_T: ‹twl_struct_invs ?T›
using st_T twl o_S_T cdcl_twl_o_twl_struct_invs by blast
moreover have twl_stgy_T: ‹twl_stgy_invs ?T›
using twl o_S_T twl_stgy_S cdcl_twl_o_twl_stgy_invs by blast
moreover {
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of ?T)›
using twl_T D D' M unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
then have ‹tl M ⊨as CNot ?D›
using M unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp add: cdcl⇩W_restart_mset_state T update_confl_tl_def)
}
moreover have ‹get_conflict ?T ≠ Some {#}›
using twl_stgy_T count_dec unfolding twl_stgy_invs_def update_confl_tl_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def T
by (auto simp: trail.simps conflicting.simps)
ultimately show ‹skip_and_resolve_loop_inv S (False, ?T)›
using WS Q D D' unfolding skip_and_resolve_loop_inv_def
by (auto simp add: cdcl⇩W_restart_mset.skip.simps cdcl⇩W_restart_mset.resolve.simps
cdcl⇩W_restart_mset_state update_confl_tl_def T)
show ‹((False, ?T), (brk, T)) ∈ measure (λ(brk, S). Suc (length (get_trail S)
- (if brk then 1 else 0)))›
using M_not_empty by (simp add: T update_confl_tl_def)
}
{
assume
LD: ‹¬- L ∉# the (get_conflict T)› and
max: ‹get_maximum_level (get_trail T) (remove1_mset (- L) (the (get_conflict T)))
≠ count_decided (get_trail T)›
show ‹skip_and_resolve_loop_inv S (True, T)›
using inv max LD D M unfolding skip_and_resolve_loop_inv_def
by (auto simp add: cdcl⇩W_restart_mset.skip.simps cdcl⇩W_restart_mset.resolve.simps
cdcl⇩W_restart_mset_state T)
show ‹((True, T), (brk, T)) ∈ measure (λ(brk, S). Suc (length (get_trail S) - (if brk then 1 else 0)))›
using M_not_empty by simp
}
next
fix brk T U
assume
inv: ‹skip_and_resolve_loop_inv S (brk, T)› and
brk: ‹¬(case (brk, T) of (brk, S) ⇒ ¬ brk ∧ ¬ is_decided (hd (get_trail S)))›
show ‹cdcl_twl_o⇧*⇧* S T›
using inv by (auto simp add: skip_and_resolve_loop_inv_def)
{ assume ‹is_decided (hd (get_trail T))›
then have ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of T)› and
‹no_step cdcl⇩W_restart_mset.resolve (state⇩W_of T)›
by (cases T; auto simp add: cdcl⇩W_restart_mset.skip.simps
cdcl⇩W_restart_mset.resolve.simps cdcl⇩W_restart_mset_state)+
}
moreover
{ assume ‹brk›
then have ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of T)› and
‹no_step cdcl⇩W_restart_mset.resolve (state⇩W_of T)›
using inv by (auto simp: skip_and_resolve_loop_inv_def)
}
ultimately show ‹¬ cdcl⇩W_restart_mset.skip (state⇩W_of T) U› and
‹¬ cdcl⇩W_restart_mset.resolve (state⇩W_of T) U›
using brk unfolding prod.case by blast+
show ‹twl_struct_invs T›
using inv unfolding skip_and_resolve_loop_inv_def by auto
show ‹twl_stgy_invs T›
using inv unfolding skip_and_resolve_loop_inv_def by auto
show ‹get_conflict T ≠ None›
using inv by (auto simp: skip_and_resolve_loop_inv_def)
show ‹clauses_to_update T = {#}›
using inv by (auto simp: skip_and_resolve_loop_inv_def)
show ‹literals_to_update T = {#}›
using inv by (auto simp: skip_and_resolve_loop_inv_def)
qed
declare skip_and_resolve_loop_spec[THEN order_trans, refine_vcg]
subsubsection ‹Backtrack›
definition extract_shorter_conflict :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹extract_shorter_conflict = (λ(M, N, U, D, NE, UE, WS, Q).
SPEC(λS'. ∃D'. S' = (M, N, U, Some D', NE, UE, WS, Q) ∧
D' ⊆# the D ∧ clause `# (N + U) + NE + UE ⊨pm D' ∧ -lit_of (hd M) ∈# D'))›
fun equality_except_conflict :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
‹equality_except_conflict (M, N, U, D, NE, UE, WS, Q) (M', N', U', D', NE', UE', WS', Q') ⟷
M = M' ∧ N = N' ∧ U = U' ∧ NE = NE' ∧ UE = UE' ∧ WS = WS' ∧ Q = Q'›
lemma extract_shorter_conflict_alt_def:
‹extract_shorter_conflict S =
SPEC(λS'. ∃D'. equality_except_conflict S S' ∧ Some D' = get_conflict S' ∧
D' ⊆# the (get_conflict S) ∧ clause `# (get_clauses S) + unit_clss S ⊨pm D' ∧
-lit_of (hd (get_trail S)) ∈# D')›
unfolding extract_shorter_conflict_def
by (cases S) (auto simp: ac_simps)
definition reduce_trail_bt :: ‹'v literal ⇒ 'v twl_st ⇒ 'v twl_st nres› where
‹reduce_trail_bt = (λL (M, N, U, D', NE, UE, WS, Q). do {
M1 ← SPEC(λM1. ∃K M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (the D' - {#-L#}) + 1);
RETURN (M1, N, U, D', NE, UE, WS, Q)
})›
definition propagate_bt :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st ⇒ 'v twl_st› where
‹propagate_bt = (λL L' (M, N, U, D, NE, UE, WS, Q).
(Propagated (-L) (the D) # M, N, add_mset (TWL_Clause {#-L, L'#} (the D - {#-L, L'#})) U, None,
NE, UE, WS, {#L#}))›
definition propagate_unit_bt :: ‹'v literal ⇒ 'v twl_st ⇒ 'v twl_st› where
‹propagate_unit_bt = (λL (M, N, U, D, NE, UE, WS, Q).
(Propagated (-L) (the D) # M, N, U, None, NE, add_mset (the D) UE, WS, {#L#}))›
definition backtrack_inv where
‹backtrack_inv S ⟷ get_trail S ≠ [] ∧ get_conflict S ≠ Some {#}›
definition backtrack :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹backtrack S =
do {
ASSERT(backtrack_inv S);
let L = lit_of (hd (get_trail S));
S ← extract_shorter_conflict S;
S ← reduce_trail_bt L S;
if size (the (get_conflict S)) > 1
then do {
L' ← SPEC(λL'. L' ∈# the (get_conflict S) - {#-L#} ∧ L ≠ -L' ∧
get_level (get_trail S) L' = get_maximum_level (get_trail S) (the (get_conflict S) - {#-L#}));
RETURN (propagate_bt L L' S)
}
else do {
RETURN (propagate_unit_bt L S)
}
}
›
lemma
assumes confl: ‹get_conflict S ≠ None› ‹get_conflict S ≠ Some {#}› and
w_q: ‹clauses_to_update S = {#}› and p: ‹literals_to_update S = {#}› and
ns_s: ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of S)› and
ns_r: ‹no_step cdcl⇩W_restart_mset.resolve (state⇩W_of S)› and
twl_struct: ‹twl_struct_invs S› and twl_stgy: ‹twl_stgy_invs S›
shows
backtrack_spec:
‹backtrack S ≤ SPEC (λT. cdcl_twl_o S T ∧ get_conflict T = None ∧ no_step cdcl_twl_o T ∧
twl_struct_invs T ∧ twl_stgy_invs T ∧ clauses_to_update T = {#} ∧
literals_to_update T ≠ {#})› (is ?spec) and
backtrack_nofail:
‹nofail (backtrack S)› (is ?fail)
proof -
let ?S = ‹state⇩W_of S›
have inv_s: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant ?S› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ?S›
using twl_struct twl_stgy unfolding twl_struct_invs_def twl_stgy_invs_def by fast+
let ?D' = ‹the (conflicting ?S)›
have M_CNot_D': ‹trail ?S ⊨as CNot ?D'›
using inv confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (cases ‹conflicting ?S›; cases S) (auto simp: cdcl⇩W_restart_mset_state)
then have trail: ‹get_trail S ≠ []›
using confl unfolding true_annots_true_cls_def_iff_negation_in_model
by (cases S) (auto simp: cdcl⇩W_restart_mset_state)
show ?spec
unfolding backtrack_def extract_shorter_conflict_def reduce_trail_bt_def
proof (refine_vcg; remove_dummy_vars; clarify?)
show ‹backtrack_inv S›
using trail confl unfolding backtrack_inv_def by fast
fix M M1 M2 :: ‹('a, 'a clause) ann_lits› and
N U :: ‹'a twl_clss› and
D :: ‹'a clause option› and D' :: ‹'a clause› and NE UE :: ‹'a clauses› and
WS :: ‹'a clauses_to_update› and Q :: ‹'a lit_queue› and K K' :: ‹'a literal›
let ?S = ‹(M, N, U, D, NE, UE, WS, Q)›
let ?T = ‹(M, N, U, Some D', NE, UE, WS, Q)›
let ?U = ‹(M1, N, U, Some D', NE, UE, WS, Q)›
let ?MS = ‹get_trail ?S›
let ?MT = ‹get_trail ?T›
assume
S: ‹S = (M, N, U, D, NE, UE, WS, Q)› and
D'_D: ‹D' ⊆# the D› and
L_D': ‹-lit_of (hd M) ∈# D'› and
N_U_NE_UE_D': ‹clause `# (N + U) + NE + UE ⊨pm D'› and
decomp: ‹(Decided K' # M1, M2) ∈ set (get_all_ann_decomposition M)› and
lev_K': ‹get_level M K' = get_maximum_level M (remove1_mset (- lit_of (hd ?MS))
(the (Some D'))) + 1›
have WS: ‹WS = {#}› and Q: ‹Q = {#}›
using w_q p unfolding S by auto
have uL_D: ‹- lit_of (hd M) ∈# the D›
using decomp N_U_NE_UE_D' D'_D L_D' lev_K'
unfolding WS Q
by auto
have D_Some_the: ‹D = Some (the D)›
using confl S by auto
let ?S' = ‹state⇩W_of S›
have inv_s: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant ?S'› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ?S'›
using twl_struct twl_stgy unfolding twl_struct_invs_def twl_stgy_invs_def by fast+
have Q: ‹Q = {#}› and WS: ‹WS = {#}›
using w_q p unfolding S by auto
have M_CNot_D': ‹M ⊨as CNot D'›
using M_CNot_D' S D'_D
by (auto simp: cdcl⇩W_restart_mset_state true_annots_true_cls_def_iff_negation_in_model)
obtain L'' M' where M: ‹M = L'' # M'›
using trail S by (cases M) auto
have D'_empty: ‹D' ≠ {#}›
using L_D' by auto
have L'_D: ‹-lit_of L'' ∈# D'›
using L_D' by (auto simp: cdcl⇩W_restart_mset_state M)
have lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv ?S'›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast
then have n_d: ‹no_dup M› and dec: ‹backtrack_lvl ?S' = count_decided M›
using S unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: cdcl⇩W_restart_mset_state)
then have uL''_M: ‹-lit_of L'' ∉ lits_of_l M›
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l M)
have ‹get_maximum_level M (remove1_mset (-lit_of (hd M)) D') < count_decided M›
proof (cases L'')
case (Decided x1) note L'' = this(1)
have ‹distinct_mset (the D)›
using inv S confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto simp: cdcl⇩W_restart_mset_state)
then have ‹distinct_mset D'›
using D'_D by (blast intro: distinct_mset_mono)
then have ‹- x1 ∉# remove1_mset (- x1) D'›
using L'_D L'' D'_D by (auto dest: distinct_mem_diff_mset)
then have H: ‹∀x∈#remove1_mset (- lit_of (hd M)) D'. undefined_lit [L''] x›
using L'' M_CNot_D' uL''_M
by (fastforce simp: atms_of_def atm_of_eq_atm_of M true_annots_true_cls_def_iff_negation_in_model
dest: in_diffD)
have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) D') =
get_maximum_level M' (remove1_mset (- lit_of (hd M)) D')›
using get_maximum_level_skip_beginning[OF H, of M'] M
by auto
then show ?thesis
using count_decided_ge_get_maximum_level[of M' ‹remove1_mset (-lit_of (hd M)) D'›] M L''
by simp
next
case (Propagated L C) note L'' = this(1)
moreover {
have ‹∀L mark a b. a @ Propagated L mark # b = trail (state⇩W_of S) ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by blast
then have ‹L ∈# C›
by (force simp: S M cdcl⇩W_restart_mset_state L'') }
moreover have D_empty: ‹the D ≠ {#}›
using D'_D D'_empty by auto
moreover have ‹-L ∈# the D›
using ns_s L'' confl D_empty
by (force simp: cdcl⇩W_restart_mset.skip.simps S M cdcl⇩W_restart_mset_state)
ultimately have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D))
< count_decided M›
using ns_r confl count_decided_ge_get_maximum_level[of M
‹remove1_mset (-lit_of (hd M)) (the D)›]
by (fastforce simp add: cdcl⇩W_restart_mset.resolve.simps S M
cdcl⇩W_restart_mset_state)
moreover have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) D') ≤
get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D))›
by (rule get_maximum_level_mono) (use D'_D in ‹auto intro: mset_le_subtract›)
ultimately show ?thesis
by simp
qed
then have ‹∃K M1 M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (remove1_mset (-lit_of (hd M)) D') + 1›
using cdcl⇩W_restart_mset.backtrack_ex_decomp n_d
by (auto simp: cdcl⇩W_restart_mset_state S)
define i where ‹i = get_maximum_level M (remove1_mset (- lit_of (hd M)) D')›
let ?T = ‹(Propagated (-lit_of (hd M)) D' # M1, N,
add_mset (TWL_Clause {#-lit_of (hd M), K#} (D' - {#-lit_of (hd M), K#})) U,
None, NE, UE, WS, {#lit_of (hd M)#})›
let ?T' = ‹(Propagated (-lit_of (hd M)) D' # M1, N,
add_mset (TWL_Clause {#-lit_of (hd M), K#} (D' - {#-lit_of (hd M), K#})) U,
None, NE, UE, WS, {#- (-lit_of (hd M))#})›
have lev_D': ‹count_decided M = get_maximum_level (L'' # M') D'›
using count_decided_ge_get_maximum_level[of M D'] L'_D
get_maximum_level_ge_get_level[of ‹-lit_of L''› D' M] unfolding M
by (auto split: if_splits)
{
assume size_D: ‹1 < size (the (get_conflict ?U))› and
K_D: ‹K ∈# remove1_mset (- lit_of (hd ?MS)) (the (get_conflict ?U))› and
lev_K: ‹get_level (get_trail ?U) K = get_maximum_level (get_trail ?U)
(remove1_mset (- lit_of (hd (get_trail ?S))) (the (get_conflict ?U)))›
have ‹∀L' ∈# D'. -L' ∈ lits_of_l M›
using M_CNot_D' uL''_M
by (fastforce simp: atms_of_def atm_of_eq_atm_of M true_annots_true_cls_def_iff_negation_in_model
dest: in_diffD)
obtain c where c: ‹M = c @ M2 @ Decided K' # M1›
using get_all_ann_decomposition_exists_prepend[OF decomp] by blast
have ‹get_level M K' = Suc (count_decided M1)›
using n_d unfolding c by auto
then have i: ‹i = count_decided M1›
using lev_K' unfolding i_def by auto
have lev_M_M1: ‹∀L' ∈# D' - {#-lit_of (hd M)#}. get_level M L' = get_level M1 L'›
proof
fix L'
assume L': ‹L' ∈# D' - {#-lit_of (hd M)#}›
have ‹get_level M L' > count_decided M1› if ‹defined_lit (c @ M2 @ Decided K' # []) L'›
using get_level_skip_end[OF that, of M1] n_d that get_level_last_decided_ge[of ‹c @ M2›]
by (auto simp: c)
moreover have ‹get_level M L' ≤ i›
using get_maximum_level_ge_get_level[OF L', of M] unfolding i_def by auto
ultimately show ‹get_level M L' = get_level M1 L'›
using n_d c L' i by (cases ‹defined_lit (c @ M2 @ Decided K' # []) L'›) auto
qed
have ‹get_level M1 `# remove1_mset (- lit_of (hd M)) D' = get_level M `# remove1_mset (- lit_of (hd M)) D'›
by (rule image_mset_cong) (use lev_M_M1 in auto)
then have max_M1_M1_D: ‹get_maximum_level M1 (remove1_mset (- lit_of (hd M)) D') =
get_maximum_level M (remove1_mset (- lit_of (hd M)) D')›
unfolding get_maximum_level_def by argo
have ‹∃L' ∈# remove1_mset (-lit_of (hd M)) D'.
get_level M L' = get_maximum_level M (remove1_mset (- lit_of (hd M)) D')›
by (rule get_maximum_level_exists_lit_of_max_level)
(use size_D in ‹auto simp: remove1_mset_empty_iff›)
have D'_ne_single: ‹D' ≠ {#- lit_of (hd M)#}›
using size_D apply (cases D', simp)
apply (rename_tac L D'')
apply (case_tac D'')
by simp_all
have ‹cdcl_twl_o (M, N, U, D, NE, UE, WS, Q) ?T'›
unfolding Q WS option.sel list.sel
apply (subst D_Some_the)
apply (rule cdcl_twl_o.backtrack_nonunit_clause[of ‹-lit_of (hd M)› _ K' M1 M2 _ _ i])
subgoal using D'_D L_D' by blast
subgoal using L'_D decomp M by auto
subgoal using L'_D decomp M by auto
subgoal using L'_D M lev_D' by auto
subgoal using i lev_D' i_def by auto
subgoal using lev_K' i_def by auto
subgoal using D'_ne_single .
subgoal using D'_D .
subgoal using N_U_NE_UE_D' .
subgoal using L_D' .
subgoal using K_D by (auto dest: in_diffD)
subgoal using lev_K lev_M_M1 K_D by (simp add: i_def max_M1_M1_D)
done
then show cdcl: ‹cdcl_twl_o ?S (propagate_bt (lit_of (hd (get_trail ?S))) K ?U)›
unfolding WS Q by (auto simp: propagate_bt_def)
show ‹get_conflict (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) = None›
by (auto simp: propagate_bt_def)
show ‹twl_struct_invs (propagate_bt (lit_of (hd (get_trail ?S))) K ?U)›
using S cdcl cdcl_twl_o_twl_struct_invs twl_struct by (auto simp: propagate_bt_def)
show ‹twl_stgy_invs (propagate_bt (lit_of (hd (get_trail ?S))) K ?U)›
using S cdcl cdcl_twl_o_twl_stgy_invs twl_struct twl_stgy by blast
show ‹clauses_to_update (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) = {#}›
using WS by (auto simp: propagate_bt_def)
show False if ‹cdcl_twl_o (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) (an, ao, ap, aq, ar, as, at, b)›
for an ao ap aq ar as at b
using that by (auto simp: cdcl_twl_o.simps propagate_bt_def)
show False if ‹literals_to_update (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) = {#}›
using that by (auto simp: propagate_bt_def)
}
{
assume ‹¬ 1 < size (the (get_conflict ?U))›
then have D': ‹D' = {#-lit_of (hd M)#}›
using L'_D by (cases D') (auto simp: M)
let ?T = ‹(Propagated (- lit_of (hd M)) D' # M1, N, U, None, NE, add_mset D' UE, WS,
unmark (hd M))›
let ?T' = ‹(Propagated (- lit_of (hd M)) D' # M1, N, U, None, NE, add_mset D' UE, WS,
{#- (-lit_of (hd M))#})›
have i_0: ‹i = 0›
using i_def by (auto simp: D')
have ‹cdcl_twl_o (M, N, U, D, NE, UE, WS, Q) ?T'›
unfolding D' option.sel WS Q apply (subst D_Some_the)
apply (rule cdcl_twl_o.backtrack_unit_clause[of _ ‹the D› K' M1 M2 _ D' i])
subgoal using D'_D D' by auto
subgoal using decomp by simp
subgoal by (simp add: M)
subgoal using D' by (auto simp: get_maximum_level_add_mset)
subgoal using i_def by simp
subgoal using lev_K' i_def[symmetric] by auto
subgoal using D' .
subgoal using D'_D .
subgoal using N_U_NE_UE_D' .
done
then show cdcl: ‹cdcl_twl_o (M, N, U, D, NE, UE, WS, Q)
(propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U)›
by (auto simp add: propagate_unit_bt_def)
show ‹get_conflict (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) = None›
by (auto simp add: propagate_unit_bt_def)
show ‹twl_struct_invs (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U)›
using S cdcl cdcl_twl_o_twl_struct_invs twl_struct by blast
show ‹twl_stgy_invs (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U)›
using S cdcl cdcl_twl_o_twl_stgy_invs twl_struct twl_stgy by blast
show ‹clauses_to_update (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) = {#}›
using WS by (auto simp add: propagate_unit_bt_def)
show False if ‹literals_to_update (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) = {#}›
using that by (auto simp add: propagate_unit_bt_def)
fix an ao ap aq ar as at b
show False if ‹cdcl_twl_o (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) (an, ao, ap, aq, ar, as, at, b) ›
using that by (auto simp: cdcl_twl_o.simps propagate_unit_bt_def)
}
qed
then show ?fail
using nofail_simps(2) pwD1 by blast
qed
declare backtrack_spec[THEN order_trans, refine_vcg]
subsubsection ‹Full loop›
definition cdcl_twl_o_prog :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
‹cdcl_twl_o_prog S =
do {
if get_conflict S = None
then decide_or_skip S
else do {
if count_decided (get_trail S) > 0
then do {
T ← skip_and_resolve_loop S;
ASSERT(get_conflict T ≠ None ∧ get_conflict T ≠ Some {#});
U ← backtrack T;
RETURN (False, U)
}
else
RETURN (True, S)
}
}
›
setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper ("split_all_tac"))›
declare split_paired_All[simp del]
lemma skip_and_resolve_same_decision_level:
assumes ‹cdcl_twl_o S T› ‹get_conflict T ≠ None›
shows ‹count_decided (get_trail T) = count_decided (get_trail S)›
using assms by (induction rule: cdcl_twl_o.induct) auto
lemma skip_and_resolve_conflict_before:
assumes ‹cdcl_twl_o S T› ‹get_conflict T ≠ None›
shows ‹get_conflict S ≠ None›
using assms by (induction rule: cdcl_twl_o.induct) auto
lemma rtranclp_skip_and_resolve_same_decision_level:
‹cdcl_twl_o⇧*⇧* S T ⟹ get_conflict S ≠ None ⟹ get_conflict T ≠ None ⟹
count_decided (get_trail T) = count_decided (get_trail S)›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using skip_and_resolve_conflict_before[of T U]
by (auto simp: skip_and_resolve_same_decision_level)
done
lemma empty_conflict_lvl0:
‹twl_stgy_invs T ⟹ get_conflict T = Some {#} ⟹ count_decided (get_trail T) = 0›
by (cases T) (auto simp: twl_stgy_invs_def cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def
trail.simps conflicting.simps)
abbreviation cdcl_twl_o_prog_spec where
‹cdcl_twl_o_prog_spec S ≡ λ(brk, T).
cdcl_twl_o⇧*⇧* S T ∧
(get_conflict T ≠ None ⟶ count_decided (get_trail T) = 0) ∧
(¬ brk ⟶ get_conflict T = None ∧ (∀S'. ¬ cdcl_twl_o T S')) ∧
(brk ⟶ get_conflict T ≠ None ∨ (∀S'. ¬ cdcl_twl_stgy T S')) ∧
twl_struct_invs T ∧ twl_stgy_invs T ∧ clauses_to_update T = {#} ∧
(¬ brk ⟶ literals_to_update T ≠ {#}) ∧
(¬brk ⟶ ¬ (∀S'. ¬ cdcl_twl_o S S') ⟶ cdcl_twl_o⇧+⇧+ S T)›
lemma cdcl_twl_o_prog_spec:
assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
‹literals_to_update S = {#}› and
ns_cp: ‹no_step cdcl_twl_cp S›
shows
‹cdcl_twl_o_prog S ≤ SPEC(cdcl_twl_o_prog_spec S)›
(is ‹_ ≤ ?S›)
proof -
have [iff]: ‹¬ cdcl_twl_cp S T› for T
using ns_cp by fast
show ?thesis
unfolding cdcl_twl_o_prog_def
apply (refine_vcg decide_or_skip_spec[THEN order_trans]; remove_dummy_vars)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by simp
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal for T using assms empty_conflict_lvl0[of T]
rtranclp_skip_and_resolve_same_decision_level[of S T] by auto
subgoal using assms by auto
subgoal using assms by (auto elim!: cdcl_twl_oE simp: image_Un)
subgoal by (auto elim!: cdcl_twl_stgyE cdcl_twl_oE cdcl_twl_cpE)
subgoal by (auto simp: rtranclp_unfold elim!: cdcl_twl_oE)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal for uip by auto
done
qed
declare cdcl_twl_o_prog_spec[THEN order_trans, refine_vcg]
subsection ‹Full Strategy›
abbreviation cdcl_twl_stgy_prog_inv where
‹cdcl_twl_stgy_prog_inv S⇩0 ≡ λ(brk, T). twl_struct_invs T ∧ twl_stgy_invs T ∧
(brk ⟶ final_twl_state T) ∧ cdcl_twl_stgy⇧*⇧* S⇩0 T ∧ clauses_to_update T = {#} ∧
(¬brk ⟶ get_conflict T = None)›
definition cdcl_twl_stgy_prog :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹cdcl_twl_stgy_prog S⇩0 =
do {
do {
(brk, T) ← WHILE⇩T⇗cdcl_twl_stgy_prog_inv S⇩0⇖
(λ(brk, _). ¬brk)
(λ(brk, S).
do {
T ← unit_propagation_outer_loop S;
cdcl_twl_o_prog T
})
(False, S⇩0);
RETURN T
}
}
›
lemma wf_cdcl_twl_stgy_measure:
‹wf ({((brkT, T), (brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy⇧+⇧+ S T}
∪ {((brkT, T), (brkS, S)). S = T ∧ brkT ∧ ¬brkS})›
(is ‹wf (?TWL ∪ ?BOOL)›)
proof (rule wf_union_compatible)
show ‹wf ?TWL›
using tranclp_wf_cdcl_twl_stgy wf_snd_wf_pair by blast
show ‹?TWL O ?BOOL ⊆ ?TWL›
by auto
show ‹wf ?BOOL›
unfolding wf_iff_no_infinite_down_chain
proof clarify
fix f :: ‹nat ⇒ bool × 'b›
assume H: ‹∀i. (f (Suc i), f i) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
then have ‹(f (Suc 0), f 0) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}› and
‹(f (Suc 1), f 1) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
by presburger+
then show False
by auto
qed
qed
lemma cdcl_twl_o_final_twl_state:
assumes
‹cdcl_twl_stgy_prog_inv S (brk, T)› and
‹case (brk, T) of (brk, _) ⇒ ¬ brk› and
twl_o: ‹cdcl_twl_o_prog_spec U (True, V)›
shows ‹final_twl_state V›
proof -
have ‹cdcl_twl_o⇧*⇧* U V› and
confl_lev: ‹get_conflict V ≠ None ⟶ count_decided (get_trail V) = 0› and
final: ‹get_conflict V ≠ None ∨ (∀S'. ¬ cdcl_twl_stgy V S')›
‹twl_struct_invs V›
‹twl_stgy_invs V›
‹clauses_to_update V = {#}›
using twl_o
by force+
show ?thesis
unfolding final_twl_state_def
using confl_lev final
by auto
qed
lemma cdcl_twl_stgy_in_measure:
assumes
twl_stgy: ‹cdcl_twl_stgy_prog_inv S (brk0, T)› and
brk0: ‹case (brk0, T) of (brk, uu_) ⇒ ¬ brk› and
twl_o: ‹cdcl_twl_o_prog_spec U V› and
[simp]: ‹twl_struct_invs U› and
TU: ‹cdcl_twl_cp⇧*⇧* T U› and
‹literals_to_update U = {#}›
shows ‹(V, brk0, T)
∈ {((brkT, T), brkS, S). twl_struct_invs S ∧ cdcl_twl_stgy⇧+⇧+ S T} ∪
{((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
proof -
have [simp]: ‹twl_struct_invs T›
using twl_stgy by fast+
obtain brk' V' where
V: ‹V = (brk', V')›
by (cases V)
have
UV: ‹cdcl_twl_o⇧*⇧* U V'› and
‹(get_conflict V' ≠ None ⟶ count_decided (get_trail V') = 0)› and
not_brk': ‹(¬ brk' ⟶ get_conflict V' = None ∧ (∀S'. ¬ cdcl_twl_o V' S'))› and
brk': ‹(brk' ⟶ get_conflict V' ≠ None ∨ (∀S'. ¬ cdcl_twl_stgy V' S'))› and
[simp]: ‹twl_struct_invs V'›
‹twl_stgy_invs V'›
‹clauses_to_update V' = {#}› and
no_lits_to_upd: ‹(0 < count_decided (get_trail V') ⟶ ¬ brk' ⟶ literals_to_update V' ≠ {#})›
‹(¬brk' ⟶ ¬ (∀S'. ¬ cdcl_twl_o U S') ⟶ cdcl_twl_o⇧+⇧+ U V')›
using twl_o unfolding V
by fast+
have ‹cdcl_twl_stgy⇧*⇧* T V'›
using TU UV by (auto dest!: rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD)
then have TV_or_tranclp_TV: ‹T = V' ∨ cdcl_twl_stgy⇧+⇧+ T V'›
unfolding rtranclp_unfold by auto
have [simp]: ‹¬ cdcl_twl_stgy⇧+⇧+ V' V'›
using wf_not_refl[OF tranclp_wf_cdcl_twl_stgy, of V'] by auto
have [simp]: ‹brk0 = False›
using brk0 by auto
have ‹brk'› if ‹T = V'›
proof -
have ns_TV: ‹¬cdcl_twl_stgy⇧+⇧+ T V'›
using that[symmetric] wf_not_refl[OF tranclp_wf_cdcl_twl_stgy, of T] by auto
have ns_T_T: ‹¬cdcl_twl_o⇧+⇧+ T T›
using wf_not_refl[OF tranclp_wf_cdcl_twl_o, of T] by auto
have ‹T = U›
by (metis (no_types, hide_lams) TU UV ns_TV rtranclp_cdcl_twl_cp_stgyD
rtranclp_cdcl_twl_o_stgyD rtranclp_tranclp_tranclp rtranclp_unfold)
show ?thesis
using assms ‹literals_to_update U = {#}› unfolding V that[symmetric] ‹T = U›[symmetric]
by (auto simp: ns_T_T)
qed
then show ?thesis
using TV_or_tranclp_TV
unfolding V
by auto
qed
lemma cdcl_twl_o_prog_cdcl_twl_stgy:
assumes
twl_stgy: ‹cdcl_twl_stgy_prog_inv S (brk, S')› and
‹case (brk, S') of (brk, uu_) ⇒ ¬ brk› and
twl_o: ‹cdcl_twl_o_prog_spec T (brk', U)› and
‹twl_struct_invs T› and
cp: ‹cdcl_twl_cp⇧*⇧* S' T› and
‹literals_to_update T = {#}› and
‹∀S'. ¬ cdcl_twl_cp T S'› and
‹twl_stgy_invs T›
shows ‹cdcl_twl_stgy⇧*⇧* S U›
proof -
have ‹cdcl_twl_stgy⇧*⇧* S S'›
using twl_stgy by fast
moreover {
have ‹cdcl_twl_o⇧*⇧* T U›
using twl_o by fast
then have ‹cdcl_twl_stgy⇧*⇧* S' U›
using cp by (auto dest!: rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD)
}
ultimately show ?thesis by auto
qed
lemma cdcl_twl_stgy_prog_spec:
assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
‹get_conflict S = None›
shows
‹cdcl_twl_stgy_prog S ≤ conclusive_TWL_run S›
unfolding cdcl_twl_stgy_prog_def full_def conclusive_TWL_run_def
apply (refine_vcg WHILEIT_rule[where
R = ‹{((brkT, T), (brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy⇧+⇧+ S T} ∪
{((brkT, T), (brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
remove_dummy_vars)
subgoal using wf_cdcl_twl_stgy_measure .
subgoal using assms by simp
subgoal using assms by simp
subgoal using assms by simp
subgoal using assms by simp
subgoal using assms by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by (simp add: no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by (rule cdcl_twl_o_final_twl_state)
subgoal by (rule cdcl_twl_o_prog_cdcl_twl_stgy)
subgoal by simp
subgoal for brk0 T U brl V
by clarsimp
subgoal for brk0 T U V
by (rule cdcl_twl_stgy_in_measure)
subgoal by simp
subgoal by fast
done
definition cdcl_twl_stgy_prog_break :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹cdcl_twl_stgy_prog_break S⇩0 =
do {
b ← SPEC(λ_. True);
(b, brk, T) ← WHILE⇩T⇗λ(b, S). cdcl_twl_stgy_prog_inv S⇩0 S⇖
(λ(b, brk, _). b ∧ ¬brk)
(λ(_, brk, S). do {
T ← unit_propagation_outer_loop S;
T ← cdcl_twl_o_prog T;
b ← SPEC(λ_. True);
RETURN (b, T)
})
(b, False, S⇩0);
if brk then RETURN T
else ―‹finish iteration is required only›
cdcl_twl_stgy_prog T
}
›
lemma wf_cdcl_twl_stgy_measure_break:
‹wf ({((bT, brkT, T), (bS, brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy⇧+⇧+ S T} ∪
{((bT, brkT, T), (bS, brkS, S)). S = T ∧ brkT ∧ ¬brkS}
)›
(is ‹?wf ?R›)
proof -
have 1: ‹wf ({((brkT, T), brkS, S). twl_struct_invs S ∧ cdcl_twl_stgy⇧+⇧+ S T} ∪
{((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS})›
(is ‹wf ?S›)
by (rule wf_cdcl_twl_stgy_measure)
have ‹wf {((bT, T), (bS, S)). (T, S) ∈ ?S}›
apply (rule wf_snd_wf_pair)
apply (rule wf_subset)
apply (rule 1)
apply auto
done
then show ?thesis
apply (rule wf_subset)
apply auto
done
qed
lemma cdcl_twl_stgy_prog_break_spec:
assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
‹get_conflict S = None›
shows
‹cdcl_twl_stgy_prog_break S ≤ conclusive_TWL_run S›
unfolding cdcl_twl_stgy_prog_break_def full_def conclusive_TWL_run_def
apply (refine_vcg cdcl_twl_stgy_prog_spec[unfolded conclusive_TWL_run_def]
WHILEIT_rule[where
R = ‹{((bT, brkT, T), (bS, brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy⇧+⇧+ S T} ∪
{((bT, brkT, T), (bS, brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
remove_dummy_vars)
subgoal using wf_cdcl_twl_stgy_measure_break .
subgoal using assms by simp
subgoal using assms by simp
subgoal using assms by simp
subgoal using assms by simp
subgoal using assms by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by (simp add: no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal for x a aa ba xa x1a
by (rule cdcl_twl_o_final_twl_state[of S a aa ba]) simp_all
subgoal for x a aa ba xa x1a
by (rule cdcl_twl_o_prog_cdcl_twl_stgy[of S a aa ba xa x1a]) fast+
subgoal by simp
subgoal for brk0 T U brl V
by clarsimp
subgoal for x a aa ba xa xb
using cdcl_twl_stgy_in_measure[of S a aa ba xa] by fast
subgoal by simp
subgoal by fast
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal using assms by auto
done
end