theory Watched_Literals_List
imports WB_More_Refinement_List Watched_Literals_Algorithm CDCL.DPLL_CDCL_W_Implementation
Refine_Monadic.Refine_Monadic
begin
lemma mset_take_mset_drop_mset: ‹(λx. mset (take 2 x) + mset (drop 2 x)) = mset›
unfolding mset_append[symmetric] append_take_drop_id ..
lemma mset_take_mset_drop_mset': ‹mset (take 2 x) + mset (drop 2 x) = mset x›
unfolding mset_append[symmetric] append_take_drop_id ..
lemma uminus_lit_of_image_mset:
‹{#- lit_of x . x ∈# A#} = {#- lit_of x. x ∈# B#} ⟷
{#lit_of x . x ∈# A#} = {#lit_of x. x ∈# B#}›
for A :: ‹('a literal, 'a literal, 'b) annotated_lit multiset›
proof -
have 1: ‹(λx. -lit_of x) `# A = uminus `# lit_of `# A›
for A :: ‹('d::uminus, 'd, 'e) annotated_lit multiset›
by auto
show ?thesis
unfolding 1
by (rule inj_image_mset_eq_iff) (auto simp: inj_on_def)
qed
section ‹Second Refinement: Lists as Clause›
subsection ‹Types›
type_synonym 'v clauses_to_update_l = ‹nat multiset›
type_synonym 'v clause_l = ‹'v literal list›
type_synonym 'v clauses_l = ‹(nat, ('v clause_l × bool)) fmap›
type_synonym 'v cconflict = ‹'v clause option›
type_synonym 'v cconflict_l = ‹'v literal list option›
type_synonym 'v twl_st_l =
‹('v, nat) ann_lits × 'v clauses_l ×
'v cconflict × 'v clauses × 'v clauses × 'v clauses_to_update_l × 'v lit_queue›
fun clauses_to_update_l :: ‹'v twl_st_l ⇒ 'v clauses_to_update_l› where
‹clauses_to_update_l (_, _, _, _, _, WS, _) = WS›
fun get_trail_l :: ‹'v twl_st_l ⇒ ('v, nat) ann_lit list› where
‹get_trail_l (M, _, _, _, _, _, _) = M›
fun set_clauses_to_update_l :: ‹'v clauses_to_update_l ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹set_clauses_to_update_l WS (M, N, D, NE, UE, _, Q) = (M, N, D, NE, UE, WS, Q)›
fun literals_to_update_l :: ‹'v twl_st_l ⇒ 'v clause› where
‹literals_to_update_l (_, _, _, _, _, _, Q) = Q›
fun set_literals_to_update_l :: ‹'v clause ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹set_literals_to_update_l Q (M, N, D, NE, UE, WS, _) = (M, N, D, NE, UE, WS, Q)›
fun get_conflict_l :: ‹'v twl_st_l ⇒ 'v cconflict› where
‹get_conflict_l (_, _, D, _, _, _, _) = D›
fun get_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses_l› where
‹get_clauses_l (M, N, D, NE, UE, WS, Q) = N›
fun get_unit_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_clauses_l (M, N, D, NE, UE, WS, Q) = NE + UE›
fun get_unit_init_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_init_clauses_l (M, N, D, NE, UE, WS, Q) = NE›
fun get_unit_learned_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_learned_clauses_l (M, N, D, NE, UE, WS, Q) = UE›
fun get_init_clauses :: ‹'v twl_st ⇒ 'v twl_clss› where
‹get_init_clauses (M, N, U, D, NE, UE, WS, Q) = N›
fun get_unit_init_clauses :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_init_clauses (M, N, D, NE, UE, WS, Q) = NE›
fun get_unit_learned_clss :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_learned_clss (M, N, D, NE, UE, WS, Q) = UE›
lemma state_decomp_to_state:
‹(case S of (M, N, U, D, NE, UE, WS, Q) ⇒ P M N U D NE UE WS Q) =
P (get_trail S) (get_init_clauses S) (get_learned_clss S) (get_conflict S)
(unit_init_clauses S) (get_init_learned_clss S)
(clauses_to_update S)
(literals_to_update S)›
by (cases S) auto
lemma state_decomp_to_state_l:
‹(case S of (M, N, D, NE, UE, WS, Q) ⇒ P M N D NE UE WS Q) =
P (get_trail_l S) (get_clauses_l S) (get_conflict_l S)
(get_unit_init_clauses_l S) (get_unit_learned_clauses_l S)
(clauses_to_update_l S)
(literals_to_update_l S)›
by (cases S) auto
definition set_conflict' :: ‹'v clause option ⇒ 'v twl_st ⇒ 'v twl_st› where
‹set_conflict' = (λC (M, N, U, D, NE, UE, WS, Q). (M, N, U, C, NE, UE, WS, Q))›
abbreviation watched_l :: ‹'a clause_l ⇒ 'a clause_l› where
‹watched_l l ≡ take 2 l›
abbreviation unwatched_l :: ‹'a clause_l ⇒ 'a clause_l› where
‹unwatched_l l ≡ drop 2 l›
fun twl_clause_of :: ‹'a clause_l ⇒ 'a clause twl_clause› where
‹twl_clause_of l = TWL_Clause (mset (watched_l l)) (mset (unwatched_l l))›
abbreviation clause_in :: ‹'v clauses_l ⇒ nat ⇒ 'v clause_l› (infix "∝" 101) where
‹N ∝ i ≡ fst (the (fmlookup N i))›
abbreviation clause_upd :: ‹'v clauses_l ⇒ nat ⇒ 'v clause_l ⇒ 'v clauses_l› where
‹clause_upd N i C ≡ fmupd i (C, snd (the (fmlookup N i))) N›
text ‹Taken from \<^term>‹fun_upd›.›
nonterminal updclsss and updclss
syntax
"_updclss" :: "'a clauses_l ⇒ 'a ⇒ updclss" ("(2_ ↪/ _)")
"" :: "updbind ⇒ updbinds" ("_")
"_updclsss":: "updclss ⇒ updclsss ⇒ updclsss" ("_,/ _")
"_Updateclss" :: "'a ⇒ updclss ⇒ 'a" ("_/'((_)')" [1000, 0] 900)
translations
"_Updateclss f (_updclsss b bs)" ⇌ "_Updateclss (_Updateclss f b) bs"
"f(x ↪ y)" ⇌ "CONST clause_upd f x y"
inductive convert_lit
:: ‹'v clauses_l ⇒ 'v clauses ⇒ ('v, nat) ann_lit ⇒ ('v, 'v clause) ann_lit ⇒ bool›
where
‹convert_lit N E (Decided K) (Decided K)› |
‹convert_lit N E (Propagated K C) (Propagated K C')›
if ‹C' = mset (N ∝ C)› and ‹C ≠ 0› |
‹convert_lit N E (Propagated K C) (Propagated K C')›
if ‹C = 0› and ‹C' ∈# E›
definition convert_lits_l where
‹convert_lits_l N E = ⟨p2rel (convert_lit N E)⟩ list_rel›
lemma convert_lits_l_nil[simp]:
‹([], a) ∈ convert_lits_l N E ⟷ a = []›
‹(b, []) ∈ convert_lits_l N E ⟷ b = []›
by (auto simp: convert_lits_l_def)
lemma convert_lits_l_cons[simp]:
‹(L # M, L' # M') ∈ convert_lits_l N E ⟷
convert_lit N E L L' ∧ (M, M') ∈ convert_lits_l N E›
by (auto simp: convert_lits_l_def p2rel_def)
lemma take_convert_lits_lD:
‹(M, M') ∈ convert_lits_l N E ⟹
(take n M, take n M') ∈ convert_lits_l N E›
by (auto simp: convert_lits_l_def list_rel_def)
lemma convert_lits_l_consE:
‹(Propagated L C # M, x) ∈ convert_lits_l N E ⟹
(⋀L' C' M'. x = Propagated L' C' # M' ⟹ (M, M') ∈ convert_lits_l N E ⟹
convert_lit N E (Propagated L C) (Propagated L' C') ⟹ P) ⟹ P›
by (cases x) (auto simp: convert_lit.simps)
lemma convert_lits_l_append[simp]:
‹length M1 = length M1' ⟹
(M1 @ M2, M1' @ M2') ∈ convert_lits_l N E ⟷ (M1, M1') ∈ convert_lits_l N E ∧
(M2, M2') ∈ convert_lits_l N E ›
by (auto simp: convert_lits_l_def list_rel_append2 list_rel_imp_same_length)
lemma convert_lits_l_map_lit_of: ‹(ay, bq) ∈ convert_lits_l N e ⟹ map lit_of ay = map lit_of bq›
apply (induction ay arbitrary: bq)
subgoal by auto
subgoal for L M bq by (cases bq) (auto simp: convert_lit.simps)
done
lemma convert_lits_l_tlD:
‹(M, M') ∈ convert_lits_l N E ⟹
(tl M, tl M') ∈ convert_lits_l N E›
by (cases M; cases M') auto
lemma get_clauses_l_set_clauses_to_update_l[simp]:
‹get_clauses_l (set_clauses_to_update_l WC S) = get_clauses_l S›
by (cases S) auto
lemma get_trail_l_set_clauses_to_update_l[simp]:
‹get_trail_l (set_clauses_to_update_l WC S) = get_trail_l S›
by (cases S) auto
lemma get_trail_set_clauses_to_update[simp]:
‹get_trail (set_clauses_to_update WC S) = get_trail S›
by (cases S) auto
abbreviation resolve_cls_l where
‹resolve_cls_l L D' E ≡ union_mset_list (remove1 (-L) D') (remove1 L E)›
lemma mset_resolve_cls_l_resolve_cls[iff]:
‹mset (resolve_cls_l L D' E) = cdcl⇩W_restart_mset.resolve_cls L (mset D') (mset E)›
by (auto simp: union_mset_list[symmetric])
lemma resolve_cls_l_nil_iff:
‹resolve_cls_l L D' E = [] ⟷ cdcl⇩W_restart_mset.resolve_cls L (mset D') (mset E) = {#}›
by (metis mset_resolve_cls_l_resolve_cls mset_zero_iff)
lemma lit_of_convert_lit[simp]:
‹convert_lit N E L L' ⟹ lit_of L' = lit_of L›
by (auto simp: p2rel_def convert_lit.simps)
lemma is_decided_convert_lit[simp]:
‹convert_lit N E L L' ⟹ is_decided L' ⟷ is_decided L›
by (cases L) (auto simp: p2rel_def convert_lit.simps)
lemma defined_lit_convert_lits_l[simp]: ‹(M, M') ∈ convert_lits_l N E ⟹
defined_lit M' = defined_lit M›
apply (induction M arbitrary: M')
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: defined_lit_cons)
done
lemma no_dup_convert_lits_l[simp]: ‹(M, M') ∈ convert_lits_l N E ⟹
no_dup M' ⟷ no_dup M›
apply (induction M arbitrary: M')
subgoal by auto
subgoal for L M M'
by (cases M') auto
done
lemma
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
count_decided_convert_lits_l[simp]:
‹count_decided M' = count_decided M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
lemma
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
get_level_convert_lits_l[simp]:
‹get_level M' = get_level M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(fastforce simp: convert_lits_l_def p2rel_def get_level_cons_if split: if_splits)+
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def get_level_cons_if)
done
lemma
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
get_maximum_level_convert_lits_l[simp]:
‹get_maximum_level M' = get_maximum_level M›
by (intro ext, rule get_maximum_level_cong)
(use assms in auto)
lemma list_of_l_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹lits_of_l M' = lits_of_l M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
lemma is_proped_hd_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E› and ‹M ≠ []›
shows ‹is_proped (hd M') ⟷ is_proped (hd M)›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def convert_lit.simps)
done
lemma is_decided_hd_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E› and ‹M ≠ []›
shows
‹is_decided (hd M') ⟷ is_decided (hd M)›
by (meson assms(1) assms(2) is_decided_no_proped_iff is_proped_hd_convert_lits_l)
lemma lit_of_hd_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E› and ‹M ≠ []›
shows
‹lit_of (hd M') = lit_of (hd M)›
by (cases M; cases M') (use assms in auto)
lemma lit_of_l_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹lit_of ` set M' = lit_of ` set M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
text ‹The order of the assumption is important for simpler use.›
lemma convert_lits_l_extend_mono:
assumes ‹(a,b) ∈ convert_lits_l N E›
‹∀L i. Propagated L i ∈ set a ⟶ mset (N∝i) = mset (N'∝i)› and ‹E ⊆# E'›
shows
‹(a,b) ∈ convert_lits_l N' E'›
using assms
apply (induction a arbitrary: b rule: ann_lit_list_induct)
subgoal by auto
subgoal for l A b
by (cases b)
(auto simp: convert_lits_l_def p2rel_def convert_lit.simps)
subgoal for l C A b
by (cases b)
(auto simp: convert_lits_l_def p2rel_def convert_lit.simps)
done
lemma convert_lits_l_nil_iff[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹M' = [] ⟷ M = []›
using assms by auto
lemma convert_lits_l_atm_lits_of_l:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows ‹atm_of ` lits_of_l M = atm_of ` lits_of_l M'›
using assms by auto
lemma convert_lits_l_true_clss_clss[simp]:
‹(M, M') ∈ convert_lits_l N E ⟹ M' ⊨as C ⟷ M ⊨as C›
unfolding true_annots_true_cls
by (auto simp: p2rel_def)
lemma convert_lit_propagated_decided[iff]:
‹convert_lit b d (Propagated x21 x22) (Decided x1) ⟷ False›
by (auto simp: convert_lit.simps)
lemma convert_lit_decided[iff]:
‹convert_lit b d (Decided x1) (Decided x2) ⟷ x1 = x2›
by (auto simp: convert_lit.simps)
lemma convert_lit_decided_propagated[iff]:
‹convert_lit b d (Decided x1) (Propagated x21 x22) ⟷ False›
by (auto simp: convert_lit.simps)
lemma convert_lits_l_lit_of_mset[simp]:
‹(a, af) ∈ convert_lits_l N E ⟹ lit_of `# mset af = lit_of `# mset a›
apply (induction a arbitrary: af)
subgoal by auto
subgoal for L M af
by (cases af) auto
done
lemma convert_lits_l_imp_same_length:
‹(a, b) ∈ convert_lits_l N E ⟹ length a = length b›
by (auto simp: convert_lits_l_def list_rel_imp_same_length)
lemma convert_lits_l_decomp_ex:
assumes
H: ‹(Decided K # a, M2) ∈ set (get_all_ann_decomposition x)› and
xxa: ‹(x, xa) ∈ convert_lits_l aa ac›
shows ‹∃M2. (Decided K # drop (length xa - length a) xa, M2)
∈ set (get_all_ann_decomposition xa)› (is ?decomp) and
‹(a, drop (length xa - length a) xa) ∈ convert_lits_l aa ac› (is ?a)
proof -
from H obtain M3 where
x: ‹x = M3 @ M2 @ Decided K # a›
by blast
obtain M3' M2' a' where
xa: ‹xa = M3' @ M2' @ Decided K # a'› and
‹(M3, M3') ∈ convert_lits_l aa ac› and
‹(M2, M2') ∈ convert_lits_l aa ac› and
aa': ‹(a, a') ∈ convert_lits_l aa ac›
using xxa unfolding x
by (auto simp: list_rel_append1 convert_lits_l_def p2rel_def convert_lit.simps
list_rel_split_right_iff)
then have a': ‹a' = drop (length xa - length a) xa› and [simp]: ‹length xa ≥ length a›
unfolding xa by (auto simp: convert_lits_l_imp_same_length)
show ?decomp
using get_all_ann_decomposition_ex[of K a' ‹M3' @ M2'›]
unfolding xa
unfolding a'
by auto
show ?a
using aa' unfolding a' .
qed
lemma in_convert_lits_lD:
‹K ∈ set TM ⟹
(M, TM) ∈ convert_lits_l N NE ⟹
∃K'. K' ∈ set M ∧ convert_lit N NE K' K›
by (auto 5 5 simp: convert_lits_l_def list_rel_append2 dest!: split_list p2relD
elim!: list_relE)
lemma in_convert_lits_lD2:
‹K ∈ set M ⟹
(M, TM) ∈ convert_lits_l N NE ⟹
∃K'. K' ∈ set TM ∧ convert_lit N NE K K'›
by (auto 5 5 simp: convert_lits_l_def list_rel_append1 dest!: split_list p2relD
elim!: list_relE)
lemma convert_lits_l_filter_decided: ‹(S, S') ∈ convert_lits_l M N ⟹
map lit_of (filter is_decided S') = map lit_of (filter is_decided S)›
apply (induction S arbitrary: S')
subgoal by auto
subgoal for L S S'
by (cases S') auto
done
lemma convert_lits_lI:
‹length M = length M' ⟹ (⋀i. i < length M ⟹ convert_lit N NE (M!i) (M'!i)) ⟹
(M, M') ∈ convert_lits_l N NE›
by (auto simp: convert_lits_l_def list_rel_def p2rel_def list_all2_conv_all_nth)
abbreviation ran_mf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
‹ran_mf N ≡ fst `# ran_m N›
abbreviation learned_clss_l :: ‹'v clauses_l ⇒ ('v clause_l × bool) multiset› where
‹learned_clss_l N ≡ {#C ∈# ran_m N. ¬snd C#}›
abbreviation learned_clss_lf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
‹learned_clss_lf N ≡ fst `# learned_clss_l N›
definition get_learned_clss_l where
‹get_learned_clss_l S = learned_clss_lf (get_clauses_l S)›
abbreviation init_clss_l :: ‹'v clauses_l ⇒ ('v clause_l × bool) multiset› where
‹init_clss_l N ≡ {#C ∈# ran_m N. snd C#}›
abbreviation init_clss_lf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
‹init_clss_lf N ≡ fst `# init_clss_l N›
abbreviation all_clss_l :: ‹'v clauses_l ⇒ ('v clause_l × bool) multiset› where
‹all_clss_l N ≡ init_clss_l N + learned_clss_l N›
lemma all_clss_l_ran_m[simp]:
‹all_clss_l N = ran_m N›
by (metis multiset_partition)
abbreviation all_clss_lf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
‹all_clss_lf N ≡ init_clss_lf N + learned_clss_lf N›
lemma all_clss_lf_ran_m: ‹all_clss_lf N = fst `# ran_m N›
by (metis (no_types) image_mset_union multiset_partition)
abbreviation irred :: ‹'v clauses_l ⇒ nat ⇒ bool› where
‹irred N C ≡ snd (the (fmlookup N C))›
definition irred' where ‹irred' = irred›
lemma ran_m_ran: ‹fset_mset (ran_m N) = fmran N›
unfolding ran_m_def ran_def
apply (auto simp: fmlookup_ran_iff dom_m_def elim!: fmdomE)
apply (metis fmdomE notin_fset option.sel)
by (metis (no_types, lifting) fmdomI fmember.rep_eq image_iff option.sel)
fun get_learned_clauses_l :: ‹'v twl_st_l ⇒ 'v clause_l multiset› where
‹get_learned_clauses_l (M, N, D, NE, UE, WS, Q) = learned_clss_lf N›
lemma ran_m_clause_upd:
assumes
NC: ‹C ∈# dom_m N›
shows ‹ran_m (N(C ↪ C')) =
add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (ran_m N))›
proof -
define N' where
‹N' = fmdrop C N›
have N_N': ‹dom_m N = add_mset C (dom_m N')›
using NC unfolding N'_def by auto
have ‹C ∉# dom_m N'›
using NC distinct_mset_dom[of N] unfolding N_N' by auto
then show ?thesis
by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong)
qed
lemma ran_m_mapsto_upd:
assumes
NC: ‹C ∈# dom_m N›
shows ‹ran_m (fmupd C C' N) =
add_mset C' (remove1_mset (N ∝ C, irred N C) (ran_m N))›
proof -
define N' where
‹N' = fmdrop C N›
have N_N': ‹dom_m N = add_mset C (dom_m N')›
using NC unfolding N'_def by auto
have ‹C ∉# dom_m N'›
using NC distinct_mset_dom[of N] unfolding N_N' by auto
then show ?thesis
by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong)
qed
lemma ran_m_mapsto_upd_notin:
assumes
NC: ‹C ∉# dom_m N›
shows ‹ran_m (fmupd C C' N) = add_mset C' (ran_m N)›
using NC
by (auto simp: ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong split: if_splits)
lemma learned_clss_l_update[simp]:
‹bh ∈# dom_m ax ⟹ size (learned_clss_l (ax(bh ↪ C))) = size (learned_clss_l ax)›
by (auto simp: ran_m_clause_upd size_Diff_singleton_if dest!: multi_member_split)
(auto simp: ran_m_def)
lemma Ball_ran_m_dom:
‹(∀x∈#ran_m N. P (fst x)) ⟷ (∀x∈#dom_m N. P (N ∝ x))›
by (auto simp: ran_m_def)
lemma Ball_ran_m_dom_struct_wf:
‹(∀x∈#ran_m N. struct_wf_twl_cls (twl_clause_of (fst x))) ⟷
(∀x∈# dom_m N. struct_wf_twl_cls (twl_clause_of (N ∝ x)))›
by (rule Ball_ran_m_dom)
lemma init_clss_lf_fmdrop[simp]:
‹irred N C ⟹ C ∈# dom_m N ⟹ init_clss_lf (fmdrop C N) = remove1_mset (N∝C) (init_clss_lf N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma init_clss_lf_fmdrop_irrelev[simp]:
‹¬irred N C ⟹ init_clss_lf (fmdrop C N) = init_clss_lf N›
using distinct_mset_dom[of N]
apply (cases ‹C ∈# dom_m N›)
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma learned_clss_lf_lf_fmdrop[simp]:
‹¬irred N C ⟹ C ∈# dom_m N ⟹ learned_clss_lf (fmdrop C N) = remove1_mset (N∝C) (learned_clss_lf N)›
using distinct_mset_dom[of N]
apply (cases ‹C ∈# dom_m N›)
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma learned_clss_l_l_fmdrop: ‹¬ irred N C ⟹ C ∈# dom_m N ⟹
learned_clss_l (fmdrop C N) = remove1_mset (the (fmlookup N C)) (learned_clss_l N)›
using distinct_mset_dom[of N]
apply (cases ‹C ∈# dom_m N›)
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma learned_clss_lf_lf_fmdrop_irrelev[simp]:
‹irred N C ⟹ learned_clss_lf (fmdrop C N) = learned_clss_lf N›
using distinct_mset_dom[of N]
apply (cases ‹C ∈# dom_m N›)
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma ran_mf_lf_fmdrop[simp]:
‹C ∈# dom_m N ⟹ ran_mf (fmdrop C N) = remove1_mset (N∝C) (ran_mf N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›] dest!: multi_member_split)
lemma ran_mf_lf_fmdrop_notin[simp]:
‹C ∉# dom_m N ⟹ ran_mf (fmdrop C N) = ran_mf N›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›] dest!: multi_member_split)
lemma lookup_None_notin_dom_m[simp]:
‹fmlookup N i = None ⟷ i ∉# dom_m N›
by (auto simp: dom_m_def fmlookup_dom_iff fmember.rep_eq[symmetric])
text ‹While it is tempting to mark the two following theorems as [simp], this would break more
simplifications since \<^term>‹ran_mf› is only an abbreviation for \<^term>‹ran_m›.
›
lemma ran_m_fmdrop:
‹C ∈# dom_m N ⟹ ran_m (fmdrop C N) = remove1_mset (N ∝ C, irred N C) (ran_m N)›
using distinct_mset_dom[of N]
by (cases ‹fmlookup N C›)
(auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma ran_m_fmdrop_notin:
‹C ∉# dom_m N ⟹ ran_m (fmdrop C N) = ran_m N›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma init_clss_l_fmdrop_irrelev:
‹¬irred N C ⟹ init_clss_l (fmdrop C N) = init_clss_l N›
using distinct_mset_dom[of N]
apply (cases ‹C ∈# dom_m N›)
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma init_clss_l_fmdrop:
‹irred N C ⟹ C ∈# dom_m N ⟹ init_clss_l (fmdrop C N) = remove1_mset (the (fmlookup N C)) (init_clss_l N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma ran_m_lf_fmdrop:
‹C ∈# dom_m N ⟹ ran_m (fmdrop C N) = remove1_mset (the (fmlookup N C)) (ran_m N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›] dest!: multi_member_split
intro!: image_mset_cong)
definition twl_st_l :: ‹_ ⇒ ('v twl_st_l × 'v twl_st) set› where
‹twl_st_l L =
{((M, N, C, NE, UE, WS, Q), (M', N', U', C', NE', UE', WS', Q')).
(M, M') ∈ convert_lits_l N (NE+UE) ∧
N' = twl_clause_of `# init_clss_lf N ∧
U' = twl_clause_of `# learned_clss_lf N ∧
C' = C ∧
NE' = NE ∧
UE' = UE ∧
WS' = (case L of None ⇒ {#} | Some L ⇒ image_mset (λj. (L, twl_clause_of (N ∝ j))) WS) ∧
Q' = Q
}›
lemma clss_state⇩W_of[twl_st]:
assumes ‹(S, R) ∈ twl_st_l L›
shows
‹init_clss (state⇩W_of R) = mset `# (init_clss_lf (get_clauses_l S)) +
get_unit_init_clauses_l S›
‹learned_clss (state⇩W_of R) = mset `# (learned_clss_lf (get_clauses_l S)) +
get_unit_learned_clauses_l S›
using assms
by (cases S; cases L; auto simp: init_clss.simps learned_clss.simps twl_st_l_def
mset_take_mset_drop_mset'; fail)+
named_theorems twl_st_l ‹Conversions simp rules›
lemma [twl_st_l]:
assumes ‹(S, T) ∈ twl_st_l L›
shows
‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› and
‹get_clauses T = twl_clause_of `# fst `# ran_m (get_clauses_l S)› and
‹get_conflict T = get_conflict_l S› and
‹L = None ⟹ clauses_to_update T = {#}›
‹L ≠ None ⟹ clauses_to_update T =
(λj. (the L, twl_clause_of (get_clauses_l S ∝ j))) `# clauses_to_update_l S› and
‹literals_to_update T = literals_to_update_l S›
‹backtrack_lvl (state⇩W_of T) = count_decided (get_trail_l S)›
‹unit_clss T = get_unit_clauses_l S›
‹cdcl⇩W_restart_mset.clauses (state⇩W_of T) =
mset `# ran_mf (get_clauses_l S) + get_unit_clauses_l S› and
‹no_dup (get_trail T) ⟷ no_dup (get_trail_l S)› and
‹lits_of_l (get_trail T) = lits_of_l (get_trail_l S)› and
‹count_decided (get_trail T) = count_decided (get_trail_l S)› and
‹get_trail T = [] ⟷ get_trail_l S = []› and
‹get_trail T ≠ [] ⟷ get_trail_l S ≠ []› and
‹get_trail T ≠ [] ⟹ is_proped (hd (get_trail T)) ⟷ is_proped (hd (get_trail_l S))›
‹get_trail T ≠ [] ⟹ is_decided (hd (get_trail T)) ⟷ is_decided (hd (get_trail_l S))›
‹get_trail T ≠ [] ⟹ lit_of (hd (get_trail T)) = lit_of (hd (get_trail_l S))›
‹get_level (get_trail T) = get_level (get_trail_l S)›
‹get_maximum_level (get_trail T) = get_maximum_level (get_trail_l S)›
‹get_trail T ⊨as D ⟷ get_trail_l S ⊨as D›
using assms unfolding twl_st_l_def all_clss_lf_ran_m[symmetric]
by (auto split: option.splits simp: trail.simps clauses_def mset_take_mset_drop_mset')
lemma (in -) [twl_st_l]:
‹(S, T)∈twl_st_l b ⟹ get_all_init_clss T = mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses S›
by (cases S; cases T; cases b) (auto simp: twl_st_l_def mset_take_mset_drop_mset')
lemma [twl_st_l]:
assumes ‹(S, T) ∈ twl_st_l L›
shows ‹lit_of ` set (get_trail T) = lit_of ` set (get_trail_l S)›
using twl_st_l[OF assms] unfolding lits_of_def
by simp
lemma [twl_st_l]:
‹get_trail_l (set_literals_to_update_l D S) = get_trail_l S›
by (cases S) auto
fun remove_one_lit_from_wq :: ‹nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹remove_one_lit_from_wq L (M, N, D, NE, UE, WS, Q) = (M, N, D, NE, UE, remove1_mset L WS, Q)›
lemma [twl_st_l]: ‹get_conflict_l (set_clauses_to_update_l W S) = get_conflict_l S›
by (cases S) auto
lemma [twl_st_l]: ‹get_conflict_l (remove_one_lit_from_wq L S) = get_conflict_l S›
by (cases S) auto
lemma [twl_st_l]: ‹literals_to_update_l (set_clauses_to_update_l Cs S) = literals_to_update_l S›
by (cases S) auto
lemma [twl_st_l]: ‹get_unit_clauses_l (set_clauses_to_update_l Cs S) = get_unit_clauses_l S›
by (cases S) auto
lemma [twl_st_l]: ‹get_unit_clauses_l (remove_one_lit_from_wq L S) = get_unit_clauses_l S›
by (cases S) auto
lemma init_clss_state_to_l[twl_st_l]: ‹(S, S') ∈ twl_st_l L ⟹
init_clss (state⇩W_of S') = mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses_l S›
by (cases S) (auto simp: twl_st_l_def init_clss.simps mset_take_mset_drop_mset')
lemma [twl_st_l]:
‹get_unit_init_clauses_l (set_clauses_to_update_l Cs S) = get_unit_init_clauses_l S›
by (cases S; auto; fail)+
lemma [twl_st_l]:
‹get_unit_init_clauses_l (remove_one_lit_from_wq L S) = get_unit_init_clauses_l S›
by (cases S; auto; fail)+
lemma [twl_st_l]:
‹get_clauses_l (remove_one_lit_from_wq L S) = get_clauses_l S›
‹get_trail_l (remove_one_lit_from_wq L S) = get_trail_l S›
by (cases S; auto; fail)+
lemma [twl_st_l]:
‹get_unit_learned_clauses_l (set_clauses_to_update_l Cs S) = get_unit_learned_clauses_l S›
by (cases S) auto
lemma [twl_st_l]:
‹get_unit_learned_clauses_l (remove_one_lit_from_wq L S) = get_unit_learned_clauses_l S›
by (cases S) auto
lemma literals_to_update_l_remove_one_lit_from_wq[simp]:
‹literals_to_update_l (remove_one_lit_from_wq L T) = literals_to_update_l T›
by (cases T) auto
lemma clauses_to_update_l_remove_one_lit_from_wq[simp]:
‹clauses_to_update_l (remove_one_lit_from_wq L T) = remove1_mset L (clauses_to_update_l T)›
by (cases T) auto
declare twl_st_l[simp]
lemma unit_init_clauses_get_unit_init_clauses_l[twl_st_l]:
‹(S, T) ∈ twl_st_l L ⟹ unit_init_clauses T = get_unit_init_clauses_l S›
by (cases S) (auto simp: twl_st_l_def init_clss.simps)
lemma clauses_state_to_l[twl_st_l]: ‹(S, S') ∈ twl_st_l L ⟹
cdcl⇩W_restart_mset.clauses (state⇩W_of S') = mset `# ran_mf (get_clauses_l S) +
get_unit_init_clauses_l S + get_unit_learned_clauses_l S›
apply (subst all_clss_l_ran_m[symmetric])
unfolding image_mset_union
by (cases S) (auto simp: twl_st_l_def init_clss.simps mset_take_mset_drop_mset' clauses_def)
lemma clauses_to_update_l_set_clauses_to_update_l[twl_st_l]:
‹clauses_to_update_l (set_clauses_to_update_l WS S) = WS›
by (cases S) auto
lemma hd_get_trail_twl_st_of_get_trail_l:
‹(S, T) ∈ twl_st_l L ⟹ get_trail_l S ≠ [] ⟹
lit_of (hd (get_trail T)) = lit_of (hd (get_trail_l S))›
by (cases S; cases ‹get_trail_l S›; cases ‹get_trail T›) (auto simp: twl_st_l_def)
lemma twl_st_l_mark_of_hd:
‹(x, y) ∈ twl_st_l b ⟹
get_trail_l x ≠ [] ⟹
is_proped (hd (get_trail_l x)) ⟹
mark_of (hd (get_trail_l x)) > 0 ⟹
mark_of (hd (get_trail y)) = mset (get_clauses_l x ∝ mark_of (hd (get_trail_l x)))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma twl_st_l_lits_of_tl:
‹(x, y) ∈ twl_st_l b ⟹
lits_of_l (tl (get_trail y)) = (lits_of_l (tl (get_trail_l x)))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma twl_st_l_mark_of_is_decided:
‹(x, y) ∈ twl_st_l b ⟹
get_trail_l x ≠ [] ⟹
is_decided (hd (get_trail y)) = is_decided (hd (get_trail_l x))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma twl_st_l_mark_of_is_proped:
‹(x, y) ∈ twl_st_l b ⟹
get_trail_l x ≠ [] ⟹
is_proped (hd (get_trail y)) = is_proped (hd (get_trail_l x))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
fun equality_except_trail :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
‹equality_except_trail (M, N, D, NE, UE, WS, Q) (M', N', D', NE', UE', WS', Q') ⟷
N = N' ∧ D = D' ∧ NE = NE' ∧ UE = UE' ∧ WS = WS' ∧ Q = Q'›
fun equality_except_conflict_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
‹equality_except_conflict_l (M, N, D, NE, UE, WS, Q) (M', N', D', NE', UE', WS', Q') ⟷
M = M' ∧ N = N' ∧ NE = NE' ∧ UE = UE' ∧ WS = WS' ∧ Q = Q'›
lemma equality_except_conflict_l_rewrite:
assumes ‹equality_except_conflict_l S T›
shows
‹get_trail_l S = get_trail_l T› and
‹get_clauses_l S = get_clauses_l T›
using assms by (cases S; cases T; auto; fail)+
lemma equality_except_conflict_l_alt_def:
‹equality_except_conflict_l S T ⟷
get_trail_l S = get_trail_l T ∧ get_clauses_l S = get_clauses_l T ∧
get_unit_init_clauses_l S = get_unit_init_clauses_l T ∧
get_unit_learned_clauses_l S = get_unit_learned_clauses_l T ∧
literals_to_update_l S = literals_to_update_l T ∧
clauses_to_update_l S = clauses_to_update_l T›
by (cases S, cases T) auto
lemma equality_except_conflict_alt_def:
‹equality_except_conflict S T ⟷
get_trail S = get_trail T ∧ get_init_clauses S = get_init_clauses T ∧
get_learned_clss S = get_learned_clss T ∧
get_init_learned_clss S = get_init_learned_clss T ∧
unit_init_clauses S = unit_init_clauses T ∧
literals_to_update S = literals_to_update T ∧
clauses_to_update S = clauses_to_update T›
by (cases S, cases T) auto
subsection ‹Additional Invariants and Definitions›
definition twl_list_invs where
‹twl_list_invs S ⟷
(∀C ∈# clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)) ∧
0 ∉# dom_m (get_clauses_l S) ∧
(∀L C. Propagated L C ∈ set (get_trail_l S) ⟶ (C > 0 ⟶ C ∈# dom_m (get_clauses_l S) ∧
(C > 0 ⟶ L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
(length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0)))) ∧
distinct_mset (clauses_to_update_l S)›
definition polarity where
‹polarity M L =
(if undefined_lit M L then None else if L ∈ lits_of_l M then Some True else Some False)›
lemma polarity_None_undefined_lit: ‹is_None (polarity M L) ⟹ undefined_lit M L›
by (auto simp: polarity_def split: if_splits)
lemma polarity_spec:
assumes ‹no_dup M›
shows
‹RETURN (polarity M L) ≤ SPEC(λv. (v = None ⟷ undefined_lit M L) ∧
(v = Some True ⟷ L ∈ lits_of_l M) ∧ (v = Some False ⟷ -L ∈ lits_of_l M))›
unfolding polarity_def
by refine_vcg
(use assms in ‹auto simp: defined_lit_map lits_of_def atm_of_eq_atm_of uminus_lit_swap
no_dup_cannot_not_lit_and_uminus
split: option.splits›)
lemma polarity_spec':
assumes ‹no_dup M›
shows
‹polarity M L = None ⟷ undefined_lit M L› and
‹polarity M L = Some True ⟷ L ∈ lits_of_l M› and
‹polarity M L = Some False ⟷ -L ∈ lits_of_l M›
unfolding polarity_def
by (use assms in ‹auto simp: defined_lit_map lits_of_def atm_of_eq_atm_of uminus_lit_swap
no_dup_cannot_not_lit_and_uminus
split: option.splits›)
definition find_unwatched_l where
‹find_unwatched_l M C = SPEC (λ(found).
(found = None ⟷ (∀L∈set (unwatched_l C). -L ∈ lits_of_l M)) ∧
(∀j. found = Some j ⟶ (j < length C ∧ (undefined_lit M (C!j) ∨ C!j ∈ lits_of_l M) ∧ j ≥ 2)))›
definition set_conflict_l :: ‹'v clause_l ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹set_conflict_l = (λC (M, N, D, NE, UE, WS, Q). (M, N, Some (mset C), NE, UE, {#}, {#}))›
definition propagate_lit_l :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹propagate_lit_l = (λL' C i (M, N, D, NE, UE, WS, Q).
let N = (if length (N ∝ C) > 2 then N(C ↪ (swap (N ∝ C) 0 (Suc 0 - i))) else N) in
(Propagated L' C # M, N, D, NE, UE, WS, add_mset (-L') Q))›
definition update_clause_l :: ‹nat ⇒ nat ⇒ nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹update_clause_l = (λC i f (M, N, D, NE, UE, WS, Q). do {
let N' = N (C ↪ (swap (N∝C) i f));
RETURN (M, N', D, NE, UE, WS, Q)
})›
definition unit_propagation_inner_loop_body_l_inv
:: ‹'v literal ⇒ nat ⇒ 'v twl_st_l ⇒ bool›
where
‹unit_propagation_inner_loop_body_l_inv L C S ⟷
(∃S'. (set_clauses_to_update_l (clauses_to_update_l S + {#C#}) S, S') ∈ twl_st_l (Some L) ∧
twl_struct_invs S' ∧
twl_stgy_invs S' ∧
C ∈# dom_m (get_clauses_l S) ∧
C > 0 ∧
0 < length (get_clauses_l S ∝ C) ∧
no_dup (get_trail_l S) ∧
(if (get_clauses_l S ∝ C) ! 0 = L then 0 else 1) < length (get_clauses_l S ∝ C) ∧
1 - (if (get_clauses_l S ∝ C) ! 0 = L then 0 else 1) < length (get_clauses_l S ∝ C) ∧
L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
get_conflict_l S = None
)
›
definition unit_propagation_inner_loop_body_l :: ‹'v literal ⇒ nat ⇒
'v twl_st_l ⇒ 'v twl_st_l nres› where
‹unit_propagation_inner_loop_body_l L C S = do {
ASSERT(unit_propagation_inner_loop_body_l_inv L C S);
K ← SPEC(λK. K ∈ set (get_clauses_l S ∝ C));
let val_K = polarity (get_trail_l S) K;
if val_K = Some True then RETURN S
else do {
let i = (if (get_clauses_l S ∝ C) ! 0 = L then 0 else 1);
let L' = (get_clauses_l S ∝ C) ! (1 - i);
let val_L' = polarity (get_trail_l S) L';
if val_L' = Some True
then RETURN S
else do {
f ← find_unwatched_l (get_trail_l S) (get_clauses_l S ∝ C);
case f of
None ⇒
if val_L' = Some False
then RETURN (set_conflict_l (get_clauses_l S ∝ C) S)
else RETURN (propagate_lit_l L' C i S)
| Some f ⇒ do {
ASSERT(f < length (get_clauses_l S ∝ C));
let K = (get_clauses_l S ∝ C)!f;
let val_K = polarity (get_trail_l S) K;
if val_K = Some True then
RETURN S
else
update_clause_l C i f S
}
}
}
}›
lemma refine_add_invariants:
assumes
‹(f S) ≤ SPEC(λS'. Q S')› and
‹y ≤ ⇓ {(S, S'). P S S'} (f S)›
shows ‹y ≤ ⇓ {(S, S'). P S S' ∧ Q S'} (f S)›
using assms unfolding pw_le_iff pw_conc_inres pw_conc_nofail by force
lemma clauses_tuple[simp]:
‹cdcl⇩W_restart_mset.clauses (M, {#f x . x ∈# init_clss_l N#} + NE,
{#f x . x ∈# learned_clss_l N#} + UE, D) = {#f x. x ∈# all_clss_l N#} + NE + UE›
by (auto simp: clauses_def simp flip: image_mset_union)
lemma valid_enqueued_alt_simps[simp]:
‹valid_enqueued S ⟷
(∀(L, C) ∈# clauses_to_update S. L ∈# watched C ∧ C ∈# get_clauses S ∧
-L ∈ lits_of_l (get_trail S) ∧ get_level (get_trail S) L = count_decided (get_trail S)) ∧
(∀L ∈# literals_to_update S.
-L ∈ lits_of_l (get_trail S) ∧ get_level (get_trail S) L = count_decided (get_trail S))›
by (cases S) auto
declare valid_enqueued.simps[simp del]
lemma set_clauses_simp[simp]:
‹f ` {a. a ∈# ran_m N ∧ ¬ snd a} ∪ f ` {a. a ∈# ran_m N ∧ snd a} ∪ A =
f ` {a. a ∈# ran_m N} ∪ A›
by auto
lemma init_clss_l_clause_upd:
‹C ∈# dom_m N ⟹ irred N C ⟹
init_clss_l (N(C ↪ C')) =
add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (init_clss_l N))›
by (auto simp: ran_m_mapsto_upd)
lemma init_clss_l_mapsto_upd:
‹C ∈# dom_m N ⟹ irred N C ⟹
init_clss_l (fmupd C (C', True) N) =
add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (init_clss_l N))›
by (auto simp: ran_m_mapsto_upd)
lemma learned_clss_l_mapsto_upd:
‹C ∈# dom_m N ⟹ ¬irred N C ⟹
learned_clss_l (fmupd C (C', False) N) =
add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (learned_clss_l N))›
by (auto simp: ran_m_mapsto_upd)
lemma init_clss_l_mapsto_upd_irrel: ‹C ∈# dom_m N ⟹ ¬irred N C ⟹
init_clss_l (fmupd C (C', False) N) = init_clss_l N›
by (auto simp: ran_m_mapsto_upd)
lemma init_clss_l_mapsto_upd_irrel_notin: ‹C ∉# dom_m N ⟹
init_clss_l (fmupd C (C', False) N) = init_clss_l N›
by (auto simp: ran_m_mapsto_upd_notin)
lemma learned_clss_l_mapsto_upd_irrel: ‹C ∈# dom_m N ⟹ irred N C ⟹
learned_clss_l (fmupd C (C', True) N) = learned_clss_l N›
by (auto simp: ran_m_mapsto_upd)
lemma learned_clss_l_mapsto_upd_notin: ‹C ∉# dom_m N ⟹
learned_clss_l (fmupd C (C', False) N) = add_mset (C', False) (learned_clss_l N)›
by (auto simp: ran_m_mapsto_upd_notin)
lemma in_ran_mf_clause_inI[intro]:
‹C ∈# dom_m N ⟹ i = irred N C ⟹ (N ∝ C, i) ∈# ran_m N›
by (auto simp: ran_m_def dom_m_def)
lemma init_clss_l_mapsto_upd_notin:
‹C ∉# dom_m N ⟹ init_clss_l (fmupd C (C', True) N) =
add_mset (C', True) (init_clss_l N)›
by (auto simp: ran_m_mapsto_upd_notin)
lemma learned_clss_l_mapsto_upd_notin_irrelev: ‹C ∉# dom_m N ⟹
learned_clss_l (fmupd C (C', True) N) = learned_clss_l N›
by (auto simp: ran_m_mapsto_upd_notin)
lemma clause_twl_clause_of: ‹clause (twl_clause_of C) = mset C› for C
by (cases C; cases ‹tl C›) auto
lemma learned_clss_l_l_fmdrop_irrelev: ‹irred N C ⟹
learned_clss_l (fmdrop C N) = learned_clss_l N›
using distinct_mset_dom[of N]
apply (cases ‹C ∈# dom_m N›)
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)
lemma init_clss_l_fmdrop_if:
‹C ∈# dom_m N ⟹ init_clss_l (fmdrop C N) = (if irred N C then remove1_mset (the (fmlookup N C)) (init_clss_l N)
else init_clss_l N)›
by (auto simp: init_clss_l_fmdrop init_clss_l_fmdrop_irrelev)
lemma init_clss_l_fmupd_if:
‹C' ∉# dom_m new ⟹ init_clss_l (fmupd C' D new) = (if snd D then add_mset D (init_clss_l new) else init_clss_l new)›
by (cases D) (auto simp: init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_notin)
lemma learned_clss_l_fmdrop_if:
‹C ∈# dom_m N ⟹ learned_clss_l (fmdrop C N) = (if ¬irred N C then remove1_mset (the (fmlookup N C)) (learned_clss_l N)
else learned_clss_l N)›
by (auto simp: learned_clss_l_l_fmdrop learned_clss_l_l_fmdrop_irrelev)
lemma learned_clss_l_fmupd_if:
‹C' ∉# dom_m new ⟹ learned_clss_l (fmupd C' D new) = (if ¬snd D then add_mset D (learned_clss_l new) else learned_clss_l new)›
by (cases D) (auto simp: learned_clss_l_mapsto_upd_notin_irrelev
learned_clss_l_mapsto_upd_notin)
lemma unit_propagation_inner_loop_body_l:
fixes i C :: nat and S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› and L :: ‹'v literal›
defines
C'[simp]: ‹C' ≡ get_clauses_l S ∝ C›
assumes
SS': ‹(S, S') ∈ twl_st_l (Some L)› and
WS: ‹C ∈# clauses_to_update_l S› and
struct_invs: ‹twl_struct_invs S'› and
add_inv: ‹twl_list_invs S› and
stgy_inv: ‹twl_stgy_invs S'›
shows
‹unit_propagation_inner_loop_body_l L C
(set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S) ≤
⇓ {(S, S''). (S, S'') ∈ twl_st_l (Some L) ∧ twl_list_invs S ∧ twl_stgy_invs S'' ∧
twl_struct_invs S''}
(unit_propagation_inner_loop_body L (twl_clause_of C')
(set_clauses_to_update (clauses_to_update (S') - {#(L, twl_clause_of C')#}) S'))›
(is ‹?A ≤ ⇓ _ ?B›)
proof -
let ?S = ‹set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S›
obtain M N D NE UE WS Q where S: ‹S = (M, N, D, NE, UE, WS, Q)›
by (cases S) auto
have C_N_U: ‹C ∈# dom_m (get_clauses_l S)›
using add_inv WS SS' by (auto simp: twl_list_invs_def)
let ?M = ‹get_trail_l S›
let ?N = ‹get_clauses_l S›
let ?WS = ‹clauses_to_update_l S›
let ?Q = ‹literals_to_update_l S›
define i :: nat where ‹i ≡ (if get_clauses_l S∝C!0 = L then 0 else 1)›
let ?L = ‹C' ! i›
let ?L' = ‹C' ! (Suc 0 - i)›
have inv: ‹twl_st_inv S'› and
cdcl_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')› and
valid: ‹valid_enqueued S'›
using struct_invs WS by (auto simp: twl_struct_invs_def)
have
w_q_inv: ‹clauses_to_update_inv S'› and
dist: ‹distinct_queued S'› and
no_dup: ‹no_duplicate_queued S'› and
confl: ‹get_conflict S' ≠ None ⟹ clauses_to_update S' = {#} ∧ literals_to_update S' = {#}›
using struct_invs unfolding twl_struct_invs_def by fast+
have n_d: ‹no_dup ?M› and confl_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of S')›
using cdcl_inv SS' unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: trail.simps comp_def twl_st)
then have consistent: ‹- L ∉ lits_of_l ?M› if ‹L ∈ lits_of_l ?M› for L
using consistent_interp_def distinct_consistent_interp that by blast
have cons_M: ‹consistent_interp (lits_of_l ?M)›
using n_d distinct_consistent_interp by fast
let ?C' = ‹twl_clause_of C'›
have C'_N_U_or: ‹?C' ∈# twl_clause_of `# (init_clss_lf ?N) ∨
?C' ∈# twl_clause_of `# learned_clss_lf ?N›
using WS valid SS'
unfolding union_iff[symmetric] image_mset_union[symmetric] mset_append[symmetric]
by (auto simp: twl_struct_invs_def
split: prod.splits simp del: twl_clause_of.simps)
have struct: ‹struct_wf_twl_cls ?C'›
using C_N_U inv SS' WS valid unfolding valid_enqueued_alt_simps
by (auto simp: twl_st_inv_alt_def Ball_ran_m_dom_struct_wf
simp del: twl_clause_of.simps)
have C'_N_U: ‹?C' ∈# twl_clause_of `# all_clss_lf ?N›
using C'_N_U_or
unfolding union_iff[symmetric] image_mset_union[symmetric] mset_append[symmetric] .
have watched_C': ‹mset (watched_l C') = {#?L, ?L'#}›
using struct i_def SS' by (cases C) (auto simp: length_list_2 take_2_if)
then have mset_watched_C: ‹mset (watched_l C') = {#watched_l C' ! i, watched_l C' ! (Suc 0 - i)#}›
using i_def by (cases ‹twl_clause_of (get_clauses_l S ∝ C)›) (auto simp: take_2_if)
have two_le_length_C: ‹2 ≤ length C'›
by (metis length_take linorder_not_le min_less_iff_conj numeral_2_eq_2 order_less_irrefl
size_add_mset size_eq_0_iff_empty size_mset watched_C')
obtain WS' where WS'_def: ‹?WS = add_mset C WS'›
using multi_member_split[OF WS] by auto
then have WS'_def': ‹WS = add_mset C WS'›
unfolding S by auto
have L: ‹L ∈ set (watched_l C')› and uL_M: ‹-L ∈ lits_of_l (get_trail_l S)›
using valid SS' by (auto simp: WS'_def)
have C'_i[simp]: ‹C'!i = L›
using L two_le_length_C by (auto simp: take_2_if i_def split: if_splits)
then have [simp]: ‹?N∝C!i = L›
by auto
have C_0: ‹C > 0› and C_neq_0[iff]: ‹C ≠ 0›
using assms(3,5) unfolding twl_list_invs_def by (auto dest!: multi_member_split)
have pre_inv: ‹unit_propagation_inner_loop_body_l_inv L C ?S›
unfolding unit_propagation_inner_loop_body_l_inv_def
proof (rule exI[of _ S'], intro conjI)
have S_readd_C_S: ‹set_clauses_to_update_l (clauses_to_update_l ?S + {#C#}) ?S = S›
unfolding S WS'_def' by auto
show ‹(set_clauses_to_update_l
(clauses_to_update_l ?S + {#C#})
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S),
S') ∈ twl_st_l (Some L)›
using SS' unfolding S_readd_C_S .
show ‹twl_stgy_invs S'› ‹twl_struct_invs S'›
using assms by fast+
show ‹C ∈# dom_m (get_clauses_l ?S)›
using assms C_N_U by auto
show ‹C > 0›
by (rule C_0)
show ‹(if get_clauses_l ?S ∝ C ! 0 = L then 0 else 1) < length (get_clauses_l ?S ∝ C)›
using two_le_length_C by auto
show ‹1 - (if get_clauses_l ?S ∝ C ! 0 = L then 0 else 1) < length (get_clauses_l ?S ∝ C)›
using two_le_length_C by auto
show ‹length (get_clauses_l ?S ∝ C) > 0›
using two_le_length_C by auto
show ‹no_dup (get_trail_l ?S)›
using n_d by auto
show ‹L ∈ set (watched_l (get_clauses_l ?S ∝ C))›
using L by auto
show ‹get_conflict_l ?S = None›
using confl SS' WS by (cases ‹get_conflict_l S›) (auto dest: in_diffD)
qed
have i_def': ‹i = (if get_clauses_l ?S ∝ C ! 0 = L then 0 else 1)›
unfolding i_def by auto
have ‹twl_list_invs ?S›
using add_inv C_N_U unfolding twl_list_invs_def S
by (auto dest: in_diffD)
then have upd_rel: ‹(?S,
set_clauses_to_update (remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S')
∈ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}›
using SS' WS
by (auto simp: twl_st_l_def image_mset_remove1_mset_if)
have ‹twl_list_invs (set_conflict_l (get_clauses_l ?S ∝ C) ?S)›
using add_inv C_N_U unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def S
set_conflict_l_def mset_take_mset_drop_mset')
then have confl_rel: ‹(set_conflict_l (get_clauses_l ?S ∝ C) ?S,
set_conflicting (twl_clause_of C')
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S'))
∈ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}›
using SS' WS by (auto simp: twl_st_l_def image_mset_remove1_mset_if set_conflicting_def
set_conflict_l_def mset_take_mset_drop_mset')
have propa_rel:
‹(propagate_lit_l (get_clauses_l ?S ∝ C ! (1 - i)) C i
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S),
propagate_lit L' (twl_clause_of C')
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S'))
∈ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}›
if
‹(get_clauses_l ?S ∝ C ! (1 - i), L') ∈ Id› and
L'_undef: ‹- L' ∉ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S')) ›
‹L' ∉ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S'))
S'))›
for L'
proof -
have [simp]: ‹mset (swap (N ∝ C) 0 (Suc 0 - i)) = mset (N ∝ C)›
apply (subst swap_multiset)
using two_le_length_C unfolding i_def
by (auto simp: S)
have mset_un_watched_swap:
‹mset (watched_l (swap (N ∝ C) 0 (Suc 0 - i))) = mset (watched_l (N ∝ C))›
‹mset (unwatched_l (swap (N ∝ C) 0 (Suc 0 - i))) = mset (unwatched_l (N ∝ C))›
using two_le_length_C unfolding i_def
apply (auto simp: S take_2_if)
by (auto simp: S swap_def)
have irred_init: ‹irred N C ⟹ (N ∝ C, True) ∈# init_clss_l N›
using C_N_U by (auto simp: S ran_def)
have init_unchanged: ‹{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)))#} =
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l N#}›
using C_N_U
by (cases ‹irred N C›) (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
mset_un_watched_swap init_clss_l_mapsto_upd_irrel
dest: multi_member_split[OF irred_init])
have irred_init: ‹¬irred N C ⟹ (N ∝ C, False) ∈# learned_clss_l N›
using C_N_U by (auto simp: S ran_def)
have learned_unchanged: ‹{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)))#} =
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l N#}›
using C_N_U
by (cases ‹irred N C›) (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
mset_un_watched_swap learned_clss_l_mapsto_upd
learned_clss_l_mapsto_upd_irrel
dest: multi_member_split[OF irred_init])
have [simp]: ‹{#(L, TWL_Clause (mset (watched_l
(fst (the (if C = x
then Some (swap (N ∝ C) 0 (Suc 0 - i), irred N C)
else fmlookup N x)))))
(mset (unwatched_l
(fst (the (if C = x
then Some (swap (N ∝ C) 0 (Suc 0 - i), irred N C)
else fmlookup N x))))))
. x ∈# WS#} = {#(L, TWL_Clause (mset (watched_l (N ∝ x))) (mset (unwatched_l (N ∝ x))))
. x ∈# WS#}›
by (rule image_mset_cong) (auto simp: mset_un_watched_swap)
have C'_0i: ‹C' ! (Suc 0 - i) ∈ set (watched_l C')›
using two_le_length_C by (auto simp: take_2_if S i_def)
have nth_swap_isabelle: ‹length a ≥ 2 ⟹ swap a 0 (Suc 0 - i) ! 0 = a ! (Suc 0 - i)›
for a :: ‹'a list›
using two_le_length_C that apply (auto simp: swap_def S i_def)
by (metis (full_types) le0 neq0_conv not_less_eq_eq nth_list_update_eq numeral_2_eq_2)
have [simp]: ‹Propagated La C ∉ set M› for La
proof (rule ccontr)
assume H:‹¬ ?thesis›
then have ‹La ∈ set (watched_l (N ∝ C))› and
‹2 < length (N ∝ C) ⟶ La = N ∝ C ! 0›
using add_inv C_N_U two_le_length_C mset_un_watched_swap C'_0i
unfolding twl_list_invs_def S by auto
moreover have ‹La ∈ lits_of_l M›
using H by (force simp: lits_of_def)
ultimately show False
using L'_undef that SS' uL_M n_d C'_i S watched_C' that(1)
apply (auto simp: S i_def dest: no_dup_consistentD split: if_splits)
apply (metis in_multiset_nempty member_add_mset no_dup_consistentD set_mset_mset)
by (metis (full_types) in_multiset_nempty member_add_mset no_dup_consistentD set_mset_mset)
qed
have ‹twl_list_invs
(Propagated (N ∝ C ! (Suc 0 - i)) C # M, N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)),
D, NE, UE, remove1_mset C WS, add_mset (- N ∝ C ! (Suc 0 - i)) Q)›
using add_inv C_N_U two_le_length_C mset_un_watched_swap C'_0i
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def
set_conflict_l_def mset_take_mset_drop_mset' S nth_swap_isabelle
dest!: mset_eq_setD)
moreover have
‹convert_lit (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i))) (NE + UE)
(Propagated (N ∝ C ! (Suc 0 - i)) C)
(Propagated (N ∝ C ! (Suc 0 - i)) (mset (N ∝ C)))›
by (auto simp: convert_lit.simps C_0)
moreover have ‹(M, x) ∈ convert_lits_l N (NE + UE) ⟹
(M, x) ∈ convert_lits_l (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i))) (NE + UE)› for x
apply (rule convert_lits_l_extend_mono)
apply assumption
apply auto
done
moreover have
‹convert_lit N (NE + UE)
(Propagated (N ∝ C ! (Suc 0 - i)) C)
(Propagated (N ∝ C ! (Suc 0 - i)) (mset (N ∝ C)))›
by (auto simp: convert_lit.simps C_0)
moreover have ‹twl_list_invs
(Propagated (N ∝ C ! (Suc 0 - i)) C # M, N, D, NE, UE,
remove1_mset C WS, add_mset (- N ∝ C ! (Suc 0 - i)) Q)›
if ‹¬ 2 < length (N ∝ C)›
using add_inv C_N_U two_le_length_C mset_un_watched_swap C'_0i that
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def
set_conflict_l_def mset_take_mset_drop_mset' S nth_swap_isabelle
dest!: mset_eq_setD)
ultimately show ?thesis
using SS' WS that by (auto simp: twl_st_l_def image_mset_remove1_mset_if propagate_lit_def
propagate_lit_l_def mset_take_mset_drop_mset' S learned_unchanged
init_unchanged mset_un_watched_swap intro: convert_lit.simps)
qed
have update_clause_rel: ‹(if polarity
(get_trail_l
(set_clauses_to_update_l
(remove1_mset C (clauses_to_update_l S)) S))
(get_clauses_l
(set_clauses_to_update_l
(remove1_mset C (clauses_to_update_l S)) S) ∝
C !
the K) =
Some True
then RETURN (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)
else update_clause_l C i (the K) (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S))
≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}
(update_clauseS L (twl_clause_of C') (set_clauses_to_update (remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S'))›
(is ‹?update_clss ≤ ⇓ _ _›)
if
L': ‹(get_clauses_l ?S ∝ C ! (1 - i), L') ∈ Id› and
L'_M: ‹L' ∉ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S'))
S'))› and
K: ‹K ∈ {found. (found = None) =
(∀L∈set (unwatched_l (get_clauses_l ?S ∝ C)).
- L ∈ lits_of_l (get_trail_l ?S)) ∧
(∀j. found = Some j ⟶
j < length (get_clauses_l ?S ∝ C) ∧
(undefined_lit (get_trail_l ?S) (get_clauses_l ?S ∝ C ! j) ∨
get_clauses_l ?S ∝ C ! j ∈ lits_of_l (get_trail_l ?S)) ∧
2 ≤ j)}› and
K_None: ‹K ≠ None›
for L' and K
proof -
obtain K' where [simp]: ‹K = Some K'›
using K_None by auto
have
K'_le: ‹K' < length (N ∝ C)› and
K'_2: ‹2 ≤ K'› and
K'_M: ‹undefined_lit M (N ∝ C ! K') ∨
N ∝ C ! K' ∈ lits_of_l (get_trail_l S) ›
using K by (auto simp: S)
have [simp]: ‹N ∝ C ! K' ∈ set (unwatched_l (N ∝ C))›
using K'_le K'_2 by (auto simp: set_drop_conv S)
have [simp]: ‹- N ∝ C ! K' ∉ lits_of_l M ›
using n_d K'_M by (auto simp: S Decided_Propagated_in_iff_in_lits_of_l
dest: no_dup_consistentD)
have irred_init: ‹irred N C ⟹ (N ∝ C, True) ∈# init_clss_l N›
using C_N_U by (auto simp: S)
have init_unchanged: ‹update_clauses
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l N#},
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l N#})
(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C)))) L
(N ∝ C ! K')
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l (N(C ↪ swap (N ∝ C) i K'))#},
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l (N(C ↪ swap (N ∝ C) i K'))#})›
proof (cases ‹irred N C›)
case J_NE: True
have L_L'_UW_N: ‹C' ∈# init_clss_lf N›
using C_N_U J_NE unfolding take_set
by (auto simp: S ran_m_def)
let ?UW = ‹unwatched_l C'›
have TWL_L_L'_UW_N: ‹TWL_Clause {#?L, ?L'#} (mset ?UW) ∈# twl_clause_of `# init_clss_lf N›
using imageI[OF L_L'_UW_N, of twl_clause_of] watched_C' by force
let ?k' = ‹the K - 2›
have ‹?k' < length (unwatched_l C')›
using K'_le two_le_length_C K'_2 by (auto simp: S)
then have H0: ‹TWL_Clause {#?UW ! ?k', ?L'#} (mset (list_update ?UW ?k' ?L)) =
update_clause (TWL_Clause {#?L, ?L'#} (mset ?UW)) ?L (?UW ! ?k')›
by (auto simp: mset_update)
have H3: ‹{#L, C' ! (Suc 0 - i)#} = mset (watched_l (N ∝ C))›
using K'_2 K'_le ‹C > 0› C'_i by (auto simp: S take_2_if C_N_U nth_tl i_def)
have H4: ‹mset (unwatched_l C') = mset (unwatched_l (N ∝ C))›
by (auto simp: S take_2_if C_N_U nth_tl)
let ?New_C = ‹(TWL_Clause {#L, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))›
have wo: "a = a' ⟹ b = b' ⟹ L = L' ⟹ K = K' ⟹ c = c' ⟹
update_clauses a K L b c ⟹
update_clauses a' K' L' b' c'" for a a' b b' K L K' L' c c'
by auto
have [simp]: ‹C' ∈ fst ` {a. a ∈# ran_m N ∧ snd a} ⟷ irred N C›
using C_N_U J_NE unfolding C' S ran_m_def
by auto
have C'_ran_N: ‹(C', True) ∈# ran_m N›
using C_N_U J_NE unfolding C' S S
by auto
have upd: ‹update_clauses
(twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N)
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C'))) (C' ! i) (C' ! the K)
(add_mset (update_clause (TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#}
(mset (unwatched_l C'))) (C' ! i) (C' ! the K))
(remove1_mset
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))
(twl_clause_of `# init_clss_lf N)), twl_clause_of `# learned_clss_lf N)›
by (rule update_clauses.intros(1)[OF TWL_L_L'_UW_N])
have K1: ‹mset (watched_l (swap (N∝C) i K')) = {#N∝C!K', N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
have K2: ‹mset (unwatched_l (swap (N∝C) i K')) = add_mset (N∝C ! i)
(remove1_mset (N∝C ! K') (mset (unwatched_l (N∝C))))›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if mset_update
take_2_if swap_def i_def drop_upd_irrelevant drop_Suc drop_update_swap)
have K3: ‹mset (watched_l (N∝C)) = {#N∝C!i, N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
show ?thesis
apply (rule wo[OF _ _ _ _ _ upd])
subgoal by auto
subgoal by (auto simp: S)
subgoal by auto
subgoal unfolding S H3[symmetric] H4[symmetric] by auto
subgoal
using J_NE C_N_U C' K'_2 K'_le two_le_length_C K1 K2 K3 C'_ran_N
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel)
done
next
assume J_NE: ‹¬irred N C›
have L_L'_UW_N: ‹C' ∈# learned_clss_lf N›
using C_N_U J_NE unfolding take_set
by (auto simp: S ran_m_def)
let ?UW = ‹unwatched_l C'›
have TWL_L_L'_UW_N: ‹TWL_Clause {#?L, ?L'#} (mset ?UW) ∈# twl_clause_of `# learned_clss_lf N›
using imageI[OF L_L'_UW_N, of twl_clause_of] watched_C' by force
let ?k' = ‹the K - 2›
have ‹?k' < length (unwatched_l C')›
using K'_le two_le_length_C K'_2 by (auto simp: S)
then have H0: ‹TWL_Clause {#?UW ! ?k', ?L'#} (mset (list_update ?UW ?k' ?L)) =
update_clause (TWL_Clause {#?L, ?L'#} (mset ?UW)) ?L (?UW ! ?k')›
by (auto simp: mset_update)
have H3: ‹{#L, C' ! (Suc 0 - i)#} = mset (watched_l (N ∝ C))›
using K'_2 K'_le ‹C > 0› C'_i by (auto simp: S take_2_if C_N_U nth_tl i_def)
have H4: ‹mset (unwatched_l C') = mset (unwatched_l (N ∝ C))›
by (auto simp: S take_2_if C_N_U nth_tl)
let ?New_C = ‹(TWL_Clause {#L, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))›
have wo: "a = a' ⟹ b = b' ⟹ L = L' ⟹ K = K' ⟹ c = c' ⟹
update_clauses a K L b c ⟹
update_clauses a' K' L' b' c'" for a a' b b' K L K' L' c c'
by auto
have [simp]: ‹C' ∈ fst ` {a. a ∈# ran_m N ∧ ¬snd a} ⟷ ¬irred N C›
using C_N_U J_NE unfolding C' S ran_m_def
by auto
have C'_ran_N: ‹(C', False) ∈# ran_m N›
using C_N_U J_NE unfolding C' S S
by auto
have upd: ‹update_clauses
(twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N)
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C'))) (C' ! i)
(C' ! the K)
(twl_clause_of `# init_clss_lf N,
add_mset
(update_clause
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C'))) (C' ! i)
(C' ! the K))
(remove1_mset
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))
(twl_clause_of `# learned_clss_lf N)))
›
by (rule update_clauses.intros(2)[OF TWL_L_L'_UW_N])
have K1: ‹mset (watched_l (swap (N∝C) i K')) = {#N∝C!K', N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
have K2: ‹mset (unwatched_l (swap (N∝C) i K')) = add_mset (N∝C ! i)
(remove1_mset (N∝C ! K') (mset (unwatched_l (N∝C))))›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if mset_update
take_2_if swap_def i_def drop_upd_irrelevant drop_Suc drop_update_swap)
have K3: ‹mset (watched_l (N∝C)) = {#N∝C!i, N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
show ?thesis
apply (rule wo[OF _ _ _ _ _ upd])
subgoal by auto
subgoal by (auto simp: S)
subgoal by auto
subgoal unfolding S H3[symmetric] H4[symmetric] by auto
subgoal
using J_NE C_N_U C' K'_2 K'_le two_le_length_C K1 K2 K3 C'_ran_N
by (auto simp: learned_clss_l_mapsto_upd S image_mset_remove1_mset_if
init_clss_l_mapsto_upd_irrel)
done
qed
have ‹distinct_mset WS›
by (metis (full_types) WS'_def WS'_def' add_inv twl_list_invs_def)
then have [simp]: ‹C ∉# WS'›
by (auto simp: WS'_def')
have H: ‹{#(L, TWL_Clause
(mset (watched_l
(fst (the (if C = x then Some (swap (N ∝ C) i K', irred N C)
else fmlookup N x)))))
(mset (unwatched_l
(fst (the (if C = x then Some (swap (N ∝ C) i K', irred N C)
else fmlookup N x)))))). x ∈# WS'#} =
{#(L, TWL_Clause (mset (watched_l (N ∝ x))) (mset (unwatched_l (N ∝ x)))). x ∈# WS'#}›
by (rule image_mset_cong) auto
have [simp]: ‹Propagated La C ∉ set M› for La
proof (rule ccontr)
assume H:‹¬ ?thesis›
then have ‹length (N ∝ C) > 2 ⟹ La = N ∝ C ! 0› and
‹La ∈ set (watched_l (N ∝ C))›
using add_inv C_N_U two_le_length_C
unfolding twl_list_invs_def S by auto
moreover have ‹La ∈ lits_of_l M›
using H by (force simp: lits_of_def)
ultimately show False
using L' L'_M SS' uL_M n_d K'_2 K'_le
by (auto simp: S i_def dest: no_dup_consistentD split: if_splits)
qed
have A: ‹?update_clss = do {let x = N ∝ C ! K';
if x ∈ lits_of_l (get_trail_l (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S))
then RETURN (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)
else update_clause_l C
(if get_clauses_l (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S) ∝
C !
0 =
L
then 0 else 1)
(the K) (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)}›
unfolding i_def
by (auto simp add: S polarity_def dest: in_lits_of_l_defined_litD)
have alt_defs: ‹C' = N ∝ C›
unfolding C' S by auto
have list_invs_blit: ‹twl_list_invs (M, N, D, NE, UE, WS', Q)›
using add_inv C_N_U two_le_length_C
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: S WS'_def')
have ‹twl_list_invs (M, N(C ↪ swap (N ∝ C) i K'), D, NE, UE, WS', Q)›
using add_inv C_N_U two_le_length_C
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def
set_conflict_l_def mset_take_mset_drop_mset' S WS'_def'
dest!: mset_eq_setD)
moreover have ‹(M, x) ∈ convert_lits_l N (NE + UE) ⟹
(M, x) ∈ convert_lits_l (N(C ↪ swap (N ∝ C) i K')) (NE + UE)› for x
apply (rule convert_lits_l_extend_mono)
by auto
ultimately show ?thesis
apply (cases S')
unfolding update_clauseS_def
apply (clarsimp simp only: clauses_to_update.simps set_clauses_to_update.simps)
apply (subst A)
apply refine_vcg
subgoal unfolding C' S by auto
subgoal using L'_M SS' K'_M unfolding C' S by (auto simp: twl_st_l_def)
subgoal using L'_M SS' K'_M unfolding C' S by (auto simp: twl_st_l_def)
subgoal using L'_M SS' K'_M add_inv list_invs_blit unfolding C' S
by (auto simp: twl_st_l_def WS'_def')
subgoal
using SS' init_unchanged unfolding i_def[symmetric] get_clauses_l_set_clauses_to_update_l
by (auto simp: S update_clause_l_def update_clauseS_def twl_st_l_def WS'_def'
RETURN_SPEC_refine RES_RES_RETURN_RES RETURN_def RES_RES2_RETURN_RES H
intro!: RES_refine exI[of _ ‹N ∝ C ! the K›])
done
qed
have H: ‹?A ≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S} ?B›
unfolding unit_propagation_inner_loop_body_l_def unit_propagation_inner_loop_body_def
option.case_eq_if find_unwatched_l_def
apply (rewrite at ‹let _ = if _ ! _ = _then _ else _ in _› Let_def)
apply (rewrite at ‹let _ = polarity _ _ in _› Let_def)
apply (refine_vcg
bind_refine_spec[where M' = ‹RETURN (polarity _ _)›, OF _ polarity_spec]
case_prod_bind[of _ ‹If _ _›]; remove_dummy_vars)
subgoal by (rule pre_inv)
subgoal unfolding C' clause_twl_clause_of by auto
subgoal using SS' by (auto simp: polarity_def Decided_Propagated_in_iff_in_lits_of_l)
subgoal by (rule upd_rel)
subgoal
using mset_watched_C by (auto simp: i_def)
subgoal for L'
using assms by (auto simp: polarity_def Decided_Propagated_in_iff_in_lits_of_l)
subgoal by (rule upd_rel)
subgoal using SS' by auto
subgoal using SS' by (auto simp: Decided_Propagated_in_iff_in_lits_of_l
polarity_def)
subgoal by (rule confl_rel)
subgoal unfolding i_def[symmetric] i_def'[symmetric] by (rule propa_rel)
subgoal by auto
subgoal for L' K unfolding i_def[symmetric] i_def'[symmetric]
by (rule update_clause_rel)
done
have D_None: ‹get_conflict_l S = None›
using confl SS' by (cases ‹get_conflict_l S›) (auto simp: S WS'_def')
have *: ‹unit_propagation_inner_loop_body (C' ! i) (twl_clause_of C')
(set_clauses_to_update (remove1_mset (C' ! i, twl_clause_of 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))›
apply (rule unit_propagation_inner_loop_body(1)[of S' ‹C' ! i› ‹twl_clause_of C'›])
using imageI[OF WS, of ‹(λj. (L, twl_clause_of (N ∝ j)))›]
struct_invs stgy_inv C_N_U WS SS' D_None by auto
have H': ‹?B ≤ SPEC (λS'. twl_stgy_invs S' ∧ twl_struct_invs S')›
using *
by (simp add: weaken_SPEC)
have ‹?A
≤ ⇓ {(S, S'). ((S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S) ∧
(twl_stgy_invs S' ∧ twl_struct_invs S')}
?B›
apply (rule refine_add_invariants)
apply (rule H')
by (rule H)
then show ?thesis by simp
qed
lemma unit_propagation_inner_loop_body_l2:
assumes
SS': ‹(S, S') ∈ twl_st_l (Some L)› and
WS: ‹C ∈# clauses_to_update_l S› and
struct_invs: ‹twl_struct_invs S'› and
add_inv: ‹twl_list_invs S› and
stgy_inv: ‹twl_stgy_invs S'›
shows
‹(unit_propagation_inner_loop_body_l L C
(set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S),
unit_propagation_inner_loop_body L (twl_clause_of (get_clauses_l S ∝ C))
(set_clauses_to_update
(remove1_mset (L, twl_clause_of (get_clauses_l S ∝ C))
(clauses_to_update S')) S'))
∈ ⟨{(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧
twl_struct_invs S'}⟩nres_rel›
using unit_propagation_inner_loop_body_l[OF assms]
by (auto simp: nres_rel_def)
text ‹This a work around equality: it allows to instantiate variables that appear in goals by
hand in a reasonable way (\<^text>‹rule\_tac I=x in EQI)›.›
definition EQ where
[simp]: ‹EQ = (=)›
lemma EQI: "EQ I I"
by auto
lemma unit_propagation_inner_loop_body_l_unit_propagation_inner_loop_body:
‹EQ L'' L'' ⟹
(uncurry2 unit_propagation_inner_loop_body_l, uncurry2 unit_propagation_inner_loop_body) ∈
{(((L, C), S0), ((L', C'), S0')). ∃S S'. L = L' ∧ C' = (twl_clause_of (get_clauses_l S ∝ C)) ∧
S0 = (set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S) ∧
S0' = (set_clauses_to_update
(remove1_mset (L, twl_clause_of (get_clauses_l S ∝ C))
(clauses_to_update S')) S') ∧
(S, S') ∈ twl_st_l (Some L) ∧ L = L'' ∧
C ∈# clauses_to_update_l S ∧ twl_struct_invs S' ∧ twl_list_invs S ∧ twl_stgy_invs S'} →⇩f
⟨{(S, S'). (S, S') ∈ twl_st_l (Some L'') ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧
twl_struct_invs S'}⟩nres_rel›
apply (intro frefI nres_relI)
using unit_propagation_inner_loop_body_l
by fastforce
definition select_from_clauses_to_update :: ‹'v twl_st_l ⇒ ('v twl_st_l × nat) nres› where
‹select_from_clauses_to_update S = SPEC (λ(S', C). C ∈# clauses_to_update_l S ∧
S' = set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S)›
definition unit_propagation_inner_loop_l_inv where
‹unit_propagation_inner_loop_l_inv L = (λ(S, n).
(∃S'. (S, S') ∈ twl_st_l (Some L) ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
twl_list_invs S ∧ (clauses_to_update S' ≠ {#} ∨ n > 0 ⟶ get_conflict S' = None) ∧
-L ∈ lits_of_l (get_trail_l S)))›
definition unit_propagation_inner_loop_body_l_with_skip where
‹unit_propagation_inner_loop_body_l_with_skip L = (λ(S, n). do {
ASSERT (clauses_to_update_l S ≠ {#} ∨ n > 0);
ASSERT(unit_propagation_inner_loop_l_inv L (S, n));
b ← SPEC(λb. (b ⟶ n > 0) ∧ (¬b ⟶ clauses_to_update_l S ≠ {#}));
if ¬b then do {
ASSERT (clauses_to_update_l S ≠ {#});
(S', C) ← select_from_clauses_to_update S;
T ← unit_propagation_inner_loop_body_l L C S';
RETURN (T, if get_conflict_l T = None then n else 0)
} else RETURN (S, n-1)
})›
definition unit_propagation_inner_loop_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹unit_propagation_inner_loop_l L S⇩0 = do {
n ← SPEC(λ_::nat. True);
(S, n) ← WHILE⇩T⇗unit_propagation_inner_loop_l_inv L⇖
(λ(S, n). clauses_to_update_l S ≠ {#} ∨ n > 0)
(unit_propagation_inner_loop_body_l_with_skip L)
(S⇩0, n);
RETURN S
}›
lemma set_mset_clauses_to_update_l_set_mset_clauses_to_update_spec:
assumes ‹(S, S') ∈ twl_st_l (Some L)›
shows
‹RES (set_mset (clauses_to_update_l S)) ≤ ⇓ {(C, (L', C')). L' = L ∧
C' = twl_clause_of (get_clauses_l S ∝ C)}
(RES (set_mset (clauses_to_update S')))›
proof -
obtain M N D NE UE WS Q where
S: ‹S = (M, N, D, NE, UE, WS, Q)›
by (cases S) auto
show ?thesis
using assms unfolding S by (auto simp add: Bex_def twl_st_l_def intro!: RES_refine)
qed
lemma refine_add_inv:
fixes f :: ‹'a ⇒ 'a nres› and f' :: ‹'b ⇒ 'b nres› and h :: ‹'b ⇒ 'a›
assumes
‹(f', f) ∈ {(S, S'). S' = h S ∧ R S} → ⟨{(T, T'). T' = h T ∧ P' T}⟩ nres_rel›
(is ‹_ ∈ ?R → ⟨{(T, T'). ?H T T' ∧ P' T}⟩ nres_rel›)
assumes
‹⋀S. R S ⟹ f (h S) ≤ SPEC (λT. Q T)›
shows
‹(f', f) ∈ ?R → ⟨{(T, T'). ?H T T' ∧ P' T ∧ Q (h T)}⟩ nres_rel›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by fastforce
lemma refine_add_inv_generalised:
fixes f :: ‹'a ⇒ 'b nres› and f' :: ‹'c ⇒ 'd nres›
assumes
‹(f', f) ∈ A →⇩f ⟨B⟩ nres_rel›
assumes
‹⋀S S'. (S, S') ∈ A ⟹ f S' ≤ RES C›
shows
‹(f', f) ∈ A →⇩f ⟨{(T, T'). (T, T') ∈ B ∧ T' ∈ C}⟩ nres_rel›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
fref_param1[symmetric]
by fastforce
lemma refine_add_inv_pair:
fixes f :: ‹'a ⇒ ('c × 'a) nres› and f' :: ‹'b ⇒ ('c × 'b) nres› and h :: ‹'b ⇒ 'a›
assumes
‹(f', f) ∈ {(S, S'). S' = h S ∧ R S} → ⟨{(S, S'). (fst S' = h' (fst S) ∧
snd S' = h (snd S)) ∧ P' S}⟩ nres_rel› (is ‹_ ∈ ?R → ⟨{(S, S'). ?H S S' ∧ P' S}⟩ nres_rel›)
assumes
‹⋀S. R S ⟹ f (h S) ≤ SPEC (λT. Q (snd T))›
shows
‹(f', f) ∈ ?R → ⟨{(S, S'). ?H S S' ∧ P' S ∧ Q (h (snd S))}⟩ nres_rel›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by fastforce
lemma clauses_to_update_l_empty_tw_st_of_Some_None[simp]:
‹clauses_to_update_l S = {#} ⟹ (S, S')∈ twl_st_l (Some L) ⟷ (S, S') ∈ twl_st_l None›
by (cases S) (auto simp: twl_st_l_def)
lemma cdcl_twl_cp_in_trail_stays_in:
‹cdcl_twl_cp⇧*⇧* S' aa ⟹ - x1 ∈ lits_of_l (get_trail S') ⟹ - x1 ∈ lits_of_l (get_trail aa)›
by (induction rule: rtranclp_induct)
(auto elim!: cdcl_twl_cpE)
lemma cdcl_twl_cp_in_trail_stays_in_l:
‹(x2, S') ∈ twl_st_l (Some x1) ⟹ cdcl_twl_cp⇧*⇧* S' aa ⟹ - x1 ∈ lits_of_l (get_trail_l x2) ⟹
(a, aa) ∈ twl_st_l (Some x1) ⟹ - x1 ∈ lits_of_l (get_trail_l a)›
using cdcl_twl_cp_in_trail_stays_in[of S' aa ‹x1›]
by (auto simp: twl_st twl_st_l)
lemma unit_propagation_inner_loop_l:
‹(uncurry unit_propagation_inner_loop_l, unit_propagation_inner_loop) ∈
{((L, S), S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_struct_invs S' ∧
twl_stgy_invs S' ∧ twl_list_invs S ∧ -L ∈ lits_of_l (get_trail_l S)} →⇩f
⟨{(T, T'). (T, T') ∈ twl_st_l None ∧ clauses_to_update_l T = {#} ∧
twl_list_invs T ∧ twl_struct_invs T' ∧ twl_stgy_invs T'}⟩ nres_rel›
(is ‹?unit_prop_inner ∈ ?A →⇩f ⟨?B⟩nres_rel›)
proof -
have SPEC_remove: ‹select_from_clauses_to_update S
≤ ⇓ {((T', C), C').
(T', set_clauses_to_update (clauses_to_update S'' - {#C'#}) S'') ∈ twl_st_l (Some L) ∧
T' = set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S ∧
C' ∈# clauses_to_update S'' ∧
C ∈# clauses_to_update_l S ∧
snd C' = twl_clause_of (get_clauses_l S ∝ C)}
(SPEC (λC. C ∈# clauses_to_update S''))›
if ‹(S, S'') ∈ {(T, T'). (T, T') ∈ twl_st_l (Some L) ∧ twl_list_invs T}›
for S :: ‹'v twl_st_l› and S'' L
using that unfolding select_from_clauses_to_update_def
by (auto simp: conc_fun_def image_mset_remove1_mset_if twl_st_l_def)
show ?thesis
unfolding unit_propagation_inner_loop_l_def unit_propagation_inner_loop_def uncurry_def
unit_propagation_inner_loop_body_l_with_skip_def
apply (intro frefI nres_relI)
subgoal for LS S'
apply (rewrite in ‹let _ = set_clauses_to_update _ _ in _› Let_def)
apply (refine_vcg set_mset_clauses_to_update_l_set_mset_clauses_to_update_spec
WHILEIT_refine_genR[where
R = ‹{(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧ clauses_to_update_l T = {#}
∧ twl_struct_invs T' ∧ twl_stgy_invs T'}
×⇩f nat_rel› and
R' = ‹{(T, T'). (T, T') ∈ twl_st_l (Some (fst LS)) ∧ twl_list_invs T}
×⇩f nat_rel›]
unit_propagation_inner_loop_body_l_unit_propagation_inner_loop_body[THEN fref_to_Down_curry2]
SPEC_remove;
remove_dummy_vars)
subgoal by simp
subgoal for x1 x2 n na x x' unfolding unit_propagation_inner_loop_l_inv_def
apply (case_tac x; case_tac x')
apply (simp only: prod.simps)
by (rule exI[of _ ‹fst x'›]) (auto intro: cdcl_twl_cp_in_trail_stays_in_l)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (subst (asm) prod_rel_iff)
apply normalize_goal
apply assumption
apply (rule_tac I=x1 in EQI)
subgoal for x1 x2 n na x1a x2a x1b x2b b ba x1c x2c x1d x2d
apply (subst in_pair_collect_simp)
apply (subst prod.case)+
apply (rule_tac x = x1b in exI)
apply (rule_tac x = x1a in exI)
apply (intro conjI)
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
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
done
qed
definition clause_to_update :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v clauses_to_update_l›where
‹clause_to_update L S =
filter_mset
(λC::nat. L ∈ set (watched_l (get_clauses_l S ∝ C)))
(dom_m (get_clauses_l S))›
lemma distinct_mset_clause_to_update: ‹distinct_mset (clause_to_update L C)›
unfolding clause_to_update_def
apply (rule distinct_mset_filter)
using distinct_mset_dom by blast
lemma in_clause_to_updateD: ‹b ∈# clause_to_update L' T ⟹ b ∈# dom_m (get_clauses_l T)›
by (auto simp: clause_to_update_def)
lemma in_clause_to_update_iff:
‹C ∈# clause_to_update L S ⟷
C ∈# dom_m (get_clauses_l S) ∧ L ∈ set (watched_l (get_clauses_l S ∝ C))›
by (auto simp: clause_to_update_def)
definition select_and_remove_from_literals_to_update :: ‹'v twl_st_l ⇒
('v twl_st_l × 'v literal) nres› where
‹select_and_remove_from_literals_to_update S = SPEC(λ(S', L). L ∈# literals_to_update_l S ∧
S' = set_clauses_to_update_l (clause_to_update L S)
(set_literals_to_update_l (literals_to_update_l S - {#L#}) S))›
definition unit_propagation_outer_loop_l_inv where
‹unit_propagation_outer_loop_l_inv S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
clauses_to_update_l S = {#})›
definition unit_propagation_outer_loop_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹unit_propagation_outer_loop_l S⇩0 =
WHILE⇩T⇗unit_propagation_outer_loop_l_inv⇖
(λS. literals_to_update_l S ≠ {#})
(λS. do {
ASSERT(literals_to_update_l S ≠ {#});
(S', L) ← select_and_remove_from_literals_to_update S;
unit_propagation_inner_loop_l L S'
})
(S⇩0 :: 'v twl_st_l)
›
lemma watched_twl_clause_of_watched: ‹watched (twl_clause_of x) = mset (watched_l x)›
by (cases x) auto
lemma twl_st_of_clause_to_update:
assumes
TT': ‹(T, T') ∈ twl_st_l None› and
‹twl_struct_invs T'›
shows
‹(set_clauses_to_update_l
(clause_to_update L' T)
(set_literals_to_update_l (remove1_mset L' (literals_to_update_l T)) T),
set_clauses_to_update
(Pair L' `# {#C ∈# get_clauses T'. L' ∈# watched C#})
(set_literals_to_update (remove1_mset L' (literals_to_update T'))
T'))
∈ twl_st_l (Some L')›
proof -
obtain M N D NE UE WS Q where
T: ‹T = (M, N, D , NE, UE, WS, Q)›
by (cases T) auto
have
‹{#(L', TWL_Clause (mset (watched_l (N ∝ x)))
(mset (unwatched_l (N ∝ x)))).
x ∈# {#C ∈# dom_m N. L' ∈ set (watched_l (N ∝ C))#}#} =
Pair L' `#
{#C ∈# {#TWL_Clause (mset (watched_l x)) (mset (unwatched_l x)). x ∈# init_clss_lf N#} +
{#TWL_Clause (mset (watched_l x)) (mset (unwatched_l x)). x ∈# learned_clss_lf N#}.
L' ∈# watched C#}›
(is ‹{#(L', ?C x). x ∈# ?S#} = Pair L' `# ?C'›)
proof -
have H: ‹{#f (N ∝ x). x ∈# {#x ∈# dom_m N. P (N ∝ x)#}#} =
{#f (fst x). x ∈# {#C ∈# ran_m N. P (fst C)#}#}› for P and f :: ‹'a literal list ⇒ 'b›
unfolding ran_m_def image_mset_filter_swap2 by auto
have H: ‹{#f (N∝x). x ∈# ?S#} =
{#f (fst x). x ∈# {#C ∈# init_clss_l N. L' ∈ set (watched_l (fst C))#}#} +
{#f (fst x). x ∈# {#C ∈# learned_clss_l N. L' ∈ set (watched_l (fst C))#}#}›
for f :: ‹'a literal list ⇒ 'b›
unfolding image_mset_union[symmetric] filter_union_mset[symmetric]
apply auto
apply (subst H)
..
have L'': ‹{#(L', ?C x). x ∈# ?S#} = Pair L' `# {#?C x. x ∈# ?S#}›
by auto
also have ‹… = Pair L' `# ?C'›
apply (rule arg_cong[of _ _ ‹(`#) (Pair L')›])
unfolding image_mset_union[symmetric] mset_append[symmetric] drop_Suc H
apply simp
apply (subst H)
unfolding image_mset_union[symmetric] mset_append[symmetric] drop_Suc H
filter_union_mset[symmetric] image_mset_filter_swap2
by auto
finally show ?thesis .
qed
then show ?thesis
using TT'
by (cases T') (auto simp del: filter_union_mset
simp: T split_beta clause_to_update_def twl_st_l_def
split: if_splits)
qed
lemma twl_list_invs_set_clauses_to_update_iff:
assumes ‹twl_list_invs T›
shows ‹twl_list_invs (set_clauses_to_update_l WS (set_literals_to_update_l Q T)) ⟷
((∀x∈#WS. case x of C ⇒ C ∈# dom_m (get_clauses_l T)) ∧
distinct_mset WS)›
proof -
obtain M N C NE UE WS Q where
T: ‹T = (M, N, C, NE, UE, WS, Q)›
by (cases T) auto
show ?thesis
using assms
unfolding twl_list_invs_def T by auto
qed
lemma unit_propagation_outer_loop_l_spec:
‹(unit_propagation_outer_loop_l, unit_propagation_outer_loop) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧
twl_stgy_invs S' ∧ twl_list_invs S ∧ clauses_to_update_l S = {#} ∧
get_conflict_l S = None} →⇩f
⟨{(T, T'). (T, T') ∈ twl_st_l None ∧
(twl_list_invs T ∧ twl_struct_invs T' ∧ twl_stgy_invs T' ∧
clauses_to_update_l T = {#}) ∧
literals_to_update T' = {#} ∧ clauses_to_update T' = {#} ∧
no_step cdcl_twl_cp T'}⟩ nres_rel›
(is ‹_ ∈ ?R →⇩f ?I› is ‹_ ∈ _ →⇩f ⟨?B⟩ nres_rel›)
proof -
have H:
‹select_and_remove_from_literals_to_update x
≤ ⇓ {((S', L'), L). L = L' ∧ S' = set_clauses_to_update_l (clause_to_update L x)
(set_literals_to_update_l (remove1_mset L (literals_to_update_l x)) x)}
(SPEC (λL. L ∈# literals_to_update x'))›
if ‹(x, x') ∈ twl_st_l None› for x :: ‹'v twl_st_l› and x' :: ‹'v twl_st›
using that unfolding select_and_remove_from_literals_to_update_def
apply (cases x; cases x')
unfolding conc_fun_def by (clarsimp simp add: twl_st_l_def conc_fun_def)
have H': ‹unit_propagation_outer_loop_l_inv T ⟹
x2 ∈# literals_to_update_l T ⟹ - x2 ∈ lits_of_l (get_trail_l T)›
for S S' T T' L L' C x2
by (auto simp: unit_propagation_outer_loop_l_inv_def twl_st_l_def twl_struct_invs_def)
have H:
‹(unit_propagation_outer_loop_l, unit_propagation_outer_loop) ∈?R →⇩f
⟨{(S, S').
(S, S') ∈ twl_st_l None ∧
clauses_to_update_l S = {#} ∧
twl_list_invs S ∧
twl_struct_invs S' ∧
twl_stgy_invs S'}⟩ nres_rel›
unfolding unit_propagation_outer_loop_l_def unit_propagation_outer_loop_def fref_param1[symmetric]
apply (refine_vcg unit_propagation_inner_loop_l[THEN fref_to_Down_curry_left]
H)
subgoal by simp
subgoal unfolding unit_propagation_outer_loop_l_inv_def by fastforce
subgoal by auto
subgoal by simp
subgoal by fast
subgoal for S S' T T' L L' C x2
by (auto simp add: twl_st_of_clause_to_update twl_list_invs_set_clauses_to_update_iff
intro: cdcl_twl_cp_twl_struct_invs cdcl_twl_cp_twl_stgy_invs
distinct_mset_clause_to_update H'
dest: in_clause_to_updateD)
done
have B: ‹?B = {(T, T'). (T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧
twl_list_invs T ∧
twl_struct_invs T' ∧
twl_stgy_invs T' ∧ clauses_to_update_l T = {#} } ∧
T' ∈ {T'. literals_to_update T' = {#} ∧
clauses_to_update T' = {#} ∧
(∀S'. ¬ cdcl_twl_cp T' S')}}›
by auto
show ?thesis
unfolding B
apply (rule refine_add_inv_generalised)
subgoal
using H apply -
apply (match_spec; (match_fun_rel; match_fun_rel?)+)
apply blast+
done
subgoal for S S'
apply (rule weaken_SPEC[OF unit_propagation_outer_loop[of S']])
apply ((solves auto)+)[4]
using no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp by blast
done
qed
lemma get_conflict_l_get_conflict_state_spec:
assumes ‹(S, S') ∈ twl_st_l None› and ‹twl_list_invs S› and ‹clauses_to_update_l S = {#}›
shows ‹((False, S), (False, S'))
∈ {((brk, S), (brk', S')). brk = brk' ∧ (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
clauses_to_update_l S = {#}}›
using assms by auto
fun lit_and_ann_of_propagated where
‹lit_and_ann_of_propagated (Propagated L C) = (L, C)› |
‹lit_and_ann_of_propagated (Decided _) = undefined›
definition tl_state_l :: ‹'v twl_st_l ⇒ 'v twl_st_l› where
‹tl_state_l = (λ(M, N, D, NE, UE, WS, Q). (tl M, N, D, NE, UE, WS, Q))›
definition resolve_cls_l' :: ‹'v twl_st_l ⇒ nat ⇒ 'v literal ⇒ 'v clause› where
‹resolve_cls_l' S C L =
remove1_mset L (remove1_mset (-L) (the (get_conflict_l S) ∪# mset (get_clauses_l S ∝ C)))›
definition update_confl_tl_l :: ‹nat ⇒ 'v literal ⇒ 'v twl_st_l ⇒ bool × 'v twl_st_l› where
‹update_confl_tl_l = (λC L (M, N, D, NE, UE, WS, Q).
let D = resolve_cls_l' (M, N, D, NE, UE, WS, Q) C L in
(False, (tl M, N, Some D, NE, UE, WS, Q)))›
definition skip_and_resolve_loop_inv_l where
‹skip_and_resolve_loop_inv_l S⇩0 brk S ⟷
(∃S' S⇩0'. (S, S') ∈ twl_st_l None ∧ (S⇩0, S⇩0') ∈ twl_st_l None ∧
skip_and_resolve_loop_inv S⇩0' (brk, S') ∧
twl_list_invs S ∧ clauses_to_update_l S = {#} ∧
(¬is_decided (hd (get_trail_l S)) ⟶ mark_of (hd(get_trail_l S)) > 0))›
definition skip_and_resolve_loop_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹skip_and_resolve_loop_l S⇩0 =
do {
ASSERT(get_conflict_l S⇩0 ≠ None);
(_, S) ←
WHILE⇩T⇗λ(brk, S). skip_and_resolve_loop_inv_l S⇩0 brk S⇖
(λ(brk, S). ¬brk ∧ ¬is_decided (hd (get_trail_l S)))
(λ(_, S).
do {
let D' = the (get_conflict_l S);
let (L, C) = lit_and_ann_of_propagated (hd (get_trail_l S));
if -L ∉# D' then
do {RETURN (False, tl_state_l S)}
else
if get_maximum_level (get_trail_l S) (remove1_mset (-L) D') = count_decided (get_trail_l S)
then
do {RETURN (update_confl_tl_l C L S)}
else
do {RETURN (True, S)}
}
)
(False, S⇩0);
RETURN S
}
›
context
begin
private lemma skip_and_resolve_l_refines:
‹((brkS), brk'S') ∈ {((brk, S), brk', S'). brk = brk' ∧ (S, S') ∈ twl_st_l None ∧
twl_list_invs S ∧ clauses_to_update_l S = {#}} ⟹
brkS = (brk, S) ⟹ brk'S' = (brk', S') ⟹
((False, tl_state_l S), False, tl_state S') ∈ {((brk, S), brk', S'). brk = brk' ∧
(S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}›
by (cases S; cases ‹get_trail_l S›)
(auto simp: twl_list_invs_def twl_st_l_def
resolve_cls_l_nil_iff tl_state_l_def tl_state_def dest: convert_lits_l_tlD)
private lemma skip_and_resolve_skip_refine:
assumes
rel: ‹((brk, S), brk', S') ∈ {((brk, S), brk', S'). brk = brk' ∧
(S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› and
dec: ‹¬ is_decided (hd (get_trail S'))› and
rel': ‹((L, C), L', C') ∈ {((L, C), L', C'). L = L' ∧ C > 0 ∧
C' = mset (get_clauses_l S ∝ C)}› and
LC: ‹lit_and_ann_of_propagated (hd (get_trail_l S)) = (L, C)› and
tr: ‹get_trail_l S ≠ []› and
struct_invs: ‹twl_struct_invs S'› and
stgy_invs: ‹twl_stgy_invs S'› and
lev: ‹count_decided (get_trail_l S) > 0› and
inv: ‹case (brk, S) of (x, xa) ⇒ skip_and_resolve_loop_inv_l S0 x xa›
shows
‹(update_confl_tl_l C L S, False,
update_confl_tl (Some (remove1_mset (- L') (the (get_conflict S')) ∪# remove1_mset L' C')) S')
∈ {((brk, S), brk', S').
brk = brk' ∧
(S, S') ∈ twl_st_l None ∧
twl_list_invs S ∧
clauses_to_update_l S = {#}}›
proof -
obtain M N D NE UE Q where S: ‹S = (Propagated L C # M, N, D, NE, UE, {#}, Q)›
using dec LC tr rel
by (cases S; cases ‹get_trail_l S›; cases ‹get_trail S'›; cases ‹hd (get_trail_l S)›)
(auto simp: twl_st_l_def)
have S': ‹(S, S') ∈ twl_st_l None› and [simp]: ‹L = L'› and
C': ‹C' = mset (get_clauses_l S ∝ C)› and
[simp]: ‹C > 0› ‹C ≠ 0›and
invs_S: ‹twl_list_invs S›
using rel rel' unfolding S by auto
have H: ‹L' ∉# the D ⟹ the D ∪# {#L', aa#} - {#L', - L'#} =
the D ∪# {#aa#} - {#- L'#}›
‹L' ∉# the D ⟹ the D ∪# {#aa, L'#} - {#L', - L'#} =
the D ∪# {#aa#} - {#- L'#}› for aa
by (auto simp: add_mset_commute)
have H': ‹a ≠ -L' ⟹ remove1_mset (- L') (the D) ∪# {#a#} =
remove1_mset (- L') (the D ∪# {#a#})› for a
by (auto simp: sup_union_right_if
dest: in_diffD multi_member_split)
have ‹D ≠ None›
using inv by (auto simp: skip_and_resolve_loop_inv_l_def S
skip_and_resolve_loop_inv_def twl_st_l_def)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of S')› and
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')›
using struct_invs unfolding twl_struct_invs_def by fast+
moreover have ‹Suc 0 ≤ backtrack_lvl (state⇩W_of S')›
using lev S' by (cases S) (auto simp: trail.simps twl_st_l_def)
moreover have ‹is_proped (cdcl⇩W_restart_mset.hd_trail (state⇩W_of S'))›
using dec tr S' by (cases ‹get_trail_l S›)
(auto simp: trail.simps is_decided_no_proped_iff twl_st_l_def)
moreover have ‹mark_of (cdcl⇩W_restart_mset.hd_trail (state⇩W_of S')) = C'›
using dec S' unfolding C' by (cases ‹get_trail S'›)
(auto simp: S trail.simps twl_st_l_def
convert_lit.simps)
ultimately have False: ‹C = 0 ⟹ False›
using C' cdcl⇩W_restart_mset.hd_trail_level_ge_1_length_gt_1[of ‹state⇩W_of S'›]
by (auto simp: is_decided_no_proped_iff)
then have L: ‹length (N ∝ C) > 2 ⟶ L = N ∝ C ! 0› and
C_dom: ‹C ∈# dom_m N› and
L: ‹L ∈ set(watched_l (N ∝ C))›
using invs_S
unfolding S C' by (auto simp: twl_list_invs_def)
moreover {
have ‹twl_st_inv S'›
using struct_invs unfolding S twl_struct_invs_def
by fast
then have
‹∀x∈#ran_m N. struct_wf_twl_cls (twl_clause_of (fst x))›
using struct_invs S' unfolding S twl_st_inv_alt_def
by simp
then have ‹Multiset.Ball (dom_m N) (λC. length (N ∝ C) ≥ 2)›
by (subst (asm) Ball_ran_m_dom_struct_wf) auto
then have ‹length (N ∝ C) ≥ 2›
using ‹C ∈# dom_m N› unfolding S by (auto simp: twl_list_invs_def)
}
moreover {
have
lev_confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of S')› and
M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of S')›
using struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
then have ‹M ⊨as CNot (remove1_mset L (mset (N ∝ C)))›
using S' False
by (force simp: S twl_st_l_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset_state convert_lit.simps
elim!: convert_lits_l_consE)
then have 1: ‹-L' ∉# mset (N ∝ C)›
apply - apply (rule, drule multi_member_split)
using S' M_lev False unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: S twl_st_l_def cdcl⇩W_restart_mset_state split: if_splits
dest: in_lits_of_l_defined_litD)
then have 2:‹remove1_mset (- L') (the D) ∪# mset (tl (N ∝ C)) =
remove1_mset (- L') (the D ∪# mset (tl (N ∝ C)))›
using L by(cases ‹N ∝ C›; cases ‹-L' ∈# mset (N ∝ C)›)
(auto simp: remove1_mset_union_distrib)
have ‹Propagated L C # M ⊨as CNot (the D)›
using S' False lev_confl ‹D ≠ None›
by (force simp: S twl_st_l_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset_state convert_lit.simps)
then have 3: ‹L' ∉# (the D)›
apply - apply (rule, drule multi_member_split)
using S' M_lev False unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: S twl_st_l_def cdcl⇩W_restart_mset_state split: if_splits
dest: in_lits_of_l_defined_litD)
note 1 and 2 and 3
}
ultimately show ?thesis
using invs_S S'
by (cases ‹N ∝ C›; cases ‹tl (N ∝ C)›)
(auto simp: skip_and_resolve_loop_inv_def twl_list_invs_def resolve_cls_l'_def
resolve_cls_l_nil_iff update_confl_tl_l_def update_confl_tl_def twl_st_l_def H H'
S S' C' dest!: False dest: convert_lits_l_tlD)
qed
lemma get_level_same_lits_cong:
assumes
‹map (atm_of o lit_of) M = map (atm_of o lit_of) M'› and
‹map is_decided M = map is_decided M'›
shows ‹get_level M L = get_level M' L›
proof -
have [dest]: ‹map is_decided M = map is_decided zsa ⟹
length (filter is_decided M) = length (filter is_decided zsa)›
for M :: ‹('d, 'e, 'f) annotated_lit list› and zsa :: ‹('g, 'h, 'i) annotated_lit list›
by (induction M arbitrary: zsa) (auto simp: get_level_def)
show ?thesis
using assms
by (induction M arbitrary: M') (auto simp: get_level_def )
qed
lemma clauses_in_unit_clss_have_level0:
assumes
struct_invs: ‹twl_struct_invs T› and
C: ‹C ∈# unit_clss T› and
LC_T: ‹Propagated L C ∈ set (get_trail T)› and
count_dec: ‹0 < count_decided (get_trail T)›
shows
‹get_level (get_trail T) L = 0› (is ?lev_L) and
‹∀K∈# C. get_level (get_trail T) K = 0› (is ?lev_K)
proof -
have
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of T)› and
ent: ‹entailed_clss_inv T›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
obtain K where
‹K ∈# C› and lev_K: ‹get_level (get_trail T) K = 0› and K_M: ‹K ∈ lits_of_l (get_trail T)›
using ent C count_dec by (cases T; cases ‹get_conflict T›) auto
thm entailed_clss_inv.simps
obtain M1 M2 where
M: ‹get_trail T = M2 @ Propagated L C # M1›
using LC_T by (blast elim: in_set_list_format)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T) ›
using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have M1: ‹M1 ⊨as CNot (remove1_mset L C)› and ‹L ∈# C›
using M unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: twl_st)
moreover have n_d: ‹no_dup (get_trail T)›
using lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by (simp add: twl_st)
ultimately have ‹L = K›
using ‹K ∈# C› M K_M
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset
dest: in_lits_of_l_defined_litD no_dup_uminus_append_in_atm_notin
no_dup_appendD no_dup_consistentD)
then show ?lev_L
using lev_K by simp
have count_dec_M1: ‹count_decided M1 = 0›
using M n_d ‹?lev_L› by auto
have ‹get_level (get_trail T) K = 0› if ‹K ∈# C› for K
proof -
have ‹-K ∈ lits_of_l (Propagated (-L) C # M1)›
using M1 M that by (auto simp: true_annots_true_cls_def_iff_negation_in_model remove1_mset_add_mset_If
dest!: multi_member_split dest: in_diffD split: if_splits)
then have ‹get_level (get_trail T) K = get_level (Propagated (-L) C # M1) K›
apply -
apply (subst (2) get_level_skip[symmetric, of M2])
using n_d M by (auto dest: no_dup_uminus_append_in_atm_notin
intro: get_level_same_lits_cong)
then show ?thesis
using count_decided_ge_get_level[of ‹Propagated (-L) C # M1› K] count_dec_M1
by (auto simp: get_level_cons_if split: if_splits)
qed
then show ?lev_K
by fast
qed
lemma clauses_clss_have_level1_notin_unit:
assumes
struct_invs: ‹twl_struct_invs T› and
LC_T: ‹Propagated L C ∈ set (get_trail T)› and
count_dec: ‹0 < count_decided (get_trail T)› and
‹get_level (get_trail T) L > 0›
shows
‹C ∉# unit_clss T›
using clauses_in_unit_clss_have_level0[of T C, OF struct_invs _ LC_T count_dec] assms
by linarith
lemma skip_and_resolve_loop_l_spec:
‹(skip_and_resolve_loop_l, skip_and_resolve_loop) ∈
{(S::'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧
twl_stgy_invs S' ∧
twl_list_invs S ∧ clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧
get_conflict S' ≠ None ∧
0 < count_decided (get_trail_l S)} →⇩f
⟨{(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs 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') ∧
literals_to_update T' = {#} ∧
clauses_to_update_l T = {#} ∧ get_conflict T' ≠ None)}⟩ nres_rel›
(is ‹_ ∈ ?R →⇩f _›)
proof -
have is_proped[iff]: ‹is_proped (hd (get_trail S')) ⟷ is_proped (hd (get_trail_l S))›
if ‹get_trail_l S ≠ []› and
‹(S, S') ∈ twl_st_l None›
for S :: ‹'v twl_st_l› and S'
by (cases S, cases ‹get_trail_l S›; cases ‹hd (get_trail_l S)›)
(use that in ‹auto split: if_splits simp: twl_st_l_def›)
have
mark_ge_0: ‹0 < mark_of (hd (get_trail_l T))› (is ?ge) and
nempty: ‹get_trail_l T ≠ []› ‹get_trail (snd brkT') ≠ []› (is ?nempty)
if
SS': ‹(S, S') ∈ ?R› and
‹get_conflict_l S ≠ None› and
brk_TT': ‹(brkT, brkT')
∈ {((brk, S), brk', S'). brk = brk' ∧ (S, S') ∈ twl_st_l None ∧
twl_list_invs S ∧ clauses_to_update_l S = {#}}› (is ‹_ ∈ ?brk›) and
loop_inv: ‹skip_and_resolve_loop_inv S' brkT'› and
brkT: ‹brkT = (brk, T)› and
dec: ‹¬ is_decided (hd (get_trail_l T))›
for S S' brkT brkT' brk T
proof -
obtain brk' T' where brkT': ‹brkT' = (brk', T')› by (cases brkT')
have ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of T')› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of T')› and
tr: ‹get_trail T' ≠ []› ‹get_trail_l T ≠ []› and
count_dec: ‹count_decided (get_trail_l T) ≠ 0› ‹count_decided (get_trail T') ≠ 0› and
TT': ‹(T,T') ∈ twl_st_l None› and
struct_invs: ‹twl_struct_invs T'›
using loop_inv brk_TT' unfolding twl_struct_invs_def skip_and_resolve_loop_inv_def brkT brkT'
by auto
moreover have ‹Suc 0 ≤ backtrack_lvl (state⇩W_of T')›
using count_dec TT' by (auto simp: trail.simps)
moreover have proped: ‹is_proped (cdcl⇩W_restart_mset.hd_trail (state⇩W_of T'))›
using dec tr TT' by (cases ‹get_trail_l T›)
(auto simp: trail.simps is_decided_no_proped_iff twl_st)
moreover have ‹mark_of (hd (get_trail T')) ∉# unit_clss T'›
using clauses_clss_have_level1_notin_unit(1)[of T' ‹lit_of (hd (get_trail T'))›
‹mark_of (hd (get_trail T'))›] dec struct_invs count_dec tr proped TT'
by (cases ‹get_trail T'›; cases ‹hd (get_trail T')›)
(auto simp: twl_st)
moreover have ‹convert_lit (get_clauses_l T) (unit_clss T') (hd (get_trail_l T))
(hd (get_trail T'))›
using tr dec TT'
by (cases ‹get_trail T'›; cases ‹get_trail_l T›)
(auto simp: twl_st_l_def)
ultimately have ‹mark_of (hd (get_trail_l T)) = 0 ⟹ False›
using tr dec TT' by (cases ‹get_trail_l T›; cases ‹hd (get_trail_l T)›)
(auto simp: trail.simps twl_st convert_lit.simps)
then show ?ge by blast
show ‹get_trail_l T ≠ []› ‹get_trail (snd brkT') ≠ []›
using tr TT' brkT' by auto
qed
have H: ‹RETURN (lit_and_ann_of_propagated (hd (get_trail_l T)))
≤ ⇓ {((L, C), (L', C')). L = L' ∧ C> 0 ∧ C' = mset (get_clauses_l T ∝ C)}
(SPEC (λ(L, C). Propagated L C = hd (get_trail T')))›
if
SS': ‹(S, S') ∈ ?R› and
confl: ‹get_conflict_l S ≠ None› and
brk_TT': ‹(brkT, brkT') ∈ ?brk› and
loop_inv: ‹skip_and_resolve_loop_inv S' brkT'› and
brkT: ‹brkT = (brk, T)› and
dec: ‹¬ is_decided (hd (get_trail_l T))› and
brkT': ‹brkT' = (brk', T')›
for S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› and T T' brk brk' brkT' brkT
using confl brk_TT' loop_inv brkT dec mark_ge_0[OF SS' confl brk_TT' loop_inv brkT dec]
nempty[OF SS' confl brk_TT' loop_inv brkT dec] unfolding brkT'
apply (cases T; cases T'; cases ‹get_trail_l T›; cases ‹hd (get_trail_l T)› ;
cases ‹get_trail T'›; cases ‹hd (get_trail T')›)
apply ((solves ‹force split: if_splits›)+)[15]
unfolding RETURN_def
by (rule RES_refine; solves ‹auto split: if_splits simp: twl_st_l_def convert_lit.simps›)+
have skip_and_resolve_loop_inv_trail_nempty: ‹skip_and_resolve_loop_inv S' (False, S) ⟹
get_trail S ≠ []› for S :: ‹'v twl_st› and S'
unfolding skip_and_resolve_loop_inv_def
by auto
have twl_list_invs_tl_state_l: ‹twl_list_invs S ⟹ twl_list_invs (tl_state_l S)›
for S :: ‹'v twl_st_l›
by (cases S, cases ‹get_trail_l S›) (auto simp: tl_state_l_def twl_list_invs_def)
have clauses_to_update_l_tl_state: ‹clauses_to_update_l (tl_state_l S) = clauses_to_update_l S›
for S :: ‹'v twl_st_l›
by (cases S, cases ‹get_trail_l S›) (auto simp: tl_state_l_def)
have H:
‹(skip_and_resolve_loop_l, skip_and_resolve_loop) ∈ ?R →⇩f
⟨{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
clauses_to_update_l T = {#}}⟩ nres_rel›
supply [[goals_limit=1]]
unfolding skip_and_resolve_loop_l_def skip_and_resolve_loop_def fref_param1[symmetric]
apply (refine_vcg H)
subgoal by auto
apply (rule get_conflict_l_get_conflict_state_spec)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S S' brkT brkT'
unfolding skip_and_resolve_loop_inv_l_def
apply(rule exI[of _ ‹snd brkT'›])
apply(rule exI[of _ S'])
apply (intro conjI impI)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule mark_ge_0)
done
subgoal by (auto dest!: skip_and_resolve_loop_inv_trail_nempty)
apply assumption+
subgoal by auto
apply assumption+
subgoal by auto
subgoal by (drule skip_and_resolve_l_refines) blast+
subgoal by (auto simp: twl_list_invs_tl_state_l)
subgoal by (rule skip_and_resolve_skip_refine)
(auto simp: skip_and_resolve_loop_inv_def)
subgoal by auto
subgoal by auto
done
have H: ‹(skip_and_resolve_loop_l, skip_and_resolve_loop)
∈ ?R →⇩f
⟨{(T::'v twl_st_l, T').
(T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ (twl_list_invs T ∧
clauses_to_update_l T = {#})} ∧
T' ∈ {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')) ∧
literals_to_update T' = {#} ∧
get_conflict T' ≠ None}}⟩nres_rel›
apply (rule refine_add_inv_generalised)
subgoal by (rule H)
subgoal for S S'
apply (rule order_trans)
apply (rule skip_and_resolve_loop_spec[of S'])
by auto
done
show ?thesis
using H apply -
apply (match_spec; (match_fun_rel; match_fun_rel?)+)
by blast+
qed
end
definition find_decomp :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹find_decomp = (λL (M, N, D, NE, UE, WS, Q).
SPEC(λS. ∃K M2 M1. S = (M1, N, D, NE, UE, WS, Q) ∧
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (the D - {#-L#}) + 1))›
lemma find_decomp_alt_def:
‹find_decomp L S =
SPEC(λT. ∃K M2 M1. equality_except_trail S T ∧ get_trail_l T = M1 ∧
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧
get_level (get_trail_l S) K =
get_maximum_level (get_trail_l S) (the (get_conflict_l S) - {#-L#}) + 1)›
unfolding find_decomp_def
by (cases S) force
definition find_lit_of_max_level :: ‹'v twl_st_l ⇒ 'v literal ⇒ 'v literal nres› where
‹find_lit_of_max_level = (λ(M, N, D, NE, UE, WS, Q) L.
SPEC(λL'. L' ∈# the D - {#-L#} ∧ get_level M L' = get_maximum_level M (the D - {#-L#})))›
definition ex_decomp_of_max_lvl :: ‹('v, nat) ann_lits ⇒ 'v cconflict ⇒ 'v literal ⇒ bool› where
‹ex_decomp_of_max_lvl M D L ⟷
(∃K M1 M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (remove1_mset (-L) (the D)) + 1)›
fun add_mset_list :: ‹'a list ⇒ 'a multiset multiset ⇒ 'a multiset multiset› where
‹add_mset_list L UE = add_mset (mset L) UE›
definition (in -)list_of_mset :: ‹'v clause ⇒ 'v clause_l nres› where
‹list_of_mset D = SPEC(λD'. D = mset D')›
fun extract_shorter_conflict_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres›
where
‹extract_shorter_conflict_l (M, N, D, NE, UE, WS, Q) = SPEC(λS.
∃D'. D' ⊆# the D ∧ S = (M, N, Some D', NE, UE, WS, Q) ∧
clause `# twl_clause_of `# ran_mf N + NE + UE ⊨pm D' ∧ -(lit_of (hd M)) ∈# D')›
declare extract_shorter_conflict_l.simps[simp del]
lemmas extract_shorter_conflict_l_def = extract_shorter_conflict_l.simps
lemma extract_shorter_conflict_l_alt_def:
‹extract_shorter_conflict_l S = SPEC(λT.
∃D'. D' ⊆# the (get_conflict_l S) ∧ equality_except_conflict_l S T ∧
get_conflict_l T = Some D' ∧
clause `# twl_clause_of `# ran_mf (get_clauses_l S) + get_unit_clauses_l S ⊨pm D' ∧
-lit_of (hd (get_trail_l S)) ∈# D')›
by (cases S) (auto simp: extract_shorter_conflict_l_def ac_simps)
definition backtrack_l_inv where
‹backtrack_l_inv S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧
get_trail_l S ≠ [] ∧
no_step cdcl⇩W_restart_mset.skip (state⇩W_of S')∧
no_step cdcl⇩W_restart_mset.resolve (state⇩W_of S') ∧
get_conflict_l S ≠ None ∧
twl_struct_invs S' ∧
twl_stgy_invs S' ∧
twl_list_invs S ∧
get_conflict_l S ≠ Some {#})
›
definition get_fresh_index :: ‹'v clauses_l ⇒ nat nres› where
‹get_fresh_index N = SPEC(λi. i > 0 ∧ i ∉# dom_m N)›
definition propagate_bt_l :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹propagate_bt_l = (λL L' (M, N, D, NE, UE, WS, Q). do {
D'' ← list_of_mset (the D);
i ← get_fresh_index N;
RETURN (Propagated (-L) i # M,
fmupd i ([-L, L'] @ (remove1 (-L) (remove1 L' D'')), False) N,
None, NE, UE, WS, {#L#})
})›
definition propagate_unit_bt_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹propagate_unit_bt_l = (λL (M, N, D, NE, UE, WS, Q).
(Propagated (-L) 0 # M, N, None, NE, add_mset (the D) UE, WS, {#L#}))›
definition backtrack_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹backtrack_l S =
do {
ASSERT(backtrack_l_inv S);
let L = lit_of (hd (get_trail_l S));
S ← extract_shorter_conflict_l S;
S ← find_decomp L S;
if size (the (get_conflict_l S)) > 1
then do {
L' ← find_lit_of_max_level S L;
propagate_bt_l L L' S
}
else do {
RETURN (propagate_unit_bt_l L S)
}
}›
lemma backtrack_l_spec:
‹(backtrack_l, backtrack) ∈
{(S::'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ get_conflict_l S ≠ None ∧
get_conflict_l S ≠ Some {#} ∧
clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧ twl_list_invs S ∧
no_step cdcl⇩W_restart_mset.skip (state⇩W_of S') ∧
no_step cdcl⇩W_restart_mset.resolve (state⇩W_of S') ∧
twl_struct_invs S' ∧ twl_stgy_invs S'} →⇩f
⟨{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ get_conflict_l T = None ∧ twl_list_invs T ∧
twl_struct_invs T' ∧ twl_stgy_invs T' ∧ clauses_to_update_l T = {#} ∧
literals_to_update_l T ≠ {#}}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I›)
proof -
have H: ‹find_decomp L S
≤ ⇓ {(T, T'). (T, T') ∈ twl_st_l None ∧ equality_except_trail S T ∧
(∃M. get_trail_l S = M @ get_trail_l T)}
(reduce_trail_bt L' S')›
(is ‹_ ≤ ⇓ ?find_decomp _›)
if
SS': ‹(S, S') ∈ twl_st_l None› and ‹L = lit_of (hd (get_trail_l S))› and
‹L' = lit_of (hd (get_trail S'))› ‹get_trail_l S ≠ []›
for S :: ‹'v twl_st_l› and S' and L' L
unfolding find_decomp_alt_def reduce_trail_bt_def
state_decomp_to_state
apply (subst RES_RETURN_RES)
apply (rule RES_refine)
unfolding in_pair_collect_simp bex_simps
using that apply (auto 5 5 intro!: RES_refine convert_lits_l_decomp_ex)
apply (rule_tac x=‹drop (length (get_trail S') - length a) (get_trail S')› in exI)
apply (intro conjI)
apply (rule_tac x=K in exI)
apply (auto simp: twl_st_l_def
intro: convert_lits_l_decomp_ex)
done
have list_of_mset: ‹list_of_mset D' ≤ SPEC (λc. (c, D'') ∈ {(c, D). D = mset c})›
if ‹D' = D''› for D' :: ‹'v clause› and D''
using that by (cases D'') (auto simp: list_of_mset_def)
have ext: ‹extract_shorter_conflict_l T
≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l None ∧
-lit_of (hd (get_trail_l S)) ∈# the (get_conflict_l S) ∧
the (get_conflict_l S) ⊆# the D⇩0 ∧ equality_except_conflict_l T S ∧ get_conflict_l S ≠ None}
(extract_shorter_conflict T')›
(is ‹_ ≤ ⇓ ?extract _›)
if ‹(T, T') ∈ twl_st_l None› and
‹D⇩0 = get_conflict_l T› and
‹get_trail_l T ≠ []›
for T :: ‹'v twl_st_l› and T' and D⇩0
unfolding extract_shorter_conflict_l_alt_def extract_shorter_conflict_alt_def
apply (rule RES_refine)
unfolding in_pair_collect_simp bex_simps
apply clarify
apply (rule_tac x=‹set_conflict' (Some D') T'› in bexI)
using that
apply (auto simp del: split_paired_Ex equality_except_conflict_l.simps
simp: set_conflict'_def[unfolded state_decomp_to_state]
intro!: RES_refine equality_except_conflict_alt_def[THEN iffD2]
del: split_paired_all)
apply (auto simp: twl_st_l_def equality_except_conflict_l_alt_def)
done
have uhd_in_D: ‹L ∈# the D›
if
inv_s: ‹twl_stgy_invs S'› and
inv: ‹twl_struct_invs S'› and
ns: ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of S')› and
confl:
‹conflicting (state⇩W_of S') ≠ None›
‹conflicting (state⇩W_of S') ≠ Some {#}› and
M_nempty: ‹get_trail_l S ≠ []› and
D: ‹D = get_conflict_l S›
‹L = - lit_of (hd (get_trail_l S))› and
SS': ‹(S, S') ∈ twl_st_l None›
for L M D and S :: ‹'v twl_st_l› and S' :: ‹'v twl_st›
unfolding D
using cdcl⇩W_restart_mset.no_step_skip_hd_in_conflicting[of ‹state⇩W_of S'›,
OF _ _ ns confl] that
by (auto simp: cdcl⇩W_restart_mset_state twl_stgy_invs_def
twl_struct_invs_def twl_st)
have find_lit:
‹find_lit_of_max_level U (lit_of (hd (get_trail_l S)))
≤ SPEC (λL''. L'' ∈# remove1_mset (- lit_of (hd (get_trail S'))) (the (get_conflict U')) ∧
lit_of (hd (get_trail S')) ≠ - L'' ∧
get_level (get_trail U') L'' = get_maximum_level (get_trail U')
(remove1_mset (- lit_of (hd (get_trail S'))) (the (get_conflict U'))))›
(is ‹_ ≤ RES ?find_lit_of_max_level›)
if
UU': ‹(S, S') ∈ ?R› and
bt_inv: ‹backtrack_l_inv S› and
RR': ‹(T, T') ∈ ?extract S (get_conflict_l S)› and
T: ‹(U, U') ∈ ?find_decomp T›
for S S' T T' U U'
proof -
have SS': ‹(S, S') ∈ twl_st_l None› ‹get_trail_l S ≠ []› and
struct_invs: ‹twl_struct_invs S'› ‹get_conflict_l S ≠ None›
using UU' bt_inv by (auto simp: backtrack_l_inv_def)
have ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of S')›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
then have dist: ‹distinct_mset (the (get_conflict_l S))›
using struct_invs SS' unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (cases S) (auto simp: cdcl⇩W_restart_mset_state twl_st)
then have dist: ‹distinct_mset (the (get_conflict_l U))›
using UU' RR' T by (cases S, cases T, cases U, auto intro: distinct_mset_mono)
show ?thesis
using T distinct_mem_diff_mset[OF dist, of _ ‹{#_#}›] SS'
unfolding find_lit_of_max_level_def
state_decomp_to_state_l
by (force simp: uminus_lit_swap)
qed
have propagate_bt:
‹propagate_bt_l (lit_of (hd (get_trail_l S))) L U
≤ SPEC (λc. (c, propagate_bt (lit_of (hd (get_trail S'))) L' U') ∈
{(T, T'). (T, T') ∈ twl_st_l None ∧ clauses_to_update_l T = {#} ∧ twl_list_invs T})›
if
SS': ‹(S, S') ∈ ?R› and
bt_inv: ‹backtrack_l_inv S› and
TT': ‹(T, T') ∈ ?extract S (get_conflict_l S)› and
UU': ‹(U, U') ∈ ?find_decomp T› and
L': ‹L' ∈ ?find_lit_of_max_level S' U'› and
LL': ‹(L, L') ∈ Id› and
size: ‹size (the (get_conflict_l U)) > 1›
for S S' T T' U U' L L'
proof -
obtain MS NS DS NES UES where
S: ‹S = (MS, NS, Some DS, NES, UES, {#}, {#})› and
S_S': ‹(S, S') ∈ twl_st_l None› and
add_invs: ‹twl_list_invs S› and
struct_inv: ‹twl_struct_invs S'› and
stgy_inv: ‹twl_stgy_invs S'› and
nss: ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of S')› and
nsr: ‹no_step cdcl⇩W_restart_mset.resolve (state⇩W_of S')› and
confl: ‹get_conflict_l S ≠ None› ‹get_conflict_l S ≠ Some {#}›
using SS' by (cases S; cases ‹get_conflict_l S›) auto
then obtain DT where
T: ‹T = (MS, NS, Some DT, NES, UES, {#}, {#})› and
T_T': ‹(T, T') ∈ twl_st_l None›
using TT' by (cases T; cases ‹get_conflict_l T›) auto
then obtain MU MU' where
U: ‹U = (MU, NS, Some DT, NES, UES, {#}, {#})› and
MU: ‹MS = MU' @ MU› and
U_U': ‹(U, U') ∈ twl_st_l None›
using UU' by (cases U) auto
have [simp]: ‹L = L'›
using LL' by simp
have [simp]: ‹MS ≠ []› and add_invs: ‹twl_list_invs S›
using SS' bt_inv unfolding twl_list_invs_def backtrack_l_inv_def S by auto
have ‹Suc 0 < size DT›
using size by (auto simp: U)
then have ‹DS ≠ {#}›
using TT' by (auto simp: S T)
moreover have ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (state⇩W_of S')›
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')›
using struct_inv stgy_inv unfolding twl_struct_invs_def twl_stgy_invs_def
by fast+
ultimately have ‹- lit_of (hd MS) ∈# DS›
using bt_inv cdcl⇩W_restart_mset.no_step_skip_hd_in_conflicting[of ‹state⇩W_of S'›]
size struct_inv stgy_inv nss nsr confl SS'
unfolding backtrack_l_inv_def
by (auto simp: cdcl⇩W_restart_mset_state S twl_st)
then have ‹- lit_of (hd MS) ∈# DT›
using TT' by (auto simp: T)
moreover have ‹L' ∈# remove1_mset (- lit_of (hd MS)) DT›
using L' S_S' U_U' by (auto simp: S U)
ultimately have DT:
‹DT = add_mset (- lit_of (hd MS)) (add_mset L' (DT - {#- lit_of (hd MS), L'#}))›
by (metis (no_types, lifting) add_mset_diff_bothsides diff_single_eq_union)
have [simp]: ‹Propagated L i ∉ set MU›
if
i_dom: ‹i ∉# dom_m NS› and
‹i > 0›
for L i
using add_invs that unfolding S MU twl_list_invs_def
by auto
have Propa:
‹((Propagated (- lit_of (hd MS)) i # MU,
fmupd i (- lit_of (hd MS) # L # remove1 (- lit_of (hd MS)) (remove1 L xa), False) NS,
None, NES, UES, {#}, unmark (hd MS)),
case U' of
(M, N, U, D, NE, UE, WS, Q) ⇒
(Propagated (- lit_of (hd (get_trail S'))) (the D) # M, N,
add_mset
(TWL_Clause {#- lit_of (hd (get_trail S')), L'#}
(the D - {#- lit_of (hd (get_trail S')), L'#}))
U,
None, NE, UE, WS, unmark (hd (get_trail S'))))
∈ twl_st_l None›
if
[symmetric, simp]: ‹DT = mset xa› and
i_dom: ‹i ∉# dom_m NS› and
‹i > 0›
for i xa
using U_U' S_S' T_T' i_dom ‹i > 0› DT apply (cases U')
apply (auto simp: U twl_st_l_def hd_get_trail_twl_st_of_get_trail_l S
init_clss_l_mapsto_upd_irrel_notin learned_clss_l_mapsto_upd_notin convert_lit.simps
intro: convert_lits_l_extend_mono)
apply (rule convert_lits_l_extend_mono)
apply assumption
apply auto
done
have [simp]: ‹Ex Not›
by auto
show ?thesis
unfolding propagate_bt_l_def list_of_mset_def propagate_bt_def U RES_RETURN_RES
get_fresh_index_def RES_RES_RETURN_RES
apply clarify
apply (rule RES_rule)
apply (subst in_pair_collect_simp)
apply (intro conjI)
subgoal using Propa
by (auto simp: hd_get_trail_twl_st_of_get_trail_l S T U)
subgoal by auto
subgoal using add_invs ‹L = L'› by (auto simp: S twl_list_invs_def MU simp del: ‹L = L'›)
done
qed
have propagate_unit_bt:
‹(propagate_unit_bt_l (lit_of (hd (get_trail_l S))) U,
propagate_unit_bt (lit_of (hd (get_trail S'))) U')
∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ clauses_to_update_l T = {#} ∧ twl_list_invs T}›
if
SS': ‹(S, S') ∈ ?R› and
bt_inv: ‹backtrack_l_inv S› and
TT': ‹(T, T') ∈ ?extract S (get_conflict_l S)› and
UU': ‹(U, U') ∈ ?find_decomp T› and
size: ‹¬size (the (get_conflict_l U)) > 1›
for S T :: ‹'v twl_st_l› and S' T' U U'
proof -
obtain MS NS DS NES UES where
S: ‹S = (MS, NS, Some DS, NES, UES, {#}, {#})›
using SS' by (cases S; cases ‹get_conflict_l S›) auto
then obtain DT where
T: ‹T = (MS, NS, Some DT, NES, UES, {#}, {#})›
using TT' by (cases T; cases ‹get_conflict_l T›) auto
then obtain MU MU' where
U: ‹U = (MU, NS, Some DT, NES, UES, {#}, {#})› and
MU: ‹MS = MU' @ MU›
using UU' by (cases U) auto
have S'_S: ‹(S, S') ∈ twl_st_l None›
using SS' by simp
have U'_U: ‹(U, U') ∈ twl_st_l None›
using UU' by simp
have [simp]: ‹MS ≠ []› and add_invs: ‹twl_list_invs S›
using SS' bt_inv unfolding twl_list_invs_def backtrack_l_inv_def S by auto
have DT: ‹DT = {#- lit_of (hd MS)#}›
using TT' size by (cases DT, auto simp: U T)
show ?thesis
apply (subst in_pair_collect_simp)
apply (intro conjI)
subgoal
using S'_S U'_U apply (auto simp: twl_st_l_def propagate_unit_bt_def propagate_unit_bt_l_def
S T U DT convert_lit.simps intro: convert_lits_l_extend_mono)
apply (rule convert_lits_l_extend_mono)
apply assumption
by auto
subgoal by (auto simp: propagate_unit_bt_def propagate_unit_bt_l_def S T U DT)
subgoal using add_invs S'_S unfolding S T U twl_list_invs_def propagate_unit_bt_l_def
by (auto 5 5 simp: propagate_unit_bt_l_def DT
twl_list_invs_def MU twl_st_l_def)
done
qed
have bt:
‹(backtrack_l, backtrack) ∈ ?R →⇩f
⟨{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ clauses_to_update_l T = {#} ∧
twl_list_invs T}⟩ nres_rel›
(is ‹_ ∈ _ →⇩f ⟨?I'⟩nres_rel›)
supply [[goals_limit=1]]
unfolding backtrack_l_def backtrack_def fref_param1[symmetric]
apply (refine_vcg H list_of_mset ext; remove_dummy_vars)
subgoal for S S'
unfolding backtrack_l_inv_def
apply (rule_tac x=S' in exI)
by (auto simp: backtrack_inv_def backtrack_l_inv_def twl_st_l)
subgoal by (auto simp: convert_lits_l_def elim: neq_NilE)
subgoal unfolding backtrack_inv_def by auto
subgoal by simp
subgoal by (auto simp: backtrack_inv_def equality_except_conflict_l_rewrite)
subgoal by (auto simp: hd_get_trail_twl_st_of_get_trail_l backtrack_l_inv_def
equality_except_conflict_l_rewrite)
subgoal by (auto simp: propagate_bt_l_def propagate_bt_def backtrack_l_inv_def
equality_except_conflict_l_rewrite)
subgoal by auto
subgoal by (rule find_lit) assumption+
subgoal by (rule propagate_bt) assumption+
subgoal by (rule propagate_unit_bt) assumption+
done
have SPEC_Id: ‹SPEC Φ = ⇓ {(T, T'). Φ T} (SPEC Φ)› for Φ
unfolding conc_fun_RES
by auto
have ‹(backtrack_l S, backtrack S') ∈ ?I› if ‹(S, S') ∈ ?R› for S S'
proof -
have ‹backtrack_l S ≤ ⇓ ?I' (backtrack S')›
by (rule bt[unfolded fref_param1[symmetric], "to_⇓", rule_format, of S S'])
(use that in auto)
moreover have ‹backtrack S' ≤ SPEC (λT. cdcl_twl_o S' T ∧
get_conflict T = None ∧
(∀S'. ¬ cdcl_twl_o T S') ∧
twl_struct_invs T ∧
twl_stgy_invs T ∧ clauses_to_update T = {#} ∧ literals_to_update T ≠ {#})›
by (rule backtrack_spec["to_⇓", of S']) (use that in ‹auto simp: twl_st_l›)
ultimately show ?thesis
apply -
apply (unfold refine_rel_defs nres_rel_def in_pair_collect_simp;
(unfold Ball2_split_def all_to_meta)?;
(intro allI impI)?)
apply (subst (asm) SPEC_Id)
apply unify_Down_invs2+
unfolding nofail_simps
apply unify_Down_invs2_normalisation_post
apply (rule "weaken_⇓")
prefer 2 apply assumption
subgoal premises p by (auto simp: twl_st_l_def)
done
qed
then show ?thesis
by (intro frefI)
qed
definition find_unassigned_lit_l :: ‹'v twl_st_l ⇒ 'v literal option nres› where
‹find_unassigned_lit_l = (λ(M, N, D, NE, UE, WS, Q).
SPEC (λL.
(L ≠ None ⟶
undefined_lit M (the L) ∧
atm_of (the L) ∈ atms_of_mm (clause `# twl_clause_of `# init_clss_lf N + NE)) ∧
(L = None ⟶ (∄L'. undefined_lit M L' ∧
atm_of L' ∈ atms_of_mm (clause `# twl_clause_of `# init_clss_lf N + NE))))
)›
definition decide_l_or_skip_pre where
‹decide_l_or_skip_pre S ⟷ (∃S'. (S, S') ∈ twl_st_l None ∧
twl_struct_invs S' ∧
twl_stgy_invs S' ∧
twl_list_invs S ∧
get_conflict_l S = None ∧
clauses_to_update_l S = {#} ∧
literals_to_update_l S = {#})
›
definition decide_lit_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹decide_lit_l = (λL' (M, N, D, NE, UE, WS, Q).
(Decided L' # M, N, D, NE, UE, WS, {#- L'#}))›
definition decide_l_or_skip :: ‹'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹decide_l_or_skip S = (do {
ASSERT(decide_l_or_skip_pre S);
L ← find_unassigned_lit_l S;
case L of
None ⇒ RETURN (True, S)
| Some L ⇒ RETURN (False, decide_lit_l L S)
})
›
method "match_⇓" =
(match conclusion in ‹f ≤ ⇓ R g› for f :: ‹'a nres› and R :: ‹('a × 'b) set› and
g :: ‹'b nres› ⇒
‹match premises in
I[thin,uncurry]: ‹f ≤ ⇓ R' g› for R' :: ‹('a × 'b) set›
⇒ ‹rule refinement_trans_long[of f f g g R' R, OF refl refl _ I]›
¦ I[thin,uncurry]: ‹_ ⟹ f ≤ ⇓ R' g› for R' :: ‹('a × 'b) set›
⇒ ‹rule refinement_trans_long[of f f g g R' R, OF refl refl _ I]›
›)
lemma decide_l_or_skip_spec:
‹(decide_l_or_skip, decide_or_skip) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ get_conflict_l S = None ∧
clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧ no_step cdcl_twl_cp S' ∧
twl_struct_invs S' ∧ twl_stgy_invs S' ∧ twl_list_invs S} →⇩f
⟨{((brk, T), (brk', T')). (T, T') ∈ twl_st_l None ∧ brk = brk' ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(get_conflict_l T ≠ None ⟶ get_conflict_l T = Some {#})∧
twl_struct_invs T' ∧ twl_stgy_invs T' ∧
(¬brk ⟶ literals_to_update_l T ≠ {#})∧
(brk ⟶ literals_to_update_l T = {#})}⟩ nres_rel›
(is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›)
proof -
have find_unassigned_lit_l: ‹find_unassigned_lit_l S ≤ ⇓ Id (find_unassigned_lit S')›
if SS': ‹(S, S') ∈ ?R›
for S S'
using that
by (cases S)
(auto simp: find_unassigned_lit_l_def find_unassigned_lit_def
mset_take_mset_drop_mset' image_image twl_st_l_def)
have I: ‹(x, x') ∈ Id ⟹ (x, x') ∈ ⟨Id⟩option_rel› for x x' by auto
have dec: ‹(decide_l_or_skip, decide_or_skip) ∈ ?R →
⟨{((brk, T), (brk', T')). (T, T') ∈ twl_st_l None ∧ brk = brk' ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(¬brk ⟶ literals_to_update_l T ≠ {#})∧
(brk ⟶ literals_to_update_l T = {#}) }⟩ nres_rel›
unfolding decide_l_or_skip_def decide_or_skip_def
apply (refine_vcg find_unassigned_lit_l I)
subgoal unfolding decide_l_or_skip_pre_def by (auto simp: twl_st_l_def)
subgoal by auto
subgoal for S S'
by (cases S)
(auto simp: decide_lit_l_def propagate_dec_def twl_list_invs_def twl_st_l_def)
done
have KK: ‹SPEC (λ(brk, T). cdcl_twl_o⇧*⇧* S' T ∧ P brk T) = ⇓ {(S, S'). snd S = S' ∧
P (fst S) (snd S)} (SPEC (cdcl_twl_o⇧*⇧* S'))›
for S' P
by (auto simp: conc_fun_def)
have nf: ‹nofail (SPEC (cdcl_twl_o⇧*⇧* S'))› ‹nofail (SPEC (cdcl_twl_o⇧*⇧* S'))› for S S'
by auto
have set: ‹{((a,b), (a', b')). P a b a' b'} = {(a, b). P (fst a) (snd a) (fst b) (snd b)}› for P
by auto
show ?thesis
proof (intro frefI nres_relI)
fix S S'
assume SS': ‹(S, S') ∈ ?R›
have ‹decide_l_or_skip S
≤ ⇓ {((brk, T), brk', T').
(T, T') ∈ twl_st_l None ∧
brk = brk' ∧
twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(¬ brk ⟶ literals_to_update_l T ≠ {#}) ∧ (brk ⟶ literals_to_update_l T = {#})}
(decide_or_skip S')›
apply (rule dec["to_⇓", of S S'])
using SS' by auto
moreover have ‹ decide_or_skip S'
≤ ⇓ {(S, S'a).
snd S = S'a ∧
get_conflict (snd S) = None ∧
(∀S'. ¬ cdcl_twl_o (snd S) S') ∧
(fst S ⟶ (∀S'. ¬ cdcl_twl_stgy (snd S) S')) ∧
twl_struct_invs (snd S) ∧
twl_stgy_invs (snd S) ∧
clauses_to_update (snd S) = {#} ∧
(¬ fst S ⟶ literals_to_update (snd S) ≠ {#}) ∧
(¬ (∀S'a. ¬ cdcl_twl_o S' S'a) ⟶ cdcl_twl_o⇧+⇧+ S' (snd S))}
(SPEC (cdcl_twl_o⇧*⇧* S'))›
by (rule decide_or_skip_spec[of S', unfolded KK]) (use SS' in auto)
ultimately show ‹decide_l_or_skip S ≤ ⇓ ?S (decide_or_skip S')›
apply -
apply unify_Down_invs2+
apply (simp only: set nf)
apply ("match_⇓")
subgoal
apply (rule; rule)
apply (clarsimp simp: twl_st_l_def)
done
subgoal by fast
done
qed
qed
lemma refinement_trans_eq:
‹A = A' ⟹ B = B' ⟹ R' = R ⟹ A ≤ ⇓ R B ⟹ A' ≤ ⇓ R' B'›
by (auto simp: pw_ref_iff)
definition cdcl_twl_o_prog_l_pre where
‹cdcl_twl_o_prog_l_pre S ⟷
(∃S' . (S, S') ∈ twl_st_l None ∧
twl_struct_invs S' ∧
twl_stgy_invs S' ∧
twl_list_invs S)›
definition cdcl_twl_o_prog_l :: ‹'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹cdcl_twl_o_prog_l S =
do {
ASSERT(cdcl_twl_o_prog_l_pre S);
do {
if get_conflict_l S = None
then decide_l_or_skip S
else if count_decided (get_trail_l S) > 0
then do {
T ← skip_and_resolve_loop_l S;
ASSERT(get_conflict_l T ≠ None ∧ get_conflict_l T ≠ Some {#});
U ← backtrack_l T;
RETURN (False, U)
}
else RETURN (True, S)
}
}
›
lemma twl_st_lE:
‹(⋀M N D NE UE WS Q. T = (M, N, D, NE, UE, WS, Q) ⟹ P (M, N, D, NE, UE, WS, Q)) ⟹ P T›
for T :: ‹'a twl_st_l›
by (cases T) auto
lemma "weaken_⇓'": ‹f ≤ ⇓ R' g ⟹ R' ⊆ R ⟹ f ≤ ⇓ R g›
by (meson pw_ref_iff subset_eq)
lemma cdcl_twl_o_prog_l_spec:
‹(cdcl_twl_o_prog_l, cdcl_twl_o_prog) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧
clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧ no_step cdcl_twl_cp S' ∧
twl_struct_invs S' ∧ twl_stgy_invs S' ∧ twl_list_invs S} →⇩f
⟨{((brk, T), (brk', T')). (T, T') ∈ twl_st_l None ∧ brk = brk' ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(get_conflict_l T ≠ None ⟶ count_decided (get_trail_l T) = 0)∧
twl_struct_invs T' ∧ twl_stgy_invs T'}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
have twl_prog:
‹(cdcl_twl_o_prog_l, cdcl_twl_o_prog) ∈ ?R →⇩f
⟨{((brk, S), (brk', S')).
(brk = brk' ∧ (S, S') ∈ twl_st_l None) ∧ twl_list_invs S ∧
clauses_to_update_l S = {#}}⟩ nres_rel›
(is ‹_ ∈ _ →⇩f ⟨?I'⟩ nres_rel›)
supply [[goals_limit=3]]
unfolding cdcl_twl_o_prog_l_def cdcl_twl_o_prog_def
find_unassigned_lit_def fref_param1[symmetric]
apply (refine_vcg
decide_l_or_skip_spec[THEN fref_to_Down, THEN "weaken_⇓'"]
skip_and_resolve_loop_l_spec[THEN fref_to_Down]
backtrack_l_spec[THEN fref_to_Down]; remove_dummy_vars)
subgoal for S S'
unfolding cdcl_twl_o_prog_l_pre_def by (rule exI[of _ S']) (force simp: twl_st_l)
subgoal by auto
subgoal by simp
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
have set: ‹{((a,b), (a', b')). P a b a' b'} = {(a, b). P (fst a) (snd a) (fst b) (snd b)}› for P
by auto
have SPEC_Id: ‹SPEC Φ = ⇓ {(T, T'). Φ T} (SPEC Φ)› for Φ
unfolding conc_fun_RES
by auto
show bt': ?thesis
proof (intro frefI nres_relI)
fix S S'
assume SS': ‹(S, S') ∈ ?R›
have ‹cdcl_twl_o_prog S' ≤ SPEC (cdcl_twl_o_prog_spec S')›
by (rule cdcl_twl_o_prog_spec[of S']) (use SS' in auto)
moreover have ‹cdcl_twl_o_prog_l S ≤ ⇓ ?I' (cdcl_twl_o_prog S')›
by (rule twl_prog[unfolded fref_param1[symmetric], "to_⇓"])
(use SS' in auto)
ultimately show ‹cdcl_twl_o_prog_l S ≤ ⇓ ?J (cdcl_twl_o_prog S')›
apply -
unfolding set
apply (subst(asm) SPEC_Id)
apply unify_Down_invs2+
apply ("match_⇓")
subgoal by (clarsimp simp del: split_paired_All simp: twl_st_l_def)
subgoal by simp
done
qed
qed
subsection ‹Full Strategy›
definition cdcl_twl_stgy_prog_l_inv :: ‹'v twl_st_l ⇒ bool × 'v twl_st_l ⇒ bool› where
‹cdcl_twl_stgy_prog_l_inv S⇩0 ≡ λ(brk, T). ∃S⇩0' T'. (T, T') ∈ twl_st_l None ∧
(S⇩0, S⇩0') ∈ twl_st_l None ∧
twl_struct_invs T' ∧
twl_stgy_invs T' ∧
(brk ⟶ final_twl_state T') ∧
cdcl_twl_stgy⇧*⇧* S⇩0' T' ∧
clauses_to_update_l T = {#} ∧
(¬brk ⟶ get_conflict_l T = None)›
definition cdcl_twl_stgy_prog_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_twl_stgy_prog_l S⇩0 =
do {
do {
(brk, T) ← WHILE⇩T⇗cdcl_twl_stgy_prog_l_inv S⇩0⇖
(λ(brk, _). ¬brk)
(λ(brk, S).
do {
T ← unit_propagation_outer_loop_l S;
cdcl_twl_o_prog_l T
})
(False, S⇩0);
RETURN T
}
}
›
lemma cdcl_twl_stgy_prog_l_spec:
‹(cdcl_twl_stgy_prog_l, cdcl_twl_stgy_prog) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
clauses_to_update_l S = {#} ∧
twl_struct_invs S' ∧ twl_stgy_invs S'} →⇩f
⟨{(T, T'). (T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
twl_struct_invs T' ∧ twl_stgy_invs T'} ∧ True}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
have R: ‹(a, b) ∈ ?R ⟹
((False, a), (False, b)) ∈ {((brk, S), (brk', S')). brk = brk' ∧ (S, S') ∈ ?R}›
for a b by auto
show ?thesis
unfolding cdcl_twl_stgy_prog_l_def cdcl_twl_stgy_prog_def cdcl_twl_o_prog_l_spec
fref_param1[symmetric] cdcl_twl_stgy_prog_l_inv_def
apply (refine_rcg R cdcl_twl_o_prog_l_spec[THEN fref_to_Down, THEN "weaken_⇓'"]
unit_propagation_outer_loop_l_spec[THEN fref_to_Down]; remove_dummy_vars)
subgoal for S⇩0 S⇩0' T T'
apply (rule exI[of _ S⇩0'])
apply (rule exI[of _ ‹snd T›])
by (auto simp add: case_prod_beta)
subgoal by auto
subgoal by fastforce
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma refine_pair_to_SPEC:
fixes f :: ‹'s ⇒ 's nres› and g :: ‹'b ⇒ 'b nres›
assumes ‹(f, g) ∈ {(S, S'). (S, S') ∈ H ∧ R S S'} →⇩f ⟨{(S, S'). (S, S') ∈ H' ∧ P' S}⟩nres_rel›
(is ‹_ ∈ ?R →⇩f ?I›)
assumes ‹R S S'› and [simp]: ‹(S, S') ∈ H›
shows ‹f S ≤ ⇓ {(S, S'). (S, S') ∈ H' ∧ P' S} (g S')›
proof -
have ‹(f S, g S') ∈ ?I›
using assms unfolding fref_def nres_rel_def by auto
then show ?thesis
unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by auto
qed
definition cdcl_twl_stgy_prog_l_pre where
‹cdcl_twl_stgy_prog_l_pre S S' ⟷
((S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
clauses_to_update_l S = {#} ∧ get_conflict_l S = None ∧ twl_list_invs S)›
lemma cdcl_twl_stgy_prog_l_spec_final:
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_l S ≤ ⇓ (twl_st_l None) (conclusive_TWL_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_l_spec[THEN refine_pair_to_SPEC,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def by (auto intro: conc_fun_R_mono)
done
lemma cdcl_twl_stgy_prog_l_spec_final':
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_l S ≤ ⇓ {(S, T). (S, T) ∈ twl_st_l None ∧ twl_list_invs S ∧
twl_struct_invs S' ∧ twl_stgy_invs S'} (conclusive_TWL_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_l_spec[THEN refine_pair_to_SPEC,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def by (auto intro: conc_fun_R_mono)
done
definition cdcl_twl_stgy_prog_break_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_twl_stgy_prog_break_l S⇩0 =
do {
b ← SPEC(λ_. True);
(b, brk, T) ← WHILE⇩T⇗λ(b, S). cdcl_twl_stgy_prog_l_inv S⇩0 S⇖
(λ(b, brk, _). b ∧ ¬brk)
(λ(_, brk, S). do {
T ← unit_propagation_outer_loop_l S;
T ← cdcl_twl_o_prog_l T;
b ← SPEC(λ_. True);
RETURN (b, T)
})
(b, False, S⇩0);
if brk then RETURN T
else cdcl_twl_stgy_prog_l T
}›
lemma cdcl_twl_stgy_prog_break_l_spec:
‹(cdcl_twl_stgy_prog_break_l, cdcl_twl_stgy_prog_break) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
clauses_to_update_l S = {#} ∧
twl_struct_invs S' ∧ twl_stgy_invs S'} →⇩f
⟨{(T, T'). (T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
twl_struct_invs T' ∧ twl_stgy_invs T'} ∧ True}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
have R: ‹(a, b) ∈ ?R ⟹ (bb, bb') ∈ bool_rel ⟹
((bb, False, a), (bb', False, b)) ∈ {((b, brk, S), (b', brk', S')). b = b' ∧ brk = brk' ∧
(S, S') ∈ ?R}›
for a b bb bb' by auto
show ?thesis
supply [[goals_limit=1]]
unfolding cdcl_twl_stgy_prog_break_l_def cdcl_twl_stgy_prog_break_def cdcl_twl_o_prog_l_spec
fref_param1[symmetric] cdcl_twl_stgy_prog_l_inv_def
apply (refine_rcg cdcl_twl_o_prog_l_spec[THEN fref_to_Down]
unit_propagation_outer_loop_l_spec[THEN fref_to_Down]
cdcl_twl_stgy_prog_l_spec[THEN fref_to_Down]; remove_dummy_vars)
apply (rule R)
subgoal by auto
subgoal by auto
subgoal for S⇩0 S⇩0' b b' T T'
apply (rule exI[of _ S⇩0'])
apply (rule exI[of _ ‹snd (snd T)›])
by (auto simp add: case_prod_beta)
subgoal
by auto
subgoal by fastforce
subgoal by (auto simp: twl_st_l)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma cdcl_twl_stgy_prog_break_l_spec_final:
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_break_l S ≤ ⇓ (twl_st_l None) (conclusive_TWL_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_break_l_spec[THEN refine_pair_to_SPEC,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_break_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def
by (auto intro: conc_fun_R_mono)
done
end