theory Watched_Literals_Watch_List_Domain_Restart
imports Watched_Literals_Watch_List_Domain Watched_Literals_Watch_List_Restart
begin
lemma cdcl_twl_restart_get_all_init_clss:
assumes ‹cdcl_twl_restart S T›
shows ‹get_all_init_clss T = get_all_init_clss S›
using assms by (induction rule: cdcl_twl_restart.induct) auto
lemma rtranclp_cdcl_twl_restart_get_all_init_clss:
assumes ‹cdcl_twl_restart⇧*⇧* S T›
shows ‹get_all_init_clss T = get_all_init_clss S›
using assms by (induction rule: rtranclp_induct) (auto simp: cdcl_twl_restart_get_all_init_clss)
text ‹As we have a specialised version of \<^term>‹correct_watching›, we defined a special version for
the inclusion of the domain:›
definition all_init_lits :: ‹(nat, 'v literal list × bool) fmap ⇒ 'v literal multiset multiset ⇒
'v literal multiset› where
‹all_init_lits S NUE = all_lits_of_mm ((λC. mset C) `# init_clss_lf S + NUE)›
abbreviation all_init_lits_st :: ‹'v twl_st_wl ⇒ 'v literal multiset› where
‹all_init_lits_st S ≡ all_init_lits (get_clauses_wl S) (get_unit_init_clss_wl S)›
definition all_init_atms :: ‹_ ⇒ _ ⇒ 'v multiset› where
‹all_init_atms N NUE = atm_of `# all_init_lits N NUE›
declare all_init_atms_def[symmetric, simp]
lemma all_init_atms_alt_def:
‹set_mset (all_init_atms N NE) = atms_of_mm (mset `# init_clss_lf N) ∪ atms_of_mm NE›
unfolding all_init_atms_def all_init_lits_def
by (auto simp: in_all_lits_of_mm_ain_atms_of_iff
all_lits_of_mm_def atms_of_ms_def image_UN
atms_of_def
dest!: multi_member_split[of ‹(_, _)› ‹ran_m N›]
dest: multi_member_split atm_of_lit_in_atms_of
simp del: set_image_mset)
abbreviation all_init_atms_st :: ‹'v twl_st_wl ⇒ 'v multiset› where
‹all_init_atms_st S ≡ atm_of `# all_init_lits_st S›
definition blits_in_ℒ⇩i⇩n' :: ‹nat twl_st_wl ⇒ bool› where
‹blits_in_ℒ⇩i⇩n' S ⟷
(∀L ∈# ℒ⇩a⇩l⇩l (all_init_atms_st S). ∀(i, K, b) ∈ set (watched_by S L). K ∈# ℒ⇩a⇩l⇩l (all_init_atms_st S))›
definition literals_are_ℒ⇩i⇩n' :: ‹nat multiset ⇒ nat twl_st_wl ⇒ bool› where
‹literals_are_ℒ⇩i⇩n' 𝒜 S ≡
is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S)
+ get_unit_init_clss_wl S)) ∧
blits_in_ℒ⇩i⇩n' S›
lemma ℒ⇩a⇩l⇩l_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ set_mset (ℒ⇩a⇩l⇩l 𝒜) = set_mset (ℒ⇩a⇩l⇩l ℬ)›
unfolding literals_are_ℒ⇩i⇩n'_def blits_in_ℒ⇩i⇩n'_def ℒ⇩a⇩l⇩l_def
by auto
lemma literals_are_ℒ⇩i⇩n'_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ literals_are_ℒ⇩i⇩n' 𝒜 S = literals_are_ℒ⇩i⇩n' ℬ S›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding literals_are_ℒ⇩i⇩n'_def blits_in_ℒ⇩i⇩n'_def is_ℒ⇩a⇩l⇩l_def
by auto
lemma literals_are_ℒ⇩i⇩n_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ literals_are_ℒ⇩i⇩n 𝒜 S = literals_are_ℒ⇩i⇩n ℬ S›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_def
by auto
lemma literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff:
assumes
Sx: ‹(S, x) ∈ state_wl_l None› and
x_xa: ‹(x, xa) ∈ twl_st_l None› and
struct_invs: ‹twl_struct_invs xa›
shows
‹literals_are_ℒ⇩i⇩n' 𝒜 S ⟷ literals_are_ℒ⇩i⇩n 𝒜 S› (is ?A)
‹literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S ⟷ literals_are_ℒ⇩i⇩n (all_atms_st S) S› (is ?B)
‹set_mset (all_init_atms_st S) = set_mset (all_atms_st S)› (is ?C)
proof -
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of xa)›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have ‹⋀L. L ∈ atm_of ` lits_of_l (get_trail_wl S) ⟹ L ∈ atms_of_ms
((λx. mset (fst x)) ` {a. a ∈# ran_m (get_clauses_wl S) ∧ snd a}) ∪
atms_of_mm (get_unit_init_clss_wl S)› and
alien_learned: ‹atms_of_mm (learned_clss (state⇩W_of xa))
⊆ atms_of_mm (init_clss (state⇩W_of xa))›
using Sx x_xa unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp add: twl_st twl_st_l twl_st_wl)
have all_init_lits_alt_def: ‹all_lits_of_mm
({#mset (fst C). C ∈# init_clss_l (get_clauses_wl S)#} +
get_unit_init_clss_wl S) = all_init_lits_st S›
by (auto simp: all_init_lits_def)
have H: ‹set_mset
(all_lits_of_mm
({#mset (fst C). C ∈# init_clss_l (get_clauses_wl S)#} +
get_unit_init_clss_wl S)) = set_mset
(all_lits_of_mm
({#mset (fst C). C ∈# ran_m (get_clauses_wl S)#} +
get_unit_clauses_wl S))›
apply (subst (2) all_clss_l_ran_m[symmetric])
using alien_learned Sx x_xa
unfolding image_mset_union all_lits_of_mm_union
by (auto simp: in_all_lits_of_mm_ain_atms_of_iff get_unit_clauses_wl_alt_def
twl_st twl_st_l twl_st_wl get_learned_clss_wl_def)
show A: ‹literals_are_ℒ⇩i⇩n' 𝒜 S ⟷ literals_are_ℒ⇩i⇩n 𝒜 S› for 𝒜
proof -
have ‹is_ℒ⇩a⇩l⇩l 𝒜
(all_lits_of_mm
({#mset C. C ∈# init_clss_lf (get_clauses_wl S)#} +
get_unit_init_clss_wl S)) ⟷
is_ℒ⇩a⇩l⇩l 𝒜
(all_lits_of_mm
({#mset (fst C). C ∈# ran_m (get_clauses_wl S)#} +
get_unit_clauses_wl S))›
using H unfolding is_ℒ⇩a⇩l⇩l_def by auto
moreover have ‹set_mset 𝒜' = set_mset (ℒ⇩a⇩l⇩l 𝒜)› if ‹is_ℒ⇩a⇩l⇩l 𝒜 𝒜'› for 𝒜'
unfolding that[unfolded is_ℒ⇩a⇩l⇩l_def]
by auto
moreover have ‹set_mset (ℒ⇩a⇩l⇩l (all_atms_st S)) = set_mset (ℒ⇩a⇩l⇩l 𝒜)› if ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_st S)›
for 𝒜 S
unfolding that[unfolded is_ℒ⇩a⇩l⇩l_def]
using ‹set_mset (ℒ⇩a⇩l⇩l 𝒜) = set_mset (all_lits_st S)› is_ℒ⇩a⇩l⇩l_all_lits_st_ℒ⇩a⇩l⇩l(1) that by blast
moreover have ‹set_mset (ℒ⇩a⇩l⇩l (all_init_atms_st S)) = set_mset (ℒ⇩a⇩l⇩l 𝒜)›
if ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_init_lits_st S)› for 𝒜 S
unfolding that[unfolded is_ℒ⇩a⇩l⇩l_def]
by (metis ‹set_mset (ℒ⇩a⇩l⇩l 𝒜) = set_mset (all_init_lits_st S)› all_init_lits_def is_ℒ⇩a⇩l⇩l_ℒ⇩a⇩l⇩l_rewrite that)
ultimately show ?thesis
using Sx x_xa unfolding cdcl⇩W_restart_mset.no_strange_atm_def literals_are_ℒ⇩i⇩n'_def
literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def
all_init_lits_def[symmetric] all_lits_def[symmetric] all_init_lits_alt_def
by (auto 5 5 dest: multi_member_split)
qed
show C: ?C
unfolding cdcl⇩W_restart_mset.no_strange_atm_def literals_are_ℒ⇩i⇩n'_def
literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def all_atms_def all_init_atms_def
all_init_lits_def all_lits_def all_init_lits_alt_def
by (auto simp: H)
show ?B
by (subst A)
(rule literals_are_ℒ⇩i⇩n_cong[OF C])
qed
lemma GC_remap_all_init_atmsD:
‹GC_remap (N, x, m) (N', x', m') ⟹ all_init_atms N NE + all_init_atms m NE = all_init_atms N' NE + all_init_atms m' NE›
by (induction rule: GC_remap.induct[split_format(complete)])
(auto simp: all_init_atms_def all_init_lits_def init_clss_l_fmdrop_if
init_clss_l_fmupd_if image_mset_remove1_mset_if
simp del: all_init_atms_def[symmetric]
simp flip: image_mset_union all_lits_of_mm_add_mset all_lits_of_mm_union)
lemma rtranclp_GC_remap_all_init_atmsD:
‹GC_remap⇧*⇧* (N, x, m) (N', x', m') ⟹ all_init_atms N NE + all_init_atms m NE = all_init_atms N' NE + all_init_atms m' NE›
by (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
(auto dest: GC_remap_all_init_atmsD)
lemma rtranclp_GC_remap_all_init_atms:
‹GC_remap⇧*⇧* (x1a, Map.empty, fmempty) (fmempty, m, x1ad) ⟹ all_init_atms x1ad NE = all_init_atms x1a NE›
by (auto dest!: rtranclp_GC_remap_all_init_atmsD[of _ _ _ _ _ _ NE])
lemma GC_remap_all_init_lits:
‹GC_remap (N, m, new) (N', m', new') ⟹ all_init_lits N NE + all_init_lits new NE = all_init_lits N' NE + all_init_lits new' NE›
by (induction rule: GC_remap.induct[split_format(complete)])
(case_tac ‹irred N C› ; auto simp: all_init_lits_def init_clss_l_fmupd_if image_mset_remove1_mset_if
simp flip: all_lits_of_mm_union)
lemma rtranclp_GC_remap_all_init_lits:
‹GC_remap⇧*⇧* (N, m, new) (N', m', new') ⟹ all_init_lits N NE + all_init_lits new NE = all_init_lits N' NE + all_init_lits new' NE›
by (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
(auto dest: GC_remap_all_init_lits)
lemma cdcl_twl_restart_is_ℒ⇩a⇩l⇩l:
assumes
ST: ‹cdcl_twl_restart⇧*⇧* S T› and
struct_invs_S: ‹twl_struct_invs S› and
L: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (clauses (get_clauses S) + unit_clss S))›
shows ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (clauses (get_clauses T) + unit_clss T))›
proof -
have ‹twl_struct_invs T›
using rtranclp_cdcl_twl_restart_twl_struct_invs[OF ST struct_invs_S] .
then have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T)›
unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have ‹?thesis ⟷ is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (get_all_init_clss T))›
unfolding cdcl⇩W_restart_mset.no_strange_atm_def is_ℒ⇩a⇩l⇩l_alt_def
by (cases T)
(auto simp: cdcl⇩W_restart_mset_state)
moreover have ‹get_all_init_clss T = get_all_init_clss S›
using rtranclp_cdcl_twl_restart_get_all_init_clss[OF ST] .
moreover {
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of S)›
using struct_invs_S
unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (get_all_init_clss S))›
using L
unfolding cdcl⇩W_restart_mset.no_strange_atm_def is_ℒ⇩a⇩l⇩l_alt_def
by (cases S)
(auto simp: cdcl⇩W_restart_mset_state)
}
ultimately show ?thesis
by argo
qed
lemma cdcl_twl_restart_is_ℒ⇩a⇩l⇩l':
assumes
ST: ‹cdcl_twl_restart⇧*⇧* S T› and
struct_invs_S: ‹twl_struct_invs S› and
L: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (get_all_init_clss S))›
shows ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (get_all_init_clss T))›
proof -
have ‹twl_struct_invs T›
using rtranclp_cdcl_twl_restart_twl_struct_invs[OF ST struct_invs_S] .
then have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T)›
unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have ‹?thesis ⟷ is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm (get_all_init_clss T))›
unfolding cdcl⇩W_restart_mset.no_strange_atm_def is_ℒ⇩a⇩l⇩l_alt_def
by (cases T)
(auto simp: cdcl⇩W_restart_mset_state)
moreover have ‹get_all_init_clss T = get_all_init_clss S›
using rtranclp_cdcl_twl_restart_get_all_init_clss[OF ST] .
then show ?thesis
using L
by argo
qed
definition remove_all_annot_true_clause_imp_wl_D_inv
:: ‹nat twl_st_wl ⇒ _ ⇒ nat × nat twl_st_wl ⇒ bool›
where
‹remove_all_annot_true_clause_imp_wl_D_inv S xs = (λ(i, T).
remove_all_annot_true_clause_imp_wl_inv S xs (i, T) ∧
literals_are_ℒ⇩i⇩n' (all_init_atms_st T) T ∧
all_init_atms_st S = all_init_atms_st T)›
definition remove_all_annot_true_clause_imp_wl_D_pre
:: ‹nat multiset ⇒ nat literal ⇒ nat twl_st_wl ⇒ bool›
where
‹remove_all_annot_true_clause_imp_wl_D_pre 𝒜 L S ⟷ (L ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ literals_are_ℒ⇩i⇩n' 𝒜 S)›
definition remove_all_annot_true_clause_imp_wl_D
:: ‹nat literal ⇒ nat twl_st_wl ⇒ (nat twl_st_wl) nres›
where
‹remove_all_annot_true_clause_imp_wl_D = (λL S. do {
ASSERT(remove_all_annot_true_clause_imp_wl_D_pre (all_init_atms_st S)
L S);
let xs = get_watched_wl S L;
(_, T) ← WHILE⇩T⇗λ(i, T).
remove_all_annot_true_clause_imp_wl_D_inv S xs
(i, T)⇖
(λ(i, T). i < length xs)
(λ(i, T). do {
ASSERT(i < length xs);
let (C, _ , _) = xs ! i;
if C ∈# dom_m (get_clauses_wl T) ∧ length ((get_clauses_wl T) ∝ C) ≠ 2
then do {
T ← remove_all_annot_true_clause_one_imp_wl (C, T);
RETURN (i+1, T)
}
else
RETURN (i+1, T)
})
(0, S);
RETURN T
})›
lemma is_ℒ⇩a⇩l⇩l_init_itself[iff]:
‹is_ℒ⇩a⇩l⇩l (all_init_atms x1h x2h) (all_init_lits x1h x2h)›
unfolding is_ℒ⇩a⇩l⇩l_def
by (auto simp: all_init_lits_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
in_all_lits_of_mm_ain_atms_of_iff all_init_atms_def)
lemma literals_are_ℒ⇩i⇩n'_alt_def: ‹literals_are_ℒ⇩i⇩n' 𝒜 S ⟷
is_ℒ⇩a⇩l⇩l 𝒜 (all_init_lits (get_clauses_wl S) (get_unit_init_clss_wl S)) ∧
blits_in_ℒ⇩i⇩n' S›
unfolding literals_are_ℒ⇩i⇩n'_def all_init_lits_def
by auto
lemma remove_all_annot_true_clause_imp_wl_remove_all_annot_true_clause_imp:
‹(uncurry remove_all_annot_true_clause_imp_wl_D, uncurry remove_all_annot_true_clause_imp_wl) ∈
{(L, L'). L = L' ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜} ×⇩f {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' 𝒜 S ∧
𝒜 = all_init_atms_st S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' 𝒜 S}⟩nres_rel›
(is ‹_ ∈ _ →⇩f ⟨?R⟩nres_rel›)
proof -
have [refine0]:
‹remove_all_annot_true_clause_one_imp_wl (C, S) ≤
⇓ {(S', T). (S', T) ∈ ?R ∧ all_init_atms_st S' = all_init_atms_st S}
(remove_all_annot_true_clause_one_imp_wl (C', S'))›
if ‹(S, S') ∈ ?R› and ‹(C, C') ∈ Id›
for S S' C C'
using that unfolding remove_all_annot_true_clause_one_imp_def
by (cases S)
(fastforce simp: init_clss_l_fmdrop_irrelev init_clss_l_fmdrop
image_mset_remove1_mset_if all_init_lits_def
remove_all_annot_true_clause_one_imp_wl_def
drop_clause_add_move_init_def
literals_are_ℒ⇩i⇩n'_def
blits_in_ℒ⇩i⇩n'_def drop_clause_def
all_init_atms_def
dest!: multi_member_split[of _ ‹ℒ⇩a⇩l⇩l 𝒜›])
show ?thesis
supply [[goals_limit=1]]
unfolding uncurry_def remove_all_annot_true_clause_imp_wl_D_def
remove_all_annot_true_clause_imp_wl_def
apply (intro frefI nres_relI)
subgoal for x y
apply (refine_vcg
WHILEIT_refine[where R = ‹{((i, S), (i', S')). i = i' ∧ (S, S') ∈ Id ∧
literals_are_ℒ⇩i⇩n' 𝒜 S' ∧ all_init_atms_st (snd x) = all_init_atms_st S}›])
subgoal unfolding remove_all_annot_true_clause_imp_wl_D_pre_def
by (auto simp flip: all_init_atms_def)
subgoal by auto
subgoal
unfolding remove_all_annot_true_clause_imp_wl_D_inv_def all_init_atms_def
by (auto simp flip: all_atms_def simp: literals_are_ℒ⇩i⇩n'_alt_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal unfolding remove_all_annot_true_clause_imp_wl_D_inv_def literals_are_ℒ⇩i⇩n'_alt_def
blits_in_ℒ⇩i⇩n_def
by (auto simp flip: all_atms_def simp: blits_in_ℒ⇩i⇩n'_def)
subgoal by auto
subgoal by auto
subgoal unfolding remove_all_annot_true_clause_imp_wl_D_pre_def by auto
done
done
qed
definition remove_one_annot_true_clause_one_imp_wl_D_pre where
‹remove_one_annot_true_clause_one_imp_wl_D_pre i T ⟷
remove_one_annot_true_clause_one_imp_wl_pre i T ∧
literals_are_ℒ⇩i⇩n' (all_init_atms_st T) T›
definition remove_one_annot_true_clause_one_imp_wl_D
:: ‹nat ⇒ nat twl_st_wl ⇒ (nat × nat twl_st_wl) nres›
where
‹remove_one_annot_true_clause_one_imp_wl_D = (λi S. do {
ASSERT(remove_one_annot_true_clause_one_imp_wl_D_pre i S);
ASSERT(is_proped (rev (get_trail_wl S) ! i));
(L, C) ← SPEC(λ(L, C). (rev (get_trail_wl S))!i = Propagated L C);
ASSERT(Propagated L C ∈ set (get_trail_wl S));
ASSERT(atm_of L ∈# all_init_atms_st S);
if C = 0 then RETURN (i+1, S)
else do {
ASSERT(C ∈# dom_m (get_clauses_wl S));
T ← replace_annot_l L C S;
ASSERT(get_clauses_wl S = get_clauses_wl T);
T ← remove_and_add_cls_l C T;
― ‹\<^text>‹S ← remove_all_annot_true_clause_imp_wl L S;››
RETURN (i+1, T)
}
})›
lemma remove_one_annot_true_clause_one_imp_wl_pre_in_trail_in_all_init_atms_st:
assumes
inv: ‹remove_one_annot_true_clause_one_imp_wl_D_pre K S› and
LC_tr: ‹Propagated L C ∈ set (get_trail_wl S)›
shows ‹atm_of L ∈# all_init_atms_st S›
proof -
obtain x xa where
Sx: ‹(S, x) ∈ state_wl_l None› and
‹correct_watching'' S› and
‹twl_list_invs x› and
‹K < length (get_trail_l x)› and
‹twl_list_invs x› and
‹get_conflict_l x = None› and
‹clauses_to_update_l x = {#}› and
x_xa: ‹(x, xa) ∈ twl_st_l None› and
struct: ‹twl_struct_invs xa›
using inv
unfolding remove_one_annot_true_clause_one_imp_wl_pre_def
remove_one_annot_true_clause_one_imp_pre_def
remove_one_annot_true_clause_one_imp_wl_D_pre_def
by blast
have ‹L ∈ lits_of_l (trail (state⇩W_of xa))›
using LC_tr Sx x_xa
by (force simp: twl_st twl_st_l twl_st_wl lits_of_def)
moreover have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of xa)›
using struct unfolding twl_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
ultimately have ‹atm_of L ∈ atms_of_mm (init_clss (state⇩W_of xa))›
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: twl_st twl_st_l twl_st_wl)
then have ‹atm_of L ∈ atms_of_mm (mset `# (init_clss_lf (get_clauses_wl S)) +
get_unit_init_clss_wl S)›
using Sx x_xa
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: twl_st twl_st_l twl_st_wl)
then show ?thesis
by (auto simp: all_init_atms_alt_def)
qed
lemma remove_one_annot_true_clause_one_imp_wl_D_remove_one_annot_true_clause_one_imp_wl:
‹(uncurry remove_one_annot_true_clause_one_imp_wl_D,
uncurry remove_one_annot_true_clause_one_imp_wl) ∈
nat_rel ×⇩f {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} →⇩f
⟨nat_rel ×⇩f {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}⟩nres_rel›
(is ‹_ ∈ _ ×⇩f ?A →⇩f _›)
proof -
have [refine0]: ‹replace_annot_l L C S ≤
⇓ {(S', T'). (S', T') ∈ ?A ∧ get_clauses_wl S' = get_clauses_wl S} (replace_annot_l L' C' T')›
if ‹(L, L') ∈ Id› and ‹(S, T') ∈ ?A› and ‹(C, C') ∈ Id› for L L' S T' C C'
using that
by (cases S; cases T')
(fastforce simp: replace_annot_l_def state_wl_l_def
literals_are_ℒ⇩i⇩n'_def blits_in_ℒ⇩i⇩n'_def
intro: RES_refine)
have [simp]: ‹all_init_atms (fmdrop C' x1a) (add_mset (mset (x1a ∝ C')) x1c) =
all_init_atms x1a x1c›
if ‹irred x1a C'› and ‹C' ∈# dom_m x1a›
for C' x1a x1c
using that
by (auto simp: all_init_atms_def all_init_lits_def
image_mset_remove1_mset_if)
have [simp]: ‹all_init_atms (fmdrop C' x1a) x1c =
all_init_atms x1a x1c›
if ‹¬irred x1a C'›
for C' x1a x1c
using that
by (auto simp: all_init_atms_def all_init_lits_def
image_mset_remove1_mset_if)
have [refine0]: ‹remove_and_add_cls_l C S ≤⇓ ?A (remove_and_add_cls_l C' S')›
if ‹(C, C') ∈ Id› and ‹(S, S') ∈ ?A› and
‹C ∈# dom_m (get_clauses_wl S)›
for C C' S S'
using that unfolding remove_and_add_cls_l_def
by refine_rcg
(auto intro!: RES_refine simp: state_wl_l_def init_clss_l_fmdrop
literals_are_ℒ⇩i⇩n'_def blits_in_ℒ⇩i⇩n'_def image_mset_remove1_mset_if
init_clss_l_fmdrop_irrelev)
show ?thesis
supply [[goals_limit=1]]
unfolding uncurry_def remove_one_annot_true_clause_one_imp_wl_def
remove_one_annot_true_clause_one_imp_wl_D_def
apply (intro frefI nres_relI)
subgoal for x y
apply (refine_vcg
remove_all_annot_true_clause_imp_wl_remove_all_annot_true_clause_imp[
of ‹all_init_atms_st (snd x)›,
THEN fref_to_Down_curry])
subgoal unfolding remove_one_annot_true_clause_one_imp_wl_D_pre_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for K S K' S' LC LC' L C L' C'
by (rule remove_one_annot_true_clause_one_imp_wl_pre_in_trail_in_all_init_atms_st)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
done
qed
definition remove_one_annot_true_clause_imp_wl_D_inv where
‹remove_one_annot_true_clause_imp_wl_D_inv S = (λ(i, T).
remove_one_annot_true_clause_imp_wl_inv S (i, T) ∧
literals_are_ℒ⇩i⇩n' (all_init_atms_st T) T)›
definition remove_one_annot_true_clause_imp_wl_D :: ‹nat twl_st_wl ⇒ (nat twl_st_wl) nres›
where
‹remove_one_annot_true_clause_imp_wl_D = (λS. do {
k ← SPEC(λk. (∃M1 M2 K. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_wl S)) ∧
count_decided M1 = 0 ∧ k = length M1)
∨ (count_decided (get_trail_wl S) = 0 ∧ k = length (get_trail_wl S)));
(_, S) ← WHILE⇩T⇗remove_one_annot_true_clause_imp_wl_D_inv S⇖
(λ(i, S). i < k)
(λ(i, S). remove_one_annot_true_clause_one_imp_wl_D i S)
(0, S);
RETURN S
})›
lemma remove_one_annot_true_clause_imp_wl_D_remove_one_annot_true_clause_imp_wl:
‹(remove_one_annot_true_clause_imp_wl_D, remove_one_annot_true_clause_imp_wl) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}⟩nres_rel›
proof -
show ?thesis
unfolding uncurry_def remove_one_annot_true_clause_imp_wl_D_def
remove_one_annot_true_clause_imp_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
WHILEIT_refine[where R=‹nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧
literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}›]
remove_one_annot_true_clause_one_imp_wl_D_remove_one_annot_true_clause_one_imp_wl[THEN fref_to_Down_curry])
subgoal by auto
subgoal by auto
subgoal for S S' k k' T T'
by (cases T') (auto simp: remove_one_annot_true_clause_imp_wl_D_inv_def)
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
definition mark_to_delete_clauses_wl_D_pre where
‹mark_to_delete_clauses_wl_D_pre S ⟷
mark_to_delete_clauses_wl_pre S ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S›
definition mark_to_delete_clauses_wl_D_inv where
‹mark_to_delete_clauses_wl_D_inv = (λS xs0 (i, T, xs).
mark_to_delete_clauses_wl_inv S xs0 (i, T, xs) ∧
literals_are_ℒ⇩i⇩n' (all_init_atms_st T) T)›
definition mark_to_delete_clauses_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹mark_to_delete_clauses_wl_D = (λS. do {
ASSERT(mark_to_delete_clauses_wl_D_pre S);
xs ← collect_valid_indices_wl S;
l ← SPEC(λ_::nat. True);
(_, S, xs) ← WHILE⇩T⇗mark_to_delete_clauses_wl_D_inv S xs⇖
(λ(i, _, xs). i < length xs)
(λ(i, T, xs). do {
if(xs!i ∉# dom_m (get_clauses_wl T)) then RETURN (i, T, delete_index_and_swap xs i)
else do {
ASSERT(0 < length (get_clauses_wl T∝(xs!i)));
ASSERT(get_clauses_wl T∝(xs!i)!0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T));
can_del ← SPEC(λb. b ⟶
(Propagated (get_clauses_wl T∝(xs!i)!0) (xs!i) ∉ set (get_trail_wl T)) ∧
¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T∝(xs!i)) ≠ 2);
ASSERT(i < length xs);
if can_del
then
RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i)
else
RETURN (i+1, T, xs)
}
})
(l, S, xs);
RETURN S
})›
lemma mark_to_delete_clauses_wl_D_mark_to_delete_clauses_wl:
‹(mark_to_delete_clauses_wl_D, mark_to_delete_clauses_wl) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}⟩nres_rel›
proof -
have [refine0]: ‹collect_valid_indices_wl S ≤ ⇓ Id (collect_valid_indices_wl T)›
if ‹(S, T) ∈ Id› for S T
using that by auto
have [iff]: ‹(∀(x::bool) xa. P x xa) ⟷ (∀xa.( P True xa ∧ P False xa))› for P
by metis
have in_Lit: ‹get_clauses_wl T' ∝ (xs ! j) ! 0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T')›
if
‹(l, l') ∈ nat_rel› and
rel: ‹(st, st') ∈ nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} ×⇩r
Id› and
inv_x: ‹mark_to_delete_clauses_wl_D_inv S ys st› and
‹mark_to_delete_clauses_wl_inv S' ys' st'› and
dom: ‹¬ xs ! j ∉# dom_m (get_clauses_wl T')› and
‹¬ xs' ! i ∉# dom_m (get_clauses_wl T)› and
assert: ‹0 < length (get_clauses_wl T ∝ (xs' ! i))› and
st: ‹st' = (i, sT)› ‹sT = (T, xs)› ‹st = (j, sT')› ‹sT' = (T', xs')› and
le: ‹case st of (i, T, xs) ⇒ i < length xs› and
‹case st' of (i, S, xs') ⇒ i < length xs'› and
‹0 < length (get_clauses_wl T' ∝ (xs ! j))›
for S S' xs' l l' st st' i T j T' sT xs sT' ys ys'
proof -
have lits_T': ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st T') T'›
using inv_x unfolding mark_to_delete_clauses_wl_D_inv_def prod.simps st
by fast
have ‹literals_are_ℒ⇩i⇩n (all_init_atms_st T) T›
proof -
obtain x xa xb where
lits_T': ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st T') T'› and
Ta_x: ‹(S, x) ∈ state_wl_l None› and
Ta_y: ‹(T', xa) ∈ state_wl_l None› and
‹correct_watching' S› and
rem: ‹remove_one_annot_true_clause⇧*⇧* x xa› and
list: ‹twl_list_invs x› and
x_xb: ‹(x, xb) ∈ twl_st_l None› and
struct: ‹twl_struct_invs xb› and
confl: ‹get_conflict_l x = None› and
upd: ‹clauses_to_update_l x = {#}›
using inv_x unfolding mark_to_delete_clauses_wl_D_inv_def st prod.case
mark_to_delete_clauses_wl_inv_def mark_to_delete_clauses_l_inv_def
by blast
obtain y where
Ta_y': ‹(xa, y) ∈ twl_st_l None› and
struct': ‹twl_struct_invs y›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list confl upd x_xb
struct] by blast
have ‹literals_are_ℒ⇩i⇩n (all_init_atms_st T') T'›
by (rule literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(1)[THEN iffD1,
OF Ta_y Ta_y' struct' lits_T'])
then show ?thesis
using rel by (auto simp: st)
qed
then have ‹literals_are_in_ℒ⇩i⇩n (all_init_atms_st T') (mset (get_clauses_wl T' ∝ (xs ! j)))›
using literals_are_in_ℒ⇩i⇩n_nth[of ‹xs!i› ‹T›] rel dom
by (auto simp: st)
then show ?thesis
by (rule literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l) (use le assert rel dom in ‹auto simp: st›)
qed
have final_rel_del:
‹((j, mark_garbage_wl (xs ! j) T', delete_index_and_swap xs j),
i, mark_garbage_wl (xs' ! i) T, delete_index_and_swap xs' i)
∈ nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}×⇩r Id›
if
rel: ‹(st, st') ∈ nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st T) S} ×⇩r
Id› and
‹case st of (i, T, xs) ⇒ i < length xs› and
‹case st' of (i, S, xs') ⇒ i < length xs'› and
inv: ‹mark_to_delete_clauses_wl_D_inv S ys st› and
‹mark_to_delete_clauses_wl_inv S' ys' st'› and
st: ‹st' = (i, sT)› ‹sT = (T, xs)› ‹st = (j, sT')› ‹sT' = (T', xs')› and
dom: ‹¬ xs ! j ∉# dom_m (get_clauses_wl T')› and
‹¬ xs' ! i ∉# dom_m (get_clauses_wl T)› and
le: ‹0 < length (get_clauses_wl T ∝ (xs' ! i))› and
‹0 < length (get_clauses_wl T' ∝ (xs ! j))› and
‹get_clauses_wl T' ∝ (xs ! j) ! 0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T')› and
‹(can_del, can_del') ∈ bool_rel› and
can_del: ‹can_del
∈ {b. b ⟶
Propagated (get_clauses_wl T' ∝ (xs ! j) ! 0) (xs ! j)
∉ set (get_trail_wl T') ∧
¬ irred (get_clauses_wl T') (xs ! j)}› and
‹can_del'
∈ {b. b ⟶
Propagated (get_clauses_wl T ∝ (xs' ! i) ! 0) (xs' ! i)
∉ set (get_trail_wl T) ∧
¬ irred (get_clauses_wl T) (xs' ! i)}› and
i_le: ‹i < length xs'› and
‹j < length xs› and
[simp]: ‹can_del› and
[simp]: ‹can_del'›
for S S' xs xs' l l' st st' i T j T' can_del can_del' sT sT' ys ys'
proof -
have ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st (mark_garbage_wl (xs' ! i) T)) (mark_garbage_wl (xs' ! i) T)›
using can_del inv rel unfolding mark_to_delete_clauses_wl_D_inv_def st mark_garbage_wl_def
by (cases T)
(auto simp: literals_are_ℒ⇩i⇩n'_def init_clss_l_fmdrop_irrelev mset_take_mset_drop_mset'
blits_in_ℒ⇩i⇩n'_def all_init_lits_def)
then show ?thesis
using inv rel unfolding st
by auto
qed
show ?thesis
unfolding uncurry_def mark_to_delete_clauses_wl_D_def mark_to_delete_clauses_wl_def
collect_valid_indices_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
WHILEIT_refine[where
R = ‹nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} ×⇩r Id›])
subgoal
unfolding mark_to_delete_clauses_wl_D_pre_def by auto
subgoal by auto
subgoal for x y xs xsa l la xa x'
unfolding mark_to_delete_clauses_wl_D_inv_def by (cases x') auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S S' xs xs' l l' st st' i T j T'
by (rule in_Lit; assumption?) auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S S' xs xs' l l' st st' i T j T' can_del can_del'
by (rule final_rel_del; assumption?) auto
subgoal by auto
subgoal by auto
done
qed
definition mark_to_delete_clauses_wl_D_post where
‹mark_to_delete_clauses_wl_D_post S T ⟷
(mark_to_delete_clauses_wl_post S T ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S)›
definition cdcl_twl_full_restart_wl_prog_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹cdcl_twl_full_restart_wl_prog_D S = do {
― ‹\<^text>‹S ← remove_one_annot_true_clause_imp_wl_D S;››
ASSERT(mark_to_delete_clauses_wl_D_pre S);
T ← mark_to_delete_clauses_wl_D S;
ASSERT (mark_to_delete_clauses_wl_post S T);
RETURN T
}›
lemma cdcl_twl_full_restart_wl_prog_D_final_rel:
assumes
‹(S, Sa) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}› and
‹mark_to_delete_clauses_wl_D_pre S› and
‹(T, Ta) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}› and
post: ‹mark_to_delete_clauses_wl_post Sa Ta› and
‹mark_to_delete_clauses_wl_post S T›
shows ‹(T, Ta) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}›
proof -
have lits_T: ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st Ta) Ta› and T: ‹T = Ta›
using assms by auto
obtain x xa xb where
Sa_x: ‹(Sa, x) ∈ state_wl_l None› and
Ta_x: ‹(Ta, xa) ∈ state_wl_l None› and
corr_S: ‹correct_watching Sa› and
corr_T: ‹correct_watching Ta› and
x_xb: ‹(x, xb) ∈ twl_st_l None› and
rem: ‹remove_one_annot_true_clause⇧*⇧* x xa› and
list: ‹twl_list_invs x› and
struct: ‹twl_struct_invs xb› and
confl: ‹get_conflict_l x = None› and
upd: ‹clauses_to_update_l x = {#}›
using post unfolding mark_to_delete_clauses_wl_post_def mark_to_delete_clauses_l_post_def
by blast
obtain y where
‹cdcl_twl_restart_l⇧*⇧* x xa› and
Ta_y: ‹(xa, y) ∈ twl_st_l None› and
‹cdcl_twl_restart⇧*⇧* xb y› and
struct: ‹twl_struct_invs y›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list confl upd x_xb
struct]
by blast
have ‹literals_are_ℒ⇩i⇩n (all_atms_st Ta) Ta›
by (rule literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(2)[THEN iffD1,
OF Ta_x Ta_y struct lits_T])
then show ?thesis
using lits_T T by auto
qed
lemma mark_to_delete_clauses_wl_pre_lits':
‹(S, T) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} ⟹
mark_to_delete_clauses_wl_pre T ⟹ mark_to_delete_clauses_wl_D_pre S›
unfolding mark_to_delete_clauses_wl_D_pre_def mark_to_delete_clauses_wl_pre_def
apply normalize_goal+
apply (intro conjI)
subgoal for U
by (rule exI[of _ U]) auto
subgoal for U
unfolding mark_to_delete_clauses_l_pre_def
apply normalize_goal+
by (subst literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(2)[of _ U]) auto
done
lemma cdcl_twl_full_restart_wl_prog_D_cdcl_twl_restart_wl_prog:
‹(cdcl_twl_full_restart_wl_prog_D, cdcl_twl_full_restart_wl_prog) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}⟩nres_rel›
proof -
show ?thesis
unfolding uncurry_def cdcl_twl_full_restart_wl_prog_D_def cdcl_twl_full_restart_wl_prog_def
apply (intro frefI nres_relI)
apply (refine_vcg
mark_to_delete_clauses_wl_D_mark_to_delete_clauses_wl[THEN fref_to_Down])
subgoal for S T
by (rule mark_to_delete_clauses_wl_pre_lits')
subgoal for S T
unfolding mark_to_delete_clauses_wl_D_pre_def by blast
subgoal by auto
subgoal for x y S Sa
by (rule cdcl_twl_full_restart_wl_prog_D_final_rel)
done
qed
definition restart_abs_wl_D_pre :: ‹nat twl_st_wl ⇒ bool ⇒ bool› where
‹restart_abs_wl_D_pre S brk ⟷
(restart_abs_wl_pre S brk ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S)›
definition cdcl_twl_local_restart_wl_D_spec
:: ‹nat twl_st_wl ⇒ nat twl_st_wl nres›
where
‹cdcl_twl_local_restart_wl_D_spec = (λ(M, N, D, NE, UE, Q, W). do {
ASSERT(restart_abs_wl_D_pre (M, N, D, NE, UE, Q, W) False);
(M, Q') ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
Q' = {#}) ∨ (M' = M ∧ Q' = Q));
RETURN (M, N, D, NE, UE, Q', W)
})›
lemma cdcl_twl_local_restart_wl_D_spec_cdcl_twl_local_restart_wl_spec:
‹(cdcl_twl_local_restart_wl_D_spec, cdcl_twl_local_restart_wl_spec)
∈ [λS. restart_abs_wl_D_pre S False]⇩f {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} →
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}⟩nres_rel›
proof -
show ?thesis
unfolding cdcl_twl_local_restart_wl_D_spec_def cdcl_twl_local_restart_wl_spec_def
rewatch_clauses_def
apply (intro frefI nres_relI)
apply (refine_vcg)
subgoal by (auto simp: state_wl_l_def)
subgoal by (auto simp: state_wl_l_def)
subgoal by (auto simp: state_wl_l_def correct_watching.simps clause_to_update_def
literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def all_atms_def[symmetric])
done
qed
definition cdcl_twl_restart_wl_D_prog where
‹cdcl_twl_restart_wl_D_prog S = do {
b ← SPEC(λ_. True);
if b then cdcl_twl_local_restart_wl_D_spec S else cdcl_twl_full_restart_wl_prog_D S
}›
lemma cdcl_twl_restart_wl_D_prog_final_rel:
assumes
post: ‹restart_abs_wl_D_pre Sa b› and
‹(S, Sa) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}›
shows ‹(S, Sa) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}›
proof -
have lits_T: ‹literals_are_ℒ⇩i⇩n (all_atms_st S) S› and T: ‹S = Sa›
using assms by auto
obtain x xa where
‹literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S› and
S_x: ‹(S, x) ∈ state_wl_l None› and
‹correct_watching S› and
x_xa: ‹(x, xa) ∈ twl_st_l None› and
struct: ‹twl_struct_invs xa› and
list: ‹twl_list_invs x› and
‹clauses_to_update_l x = {#}› and
‹twl_stgy_invs xa› and
confl: ‹¬b ⟶ get_conflict xa = None›
using post unfolding restart_abs_wl_D_pre_def restart_abs_wl_pre_def restart_abs_l_pre_def
restart_prog_pre_def T by blast
have ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S›
by (rule literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(2)[THEN iffD2,
OF S_x x_xa struct lits_T])
then show ?thesis
using T by auto
qed
lemma cdcl_twl_restart_wl_D_prog_cdcl_twl_restart_wl_prog:
‹(cdcl_twl_restart_wl_D_prog, cdcl_twl_restart_wl_prog)
∈ [λS. restart_abs_wl_D_pre S False]⇩f {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} →
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}⟩nres_rel›
unfolding cdcl_twl_restart_wl_D_prog_def cdcl_twl_restart_wl_prog_def
rewatch_clauses_def
apply (intro frefI nres_relI)
apply (refine_vcg
cdcl_twl_local_restart_wl_D_spec_cdcl_twl_local_restart_wl_spec[THEN fref_to_Down]
cdcl_twl_full_restart_wl_prog_D_cdcl_twl_restart_wl_prog[THEN fref_to_Down])
subgoal by (auto simp: state_wl_l_def)
subgoal for x y b b'
by auto
done
context twl_restart_ops
begin
definition mark_to_delete_clauses_wl2_D_inv where
‹mark_to_delete_clauses_wl2_D_inv = (λS xs0 (i, T, xs).
mark_to_delete_clauses_wl2_inv S xs0 (i, T, xs) ∧
literals_are_ℒ⇩i⇩n' (all_init_atms_st T) T)›
definition mark_to_delete_clauses_wl2_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹mark_to_delete_clauses_wl2_D = (λS. do {
ASSERT(mark_to_delete_clauses_wl_D_pre S);
xs ← collect_valid_indices_wl S;
l ← SPEC(λ_::nat. True);
(_, S, xs) ← WHILE⇩T⇗mark_to_delete_clauses_wl2_D_inv S xs⇖
(λ(i, _, xs). i < length xs)
(λ(i, T, xs). do {
if(xs!i ∉# dom_m (get_clauses_wl T)) then RETURN (i, T, delete_index_and_swap xs i)
else do {
ASSERT(0 < length (get_clauses_wl T∝(xs!i)));
ASSERT(get_clauses_wl T∝(xs!i)!0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T));
can_del ← SPEC(λb. b ⟶
(Propagated (get_clauses_wl T∝(xs!i)!0) (xs!i) ∉ set (get_trail_wl T)) ∧
¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T∝(xs!i)) ≠ 2);
ASSERT(i < length xs);
if can_del
then
RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i)
else
RETURN (i+1, T, xs)
}
})
(l, S, xs);
RETURN S
})›
lemma mark_to_delete_clauses_wl_D_mark_to_delete_clauses_wl2:
‹(mark_to_delete_clauses_wl2_D, mark_to_delete_clauses_wl2) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}⟩nres_rel›
proof -
have [refine0]: ‹collect_valid_indices_wl S ≤ ⇓ Id (collect_valid_indices_wl T)›
if ‹(S, T) ∈ Id› for S T
using that by auto
have [iff]: ‹(∀(x::bool) xa. P x xa) ⟷ (∀xa.( P True xa ∧ P False xa))› for P
by metis
have in_Lit: ‹get_clauses_wl T' ∝ (xs ! j) ! 0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T')›
if
‹(l, l') ∈ nat_rel› and
rel: ‹(st, st') ∈ nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} ×⇩r
Id› and
inv_x: ‹mark_to_delete_clauses_wl2_D_inv S ys st› and
‹mark_to_delete_clauses_wl2_inv S' ys' st'› and
dom: ‹¬ xs ! j ∉# dom_m (get_clauses_wl T')› and
‹¬ xs' ! i ∉# dom_m (get_clauses_wl T)› and
assert: ‹0 < length (get_clauses_wl T ∝ (xs' ! i))› and
st: ‹st' = (i, sT)› ‹sT = (T, xs)› ‹st = (j, sT')› ‹sT' = (T', xs')› and
le: ‹case st of (i, T, xs) ⇒ i < length xs› and
‹case st' of (i, S, xs') ⇒ i < length xs'› and
‹0 < length (get_clauses_wl T' ∝ (xs ! j))›
for S S' xs' l l' st st' i T j T' sT xs sT' ys ys'
proof -
have lits_T': ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st T') T'›
using inv_x unfolding mark_to_delete_clauses_wl2_D_inv_def prod.simps st
by fast
have ‹literals_are_ℒ⇩i⇩n (all_init_atms_st T) T›
proof -
obtain x xa xb where
lits_T': ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st T') T'› and
Ta_x: ‹(S, x) ∈ state_wl_l None› and
Ta_y: ‹(T', xa) ∈ state_wl_l None› and
‹correct_watching'' S› and
rem: ‹remove_one_annot_true_clause⇧*⇧* x xa› and
list: ‹twl_list_invs x› and
x_xb: ‹(x, xb) ∈ twl_st_l None› and
struct: ‹twl_struct_invs xb› and
confl: ‹get_conflict_l x = None› and
upd: ‹clauses_to_update_l x = {#}›
using inv_x unfolding mark_to_delete_clauses_wl2_D_inv_def st prod.case
mark_to_delete_clauses_wl2_inv_def mark_to_delete_clauses_l_inv_def
by blast
obtain y where
Ta_y': ‹(xa, y) ∈ twl_st_l None› and
struct': ‹twl_struct_invs y›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list confl upd x_xb
struct] by blast
have ‹literals_are_ℒ⇩i⇩n (all_init_atms_st T') T'›
by (rule literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(1)[THEN iffD1,
OF Ta_y Ta_y' struct' lits_T'])
then show ?thesis
using rel by (auto simp: st)
qed
then have ‹literals_are_in_ℒ⇩i⇩n (all_init_atms_st T') (mset (get_clauses_wl T' ∝ (xs ! j)))›
using literals_are_in_ℒ⇩i⇩n_nth[of ‹xs!i› ‹T›] rel dom
by (auto simp: st)
then show ?thesis
by (rule literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l) (use le assert rel dom in ‹auto simp: st›)
qed
have final_rel_del:
‹((j, mark_garbage_wl (xs ! j) T', delete_index_and_swap xs j),
i, mark_garbage_wl (xs' ! i) T, delete_index_and_swap xs' i)
∈ nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}×⇩r Id›
if
rel: ‹(st, st') ∈ nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st T) S} ×⇩r
Id› and
‹case st of (i, T, xs) ⇒ i < length xs› and
‹case st' of (i, S, xs') ⇒ i < length xs'› and
inv: ‹mark_to_delete_clauses_wl2_D_inv S ys st› and
‹mark_to_delete_clauses_wl2_inv S' ys' st'› and
st: ‹st' = (i, sT)› ‹sT = (T, xs)› ‹st = (j, sT')› ‹sT' = (T', xs')› and
dom: ‹¬ xs ! j ∉# dom_m (get_clauses_wl T')› and
‹¬ xs' ! i ∉# dom_m (get_clauses_wl T)› and
le: ‹0 < length (get_clauses_wl T ∝ (xs' ! i))› and
‹0 < length (get_clauses_wl T' ∝ (xs ! j))› and
‹get_clauses_wl T' ∝ (xs ! j) ! 0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T')› and
‹(can_del, can_del') ∈ bool_rel› and
can_del: ‹can_del
∈ {b. b ⟶
Propagated (get_clauses_wl T' ∝ (xs ! j) ! 0) (xs ! j)
∉ set (get_trail_wl T') ∧
¬ irred (get_clauses_wl T') (xs ! j)}› and
‹can_del'
∈ {b. b ⟶
Propagated (get_clauses_wl T ∝ (xs' ! i) ! 0) (xs' ! i)
∉ set (get_trail_wl T) ∧
¬ irred (get_clauses_wl T) (xs' ! i)}› and
i_le: ‹i < length xs'› and
‹j < length xs› and
[simp]: ‹can_del› and
[simp]: ‹can_del'›
for S S' xs xs' l l' st st' i T j T' can_del can_del' sT sT' ys ys'
proof -
have ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st (mark_garbage_wl (xs' ! i) T)) (mark_garbage_wl (xs' ! i) T)›
using can_del inv rel unfolding mark_to_delete_clauses_wl2_D_inv_def st mark_garbage_wl_def
by (cases T)
(auto simp: literals_are_ℒ⇩i⇩n'_def init_clss_l_fmdrop_irrelev mset_take_mset_drop_mset'
blits_in_ℒ⇩i⇩n'_def all_init_lits_def)
then show ?thesis
using inv rel unfolding st
by auto
qed
show ?thesis
unfolding uncurry_def mark_to_delete_clauses_wl2_D_def mark_to_delete_clauses_wl2_def
collect_valid_indices_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
WHILEIT_refine[where
R = ‹nat_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} ×⇩r Id›])
subgoal
unfolding mark_to_delete_clauses_wl_D_pre_def by auto
subgoal by auto
subgoal for x y xs xsa l la xa x'
unfolding mark_to_delete_clauses_wl2_D_inv_def by (cases x') auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S S' xs xs' l l' st st' i T j T'
by (rule in_Lit; assumption?) auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S S' xs xs' l l' st st' i T j T' can_del can_del'
by (rule final_rel_del; assumption?) auto
subgoal by auto
subgoal by auto
done
qed
definition cdcl_GC_clauses_prog_copy_wl_entry
:: ‹'v clauses_l ⇒ 'v watched ⇒ 'v literal ⇒
'v clauses_l ⇒ ('v clauses_l × 'v clauses_l) nres›
where
‹cdcl_GC_clauses_prog_copy_wl_entry = (λN W A N'. do {
let le = length W;
(i, N, N') ← WHILE⇩T
(λ(i, N, N'). i < le)
(λ(i, N, N'). do {
ASSERT(i < length W);
let C = fst (W ! i);
if C ∈# dom_m N then do {
D ← SPEC(λD. D ∉# dom_m N' ∧ D ≠ 0);
RETURN (i+1, fmdrop C N, fmupd D (N ∝ C, irred N C) N')
} else RETURN (i+1, N, N')
}) (0, N, N');
RETURN (N, N')
})›
definition clauses_pointed_to :: ‹'v literal set ⇒ ('v literal ⇒ 'v watched) ⇒ nat set›
where
‹clauses_pointed_to 𝒜 W ≡ ⋃(((`) fst) ` set ` W ` 𝒜)›
lemma clauses_pointed_to_insert[simp]:
‹clauses_pointed_to (insert A 𝒜) W =
fst ` set (W A) ∪
clauses_pointed_to 𝒜 W› and
clauses_pointed_to_empty[simp]:
‹clauses_pointed_to {} W = {}›
by (auto simp: clauses_pointed_to_def)
lemma cdcl_GC_clauses_prog_copy_wl_entry:
fixes A :: ‹'v literal› and WS :: ‹'v literal ⇒ 'v watched›
defines [simp]: ‹W ≡ WS A›
assumes ‹
ran m0 ⊆ set_mset (dom_m N0') ∧
(∀L∈dom m0. L ∉# (dom_m N0)) ∧
set_mset (dom_m N0) ⊆ clauses_pointed_to (set_mset 𝒜) WS ∧
0 ∉# dom_m N0'›
shows
‹cdcl_GC_clauses_prog_copy_wl_entry N0 W A N0' ≤
SPEC(λ(N, N'). (∃m. GC_remap⇧*⇧* (N0, m0, N0') (N, m, N') ∧
ran m ⊆ set_mset (dom_m N') ∧
(∀L∈dom m. L ∉# (dom_m N)) ∧
set_mset (dom_m N) ⊆ clauses_pointed_to (set_mset (remove1_mset A 𝒜)) WS) ∧
(∀L ∈ set W. fst L ∉# dom_m N) ∧
0 ∉# dom_m N')›
proof -
have [simp]:
‹x ∈# remove1_mset a (dom_m aaa) ⟷ x ≠ a ∧ x ∈# dom_m aaa› for x a aaa
using distinct_mset_dom[of aaa]
by (cases ‹a ∈# dom_m aaa›)
(auto dest!: multi_member_split simp: add_mset_eq_add_mset)
show ?thesis
unfolding cdcl_GC_clauses_prog_copy_wl_entry_def
apply (refine_vcg
WHILET_rule[where I = ‹λ(i, N, N'). ∃m. GC_remap⇧*⇧* (N0, m0, N0') (N, m, N') ∧
ran m ⊆ set_mset (dom_m N') ∧
(∀L∈dom m. L ∉# (dom_m N)) ∧
set_mset (dom_m N) ⊆ clauses_pointed_to (set_mset (remove1_mset A 𝒜)) WS ∪
(fst) ` set (drop i W) ∧
(∀L ∈ set (take i W). fst L ∉# dom_m N) ∧
0 ∉# dom_m N'› and
R = ‹measure (λ(i, N, N'). length W -i)›])
subgoal by auto
subgoal
using assms
by (cases ‹A ∈# 𝒜›) (auto dest!: multi_member_split)
subgoal by auto
subgoal for s aa ba aaa baa x x1 x2 x1a x2a
apply clarify
apply (subgoal_tac ‹(∃m'. GC_remap (aaa, m, baa) (fmdrop (fst (W ! aa)) aaa, m',
fmupd x (the (fmlookup aaa (fst (W ! aa)))) baa) ∧
ran m' ⊆ set_mset (dom_m (fmupd x (the (fmlookup aaa (fst (W ! aa)))) baa)) ∧
(∀L∈dom m'. L ∉# (dom_m (fmdrop (fst (W ! aa)) aaa)))) ∧
set_mset (dom_m (fmdrop (fst (W ! aa)) aaa)) ⊆
clauses_pointed_to (set_mset (remove1_mset A 𝒜)) WS ∪
fst ` set (drop (Suc aa) W) ∧
(∀L ∈ set (take (Suc aa) W). fst L ∉# dom_m (fmdrop (fst (W ! aa)) aaa))›)
apply (auto intro: rtranclp.rtrancl_into_rtrancl)[]
apply (auto simp: GC_remap.simps Cons_nth_drop_Suc[symmetric]
take_Suc_conv_app_nth
dest: multi_member_split)
apply (rule_tac x= ‹m(fst (W ! aa) ↦ x)› in exI)
apply (intro conjI)
apply (rule_tac x=x in exI)
apply (rule_tac x= ‹fst (W ! aa)› in exI)
apply (force dest: rtranclp_GC_remap_ran_m_no_lost)
apply auto
by (smt basic_trans_rules(31) fun_upd_apply mem_Collect_eq option.simps(1) ran_def)
subgoal by auto
subgoal by (auto 5 5 simp: GC_remap.simps Cons_nth_drop_Suc[symmetric]
take_Suc_conv_app_nth
dest: multi_member_split)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
definition cdcl_GC_clauses_prog_single_wl
:: ‹'v clauses_l ⇒ ('v literal ⇒ 'v watched) ⇒ 'v ⇒
'v clauses_l ⇒ ('v clauses_l × 'v clauses_l × ('v literal ⇒ 'v watched)) nres›
where
‹cdcl_GC_clauses_prog_single_wl = (λN WS A N'. do {
L ← RES {Pos A, Neg A};
(N, N') ← cdcl_GC_clauses_prog_copy_wl_entry N (WS L) L N';
let WS = WS(L := []);
(N, N') ← cdcl_GC_clauses_prog_copy_wl_entry N (WS (-L)) (-L) N';
let WS = WS(-L := []);
RETURN (N, N', WS)
})›
lemma clauses_pointed_to_remove1_if:
‹∀L∈set (W L). fst L ∉# dom_m aa ⟹ xa ∈# dom_m aa ⟹
xa ∈ clauses_pointed_to (set_mset (remove1_mset L 𝒜))
(λa. if a = L then [] else W a) ⟷
xa ∈ clauses_pointed_to (set_mset (remove1_mset L 𝒜)) W›
by (cases ‹L ∈# 𝒜›)
(fastforce simp: clauses_pointed_to_def
dest!: multi_member_split)+
lemma clauses_pointed_to_remove1_if2:
‹∀L∈set (W L). fst L ∉# dom_m aa ⟹ xa ∈# dom_m aa ⟹
xa ∈ clauses_pointed_to (set_mset (𝒜 - {#L, L'#}))
(λa. if a = L then [] else W a) ⟷
xa ∈ clauses_pointed_to (set_mset (𝒜 - {#L, L'#})) W›
‹∀L∈set (W L). fst L ∉# dom_m aa ⟹ xa ∈# dom_m aa ⟹
xa ∈ clauses_pointed_to (set_mset (𝒜 - {#L', L#}))
(λa. if a = L then [] else W a) ⟷
xa ∈ clauses_pointed_to (set_mset (𝒜 - {#L', L#})) W›
by (cases ‹L ∈# 𝒜›; fastforce simp: clauses_pointed_to_def
dest!: multi_member_split)+
lemma clauses_pointed_to_remove1_if2_eq:
‹∀L∈set (W L). fst L ∉# dom_m aa ⟹
set_mset (dom_m aa) ⊆ clauses_pointed_to (set_mset (𝒜 - {#L, L'#}))
(λa. if a = L then [] else W a) ⟷
set_mset (dom_m aa) ⊆ clauses_pointed_to (set_mset (𝒜 - {#L, L'#})) W›
‹∀L∈set (W L). fst L ∉# dom_m aa ⟹
set_mset (dom_m aa) ⊆ clauses_pointed_to (set_mset (𝒜 - {#L', L#}))
(λa. if a = L then [] else W a) ⟷
set_mset (dom_m aa) ⊆ clauses_pointed_to (set_mset (𝒜 - {#L', L#})) W›
by (auto simp: clauses_pointed_to_remove1_if2)
lemma negs_remove_Neg: ‹A ∉# 𝒜 ⟹ negs 𝒜 + poss 𝒜 - {#Neg A, Pos A#} =
negs 𝒜 + poss 𝒜›
by (induction 𝒜) auto
lemma poss_remove_Pos: ‹A ∉# 𝒜 ⟹ negs 𝒜 + poss 𝒜 - {#Pos A, Neg A#} =
negs 𝒜 + poss 𝒜›
by (induction 𝒜) auto
lemma cdcl_GC_clauses_prog_single_wl_removed:
‹∀L∈set (W (Pos A)). fst L ∉# dom_m aaa ⟹
∀L∈set (W (Neg A)). fst L ∉# dom_m a ⟹
GC_remap⇧*⇧* (aaa, ma, baa) (a, mb, b) ⟹
set_mset (dom_m a) ⊆ clauses_pointed_to (set_mset (negs 𝒜 + poss 𝒜 - {#Neg A, Pos A#})) W ⟹
xa ∈# dom_m a ⟹
xa ∈ clauses_pointed_to (Neg ` set_mset (remove1_mset A 𝒜) ∪ Pos ` set_mset (remove1_mset A 𝒜))
(W(Pos A := [], Neg A := []))›
‹∀L∈set (W (Neg A)). fst L ∉# dom_m aaa ⟹
∀L∈set (W (Pos A)). fst L ∉# dom_m a ⟹
GC_remap⇧*⇧* (aaa, ma, baa) (a, mb, b) ⟹
set_mset (dom_m a) ⊆ clauses_pointed_to (set_mset (negs 𝒜 + poss 𝒜 - {#Pos A, Neg A#})) W ⟹
xa ∈# dom_m a ⟹
xa ∈ clauses_pointed_to
(Neg ` set_mset (remove1_mset A 𝒜) ∪ Pos ` set_mset (remove1_mset A 𝒜))
(W(Neg A := [], Pos A := []))›
supply poss_remove_Pos[simp] negs_remove_Neg[simp]
by (case_tac [!] ‹A ∈# 𝒜›)
(fastforce simp: clauses_pointed_to_def
dest!: multi_member_split
dest: rtranclp_GC_remap_ran_m_no_lost)+
lemma cdcl_GC_clauses_prog_single_wl:
fixes A :: ‹'v› and WS :: ‹'v literal ⇒ 'v watched› and
N0 :: ‹'v clauses_l›
assumes ‹ran m ⊆ set_mset (dom_m N0') ∧
(∀L∈dom m. L ∉# (dom_m N0)) ∧
set_mset (dom_m N0) ⊆
clauses_pointed_to (set_mset (negs 𝒜 + poss 𝒜)) W ∧
0 ∉# dom_m N0'›
shows
‹cdcl_GC_clauses_prog_single_wl N0 W A N0' ≤
SPEC(λ(N, N', WS'). ∃m'. GC_remap⇧*⇧* (N0, m, N0') (N, m', N') ∧
ran m' ⊆ set_mset (dom_m N') ∧
(∀L∈dom m'. L ∉# dom_m N) ∧
WS' (Pos A) = [] ∧ WS' (Neg A) = [] ∧
(∀L. L ≠ Pos A ⟶ L ≠ Neg A ⟶ W L = WS' L) ∧
set_mset (dom_m N) ⊆
clauses_pointed_to
(set_mset (negs (remove1_mset A 𝒜) + poss (remove1_mset A 𝒜))) WS' ∧
0 ∉# dom_m N'
)›
proof -
have [simp]: ‹A ∉# 𝒜 ⟹ negs 𝒜 + poss 𝒜 - {#Neg A, Pos A#} =
negs 𝒜 + poss 𝒜›
by (induction 𝒜) auto
have [simp]: ‹A ∉# 𝒜 ⟹ negs 𝒜 + poss 𝒜 - {#Pos A, Neg A#} =
negs 𝒜 + poss 𝒜›
by (induction 𝒜) auto
show ?thesis
unfolding cdcl_GC_clauses_prog_single_wl_def
apply (refine_vcg)
subgoal for x
apply (rule order_trans, rule cdcl_GC_clauses_prog_copy_wl_entry[of _ _ _
‹negs 𝒜 + poss 𝒜›])
apply(solves ‹use assms in auto›)
apply (rule RES_rule)
apply (refine_vcg)
apply clarify
subgoal for aa ba aaa baa ma
apply (rule order_trans,
rule cdcl_GC_clauses_prog_copy_wl_entry[of ma _ _
‹remove1_mset x (negs 𝒜 + poss 𝒜)›])
apply (solves ‹auto simp: clauses_pointed_to_remove1_if›)[]
unfolding Let_def
apply (rule RES_rule)
apply clarsimp
apply (simp add: eq_commute[of ‹Neg _›]
uminus_lit_swap clauses_pointed_to_remove1_if)
apply auto
apply (rule_tac x=mb in exI)
apply (auto dest!:
simp: clauses_pointed_to_remove1_if
clauses_pointed_to_remove1_if2
clauses_pointed_to_remove1_if2_eq)
apply (subst (asm) clauses_pointed_to_remove1_if2_eq)
apply (force dest: rtranclp_GC_remap_ran_m_no_lost)
apply (auto intro!: cdcl_GC_clauses_prog_single_wl_removed)[]
apply (rule_tac x=mb in exI)
apply (auto dest: multi_member_split[of A]
simp: clauses_pointed_to_remove1_if
clauses_pointed_to_remove1_if2
clauses_pointed_to_remove1_if2_eq)
apply (subst (asm) clauses_pointed_to_remove1_if2_eq)
apply (force dest: rtranclp_GC_remap_ran_m_no_lost)
apply (auto intro!: cdcl_GC_clauses_prog_single_wl_removed)[]
done
done
done
qed
definition cdcl_GC_clauses_prog_wl_inv
:: ‹'v multiset ⇒ 'v clauses_l ⇒
'v multiset × ('v clauses_l × 'v clauses_l × ('v literal ⇒ 'v watched)) ⇒ bool›
where
‹cdcl_GC_clauses_prog_wl_inv 𝒜 N0 = (λ(ℬ, (N, N', WS)). ℬ ⊆# 𝒜 ∧
(∀A ∈ set_mset 𝒜 - set_mset ℬ. (WS (Pos A) = []) ∧ WS (Neg A) = []) ∧
0 ∉# dom_m N' ∧
(∃m. GC_remap⇧*⇧* (N0, (λ_. None), fmempty) (N, m, N')∧
ran m ⊆ set_mset (dom_m N') ∧
(∀L∈dom m. L ∉# dom_m N) ∧
set_mset (dom_m N) ⊆ clauses_pointed_to (Neg ` set_mset ℬ ∪ Pos ` set_mset ℬ) WS))›
definition cdcl_GC_clauses_prog_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹cdcl_GC_clauses_prog_wl = (λ(M, N0, D, NE, UE, Q, WS). do {
ASSERT(cdcl_GC_clauses_pre_wl (M, N0, D, NE, UE, Q, WS));
𝒜 ← SPEC(λ𝒜. set_mset 𝒜 = set_mset (all_init_atms N0 NE));
(_, (N, N', WS)) ← WHILE⇩T⇗cdcl_GC_clauses_prog_wl_inv 𝒜 N0⇖
(λ(ℬ, _). ℬ ≠ {#})
(λ(ℬ, (N, N', WS)). do {
ASSERT(ℬ ≠ {#});
A ← SPEC (λA. A ∈# ℬ);
(N, N', WS) ← cdcl_GC_clauses_prog_single_wl N WS A N';
RETURN (remove1_mset A ℬ, (N, N', WS))
})
(𝒜, (N0, fmempty, WS));
RETURN (M, N', D, NE, UE, Q, WS)
})›
lemma cdcl_GC_clauses_prog_wl:
assumes ‹((M, N0, D, NE, UE, Q, WS), S) ∈ state_wl_l None ∧
correct_watching'' (M, N0, D, NE, UE, Q, WS) ∧ cdcl_GC_clauses_pre S ∧
set_mset (dom_m N0) ⊆ clauses_pointed_to
(Neg ` set_mset (all_init_atms N0 NE) ∪ Pos ` set_mset (all_init_atms N0 NE)) WS›
shows
‹cdcl_GC_clauses_prog_wl (M, N0, D, NE, UE, Q, WS) ≤
(SPEC(λ(M', N', D', NE', UE', Q', WS'). (M', D', NE', UE', Q') = (M, D, NE, UE, Q) ∧
(∃m. GC_remap⇧*⇧* (N0, (λ_. None), fmempty) (fmempty, m, N')) ∧
0 ∉# dom_m N' ∧ (∀L ∈# all_init_lits N0 NE. WS' L = [])))›
proof -
show ?thesis
supply[[goals_limit=1]]
unfolding cdcl_GC_clauses_prog_wl_def
apply (refine_vcg
WHILEIT_rule[where R = ‹measure (λ(𝒜::'v multiset, (_::'v clauses_l, _ ::'v clauses_l,
_:: 'v literal ⇒ 'v watched)). size 𝒜)›])
subgoal
using assms
unfolding cdcl_GC_clauses_pre_wl_def
by blast
subgoal by auto
subgoal using assms unfolding cdcl_GC_clauses_prog_wl_inv_def by auto
subgoal by auto
subgoal for a b aa ba ab bb ac bc ad bd ae be x s af bf ag bg ah bh xa
unfolding cdcl_GC_clauses_prog_wl_inv_def
apply clarify
apply (rule order_trans,
rule_tac m=m and 𝒜=af in cdcl_GC_clauses_prog_single_wl)
subgoal by auto
subgoal
apply (rule RES_rule)
apply clarify
apply (rule RETURN_rule)
apply clarify
apply (intro conjI)
apply (solves auto)
apply (solves ‹auto dest!: multi_member_split›)
apply (solves auto)
apply (rule_tac x=m' in exI)
apply (solves auto)[]
apply (simp_all add: size_Diff1_less)[]
done
done
subgoal
unfolding cdcl_GC_clauses_prog_wl_inv_def
by auto
subgoal
unfolding cdcl_GC_clauses_prog_wl_inv_def
by auto
subgoal
unfolding cdcl_GC_clauses_prog_wl_inv_def
by auto
subgoal
unfolding cdcl_GC_clauses_prog_wl_inv_def
by (intro ballI, rename_tac L, case_tac L)
(auto simp: in_all_lits_of_mm_ain_atms_of_iff all_init_atms_def
simp del: all_init_atms_def[symmetric]
dest!: multi_member_split)
done
qed
lemma all_init_atms_fmdrop_add_mset_unit:
‹C ∈# dom_m baa ⟹ irred baa C ⟹
all_init_atms (fmdrop C baa) (add_mset (mset (baa ∝ C)) da) =
all_init_atms baa da›
‹C ∈# dom_m baa ⟹ ¬irred baa C ⟹
all_init_atms (fmdrop C baa) da =
all_init_atms baa da›
by (auto simp del: all_init_atms_def[symmetric]
simp: all_init_atms_def all_init_lits_def
init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if)
lemma cdcl_GC_clauses_prog_wl2:
assumes ‹((M, N0, D, NE, UE, Q, WS), S) ∈ state_wl_l None ∧
correct_watching'' (M, N0, D, NE, UE, Q, WS) ∧ cdcl_GC_clauses_pre S ∧
set_mset (dom_m N0) ⊆ clauses_pointed_to
(Neg ` set_mset (all_init_atms N0 NE) ∪ Pos ` set_mset (all_init_atms N0 NE)) WS› and
‹N0 = N0'›
shows
‹cdcl_GC_clauses_prog_wl (M, N0, D, NE, UE, Q, WS) ≤
⇓ {((M', N'', D', NE', UE', Q', WS'), (N, N')). (M', D', NE', UE', Q') = (M, D, NE, UE, Q) ∧
N'' = N ∧ (∀L∈#all_init_lits N0 NE. WS' L = [])∧
all_init_lits N0 NE = all_init_lits N NE' ∧
(∃m. GC_remap⇧*⇧* (N0, (λ_. None), fmempty) (fmempty, m, N))}
(SPEC(λ(N'::(nat, 'a literal list × bool) fmap, m).
GC_remap⇧*⇧* (N0', (λ_. None), fmempty) (fmempty, m, N') ∧
0 ∉# dom_m N'))›
proof -
show ?thesis
unfolding ‹N0 = N0'›[symmetric]
apply (rule order_trans[OF cdcl_GC_clauses_prog_wl[OF assms(1)]])
apply (rule RES_refine)
apply (fastforce dest: rtranclp_GC_remap_all_init_lits)
done
qed
definition cdcl_twl_stgy_restart_abs_wl_D_inv where
‹cdcl_twl_stgy_restart_abs_wl_D_inv S0 brk T n ⟷
cdcl_twl_stgy_restart_abs_wl_inv S0 brk T n ∧
literals_are_ℒ⇩i⇩n (all_atms_st T) T›
definition cdcl_GC_clauses_pre_wl_D :: ‹nat twl_st_wl ⇒ bool› where
‹cdcl_GC_clauses_pre_wl_D S ⟷ (
∃T. (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S ∧
cdcl_GC_clauses_pre_wl T
)›
definition cdcl_twl_full_restart_wl_D_GC_prog_post :: ‹'v twl_st_wl ⇒ 'v twl_st_wl ⇒ bool› where
‹cdcl_twl_full_restart_wl_D_GC_prog_post S T ⟷
(∃S' T'. (S, S') ∈ Id ∧ (T, T') ∈ Id ∧
cdcl_twl_full_restart_wl_GC_prog_post S' T')›
definition cdcl_GC_clauses_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹cdcl_GC_clauses_wl_D = (λ(M, N, D, NE, UE, WS, Q). do {
ASSERT(cdcl_GC_clauses_pre_wl_D (M, N, D, NE, UE, WS, Q));
let b = True;
if b then do {
(N', _) ← SPEC (λ(N'', m). GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, m, N'') ∧
0 ∉# dom_m N'');
Q ← SPEC(λQ. correct_watching' (M, N', D, NE, UE, WS, Q) ∧
blits_in_ℒ⇩i⇩n' (M, N', D, NE, UE, WS, Q));
RETURN (M, N', D, NE, UE, WS, Q)
}
else RETURN (M, N, D, NE, UE, WS, Q)})›
lemma cdcl_GC_clauses_wl_D_cdcl_GC_clauses_wl:
‹(cdcl_GC_clauses_wl_D, cdcl_GC_clauses_wl) ∈ {(S::nat twl_st_wl, S').
(S, S') ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} →⇩f ⟨{(S::nat twl_st_wl, S').
(S, S') ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}⟩nres_rel›
unfolding cdcl_GC_clauses_wl_D_def cdcl_GC_clauses_wl_def
apply (intro frefI nres_relI)
apply refine_vcg
subgoal unfolding cdcl_GC_clauses_pre_wl_D_def by blast
subgoal by (auto simp: state_wl_l_def)
subgoal by (auto simp: state_wl_l_def)
subgoal by auto
subgoal by (auto simp: state_wl_l_def)
subgoal by (auto simp: state_wl_l_def literals_are_ℒ⇩i⇩n'_def is_ℒ⇩a⇩l⇩l_def
all_init_atms_def all_init_lits_def
dest: rtranclp_GC_remap_init_clss_l_old_new)
subgoal by (auto simp: state_wl_l_def)
done
definition cdcl_twl_full_restart_wl_D_GC_prog where
‹cdcl_twl_full_restart_wl_D_GC_prog S = do {
ASSERT(cdcl_twl_full_restart_wl_GC_prog_pre S);
S' ← cdcl_twl_local_restart_wl_spec0 S;
T ← remove_one_annot_true_clause_imp_wl_D S';
ASSERT(mark_to_delete_clauses_wl_D_pre T);
U ← mark_to_delete_clauses_wl2_D T;
V ← cdcl_GC_clauses_wl_D U;
ASSERT(cdcl_twl_full_restart_wl_D_GC_prog_post S V);
RETURN V
}›
lemma ℒ⇩a⇩l⇩l_all_init_atms_all_init_lits:
‹set_mset (ℒ⇩a⇩l⇩l (all_init_atms N NE)) = set_mset (all_init_lits N NE)›
using is_ℒ⇩a⇩l⇩l_def by blast
lemma ℒ⇩a⇩l⇩l_all_atms_all_lits:
‹set_mset (ℒ⇩a⇩l⇩l (all_atms N NE)) = set_mset (all_lits N NE)›
by (simp add: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm all_atms_def all_lits_def)
lemma all_lits_alt_def:
‹all_lits S NUE = all_lits_of_mm (mset `# ran_mf S + NUE)›
unfolding all_lits_def
by auto
lemma cdcl_twl_full_restart_wl_D_GC_prog:
‹(cdcl_twl_full_restart_wl_D_GC_prog, cdcl_twl_full_restart_wl_GC_prog) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_init_atms_st S) S}⟩nres_rel›
(is ‹_ ∈ ?R →⇩f _›)
proof -
have [refine0]: ‹cdcl_twl_local_restart_wl_spec0 x
≤ ⇓ ?R (cdcl_twl_local_restart_wl_spec0 y)›
if ‹(x, y) ∈ ?R›
for x y
using that apply (case_tac x; case_tac y)
by (auto 5 1 simp: cdcl_twl_local_restart_wl_spec0_def image_iff
RES_RES_RETURN_RES2 intro!: RES_refine)
(auto simp: literals_are_ℒ⇩i⇩n'_def blits_in_ℒ⇩i⇩n'_def)
show ?thesis
unfolding cdcl_twl_full_restart_wl_D_GC_prog_def cdcl_twl_full_restart_wl_GC_prog_def
apply (intro frefI nres_relI)
apply (refine_vcg
remove_one_annot_true_clause_imp_wl_D_remove_one_annot_true_clause_imp_wl[THEN fref_to_Down]
mark_to_delete_clauses_wl_D_mark_to_delete_clauses_wl2[THEN fref_to_Down]
cdcl_GC_clauses_wl_D_cdcl_GC_clauses_wl[THEN fref_to_Down])
subgoal by fast
subgoal unfolding mark_to_delete_clauses_wl_D_pre_def by fast
subgoal unfolding cdcl_twl_full_restart_wl_D_GC_prog_post_def by fast
subgoal unfolding cdcl_twl_full_restart_wl_GC_prog_post_def
literals_are_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n'_def
is_ℒ⇩a⇩l⇩l_def blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def
ℒ⇩a⇩l⇩l_all_init_atms_all_init_lits
all_atms_def[symmetric]
all_init_atms_def[symmetric]
all_lits_alt_def[symmetric]
all_init_lits_def[symmetric]
ℒ⇩a⇩l⇩l_all_atms_all_lits
by fastforce
done
qed
definition restart_prog_wl_D :: "nat twl_st_wl ⇒ nat ⇒ bool ⇒ (nat twl_st_wl × nat) nres" where
‹restart_prog_wl_D S n brk = do {
ASSERT(restart_abs_wl_D_pre S brk);
b ← restart_required_wl S n;
b2 ← SPEC(λ_. True);
if b2 ∧ b ∧ ¬brk then do {
T ← cdcl_twl_full_restart_wl_D_GC_prog S;
RETURN (T, n + 1)
}
else if b ∧ ¬brk then do {
T ← cdcl_twl_restart_wl_D_prog S;
RETURN (T, n + 1)
}
else
RETURN (S, n)
}›
lemma restart_abs_wl_D_pre_literals_are_ℒ⇩i⇩n':
assumes
‹(x, y)
∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩f
nat_rel ×⇩f
bool_rel› and
‹x1 = (x1a, x2)› and
‹y = (x1, x2a)› and
‹x1b = (x1c, x2b)› and
‹x = (x1b, x2c)› and
pre: ‹restart_abs_wl_D_pre x1c x2c› and
‹b2 ∧ b ∧ ¬ x2c› and
‹b2a ∧ ba ∧ ¬ x2a›
shows ‹(x1c, x1a)
∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n' (all_init_atms_st S) S}›
proof -
have y: ‹y = ((x1a, x2), x2a)› and
x_y: ‹x = y› and
[simp]: ‹x1c = x1a›
using assms by auto
obtain x xa where
lits: ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st x1c) x1c› and
x1c_x: ‹(x1c, x) ∈ state_wl_l None› and
‹correct_watching x1c› and
x_xa: ‹(x, xa) ∈ twl_st_l None› and
‹restart_prog_pre xa x2c› and
list_invs: ‹twl_list_invs x› and
struct_invs: ‹twl_struct_invs xa› and
‹clauses_to_update_l x = {#}›
using pre unfolding restart_abs_wl_D_pre_def restart_abs_wl_pre_def
restart_abs_l_pre_def restart_prog_pre_def by blast
have ‹set_mset (all_init_atms_st x1a) = set_mset (all_atms_st x1a)›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(3)[OF x1c_x x_xa struct_invs]
lits
by auto
with ℒ⇩a⇩l⇩l_cong[OF this] have ‹literals_are_ℒ⇩i⇩n' (all_init_atms_st x1a) x1a›
using assms(1)
unfolding literals_are_ℒ⇩i⇩n'_def literals_are_ℒ⇩i⇩n_def
all_init_lits_def[symmetric] y x_y
blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def
by auto
then show ?thesis
using x_y by auto
qed
lemma restart_prog_wl_D_restart_prog_wl:
‹(uncurry2 restart_prog_wl_D, uncurry2 restart_prog_wl) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩f nat_rel ×⇩f bool_rel →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩r nat_rel⟩nres_rel›
proof -
have [refine0]: ‹restart_required_wl x1c x2b ≤ ⇓ Id (restart_required_wl x1a x2)›
if ‹(x1c, x1a) ∈ Id› ‹(x2b, x2) ∈ Id›
for x1c x1a x2b x2
using that by auto
have restart_abs_wl_D_pre: ‹restart_abs_wl_D_pre x1c x2c›
if
‹(x, y) ∈ {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩f nat_rel ×⇩f bool_rel› and
‹x1 = (x1a, x2)› and
‹y = (x1, x2a)› and
‹x1b = (x1c, x2b)› and
‹x = (x1b, x2c)› and
pre: ‹restart_abs_wl_pre x1a x2a›
for x y x1 x1a x2 x2a x1b x1c x2b x2c
proof -
have ‹restart_abs_wl_pre x1a x2c› and lits_T: ‹literals_are_ℒ⇩i⇩n (all_atms_st x1a) x1a›
using pre that
unfolding restart_abs_wl_D_pre_def
by auto
then obtain xa x where
S_x: ‹(x1a, x) ∈ state_wl_l None› and
‹correct_watching x1a› and
x_xa: ‹(x, xa) ∈ twl_st_l None› and
struct: ‹twl_struct_invs xa› and
list: ‹twl_list_invs x› and
‹clauses_to_update_l x = {#}› and
‹twl_stgy_invs xa› and
‹¬ x2c ⟶ get_conflict xa = None›
unfolding restart_abs_wl_pre_def restart_abs_l_pre_def restart_prog_pre_def by blast
show ?thesis
using pre that literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(1,2)[THEN iffD2,
OF S_x x_xa struct lits_T]
unfolding restart_abs_wl_D_pre_def
by auto
qed
show ?thesis
unfolding uncurry_def restart_prog_wl_D_def restart_prog_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
cdcl_twl_restart_wl_D_prog_cdcl_twl_restart_wl_prog[THEN fref_to_Down]
cdcl_twl_full_restart_wl_D_GC_prog[THEN fref_to_Down])
subgoal by (rule restart_abs_wl_D_pre)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule restart_abs_wl_D_pre_literals_are_ℒ⇩i⇩n')
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
definition cdcl_twl_stgy_restart_prog_wl_D
:: "nat twl_st_wl ⇒ nat twl_st_wl nres"
where
‹cdcl_twl_stgy_restart_prog_wl_D S⇩0 =
do {
(brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_D_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop_wl_D S;
(brk, T) ← cdcl_twl_o_prog_wl_D T;
(T, n) ← restart_prog_wl_D T n brk;
RETURN (brk, T, n)
})
(False, S⇩0::nat twl_st_wl, 0);
RETURN T
}›
theorem cdcl_twl_o_prog_wl_D_spec':
‹(cdcl_twl_o_prog_wl_D, cdcl_twl_o_prog_wl) ∈
{(S,S'). (S,S') ∈ Id ∧literals_are_ℒ⇩i⇩n (all_atms_st S) S} →⇩f
⟨bool_rel ×⇩r {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n (all_atms_st T) T}⟩ nres_rel›
apply (intro frefI nres_relI)
subgoal for x y
apply (rule order_trans)
apply (rule cdcl_twl_o_prog_wl_D_spec[of "all_atms_st x" x])
apply (auto simp: prod_rel_def intro: conc_fun_R_mono)
done
done
lemma unit_propagation_outer_loop_wl_D_spec':
shows ‹(unit_propagation_outer_loop_wl_D, unit_propagation_outer_loop_wl) ∈
{(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n (all_atms_st T) T} →⇩f
⟨{(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n (all_atms_st T) T}⟩nres_rel›
apply (intro frefI nres_relI)
subgoal for x y
apply (rule order_trans)
apply (rule unit_propagation_outer_loop_wl_D_spec[of "all_atms_st x" x])
apply (auto simp: prod_rel_def intro: conc_fun_R_mono)
done
done
lemma cdcl_twl_stgy_restart_prog_wl_D_cdcl_twl_stgy_restart_prog_wl:
‹(cdcl_twl_stgy_restart_prog_wl_D, cdcl_twl_stgy_restart_prog_wl) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}⟩nres_rel›
unfolding uncurry_def cdcl_twl_stgy_restart_prog_wl_D_def
cdcl_twl_stgy_restart_prog_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
restart_prog_wl_D_restart_prog_wl[THEN fref_to_Down_curry2]
cdcl_twl_o_prog_wl_D_spec'[THEN fref_to_Down]
unit_propagation_outer_loop_wl_D_spec'[THEN fref_to_Down]
WHILEIT_refine[where R=‹bool_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩r nat_rel›])
subgoal by auto
subgoal unfolding cdcl_twl_stgy_restart_abs_wl_D_inv_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
definition cdcl_twl_stgy_restart_prog_early_wl_D
:: "nat twl_st_wl ⇒ nat twl_st_wl nres"
where
‹cdcl_twl_stgy_restart_prog_early_wl_D S⇩0 = do {
ebrk ← RES UNIV;
(ebrk, brk, T, n) ← WHILE⇩T⇗λ(_, brk, T, n). cdcl_twl_stgy_restart_abs_wl_D_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(_, brk, S, n).
do {
T ← unit_propagation_outer_loop_wl_D S;
(brk, T) ← cdcl_twl_o_prog_wl_D T;
(T, n) ← restart_prog_wl_D T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0::nat twl_st_wl, 0);
if ¬brk then do {
(brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_D_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop_wl_D S;
(brk, T) ← cdcl_twl_o_prog_wl_D T;
(T, n) ← restart_prog_wl_D T n brk;
RETURN (brk, T, n)
})
(False, T::nat twl_st_wl, n);
RETURN T
}
else RETURN T
}›
lemma cdcl_twl_stgy_restart_prog_early_wl_D_cdcl_twl_stgy_restart_prog_early_wl:
‹(cdcl_twl_stgy_restart_prog_early_wl_D, cdcl_twl_stgy_restart_prog_early_wl) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} →⇩f
⟨{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}⟩nres_rel›
unfolding uncurry_def cdcl_twl_stgy_restart_prog_early_wl_D_def
cdcl_twl_stgy_restart_prog_early_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
restart_prog_wl_D_restart_prog_wl[THEN fref_to_Down_curry2]
cdcl_twl_o_prog_wl_D_spec'[THEN fref_to_Down]
unit_propagation_outer_loop_wl_D_spec'[THEN fref_to_Down]
WHILEIT_refine[where R=‹bool_rel ×⇩r bool_rel ×⇩r {(S, T). (S, T) ∈ Id ∧
literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩r nat_rel›]
WHILEIT_refine[where R=‹bool_rel ×⇩r {(S, T). (S, T) ∈ Id ∧
literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩r nat_rel›])
subgoal by auto
subgoal unfolding cdcl_twl_stgy_restart_abs_wl_D_inv_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal unfolding cdcl_twl_stgy_restart_abs_wl_D_inv_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
definition cdcl_twl_stgy_restart_prog_bounded_wl_D
:: "nat twl_st_wl ⇒ (bool × nat twl_st_wl) nres"
where
‹cdcl_twl_stgy_restart_prog_bounded_wl_D S⇩0 = do {
ebrk ← RES UNIV;
(ebrk, brk, T, n) ← WHILE⇩T⇗λ(_, brk, T, n). cdcl_twl_stgy_restart_abs_wl_D_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(_, brk, S, n).
do {
T ← unit_propagation_outer_loop_wl_D S;
(brk, T) ← cdcl_twl_o_prog_wl_D T;
(T, n) ← restart_prog_wl_D T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0::nat twl_st_wl, 0);
RETURN (brk, T)
}›
lemma cdcl_twl_stgy_restart_prog_bounded_wl_D_cdcl_twl_stgy_restart_prog_bounded_wl:
‹(cdcl_twl_stgy_restart_prog_bounded_wl_D, cdcl_twl_stgy_restart_prog_bounded_wl) ∈
{(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S} →⇩f
⟨bool_rel ×⇩r {(S, T). (S, T) ∈ Id ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S}⟩nres_rel›
unfolding uncurry_def cdcl_twl_stgy_restart_prog_bounded_wl_D_def
cdcl_twl_stgy_restart_prog_bounded_wl_def
apply (intro frefI nres_relI)
apply (refine_vcg
restart_prog_wl_D_restart_prog_wl[THEN fref_to_Down_curry2]
cdcl_twl_o_prog_wl_D_spec'[THEN fref_to_Down]
unit_propagation_outer_loop_wl_D_spec'[THEN fref_to_Down]
WHILEIT_refine[where R=‹bool_rel ×⇩r bool_rel ×⇩r {(S, T). (S, T) ∈ Id ∧
literals_are_ℒ⇩i⇩n (all_atms_st S) S} ×⇩r nat_rel›])
subgoal by auto
subgoal unfolding cdcl_twl_stgy_restart_abs_wl_D_inv_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
end
end