theory Watched_Literals_Watch_List
imports Watched_Literals_List Weidenbach_Book_Base.Explorer
begin
section ‹Third Refinement: Remembering watched›
subsection ‹Types›
type_synonym clauses_to_update_wl = ‹nat multiset›
type_synonym 'v watcher = ‹(nat × 'v literal × bool)›
type_synonym 'v watched = ‹'v watcher list›
type_synonym 'v lit_queue_wl = ‹'v literal multiset›
type_synonym 'v twl_st_wl =
‹('v, nat) ann_lits × 'v clauses_l ×
'v cconflict × 'v clauses × 'v clauses × 'v lit_queue_wl ×
('v literal ⇒ 'v watched)›
subsection ‹Access Functions›
fun clauses_to_update_wl :: ‹'v twl_st_wl ⇒ 'v literal ⇒ nat ⇒ clauses_to_update_wl› where
‹clauses_to_update_wl (_, N, _, _, _, _, W) L i =
filter_mset (λi. i ∈# dom_m N) (mset (drop i (map fst (W L))))›
fun get_trail_wl :: ‹'v twl_st_wl ⇒ ('v, nat) ann_lit list› where
‹get_trail_wl (M, _, _, _, _, _, _) = M›
fun literals_to_update_wl :: ‹'v twl_st_wl ⇒ 'v lit_queue_wl› where
‹literals_to_update_wl (_, _, _, _, _, Q, _) = Q›
fun set_literals_to_update_wl :: ‹'v lit_queue_wl ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹set_literals_to_update_wl Q (M, N, D, NE, UE, _, W) = (M, N, D, NE, UE, Q, W)›
fun get_conflict_wl :: ‹'v twl_st_wl ⇒ 'v cconflict› where
‹get_conflict_wl (_, _, D, _, _, _, _) = D›
fun get_clauses_wl :: ‹'v twl_st_wl ⇒ 'v clauses_l› where
‹get_clauses_wl (M, N, D, NE, UE, WS, Q) = N›
fun get_unit_learned_clss_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
‹get_unit_learned_clss_wl (M, N, D, NE, UE, Q, W) = UE›
fun get_unit_init_clss_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
‹get_unit_init_clss_wl (M, N, D, NE, UE, Q, W) = NE›
fun get_unit_clauses_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
‹get_unit_clauses_wl (M, N, D, NE, UE, Q, W) = NE + UE›
lemma get_unit_clauses_wl_alt_def:
‹get_unit_clauses_wl S = get_unit_init_clss_wl S + get_unit_learned_clss_wl S›
by (cases S) auto
fun get_watched_wl :: ‹'v twl_st_wl ⇒ ('v literal ⇒ 'v watched)› where
‹get_watched_wl (_, _, _, _, _, _, W) = W›
definition get_learned_clss_wl where
‹get_learned_clss_wl S = learned_clss_lf (get_clauses_wl S)›
definition all_lits_of_mm :: ‹'a clauses ⇒ 'a literal multiset› where
‹all_lits_of_mm Ls = Pos `# (atm_of `# (⋃# Ls)) + Neg `# (atm_of `# (⋃# Ls))›
lemma all_lits_of_mm_empty[simp]: ‹all_lits_of_mm {#} = {#}›
by (auto simp: all_lits_of_mm_def)
text ‹
We cannot just extract the literals of the clauses: we cannot be sure that atoms appear ∗‹both›
positively and negatively in the clauses. If we could ensure that there are no pure literals, the
definition of \<^term>‹all_lits_of_mm› can be changed to ‹all_lits_of_mm Ls = ⋃# Ls›.
In this definition \<^term>‹K› is the blocking literal.
›
fun correctly_marked_as_binary where
‹correctly_marked_as_binary N (i, K, b) ⟷ (b ⟷ (length (N ∝ i) = 2))›
declare correctly_marked_as_binary.simps[simp del]
abbreviation distinct_watched :: ‹'v watched ⇒ bool› where
‹distinct_watched xs ≡ distinct (map (λ(i, j, k). i) xs)›
lemma distinct_watched_alt_def: ‹distinct_watched xs = distinct (map fst xs)›
by (induction xs; auto)
fun correct_watching_except :: ‹nat ⇒ nat ⇒ 'v literal ⇒ 'v twl_st_wl ⇒ bool› where
‹correct_watching_except i j K (M, N, D, NE, UE, Q, W) ⟷
(∀L ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE)).
(L = K ⟶
distinct_watched (take i (W L) @ drop j (W L)) ∧
((∀(i, K, b)∈#mset (take i (W L) @ drop j (W L)). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧
K ≠ L ∧ correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (take i (W L) @ drop j (W L)). b ⟶ i ∈# dom_m N) ∧
filter_mset (λi. i ∈# dom_m N) (fst `# mset (take i (W L) @ drop j (W L))) = clause_to_update L (M, N, D, NE, UE, {#}, {#}))) ∧
(L ≠ K ⟶
distinct_watched (W L) ∧
((∀(i, K, b)∈#mset (W L). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (W L). b ⟶ i ∈# dom_m N) ∧
filter_mset (λi. i ∈# dom_m N) (fst `# mset (W L)) = clause_to_update L (M, N, D, NE, UE, {#}, {#}))))›
fun correct_watching :: ‹'v twl_st_wl ⇒ bool› where
‹correct_watching (M, N, D, NE, UE, Q, W) ⟷
(∀L ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE)).
distinct_watched (W L) ∧
(∀(i, K, b)∈#mset (W L). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (W L). b ⟶ i ∈# dom_m N) ∧
filter_mset (λi. i ∈# dom_m N) (fst `# mset (W L)) = clause_to_update L (M, N, D, NE, UE, {#}, {#}))›
declare correct_watching.simps[simp del]
lemma correct_watching_except_correct_watching:
assumes
j: ‹j ≥ length (W K)› and
corr: ‹correct_watching_except i j K (M, N, D, NE, UE, Q, W)›
shows ‹correct_watching (M, N, D, NE, UE, Q, W(K := take i (W K)))›
proof -
have
H1: ‹⋀L i' K' b. L ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
(L = K ⟹
distinct_watched (take i (W L) @ drop j (W L)) ∧
(((i', K', b)∈#mset (take i (W L) @ drop j (W L)) ⟶ i' ∈# dom_m N ⟶
K' ∈ set (N ∝ i') ∧ K' ≠ L ∧ correctly_marked_as_binary N (i', K', b)) ∧
((i', K', b)∈#mset (take i (W L) @ drop j (W L)) ⟶ b ⟶ i' ∈# dom_m N) ∧
filter_mset (λi. i ∈# dom_m N) (fst `# mset (take i (W L) @ drop j (W L))) =
clause_to_update L (M, N, D, NE, UE, {#}, {#})))› and
H2: ‹⋀L i K' b. L ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹ (L ≠ K ⟹
distinct_watched (W L) ∧
(((i, K', b)∈#mset (W L) ⟶ i ∈# dom_m N ⟶ K' ∈ set (N ∝ i) ∧ K' ≠ L ∧
(correctly_marked_as_binary N (i, K', b))) ∧
((i, K', b)∈#mset (W L) ⟶ b ⟶ i ∈# dom_m N) ∧
filter_mset (λi. i ∈# dom_m N) (fst `# mset (W L)) =
clause_to_update L (M, N, D, NE, UE, {#}, {#})))›
using corr unfolding correct_watching_except.simps
by fast+
show ?thesis
unfolding correct_watching.simps
apply (intro conjI allI impI ballI)
subgoal for L
apply (cases ‹L = K›)
subgoal
using H1[of L] j
by (auto split: if_splits)
subgoal
using H2[of L] j
by (auto split: if_splits)
done
subgoal for L x
apply (cases ‹L = K›)
subgoal
using H1[of L ‹fst x› ‹fst (snd x)› ‹snd (snd x)›] j
by (auto split: if_splits)
subgoal
using H2[of L ‹fst x› ‹fst (snd x)› ‹snd (snd x)›]
by auto
done
subgoal for L
apply (cases ‹L = K›)
subgoal
using H1[of L _ _] j
by (auto split: if_splits)
subgoal
using H2[of L _ _]
by auto
done
subgoal for L
apply (cases ‹L = K›)
subgoal
using H1[of L _ _] j
by (auto split: if_splits)
subgoal
using H2[of L _ _]
by auto
done
done
qed
fun watched_by :: ‹'v twl_st_wl ⇒ 'v literal ⇒ 'v watched› where
‹watched_by (M, N, D, NE, UE, Q, W) L = W L›
fun update_watched :: ‹'v literal ⇒ 'v watched ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹update_watched L WL (M, N, D, NE, UE, Q, W) = (M, N, D, NE, UE, Q, W(L:= WL))›
lemma bspec': ‹x ∈ a ⟹ ∀x∈a. P x ⟹ P x›
by (rule bspec)
lemma correct_watching_exceptD:
assumes
‹correct_watching_except i j L S› and
‹L ∈# all_lits_of_mm
(mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S)› and
w: ‹w < length (watched_by S L)› ‹w ≥ j› ‹fst (watched_by S L ! w) ∈# dom_m (get_clauses_wl S)›
shows ‹fst (snd (watched_by S L ! w)) ∈ set (get_clauses_wl S ∝ (fst (watched_by S L ! w)))›
proof -
have H: ‹⋀x. x∈set (take i (watched_by S L)) ∪ set (drop j (watched_by S L)) ⟹
case x of (i, K, b) ⇒ i ∈# dom_m (get_clauses_wl S) ⟶ K ∈ set (get_clauses_wl S ∝ i) ∧
K ≠ L›
using assms
by (cases S; cases ‹watched_by S L ! w›)
(auto simp add: add_mset_eq_add_mset simp del: Un_iff
dest!: multi_member_split[of L] dest: bspec)
have ‹∃i≥j. i < length (watched_by S L) ∧
watched_by S L ! w = watched_by S L ! i›
by (rule exI[of _ w])
(use w in auto)
then show ?thesis
using H[of ‹watched_by S L ! w›] w
by (cases ‹watched_by S L ! w›) (auto simp: in_set_drop_conv_nth)
qed
declare correct_watching_except.simps[simp del]
lemma in_all_lits_of_mm_ain_atms_of_iff:
‹L ∈# all_lits_of_mm N ⟷ atm_of L ∈ atms_of_mm N›
by (cases L) (auto simp: all_lits_of_mm_def atms_of_ms_def atms_of_def)
lemma all_lits_of_mm_union:
‹all_lits_of_mm (M + N) = all_lits_of_mm M + all_lits_of_mm N›
unfolding all_lits_of_mm_def by auto
definition all_lits_of_m :: ‹'a clause ⇒ 'a literal multiset› where
‹all_lits_of_m Ls = Pos `# (atm_of `# Ls) + Neg `# (atm_of `# Ls)›
lemma all_lits_of_m_empty[simp]: ‹all_lits_of_m {#} = {#}›
by (auto simp: all_lits_of_m_def)
lemma all_lits_of_m_empty_iff[iff]: ‹all_lits_of_m A = {#} ⟷ A = {#}›
by (cases A) (auto simp: all_lits_of_m_def)
lemma in_all_lits_of_m_ain_atms_of_iff: ‹L ∈# all_lits_of_m N ⟷ atm_of L ∈ atms_of N›
by (cases L) (auto simp: all_lits_of_m_def atms_of_ms_def atms_of_def)
lemma in_clause_in_all_lits_of_m: ‹x ∈# C ⟹ x ∈# all_lits_of_m C›
using atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff by blast
lemma all_lits_of_mm_add_mset:
‹all_lits_of_mm (add_mset C N) = (all_lits_of_m C) + (all_lits_of_mm N)›
by (auto simp: all_lits_of_mm_def all_lits_of_m_def)
lemma all_lits_of_m_add_mset:
‹all_lits_of_m (add_mset L C) = add_mset L (add_mset (-L) (all_lits_of_m C))›
by (cases L) (auto simp: all_lits_of_m_def)
lemma all_lits_of_m_union:
‹all_lits_of_m (A + B) = all_lits_of_m A + all_lits_of_m B›
by (auto simp: all_lits_of_m_def)
lemma all_lits_of_m_mono:
‹D ⊆# D' ⟹ all_lits_of_m D ⊆# all_lits_of_m D'›
by (auto elim!: mset_le_addE simp: all_lits_of_m_union)
lemma in_all_lits_of_mm_uminusD: ‹x2 ∈# all_lits_of_mm N ⟹ -x2 ∈# all_lits_of_mm N›
by (auto simp: all_lits_of_mm_def)
lemma in_all_lits_of_mm_uminus_iff: ‹-x2 ∈# all_lits_of_mm N ⟷ x2 ∈# all_lits_of_mm N›
by (cases x2) (auto simp: all_lits_of_mm_def)
lemma all_lits_of_mm_diffD:
‹L ∈# all_lits_of_mm (A - B) ⟹ L ∈# all_lits_of_mm A›
apply (induction A arbitrary: B)
subgoal by auto
subgoal for a A' B
by (cases ‹a ∈# B›)
(fastforce dest!: multi_member_split[of a B] simp: all_lits_of_mm_add_mset)+
done
lemma all_lits_of_mm_mono:
‹set_mset A ⊆ set_mset B ⟹ set_mset (all_lits_of_mm A) ⊆ set_mset (all_lits_of_mm B)›
by (auto simp: all_lits_of_mm_def)
fun st_l_of_wl :: ‹('v literal × nat) option ⇒ 'v twl_st_wl ⇒ 'v twl_st_l› where
‹st_l_of_wl None (M, N, D, NE, UE, Q, W) = (M, N, D, NE, UE, {#}, Q)›
| ‹st_l_of_wl (Some (L, j)) (M, N, D, NE, UE, Q, W) =
(M, N, D, NE, UE, (if D ≠ None then {#} else clauses_to_update_wl (M, N, D, NE, UE, Q, W) L j,
Q))›
definition state_wl_l :: ‹('v literal × nat) option ⇒ ('v twl_st_wl × 'v twl_st_l) set› where
‹state_wl_l L = {(T, T'). T' = st_l_of_wl L T}›
fun twl_st_of_wl :: ‹('v literal × nat) option ⇒ ('v twl_st_wl × 'v twl_st) set› where
‹twl_st_of_wl L = state_wl_l L O twl_st_l (map_option fst L)›
named_theorems twl_st_wl ‹Conversions simp rules›
lemma [twl_st_wl]:
assumes ‹(S, T) ∈ state_wl_l L›
shows
‹get_trail_l T = get_trail_wl S› and
‹get_clauses_l T = get_clauses_wl S› and
‹get_conflict_l T = get_conflict_wl S› and
‹L = None ⟹ clauses_to_update_l T = {#}›
‹L ≠ None ⟹ get_conflict_wl S ≠ None ⟹ clauses_to_update_l T = {#}›
‹L ≠ None ⟹ get_conflict_wl S = None ⟹ clauses_to_update_l T =
clauses_to_update_wl S (fst (the L)) (snd (the L))› and
‹literals_to_update_l T = literals_to_update_wl S›
‹get_unit_learned_clauses_l T = get_unit_learned_clss_wl S›
‹get_unit_init_clauses_l T = get_unit_init_clss_wl S›
‹get_unit_learned_clauses_l T = get_unit_learned_clss_wl S›
‹get_unit_clauses_l T = get_unit_clauses_wl S›
using assms unfolding state_wl_l_def all_clss_lf_ran_m[symmetric]
by (cases S; cases T; cases L; auto split: option.splits simp: trail.simps; fail)+
lemma [twl_st_l]:
‹(a, a') ∈ state_wl_l None ⟹
get_learned_clss_l a' = get_learned_clss_wl a›
unfolding state_wl_l_def by (cases a; cases a')
(auto simp: get_learned_clss_l_def get_learned_clss_wl_def)
lemma remove_one_lit_from_wq_def:
‹remove_one_lit_from_wq L S = set_clauses_to_update_l (clauses_to_update_l S - {#L#}) S›
by (cases S) auto
lemma correct_watching_set_literals_to_update[simp]:
‹correct_watching (set_literals_to_update_wl WS T') = correct_watching T'›
by (cases T') (auto simp: correct_watching.simps)
lemma [twl_st_wl]:
‹get_clauses_wl (set_literals_to_update_wl W S) = get_clauses_wl S›
‹get_unit_init_clss_wl (set_literals_to_update_wl W S) = get_unit_init_clss_wl S›
by (cases S; auto; fail)+
lemma get_conflict_wl_set_literals_to_update_wl[twl_st_wl]:
‹get_conflict_wl (set_literals_to_update_wl P S) = get_conflict_wl S›
‹get_unit_clauses_wl (set_literals_to_update_wl P S) = get_unit_clauses_wl S›
by (cases S; auto; fail)+
definition set_conflict_wl :: ‹'v clause_l ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹set_conflict_wl = (λC (M, N, D, NE, UE, Q, W). (M, N, Some (mset C), NE, UE, {#}, W))›
lemma [twl_st_wl]: ‹get_clauses_wl (set_conflict_wl D S) = get_clauses_wl S›
by (cases S) (auto simp: set_conflict_wl_def)
lemma [twl_st_wl]:
‹get_unit_init_clss_wl (set_conflict_wl D S) = get_unit_init_clss_wl S›
‹get_unit_clauses_wl (set_conflict_wl D S) = get_unit_clauses_wl S›
by (cases S; auto simp: set_conflict_wl_def; fail)+
lemma state_wl_l_mark_of_is_decided:
‹(x, y) ∈ state_wl_l b ⟹
get_trail_wl x ≠ [] ⟹
is_decided (hd (get_trail_l y)) = is_decided (hd (get_trail_wl x))›
by (cases ‹get_trail_wl x›; cases ‹get_trail_l y›; cases ‹hd (get_trail_wl x)›;
cases ‹hd (get_trail_l y)›; cases b; cases x)
(auto simp: state_wl_l_def convert_lit.simps st_l_of_wl.simps)
lemma state_wl_l_mark_of_is_proped:
‹(x, y) ∈ state_wl_l b ⟹
get_trail_wl x ≠ [] ⟹
is_proped (hd (get_trail_l y)) = is_proped (hd (get_trail_wl x))›
by (cases ‹get_trail_wl x›; cases ‹get_trail_l y›; cases ‹hd (get_trail_wl x)›;
cases ‹hd (get_trail_l y)›; cases b; cases x)
(auto simp: state_wl_l_def convert_lit.simps)
text ‹We here also update the list of watched clauses \<^term>‹WL›.›
declare twl_st_wl[simp]
definition unit_prop_body_wl_inv where
‹unit_prop_body_wl_inv T j i L ⟷ (i < length (watched_by T L) ∧ j ≤ i ∧
(fst (watched_by T L ! i) ∈# dom_m (get_clauses_wl T) ⟶
(∃T'. (T, T') ∈ state_wl_l (Some (L, i)) ∧ j ≤ i ∧
unit_propagation_inner_loop_body_l_inv L (fst (watched_by T L ! i))
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T')∧
L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl T) + get_unit_clauses_wl T) ∧
correct_watching_except j i L T)))›
lemma unit_prop_body_wl_inv_alt_def:
‹unit_prop_body_wl_inv T j i L ⟷ (i < length (watched_by T L) ∧ j ≤ i ∧
(fst (watched_by T L ! i) ∈# dom_m (get_clauses_wl T) ⟶
(∃T'. (T, T') ∈ state_wl_l (Some (L, i)) ∧
unit_propagation_inner_loop_body_l_inv L (fst (watched_by T L ! i))
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T')∧
L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl T) + get_unit_clauses_wl T) ∧
correct_watching_except j i L T ∧
get_conflict_wl T = None ∧
length (get_clauses_wl T ∝ fst (watched_by T L ! i)) ≥ 2)))›
(is ‹?A = ?B›)
proof
assume ?B
then show ?A
unfolding unit_prop_body_wl_inv_def
by blast
next
assume ?A
then show ?B
proof (cases ‹fst (watched_by T L ! i) ∈# dom_m (get_clauses_wl T)›)
case False
then show ?B
using ‹?A› unfolding unit_prop_body_wl_inv_def
by blast
next
case True
then obtain T' where
‹i < length (watched_by T L)›
‹j ≤ i› and
TT': ‹(T, T') ∈ state_wl_l (Some (L, i))› and
inv: ‹unit_propagation_inner_loop_body_l_inv L (fst (watched_by T L ! i))
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T')› and
‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl T) + get_unit_clauses_wl T)›
‹correct_watching_except j i L T›
using ‹?A› unfolding unit_prop_body_wl_inv_def
by blast
obtain x where
x: ‹(set_clauses_to_update_l
(clauses_to_update_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') +
{#fst (watched_by T L ! i)#})
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T'),
x)
∈ twl_st_l (Some L)› and
struct_invs: ‹twl_struct_invs x› and
‹twl_stgy_invs x› and
‹fst (watched_by T L ! i)
∈# dom_m
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T'))› and
‹0 < fst (watched_by T L ! i)› and
‹0 < length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') ∝
fst (watched_by T L ! i))› and
‹no_dup
(get_trail_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T'))› and
‹(if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') ∝
fst (watched_by T L ! i) !
0 =
L
then 0 else 1)
< length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') ∝
fst (watched_by T L ! i))› and
‹1 -
(if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') ∝
fst (watched_by T L ! i) !
0 =
L
then 0 else 1)
< length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') ∝
fst (watched_by T L ! i))› and
‹L ∈ set (watched_l
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by T L ! i)) T') ∝
fst (watched_by T L ! i)))› and
confl: ‹get_conflict_l (remove_one_lit_from_wq (fst (watched_by T L ! i)) T') = None›
using inv unfolding unit_propagation_inner_loop_body_l_inv_def by blast
have ‹Multiset.Ball (get_clauses x) struct_wf_twl_cls›
using struct_invs unfolding twl_struct_invs_def twl_st_inv_alt_def by blast
moreover have ‹twl_clause_of (get_clauses_wl T ∝ fst (watched_by T L ! i)) ∈# get_clauses x›
using TT' x True by auto
ultimately have 1: ‹length (get_clauses_wl T ∝ fst (watched_by T L ! i)) ≥ 2›
by auto
have 2: ‹get_conflict_wl T = None›
using confl TT' x by auto
show ?B
using ‹?A› 1 2 unfolding unit_prop_body_wl_inv_def
by blast
qed
qed
definition propagate_lit_wl_general :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹propagate_lit_wl_general = (λL' C i (M, N, D, NE, UE, Q, W).
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, add_mset (-L') Q, W))›
definition propagate_lit_wl :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹propagate_lit_wl = (λL' C i (M, N, D, NE, UE, Q, W).
let N = N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)) in
(Propagated L' C # M, N, D, NE, UE, add_mset (-L') Q, W))›
definition propagate_lit_wl_bin :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹propagate_lit_wl_bin = (λL' C i (M, N, D, NE, UE, Q, W).
(Propagated L' C # M, N, D, NE, UE, add_mset (-L') Q, W))›
definition keep_watch where
‹keep_watch = (λL i j (M, N, D, NE, UE, Q, W).
(M, N, D, NE, UE, Q, W(L := (W L)[i := W L ! j])))›
lemma length_watched_by_keep_watch[twl_st_wl]:
‹length (watched_by (keep_watch L i j S) K) = length (watched_by S K)›
by (cases S) (auto simp: keep_watch_def)
lemma watched_by_keep_watch_neq[twl_st_wl, simp]:
‹w < length (watched_by S L) ⟹ watched_by (keep_watch L j w S) L ! w = watched_by S L ! w›
by (cases S) (auto simp: keep_watch_def)
lemma watched_by_keep_watch_eq[twl_st_wl, simp]:
‹j < length (watched_by S L) ⟹ watched_by (keep_watch L j w S) L ! j = watched_by S L ! w›
by (cases S) (auto simp: keep_watch_def)
definition update_clause_wl :: ‹'v literal ⇒ nat ⇒ bool ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ 'v twl_st_wl ⇒
(nat × nat × 'v twl_st_wl) nres› where
‹update_clause_wl = (λ(L::'v literal) C b j w i f (M, N, D, NE, UE, Q, W). do {
let K' = (N∝C) ! f;
let N' = N(C ↪ swap (N ∝ C) i f);
RETURN (j, w+1, (M, N', D, NE, UE, Q, W(K' := W K' @ [(C, L, b)])))
})›
definition update_blit_wl :: ‹'v literal ⇒ nat ⇒ bool ⇒ nat ⇒ nat ⇒ 'v literal ⇒ 'v twl_st_wl ⇒
(nat × nat × 'v twl_st_wl) nres› where
‹update_blit_wl = (λ(L::'v literal) C b j w K (M, N, D, NE, UE, Q, W). do {
RETURN (j+1, w+1, (M, N, D, NE, UE, Q, W(L := (W L)[j:=(C, K, b)])))
})›
definition unit_prop_body_wl_find_unwatched_inv where
‹unit_prop_body_wl_find_unwatched_inv f C S ⟷
get_clauses_wl S ∝ C ≠ [] ∧
(f = None ⟷ (∀L∈#mset (unwatched_l (get_clauses_wl S ∝ C)). - L ∈ lits_of_l (get_trail_wl S)))›
abbreviation remaining_nondom_wl where
‹remaining_nondom_wl w L S ≡
(if get_conflict_wl S = None
then size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl S)) (mset (drop w (watched_by S L)))) else 0)›
definition unit_propagation_inner_loop_wl_loop_inv where
‹unit_propagation_inner_loop_wl_loop_inv L = (λ(j, w, S).
(∃S'. (S, S') ∈ state_wl_l (Some (L, w)) ∧ j≤ w ∧
unit_propagation_inner_loop_l_inv L (S', remaining_nondom_wl w L S) ∧
correct_watching_except j w L S ∧ w ≤ length (watched_by S L)))›
lemma correct_watching_except_correct_watching_except_Suc_Suc_keep_watch:
assumes
j_w: ‹j ≤ w› and
w_le: ‹w < length (watched_by S L)› and
corr: ‹correct_watching_except j w L S›
shows ‹correct_watching_except (Suc j) (Suc w) L (keep_watch L j w S)›
proof -
obtain M N D NE UE Q W where S: ‹S = (M, N, D, NE, UE, Q, W)› by (cases S)
have
Hneq: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟶
(La ≠ L ⟶
distinct_watched (W La) ∧
(∀(i, K, b)∈#mset (W La). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (W La). b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `# mset (W La). i ∈# dom_m N#} = clause_to_update La (M, N, D, NE, UE, {#}, {#}))› and
Heq: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟶
(La = L ⟶
distinct_watched (take j (W La) @ drop w (W La)) ∧
(∀(i, K, b)∈#mset (take j (W La) @ drop w (W La)). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧
K ≠ La ∧ correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (take j (W La) @ drop w (W La)). b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `# mset (take j (W La) @ drop w (W La)). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#}))›
using corr unfolding S correct_watching_except.simps
by fast+
have eq: ‹mset (take (Suc j) ((W(L := (W L)[j := W L ! w])) La) @ drop (Suc w) ((W(L := (W L)[j := W L ! w])) La)) =
mset (take j (W La) @ drop w (W La))› if [simp]: ‹La = L› for La
using w_le j_w
by (auto simp: S take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]
list_update_append)
have ‹case x of (i, K, b) ⇒ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L› and
‹x ∈# mset (take (Suc j) ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La))›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Heq[of L]
apply (subst (asm) eq)
by (simp_all add: eq)
moreover have ‹case x of (i, K, b) ⇒ b ⟶ i ∈# dom_m N›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L› and
‹x ∈# mset (take (Suc j) ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La))›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Heq[of L]
by (subst (asm) eq) blast+
moreover have ‹{#i ∈# fst `#
mset
(take (Suc j) ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La)).
i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L›
for La :: ‹'a literal›
using that Heq[of L]
by (subst eq) simp_all
moreover have ‹case x of (i, K, b) ⇒ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L› and
‹x ∈# mset ((W(L := (W L)[j := W L ! w])) La)›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Hneq[of La]
by simp
moreover have ‹case x of (i, K, b) ⇒ b ⟶ i ∈# dom_m N›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L› and
‹x ∈# mset ((W(L := (W L)[j := W L ! w])) La)›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Hneq[of La]
by auto
moreover have ‹{#i ∈# fst `# mset ((W(L := (W L)[j := W L ! w])) La). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L›
for La :: ‹'a literal›
using that Hneq[of La]
by simp
moreover have ‹distinct_watched ((W(L := (W L)[j := W L ! w])) La)›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L›
for La :: ‹'a literal›
using that Hneq[of La]
by simp
moreover have ‹distinct_watched (take (Suc j) ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La))›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L›
for La :: ‹'a literal›
using that Heq[of La]
apply (subst distinct_mset_mset_distinct[symmetric])
apply (subst mset_map)
apply (subst eq)
apply (simp add: that)
apply (subst mset_map[symmetric])
apply (subst distinct_mset_mset_distinct)
apply simp
done
ultimately show ?thesis
unfolding S keep_watch_def prod.simps correct_watching_except.simps
by meson
qed
lemma correct_watching_except_update_blit:
assumes
corr: ‹correct_watching_except i j L (a, b, c, d, e, f, g(L := (g L)[j' := (x1, C, b')]))› and
C': ‹C' ∈# all_lits_of_mm (mset `# ran_mf b + (d + e))›
‹C' ∈ set (b ∝ x1)›
‹C' ≠ L› and
corr_watched: ‹correctly_marked_as_binary b (x1, C', b')›
shows ‹correct_watching_except i j L (a, b, c, d, e, f, g(L := (g L)[j' := (x1, C', b')]))›
proof -
have
Hdisteq: ‹⋀La i' K' b''. La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
(La = L ⟶
distinct_watched (take i ((g(L := (g L)[j' := (x1, C, b')])) La) @ drop j ((g(L := (g L)[j' := (x1, C, b')])) La)))› and
Heq: ‹⋀La i' K' b''. La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
(La = L ⟶
(((i', K', b'')∈#mset (take i ((g(L := (g L)[j' := (x1, C, b')])) La) @ drop j ((g(L := (g L)[j' := (x1, C, b')])) La)) ⟶
i' ∈# dom_m b ⟶ K' ∈ set (b ∝ i') ∧ K' ≠ La ∧ correctly_marked_as_binary b (i', K', b'')) ∧
((i', K', b'')∈#mset (take i ((g(L := (g L)[j' := (x1, C, b')])) La) @ drop j ((g(L := (g L)[j' := (x1, C, b')])) La)) ⟶
b'' ⟶ i' ∈# dom_m b)) ∧
{#i ∈# fst `# mset (take i ((g(L := (g L)[j' := (x1, C, b')])) La) @ drop j ((g(L := (g L)[j' := (x1, C, b')])) La)).
i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#}))› and
Hdistneq: ‹⋀La i' K' b''. La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
(La ≠ L ⟶ distinct_watched (((g(L := (g L)[j' := (x1, C, b')])) La)))› and
Hneq: ‹⋀La i K b''. La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹ La ≠ L ⟹
distinct_watched (((g(L := (g L)[j' := (x1, C, b')])) La)) ∧
((i, K, b'')∈#mset ((g(L := (g L)[j' := (x1, C, b')])) La)⟶ i ∈# dom_m b ⟶
K ∈ set (b ∝ i) ∧ K ≠ La ∧ correctly_marked_as_binary b (i, K, b'')) ∧
((i, K, b'')∈#mset ((g(L := (g L)[j' := (x1, C, b')])) La)⟶ b'' ⟶ i ∈# dom_m b) ∧
{#i ∈# fst `# mset ((g(L := (g L)[j' := (x1, C, b')])) La). i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#})›
using corr unfolding correct_watching_except.simps
by fast+
define g' where ‹g' = g(L := (g L)[j' := (x1, C, b')])›
have g_g': ‹g(L := (g L)[j' := (x1, C', b')]) = g'(L := (g' L)[j' := (x1, C', b')])›
unfolding g'_def by auto
have H2: ‹fst `# mset ((g'(L := (g' L)[j' := (x1, C', b')])) La) = fst `# mset (g' La)› for La
unfolding g'_def
by (auto simp flip: mset_map simp: map_update)
have H3: ‹fst `#
mset
(take i ((g'(L := (g' L)[j' := (x1, C', b')])) La) @
drop j ((g'(L := (g' L)[j' := (x1, C', b')])) La)) =
fst `#
mset
(take i (g' La) @
drop j (g' La))› for La
unfolding g'_def
by (auto simp flip: mset_map drop_map simp: map_update)
have [simp]:
‹fst `# mset ((take i (g' L))[j' := (x1, C', b')]) = fst `# mset (take i (g' L))›
‹fst `# mset ((drop j ((g' L)[j' := (x1, C', b')]))) = fst `# mset (drop j (g' L))›
‹¬j' < j ⟹ fst `# mset ((drop j (g' L))[j' - j := (x1, C', b')]) = fst `# mset (drop j (g' L))›
unfolding g'_def
apply (auto simp flip: mset_map drop_map simp: map_update drop_update_swap; fail)
apply (auto simp flip: mset_map drop_map simp: map_update drop_update_swap; fail)
apply (auto simp flip: mset_map drop_map simp: map_update drop_update_swap; fail)
done
have ‹j' < length (g' L) ⟹ j' < i ⟹ (x1, C, b') ∈ set ((take i (g L))[j' := (x1, C, b')])›
using nth_mem[of ‹j'› ‹(take i (g L))[j' := (x1, C, b')]›] unfolding g'_def
by auto
then have H: ‹L ∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹ j' < length (g' L) ⟹
j' < i ⟹ b' ⟹ x1 ∈# dom_m b›
using C' Heq[of L x1 C b']
by (cases ‹j' < j›) (simp, auto)
have ‹¬ j' < j ⟹ j' - j < length (g' L) - j ⟹
(x1, C, b') ∈ set (drop j ((g L)[j' := (x1, C, b')]))›
using nth_mem[of ‹j'-j› ‹drop j ((g L)[j' := (x1, C, b')])›] unfolding g'_def
by auto
then have H': ‹L ∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹ ¬ j' < j ⟹
j' - j < length (g' L) - j ⟹ b' ⟹ x1 ∈# dom_m b›
using C' Heq[of L x1 C b'] unfolding g'_def
by (cases ‹j' < j›) auto
have dist: ‹La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
La = L ⟹
distinct_watched (take i ((g'(L := (g' L)[j' := (x1, C', b')])) La) @ drop j ((g'(L := (g' L)[j' := (x1, C', b')])) La))›
for La
using Hdisteq[of L] unfolding g_g'[symmetric]
by (cases ‹j' < j›)
(auto simp: map_update drop_update_swap)
have ‹La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
La = L ⟹
distinct_watched (take i ((g'(L := (g' L)[j' := (x1, C', b')])) La) @ drop j ((g'(L := (g' L)[j' := (x1, C', b')])) La)) ∧
((i', K, b'')∈#mset (take i ((g'(L := (g' L)[j' := (x1, C', b')])) La) @ drop j ((g'(L := (g' L)[j' := (x1, C', b')])) La)) ⟶
i' ∈# dom_m b ⟶ K ∈ set (b ∝ i') ∧ K ≠ La ∧ correctly_marked_as_binary b (i', K, b'')) ∧
((i', K, b'')∈#mset (take i ((g'(L := (g' L)[j' := (x1, C', b')])) La) @ drop j ((g'(L := (g' L)[j' := (x1, C', b')])) La)) ⟶
b'' ⟶ i' ∈# dom_m b) ∧
{#i ∈# fst `# mset (take i ((g'(L := (g' L)[j' := (x1, C', b')])) La) @ drop j ((g'(L := (g' L)[j' := (x1, C', b')])) La)).
i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#})› for La i' K b''
using C' Heq[of La i' K] Heq[of La i' K b'] H H' dist[of La] corr_watched unfolding g_g' g'_def[symmetric]
by (cases ‹j' < j›)
(auto elim!: in_set_upd_cases simp: drop_update_swap simp del: distinct_append)
moreover have ‹La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
(La ≠ L ⟶
distinct_watched ((g'(L := (g' L)[j' := (x1, C', b')])) La) ∧
(∀(i, K, ba)∈#mset ((g'(L := (g' L)[j' := (x1, C', b')])) La).
i ∈# dom_m b ⟶
K ∈ set (b ∝ i) ∧
K ≠ La ∧ correctly_marked_as_binary b (i, K, ba)) ∧
(∀(i, K, ba)∈#mset ((g'(L := (g' L)[j' := (x1, C', b')])) La).
ba ⟶ i ∈# dom_m b) ∧
{#i ∈# fst `# mset ((g'(L := (g' L)[j' := (x1, C', b')])) La).
i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#}))›
for La
using Hneq Hdistneq
unfolding correct_watching_except.simps g_g' g'_def[symmetric]
by auto
ultimately show ?thesis
unfolding correct_watching_except.simps g_g' g'_def[symmetric]
unfolding H2 H3
by blast
qed
lemma correct_watching_except_correct_watching_except_Suc_notin:
assumes
‹fst (watched_by S L ! w) ∉# dom_m (get_clauses_wl S)› and
j_w: ‹j ≤ w› and
w_le: ‹w < length (watched_by S L)› and
corr: ‹correct_watching_except j w L S›
shows ‹correct_watching_except j (Suc w) L (keep_watch L j w S)›
proof -
obtain M N D NE UE Q W where S: ‹S = (M, N, D, NE, UE, Q, W)› by (cases S)
have [simp]: ‹fst (W L ! w) ∉# dom_m N›
using assms unfolding S by auto
have
Hneq: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟶
(La ≠ L ⟶
distinct_watched (W La) ∧
((∀(i, K, b)∈#mset (W La). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (W La). b ⟶ i ∈# dom_m N)) ∧
{#i ∈# fst `# mset (W La). i ∈# dom_m N#} = clause_to_update La (M, N, D, NE, UE, {#}, {#}))› and
Heq: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟶
(La = L ⟶
distinct_watched (take j (W La) @ drop w (W La)) ∧
((∀(i, K, b)∈#mset (take j (W La) @ drop w (W La)). i ∈# dom_m N ⟶
K ∈ set (N ∝ i) ∧ K ≠ La ∧ correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (take j (W La) @ drop w (W La)). b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `# mset (take j (W La) @ drop w (W La)). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})))›
using corr unfolding S correct_watching_except.simps
by fast+
have eq: ‹mset (take j ((W(L := (W L)[j := W L ! w])) La) @ drop (Suc w) ((W(L := (W L)[j := W L ! w])) La)) =
remove1_mset (W L ! w) (mset (take j (W La) @ drop w (W La)))› if [simp]: ‹La = L› for La
using w_le j_w
by (auto simp: S take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]
list_update_append)
have ‹case x of (i, K, b) ⇒ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L› and
‹x ∈# mset (take j ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La))›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Heq[of L] w_le j_w
by (subst (asm) eq) (auto dest!: in_diffD)
moreover have ‹case x of (i, K, b) ⇒ b ⟶ i ∈# dom_m N›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L› and
‹x ∈# mset (take j ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La))›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Heq[of L] w_le j_w
by (subst (asm) eq) (force dest: in_diffD)+
moreover have ‹{#i ∈# fst `#
mset
(take j ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La)).
i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L›
for La :: ‹'a literal›
using that Heq[of L] w_le j_w
by (subst eq) (auto dest!: in_diffD simp: image_mset_remove1_mset_if)
moreover have ‹case x of (i, K, b) ⇒ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L› and
‹x ∈# mset ((W(L := (W L)[j := W L ! w])) La)›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Hneq[of La]
by simp
moreover have ‹case x of (i, K, b) ⇒ b ⟶ i ∈# dom_m N›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L› and
‹x ∈# mset ((W(L := (W L)[j := W L ! w])) La)›
for La :: ‹'a literal› and x :: ‹nat × 'a literal × bool›
using that Hneq[of La]
by auto
moreover have ‹{#i ∈# fst `# mset ((W(L := (W L)[j := W L ! w])) La). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L›
for La :: ‹'a literal›
using that Hneq[of La]
by simp
moreover have ‹distinct_watched ((W(L := (W L)[j := W L ! w])) La)›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La ≠ L›
for La :: ‹'a literal›
using that Hneq[of La]
by simp
moreover have ‹distinct_watched (take j ((W(L := (W L)[j := W L ! w])) La) @
drop (Suc w) ((W(L := (W L)[j := W L ! w])) La))›
if
‹La ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))› and
‹La = L›
for La :: ‹'a literal›
using that Heq[of L] w_le j_w apply -
apply (subst distinct_mset_mset_distinct[symmetric])
apply (subst mset_map)
apply (subst eq)
apply (solves simp)
apply (subst (asm) distinct_mset_mset_distinct[symmetric])
apply (subst (asm) mset_map)
apply (rule distinct_mset_mono[of _ ‹{#i. (i, j, k) ∈# mset (take j (W L) @ drop w (W L))#}›])
by (auto simp: image_mset_remove1_mset_if split: if_splits)
ultimately show ?thesis
unfolding S keep_watch_def prod.simps correct_watching_except.simps
by fast
qed
lemma correct_watching_except_correct_watching_except_update_clause:
assumes
corr: ‹correct_watching_except (Suc j) (Suc w) L
(M, N, D, NE, UE, Q, W(L := (W L)[j := W L ! w]))› and
j_w: ‹j ≤ w› and
w_le: ‹w < length (W L)› and
L': ‹L' ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))›
‹L' ∈ set (N ∝ x1)›and
L_L: ‹L ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE))› and
L: ‹L ≠ N ∝ x1 ! xa› and
dom: ‹x1 ∈# dom_m N› and
i_xa: ‹i < length (N ∝ x1)› ‹xa < length (N ∝ x1)› and
[simp]: ‹W L ! w = (x1, x2, b)› and
N_i: ‹N ∝ x1 ! i = L› ‹N ∝ x1 ! (1 -i) ≠ L›‹N ∝ x1 ! xa ≠ L› and
N_xa: ‹N ∝ x1 ! xa ≠ N ∝ x1 ! i› ‹N ∝ x1 ! xa ≠ N ∝ x1 ! (Suc 0 - i)›and
i_2: ‹i < 2› and ‹xa ≥ 2› and
L_neq: ‹L' ≠ N ∝ x1 ! xa›
shows ‹correct_watching_except j (Suc w) L
(M, N(x1 ↪ swap (N ∝ x1) i xa), D, NE, UE, Q, W
(L := (W L)[j := (x1, x2, b)],
N ∝ x1 ! xa := W (N ∝ x1 ! xa) @ [(x1, L', b)]))›
proof -
define W' where ‹W' ≡ W(L := (W L)[j := W L ! w])›
have ‹length (N ∝ x1) > 2›
using i_2 i_xa assms
by (auto simp: correctly_marked_as_binary.simps)
have
Heq: ‹⋀La i K b. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
La = L ⟹
distinct_watched (take (Suc j) (W' La) @ drop (Suc w) (W' La)) ∧
((i, K, b)∈#mset (take (Suc j) (W' La) @ drop (Suc w) (W' La)) ⟶
i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧ correctly_marked_as_binary N (i, K, b)) ∧
((i, K, b)∈#mset (take (Suc j) (W' La) @ drop (Suc w) (W' La)) ⟶
b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `#
mset
(take (Suc j) (W' La) @ drop (Suc w) (W' La)).
i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})› and
Hneq: ‹⋀La i K b. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
La ≠ L ⟹
distinct_watched (W' La) ∧
((i, K, b)∈#mset (W' La) ⟶ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)) ∧
((i, K, b)∈#mset (W' La) ⟶ b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `# mset (W' La). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})› and
Hneq2: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
(La ≠ L ⟶
distinct_watched (W' La) ∧
{#i ∈# fst `# mset (W' La). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#}))›
using corr unfolding correct_watching_except.simps W'_def[symmetric]
by fast+
have H1: ‹mset `# ran_mf (N(x1 ↪ swap (N ∝ x1) i xa)) = mset `# ran_mf N›
using dom i_xa distinct_mset_dom[of N]
by (auto simp: ran_m_def dest!: multi_member_split intro!: image_mset_cong2)
have W_W': ‹W
(L := (W L)[j := (x1, x2, b)], N ∝ x1 ! xa := W (N ∝ x1 ! xa) @ [(x1, L', b)]) =
W'(N ∝ x1 ! xa := W (N ∝ x1 ! xa) @ [(x1, L', b)])›
unfolding W'_def
by auto
have W_W2: ‹W (N ∝ x1 ! xa) = W' (N ∝ x1 ! xa)›
using L unfolding W'_def by auto
have H2: ‹set (swap (N ∝ x1) i xa) = set (N ∝ x1)›
using i_xa by auto
have [simp]:
‹set (fst (the (if x1 = ia then Some (swap (N ∝ x1) i xa, irred N x1) else fmlookup N ia))) =
set (fst (the (fmlookup N ia)))› for ia
using H2
by auto
have H3: ‹i = x1 ∨ i ∈# remove1_mset x1 (dom_m N) ⟷ i ∈# dom_m N› for i
using dom by (auto dest: multi_member_split)
have set_N_swap_x1: ‹set (watched_l (swap (N ∝ x1) i xa)) = {N ∝ x1 ! (1 -i), N ∝ x1 ! xa}›
using i_2 i_xa ‹xa ≥ 2› N_i
by (cases ‹N ∝ x1›; cases ‹tl (N ∝ x1)›; cases i; cases ‹i-1›; cases xa)
(auto simp: swap_def split: nat.splits)
have set_N_x1: ‹set (watched_l (N ∝ x1)) = {N ∝ x1 ! (1 -i), N ∝ x1 ! i}›
using i_2 i_xa ‹xa ≥ 2› N_i
by (cases i) (auto simp: swap_def take_2_if)
have La_in_notin_swap: ‹La ∈ set (watched_l (N ∝ x1)) ⟹
La ∉ set (watched_l (swap (N ∝ x1) i xa)) ⟹ La = L› for La
using i_2 i_xa ‹xa ≥ 2› N_i
by (auto simp: set_N_x1 set_N_swap_x1)
have L_notin_swap: ‹L ∉ set (watched_l (swap (N ∝ x1) i xa))›
using i_2 i_xa ‹xa ≥ 2› N_i
by (auto simp: set_N_x1 set_N_swap_x1)
have N_xa_in_swap: ‹N ∝ x1 ! xa ∈ set (watched_l (swap (N ∝ x1) i xa))›
using i_2 i_xa ‹xa ≥ 2› N_i
by (auto simp: set_N_x1 set_N_swap_x1)
have H4: ‹(i = x1 ⟶ K ∈ set (N ∝ x1) ∧ K ≠ La) ∧ (i ∈# remove1_mset x1 (dom_m N) ⟶ K ∈ set (N ∝ i) ∧ K ≠ La) ⟷
(i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La)› for i P K La
using dom by (auto dest: multi_member_split)
have [simp]: ‹x1 ∉# Ab ⟹
{#C ∈# Ab.
(x1 = C ⟶ Q C) ∧
(x1 ≠ C ⟶ R C)#} =
{#C ∈# Ab. R C#}› for Ab Q R
by (auto intro: filter_mset_cong)
have bin:
‹correctly_marked_as_binary N (x1, x2, b)›
using Heq[of L ‹fst (W L ! w)› ‹fst (snd (W L ! w ))› ‹snd (snd (W L ! w))›] j_w w_le dom L'
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append L_L)
have x1_new: ‹x1 ∉ fst ` set (W (N ∝ x1 ! xa))›
proof (rule ccontr)
assume H: "¬ ?thesis"
have ‹N ∝ x1 ! xa
∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE))›
using dom in_clause_in_all_lits_of_m[of ‹N ∝ x1 ! xa› ‹mset (N ∝ x1)›] i_xa
by (auto simp: all_lits_of_mm_union ran_m_def all_lits_of_mm_add_mset
dest!: multi_member_split)
then have ‹{#i ∈# fst `# mset (W (N ∝ x1 ! xa)). i ∈# dom_m N#} =
clause_to_update (N ∝ x1 ! xa) (M, N, D, NE, UE, {#}, {#})›
using Hneq[of ‹N ∝ x1 ! xa›] L unfolding W'_def
by simp
then have ‹x1 ∈# clause_to_update (N ∝ x1 ! xa) (M, N, D, NE, UE, {#}, {#})›
using H dom by (metis (no_types, lifting) mem_Collect_eq set_image_mset
set_mset_filter set_mset_mset)
then show False
using N_xa i_2 i_xa
by (cases i; cases ‹N ∝ x1 ! xa›)
(auto simp: clause_to_update_def take_2_if split: if_splits)
qed
let ?N = ‹N(x1 ↪ swap (N ∝ x1) i xa)›
have ‹L ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹ La = L ⟹
x ∈ set (take j (W L)) ∨ x ∈ set (drop (Suc w) (W L)) ⟹
case x of (i, K, b) ⇒ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ L ∧
correctly_marked_as_binary ?N (i, K, b)› for La x
using Heq[of L ‹fst x› ‹fst (snd x)› ‹snd (snd x)›] j_w w_le
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append correctly_marked_as_binary.simps
split: if_splits)
moreover have ‹L ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹ La = L ⟹
x ∈ set (take j (W L)) ∨ x ∈ set (drop (Suc w) (W L)) ⟹
case x of (i, K, b) ⇒b ⟶ i ∈# dom_m N› for La x
using Heq[of L ‹fst x› ‹fst (snd x)› ‹snd (snd x)›] j_w w_le
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append correctly_marked_as_binary.simps split: if_splits)
moreover have ‹L ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹
La = L ⟹
distinct_watched (take j (W L) @ drop (Suc w) (W L)) ∧
{#i ∈# fst `# mset (take j (W L)). i ∈# dom_m N#} + {#i ∈# fst `# mset (drop (Suc w) (W L)). i ∈# dom_m N#} =
clause_to_update L (M, N(x1 ↪ swap (N ∝ x1) i xa), D, NE, UE, {#}, {#})› for La
using Heq[of L x1 x2 b] j_w w_le dom L_notin_swap N_xa_in_swap distinct_mset_dom[of N]
i_xa i_2 assms(12)
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append set_N_x1 assms(11)
clause_to_update_def dest!: multi_member_split split: if_splits
intro: filter_mset_cong2)
moreover have ‹La ∈# all_lits_of_mm
({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹
La ≠ L ⟹
x ∈ set (if La = N ∝ x1 ! xa
then W' (N ∝ x1 ! xa) @ [(x1, L', b)]
else (W(L := (W L)[j := (x1, x2, b)])) La) ⟹
case x of
(i, K, b) ⇒ i ∈# dom_m ?N ⟶ K ∈ set (?N ∝ i) ∧ K ≠ La ∧ correctly_marked_as_binary ?N (i, K, b)› for La x
using Hneq[of La ‹fst x› ‹fst (snd x)› ‹snd (snd x)›] j_w w_le L' L_neq bin dom
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append
correctly_marked_as_binary.simps split: if_splits)
moreover have ‹La ∈# all_lits_of_mm
({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹
La ≠ L ⟹
x ∈ set (if La = N ∝ x1 ! xa
then W' (N ∝ x1 ! xa) @ [(x1, L', b)]
else (W(L := (W L)[j := (x1, x2, b)])) La) ⟹
case x of (i, K, b) ⇒ b ⟶ i ∈# dom_m N› for La x
using Hneq[of La ‹fst x› ‹fst (snd x)› ‹snd (snd x)›] j_w w_le L' L_neq ‹length (N ∝ x1) > 2›
dom
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append correctly_marked_as_binary.simps split: if_splits)
moreover have ‹La ∈# all_lits_of_mm
({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹
La ≠ L ⟹ distinct_watched ((W
(L := (W L)[j := (x1, x2, b)],
N ∝ x1 ! xa := W (N ∝ x1 ! xa) @ [(x1, L', b)])) La)› for La x
using Hneq[of La] j_w w_le L' L_neq ‹length (N ∝ x1) > 2›
dom x1_new
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append correctly_marked_as_binary.simps split: if_splits)
moreover {
have ‹N ∝ x1 ! xa ∉ set (watched_l (N ∝ x1))›
using N_xa
by (auto simp: set_N_x1 set_N_swap_x1)
then have ‹ ⋀Ab Ac La.
all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) = add_mset L' (add_mset (N ∝ x1 ! xa) Ac) ⟹
dom_m N = add_mset x1 Ab ⟹
N ∝ x1 ! xa ≠ L ⟹
{#i ∈# fst `# mset (W (N ∝ x1 ! xa)). i = x1 ∨ i ∈# Ab#} =
{#C ∈# Ab. N ∝ x1 ! xa ∈ set (watched_l (N ∝ C))#} ›
using Hneq2[of ‹N ∝ x1 ! xa›] L_neq unfolding W_W' W_W2
by (auto simp: clause_to_update_def split: if_splits)
then have ‹La ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE)) ⟹
La ≠ L ⟹
distinct_watched (W' La) ∧
(x1 ∈# dom_m N ⟶
(La = N ∝ x1 ! xa ⟶
add_mset x1 {#i ∈# fst `# mset (W' (N ∝ x1 ! xa)). i ∈# dom_m N#} =
clause_to_update (N ∝ x1 ! xa) (M, N(x1 ↪ swap (N ∝ x1) i xa), D, NE, UE, {#}, {#})) ∧
(La ≠ N ∝ x1 ! xa ⟶
{#i ∈# fst `# mset (W La). i ∈# dom_m N#} =
clause_to_update La (M, N(x1 ↪ swap (N ∝ x1) i xa), D, NE, UE, {#}, {#}))) ∧
(x1 ∉# dom_m N ⟶
(La = N ∝ x1 ! xa ⟶
{#i ∈# fst `# mset (W' (N ∝ x1 ! xa)). i ∈# dom_m N#} =
clause_to_update (N ∝ x1 ! xa) (M, N(x1 ↪ swap (N ∝ x1) i xa), D, NE, UE, {#}, {#})) ∧
(La ≠ N ∝ x1 ! xa ⟶
{#i ∈# fst `# mset (W La). i ∈# dom_m N#} =
clause_to_update La (M, N(x1 ↪ swap (N ∝ x1) i xa), D, NE, UE, {#}, {#})))› for La
using Hneq2[of La] j_w w_le L' dom distinct_mset_dom[of N] L_notin_swap N_xa_in_swap L_neq
by (auto simp: take_Suc_conv_app_nth W'_def list_update_append clause_to_update_def
add_mset_eq_add_mset set_N_x1 set_N_swap_x1 assms(11) N_i
dest!: multi_member_split La_in_notin_swap
split: if_splits
intro: image_mset_cong2 intro: filter_mset_cong2)
}
ultimately show ?thesis
using L j_w
unfolding correct_watching_except.simps H1 W'_def[symmetric] W_W' H2 W_W2 H4 H3
by (intro conjI impI ballI)
(simp_all add: L' W_W' W_W2 H3 H4 drop_map)
qed
definition unit_propagation_inner_loop_wl_loop_pre where
‹unit_propagation_inner_loop_wl_loop_pre L = (λ(j, w, S).
w < length (watched_by S L) ∧ j ≤ w ∧
unit_propagation_inner_loop_wl_loop_inv L (j, w, S))›
text ‹It was too hard to align the programi unto a refinable form directly.›
definition unit_propagation_inner_loop_body_wl_int :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_wl ⇒
(nat × nat × 'v twl_st_wl) nres› where
‹unit_propagation_inner_loop_body_wl_int L j w S = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let S = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S j w L);
let val_K = polarity (get_trail_wl S) K;
if val_K = Some True
then RETURN (j+1, w+1, S)
else do { ―‹Now the costly operations:›
if C ∉# dom_m (get_clauses_wl S)
then RETURN (j, w+1, S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S)∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S) L';
if val_L' = Some True
then update_blit_wl L C b j w L' S
else do {
f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S);
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)}
else do {RETURN (j+1, w+1, propagate_lit_wl_general L' C i S)}
}
| Some f ⇒ do {
let K = get_clauses_wl S ∝ C ! f;
let val_L' = polarity (get_trail_wl S) K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L C b j w i f S
}
}
}
}
}›
definition propagate_proper_bin_case where
‹propagate_proper_bin_case L L' S C ⟷
C ∈# dom_m (get_clauses_wl S) ∧ length ((get_clauses_wl S)∝C) = 2 ∧
set (get_clauses_wl S∝C) = {L, L'} ∧ L ≠ L'›
definition unit_propagation_inner_loop_body_wl :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_wl ⇒
(nat × nat × 'v twl_st_wl) nres› where
‹unit_propagation_inner_loop_body_wl L j w S = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let S = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S j w L);
let val_K = polarity (get_trail_wl S) K;
if val_K = Some True
then RETURN (j+1, w+1, S)
else do {
if b then do {
ASSERT(propagate_proper_bin_case L K S C);
if val_K = Some False
then RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)
else do { ―‹This is non-optimal (memory access: relax invariant!):›
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
RETURN (j+1, w+1, propagate_lit_wl_bin K C i S)}
} ―‹Now the costly operations:›
else if C ∉# dom_m (get_clauses_wl S)
then RETURN (j, w+1, S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S)∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S) L';
if val_L' = Some True
then update_blit_wl L C b j w L' S
else do {
f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S);
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)}
else do {RETURN (j+1, w+1, propagate_lit_wl L' C i S)}
}
| Some f ⇒ do {
let K = get_clauses_wl S ∝ C ! f;
let val_L' = polarity (get_trail_wl S) K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L C b j w i f S
}
}
}
}
}›
lemma [twl_st_wl]: ‹get_clauses_wl (keep_watch L j w S) = get_clauses_wl S›
by (cases S) (auto simp: keep_watch_def)
lemma unit_propagation_inner_loop_body_wl_int_alt_def:
‹unit_propagation_inner_loop_body_wl_int L j w S = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let b' = (C ∉# dom_m (get_clauses_wl S));
if b' then do {
let S = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S j w L);
let K = K;
let val_K = polarity (get_trail_wl S) K in
if val_K = Some True
then RETURN (j+1, w+1, S)
else ―‹Now the costly operations:›
RETURN (j, w+1, S)
}
else do {
let S' = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S' j w L);
K ← SPEC((=) K);
let val_K = polarity (get_trail_wl S') K in
if val_K = Some True
then RETURN (j+1, w+1, S')
else do { ―‹Now the costly operations:›
let i = (if ((get_clauses_wl S')∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S')∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S') L';
if val_L' = Some True
then update_blit_wl L C b j w L' S'
else do {
f ← find_unwatched_l (get_trail_wl S') (get_clauses_wl S'∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S');
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S' ∝ C) S')}
else do {RETURN (j+1, w+1, propagate_lit_wl_general L' C i S')}
}
| Some f ⇒ do {
let K = get_clauses_wl S' ∝ C ! f;
let val_L' = polarity (get_trail_wl S') K;
if val_L' = Some True
then update_blit_wl L C b j w K S'
else update_clause_wl L C b j w i f S'
}
}
}
}
}›
proof -
text ‹We first define an intermediate step where both then and else branches are the same.›
have E: ‹unit_propagation_inner_loop_body_wl_int L j w S = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let b' = (C ∉# dom_m (get_clauses_wl S));
if b' then do {
let S = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S j w L);
let K = K;
let val_K = polarity (get_trail_wl S) K in
if val_K = Some True
then RETURN (j+1, w+1, S)
else do { ―‹Now the costly operations:›
if b'
then RETURN (j, w+1, S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S)∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S) L';
if val_L' = Some True
then update_blit_wl L C b j w L' S
else do {
f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S);
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)}
else do {RETURN (j+1, w+1, propagate_lit_wl_general L' C i S)}
}
| Some f ⇒ do {
let K = get_clauses_wl S ∝ C ! f;
let val_L' = polarity (get_trail_wl S) K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L C b j w i f S
}
}
}
}
}
else do {
let S' = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S' j w L);
K ← SPEC((=) K);
let val_K = polarity (get_trail_wl S') K in
if val_K = Some True
then RETURN (j+1, w+1, S')
else do { ―‹Now the costly operations:›
if b'
then RETURN (j, w+1, S')
else do {
let i = (if ((get_clauses_wl S')∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S')∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S') L';
if val_L' = Some True
then update_blit_wl L C b j w L' S'
else do {
f ← find_unwatched_l (get_trail_wl S') (get_clauses_wl S'∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S');
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S' ∝ C) S')}
else do {RETURN (j+1, w+1, propagate_lit_wl_general L' C i S')}
}
| Some f ⇒ do {
let K = get_clauses_wl S' ∝ C ! f;
let val_L' = polarity (get_trail_wl S') K;
if val_L' = Some True
then update_blit_wl L C b j w K S'
else update_clause_wl L C b j w i f S'
}
}
}
}
}
}›
(is ‹_ = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let b' = (C ∉# dom_m (get_clauses_wl S));
if b' then do {
?P C K b b'
}
else do {
?Q C K b b'
}
}›)
unfolding unit_propagation_inner_loop_body_wl_int_def if_not_swap bind_to_let_conv
SPEC_eq_is_RETURN twl_st_wl
unfolding Let_def if_not_swap bind_to_let_conv
SPEC_eq_is_RETURN twl_st_wl
apply (subst if_cancel)
apply (intro bind_cong_nres case_prod_cong if_cong[OF refl] refl)
done
show ?thesis
unfolding E
apply (subst if_replace_cond[of _ ‹?P _ _ _›])
unfolding if_True if_False
apply auto
done
qed
subsection ‹The Functions›
subsubsection ‹Inner Loop›
lemma clause_to_update_mapsto_upd_If:
assumes
i: ‹i ∈# dom_m N›
shows
‹clause_to_update L (M, N(i ↪ C'), C, NE, UE, WS, Q) =
(if L ∈ set (watched_l C')
then add_mset i (remove1_mset i (clause_to_update L (M, N, C, NE, UE, WS, Q)))
else remove1_mset i (clause_to_update L (M, N, C, NE, UE, WS, Q)))›
proof -
define D' where ‹D' = dom_m N - {#i#}›
then have [simp]: ‹dom_m N = add_mset i D'›
using assms by (simp add: mset_set.remove)
have [simp]: ‹i ∉# D'›
using assms distinct_mset_dom[of N] unfolding D'_def by auto
have ‹{#C ∈# D'.
(i = C ⟶ L ∈ set (watched_l C')) ∧
(i ≠ C ⟶ L ∈ set (watched_l (N ∝ C)))#} =
{#C ∈# D'. L ∈ set (watched_l (N ∝ C))#}›
by (rule filter_mset_cong2) auto
then show ?thesis
unfolding clause_to_update_def
by auto
qed
lemma unit_propagation_inner_loop_body_l_with_skip_alt_def:
‹unit_propagation_inner_loop_body_l_with_skip L (S', n) = do {
ASSERT (clauses_to_update_l S' ≠ {#} ∨ 0 < n);
ASSERT (unit_propagation_inner_loop_l_inv L (S', n));
b ← SPEC (λb. (b ⟶ 0 < n) ∧ (¬ b ⟶ clauses_to_update_l S' ≠ {#}));
if ¬ b
then do {
ASSERT (clauses_to_update_l S' ≠ {#});
X2 ← select_from_clauses_to_update S';
ASSERT (unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2));
x ← SPEC (λK. K ∈ set (get_clauses_l (fst X2) ∝ snd X2));
let v = polarity (get_trail_l (fst X2)) x;
if v = Some True then let T = fst X2 in RETURN (T, if get_conflict_l T = None then n else 0)
else let v = if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1;
va = get_clauses_l (fst X2) ∝ snd X2 ! (1 - v); vaa = polarity (get_trail_l (fst X2)) va
in
if vaa = Some True
then let T = fst X2 in RETURN (T, if get_conflict_l T = None then n else 0)
else do {
x ← find_unwatched_l (get_trail_l (fst X2)) (get_clauses_l (fst X2) ∝ snd X2);
case x of
None ⇒
if vaa = Some False
then let T = set_conflict_l (get_clauses_l (fst X2) ∝ snd X2) (fst X2)
in RETURN (T, if get_conflict_l T = None then n else 0)
else let T = propagate_lit_l va (snd X2) v (fst X2)
in RETURN (T, if get_conflict_l T = None then n else 0)
| Some a ⇒ do {
x ← ASSERT (a < length (get_clauses_l (fst X2) ∝ snd X2));
let K = (get_clauses_l (fst X2) ∝ (snd X2))!a;
let val_K = polarity (get_trail_l (fst X2)) K;
if val_K = Some True
then let T = fst X2 in RETURN (T, if get_conflict_l T = None then n else 0)
else do {
T ← update_clause_l (snd X2) v a (fst X2);
RETURN (T, if get_conflict_l T = None then n else 0)
}
}
}
}
else RETURN (S', n - 1)
}›
proof -
have remove_pairs: ‹do {(x2, x2') ← (b0 :: _ nres); F x2 x2'} =
do {X2 ← b0; F (fst X2) (snd X2)}› for T a0 b0 a b c f t F
by (meson case_prod_unfold)
have H1: ‹do {T ← do {x ← a ; b x}; RETURN (f T)} =
do {x ← a; T ← b x; RETURN (f T)}› for T a0 b0 a b c f t
by auto
have H2: ‹do{T ← let v = val in g v; (f T :: _ nres)} =
do{let v = val; T ← g v; f T} › for g f T val
by auto
have H3: ‹do{T ← if b then g else g'; (f T :: _ nres)} =
(if b then do{T ← g; f T} else do{T ← g'; f T}) › for g g' f T b
by auto
have H4: ‹do{T ← case x of None ⇒ g | Some a ⇒ g' a; (f T :: _ nres)} =
(case x of None ⇒ do{T ← g; f T} | Some a ⇒ do{T ← g' a; f T}) › for g g' f T b x
by (cases x) auto
show ?thesis
unfolding unit_propagation_inner_loop_body_l_with_skip_def prod.case
unit_propagation_inner_loop_body_l_def remove_pairs
unfolding H1 H2 H3 H4 bind_to_let_conv
by simp
qed
lemma keep_watch_st_wl[twl_st_wl]:
‹get_unit_clauses_wl (keep_watch L j w S) = get_unit_clauses_wl S›
‹get_conflict_wl (keep_watch L j w S) = get_conflict_wl S›
‹get_trail_wl (keep_watch L j w S) = get_trail_wl S›
by (cases S; auto simp: keep_watch_def; fail)+
declare twl_st_wl[simp]
lemma correct_watching_except_correct_watching_except_propagate_lit_wl:
assumes
corr: ‹correct_watching_except j w L S› and
i_le: ‹Suc 0 < length (get_clauses_wl S ∝ C)› and
C: ‹C ∈# dom_m (get_clauses_wl S)›
shows ‹correct_watching_except j w L (propagate_lit_wl_general L' C i S)›
proof -
obtain M N D NE UE Q W where S: ‹S = (M, N, D, NE, UE, Q, W)› by (cases S)
have
Hneq: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
La ≠ L ⟹
(∀(i, K, b)∈#mset (W La). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (W La). b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `# mset (W La). i ∈# dom_m N#} = clause_to_update La (M, N, D, NE, UE, {#}, {#})› and
Heq: ‹⋀La. La∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
La = L ⟹
(∀(i, K, b)∈#mset (take j (W La) @ drop w (W La)). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ La ∧
correctly_marked_as_binary N (i, K, b)) ∧
(∀(i, K, b)∈#mset (take j (W La) @ drop w (W La)). b ⟶ i ∈# dom_m N) ∧
{#i ∈# fst `# mset (take j (W La) @ drop w (W La)). i ∈# dom_m N#} =
clause_to_update La (M, N, D, NE, UE, {#}, {#})›
using corr unfolding S correct_watching_except.simps
by fast+
let ?N = ‹if length (N ∝ C) > 2 then N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)) else N›
have ‹Suc 0 - i < length (N ∝ C)› and ‹0 < length (N ∝ C)›
using i_le
by (auto simp: S)
then have [simp]: ‹mset (swap (N ∝ C) 0 (Suc 0 - i)) = mset (N ∝ C)›
by (auto simp: S)
have H1[simp]: ‹{#mset (fst x). x ∈# ran_m ?N#} =
{#mset (fst x). x ∈# ran_m N#}›
using C
by (auto dest!: multi_member_split simp: ran_m_def S
intro!: image_mset_cong)
have H2: ‹mset `# ran_mf ?N = mset `# ran_mf N›
using H1 by auto
have H3: ‹dom_m ?N = dom_m N›
using C by (auto simp: S)
have H4: ‹set (?N ∝ ia) =
set (N ∝ ia)› for ia
using i_le
by (cases ‹C = ia›) (auto simp: S)
have H5: ‹set (watched_l (?N ∝ ia)) = set (watched_l (N ∝ ia))› for ia
using i_le
by (cases ‹C = ia›; cases i; cases ‹N ∝ ia›; cases ‹tl (N ∝ ia)›) (auto simp: S swap_def)
have [iff]: ‹correctly_marked_as_binary N C' ⟷ correctly_marked_as_binary ?N C'› for C' ia
by (cases C')
(auto simp: correctly_marked_as_binary.simps)
show ?thesis
using corr
unfolding S propagate_lit_wl_general_def prod.simps correct_watching_except.simps Let_def
H1 H2 H3 H4 clause_to_update_def get_clauses_l.simps H5
by fast
qed
lemma unit_propagation_inner_loop_body_wl_int_alt_def2:
‹unit_propagation_inner_loop_body_wl_int L j w S = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let S = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S j w L);
let val_K = polarity (get_trail_wl S) K;
if val_K = Some True
then RETURN (j+1, w+1, S)
else do { ―‹Now the costly operations:›
if b then
if C ∉# dom_m (get_clauses_wl S)
then RETURN (j, w+1, S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S)∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S) L';
if val_L' = Some True
then update_blit_wl L C b j w L' S
else do {
f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S);
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)}
else do {RETURN (j+1, w+1, propagate_lit_wl_general L' C i S)}
}
| Some f ⇒ do {
let K = get_clauses_wl S ∝ C ! f;
let val_L' = polarity (get_trail_wl S) K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L C b j w i f S
}
}
}
else
if C ∉# dom_m (get_clauses_wl S)
then RETURN (j, w+1, S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S)∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S) L';
if val_L' = Some True
then update_blit_wl L C b j w L' S
else do {
f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S);
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)}
else do {RETURN (j+1, w+1, propagate_lit_wl_general L' C i S)}
}
| Some f ⇒ do {
let K = get_clauses_wl S ∝ C ! f;
let val_L' = polarity (get_trail_wl S) K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L C b j w i f S
}
}
}
}
}›
unfolding unit_propagation_inner_loop_body_wl_int_def if_not_swap bind_to_let_conv
SPEC_eq_is_RETURN twl_st_wl
unfolding Let_def if_not_swap bind_to_let_conv
SPEC_eq_is_RETURN twl_st_wl
apply (subst if_cancel)
apply (intro bind_cong_nres case_prod_cong if_cong[OF refl] refl)
done
lemma unit_propagation_inner_loop_body_wl_alt_def:
‹unit_propagation_inner_loop_body_wl L j w S = do {
ASSERT(unit_propagation_inner_loop_wl_loop_pre L (j, w, S));
let (C, K, b) = (watched_by S L) ! w;
let S = keep_watch L j w S;
ASSERT(unit_prop_body_wl_inv S j w L);
let val_K = polarity (get_trail_wl S) K;
if val_K = Some True
then RETURN (j+1, w+1, S)
else do {
if b then do {
if False
then RETURN (j, w+1, S)
else
if False ― ‹\<^term>‹val_L' = Some True››
then RETURN (j, w+1, S)
else do {
f ← RETURN (None :: nat option);
case f of
None ⇒ do {
ASSERT(propagate_proper_bin_case L K S C);
if val_K = Some False
then RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
RETURN (j+1, w+1, propagate_lit_wl_bin K C i S)}
}
| _ ⇒ RETURN (j, w+1, S)
}
} ―‹Now the costly operations:›
else if C ∉# dom_m (get_clauses_wl S)
then RETURN (j, w+1, S)
else do {
let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1);
let L' = ((get_clauses_wl S)∝C) ! (1 - i);
let val_L' = polarity (get_trail_wl S) L';
if val_L' = Some True
then update_blit_wl L C b j w L' S
else do {
f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C);
ASSERT (unit_prop_body_wl_find_unwatched_inv f C S);
case f of
None ⇒ do {
if val_L' = Some False
then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)}
else do {RETURN (j+1, w+1, propagate_lit_wl L' C i S)}
}
| Some f ⇒ do {
let K = get_clauses_wl S ∝ C ! f;
let val_L' = polarity (get_trail_wl S) K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L C b j w i f S
}
}
}
}
}›
unfolding unit_propagation_inner_loop_body_wl_def if_not_swap bind_to_let_conv
SPEC_eq_is_RETURN twl_st_wl
unfolding Let_def if_not_swap bind_to_let_conv
SPEC_eq_is_RETURN twl_st_wl if_False
apply (intro bind_cong_nres case_prod_cong if_cong[OF refl] refl)
apply auto
done
lemma
fixes S :: ‹'v twl_st_wl› and S' :: ‹'v twl_st_l› and L :: ‹'v literal› and w :: nat
defines [simp]: ‹C' ≡ fst (watched_by S L ! w)›
defines
[simp]: ‹T ≡ remove_one_lit_from_wq C' S'›
defines
[simp]: ‹C'' ≡ get_clauses_l S' ∝ C'›
assumes
S_S': ‹(S, S') ∈ state_wl_l (Some (L, w))› and
w_le: ‹w < length (watched_by S L)› and
j_w: ‹j ≤ w› and
corr_w: ‹correct_watching_except j w L S› and
inner_loop_inv: ‹unit_propagation_inner_loop_wl_loop_inv L (j, w, S)› and
n: ‹n = size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl S)) (mset (drop w (watched_by S L))))› and
confl_S: ‹get_conflict_wl S = None›
shows unit_propagation_inner_loop_body_wl_wl_int: ‹unit_propagation_inner_loop_body_wl L j w S ≤
⇓ Id (unit_propagation_inner_loop_body_wl_int L j w S)›
proof -
obtain bL bin where SLw: ‹watched_by S L ! w = (C', bL, bin)›
using C'_def by (cases ‹watched_by S L ! w›) auto
define i :: nat where
‹i ≡ (if get_clauses_wl S ∝ C' ! 0 = L then 0 else 1)›
have
l_wl_inv: ‹unit_prop_body_wl_inv S j w L› (is ?inv) and
clause_ge_0: ‹0 < length (get_clauses_l T ∝ C')› (is ?ge) and
L_def: ‹defined_lit (get_trail_wl S) L› ‹-L ∈ lits_of_l (get_trail_wl S)›
‹L ∉ lits_of_l (get_trail_wl S)› (is ?L_def) and
i_le: ‹i < length (get_clauses_wl S ∝ C')› (is ?i_le) and
i_le2: ‹1-i < length (get_clauses_wl S ∝ C')› (is ?i_le2) and
C'_dom: ‹C' ∈# dom_m (get_clauses_l T)› (is ?C'_dom) and
L_watched: ‹L ∈ set (watched_l (get_clauses_l T ∝ C'))› (is ?L_w) and
dist_clss: ‹distinct_mset_mset (mset `# ran_mf (get_clauses_wl S))› and
confl: ‹get_conflict_l T = None› (is ?confl) and
alien_L:
‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)›
(is ?alien) and
alien_L':
‹L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S)›
(is ?alien') and
alien_L'':
‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_clauses_wl S)›
(is ?alien'') and
correctly_marked_as_binary: ‹correctly_marked_as_binary (get_clauses_wl S) (C', bL, bin)›
if
‹unit_propagation_inner_loop_body_l_inv L C' T›
proof -
have ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that unfolding unit_prop_body_wl_inv_def by fast+
then obtain T' where
T_T': ‹(set_clauses_to_update_l (clauses_to_update_l T + {#C'#}) T, T') ∈ twl_st_l (Some L)› and
struct_invs: ‹twl_struct_invs T'› and
‹twl_stgy_invs T'› and
C'_dom: ‹C' ∈# dom_m (get_clauses_l T)› and
‹0 < C'› and
ge_0: ‹0 < length (get_clauses_l T ∝ C')› and
‹no_dup (get_trail_l T)› and
i_le: ‹(if get_clauses_l T ∝ C' ! 0 = L then 0 else 1)
< length (get_clauses_l T ∝ C')› and
i_le2: ‹1 - (if get_clauses_l T ∝ C' ! 0 = L then 0 else 1)
< length (get_clauses_l T ∝ C')› and
L_watched: ‹L ∈ set (watched_l (get_clauses_l T ∝ C'))› and
confl: ‹get_conflict_l T = None›
unfolding unit_propagation_inner_loop_body_l_inv_def by blast
show ?i_le and ?C'_dom and ?L_w and ?i_le2
using S_S' i_le C'_dom L_watched i_le2 unfolding i_def by auto
have
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T')› and
dup: ‹no_duplicate_queued T'› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T')› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of T')›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by blast+
have n_d: ‹no_dup (trail (state⇩W_of T'))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by auto
have 1: ‹C ∈# clauses_to_update T' ⟹
add_mset (fst C) (literals_to_update T') ⊆#
uminus `# lit_of `# mset (get_trail T')› for C
using dup unfolding no_duplicate_queued_alt_def
by blast
have H: ‹(L, twl_clause_of C'') ∈# clauses_to_update T'›
using twl_st_l(5)[OF T_T']
by (auto simp: twl_st_l)
have uL_M: ‹-L ∈ lits_of_l (get_trail T')›
using mset_le_add_mset_decr_left2[OF 1[OF H]]
by (auto simp: lits_of_def)
then show ‹defined_lit (get_trail_wl S) L› ‹-L ∈ lits_of_l (get_trail_wl S)›
‹L ∉ lits_of_l (get_trail_wl S)›
using S_S' T_T' n_d by (auto simp: Decided_Propagated_in_iff_in_lits_of_l twl_st
dest: no_dup_consistentD)
show L: ?alien
using alien uL_M twl_st_l(1-8)[OF T_T'] S_S'
init_clss_state_to_l[OF T_T']
unit_init_clauses_get_unit_init_clauses_l[OF T_T']
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: in_all_lits_of_mm_ain_atms_of_iff twl_st_wl twl_st twl_st_l)
then show alien': ?alien'
apply (rule set_rev_mp)
apply (rule all_lits_of_mm_mono)
by (cases S) auto
show ?alien''
using L
apply (rule set_rev_mp)
apply (rule all_lits_of_mm_mono)
by (cases S) auto
then have l_wl_inv: ‹(S, S') ∈ state_wl_l (Some (L, w)) ∧
unit_propagation_inner_loop_body_l_inv L (fst (watched_by S L ! w))
(remove_one_lit_from_wq (fst (watched_by S L ! w)) S') ∧
L ∈# all_lits_of_mm
(mset `# init_clss_lf (get_clauses_wl S) +
get_unit_clauses_wl S) ∧
correct_watching_except j w L S ∧
w < length (watched_by S L) ∧ get_conflict_wl S = None›
using that assms L unfolding unit_prop_body_wl_inv_def unit_propagation_inner_loop_body_l_inv_def
by (auto simp: twl_st)
then show ?inv
using that assms unfolding unit_prop_body_wl_inv_def unit_propagation_inner_loop_body_l_inv_def
by blast
show ?ge
by (rule ge_0)
show ‹distinct_mset_mset (mset `# ran_mf (get_clauses_wl S))›
using dist S_S' twl_st_l(1-8)[OF T_T'] T_T' unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_alt_def
by (auto simp: twl_st)
show ?confl
using confl .
have ‹watched_by S L ! w ∈ set (take j (watched_by S L)) ∪ set (drop w (watched_by S L))›
using L alien' C'_dom SLw w_le
by (cases S)
(auto simp: in_set_drop_conv_nth)
then show ‹correctly_marked_as_binary (get_clauses_wl S) (C', bL, bin)›
using corr_w alien' C'_dom SLw S_S'
by (cases S; cases ‹watched_by S L ! w›)
(clarsimp simp: correct_watching_except.simps Ball_def all_conj_distrib state_wl_l_def
simp del: Un_iff
dest!: multi_member_split[of L])
qed
have f': ‹(f, f') ∈ ⟨Id⟩option_rel›
if ‹(f, f') ∈ {(f, f'). f = f' ∧ f' = None}› for f f'
using that by auto
have f'': ‹(f, f') ∈ ⟨Id⟩option_rel›
if ‹(f, f') ∈ Id› for f f'
using that by auto
have i_def': ‹i = (if get_clauses_l T ∝ C' ! 0 = L then 0 else 1)›
using S_S' unfolding i_def by auto
have
bin_dom: ‹propagate_proper_bin_case L x1c (keep_watch L j w S) x1› and
bin_in_dom: ‹False = (x1 ∉# dom_m (get_clauses_wl (keep_watch L j w S)))› and
bin_pol_not_True:
‹False =
(polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) =
Some True)› and
bin_cannot_find_new:
‹RETURN None ≤ ⇓ {(f, f'). f = f' ∧ f' = None}
(find_unwatched_l (get_trail_wl (keep_watch L j w S)) (get_clauses_wl (keep_watch L j w S) ∝ x1))›
and
bin_pol_False:
‹(polarity (get_trail_wl (keep_watch L j w S)) x1c = Some False) =
(polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) =
Some False)› and
bin_prop:
‹(let i = if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0 else 1
in RETURN (j + 1, w + 1, propagate_lit_wl_bin x1c x1b i (keep_watch L j w S)))
≤ SPEC (λc. (c, j + 1, w + 1,
propagate_lit_wl_general
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)))
x1 (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)
(keep_watch L j w S))
∈ Id)›
if
pre: ‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
st: ‹x2 = (x1a, x2a)› ‹x2b = (x1c, x2c)› and
SLw': ‹watched_by S L ! w = (x1, x2)› and
SLw'': ‹watched_by S L ! w = (x1b, x2b)› and
inv: ‹unit_prop_body_wl_inv (keep_watch L j w S) j w L› and
‹unit_prop_body_wl_inv (keep_watch L j w S) j w L› and
‹polarity (get_trail_wl (keep_watch L j w S)) x1c ≠ Some True› and
bin: ‹x2c› ‹x2a›
for x1 x2 x1a x2a x1b x2b x1c x2c
proof -
obtain T where
S_T: ‹(S, T) ∈ state_wl_l (Some (L, w))› and
‹j ≤ w› and
w_le: ‹w < length (watched_by S L)›
‹unit_propagation_inner_loop_l_inv L (T, remaining_nondom_wl w L S)› and
‹correct_watching_except j w L S ∧ w ≤ length (watched_by S L)›
using pre unfolding unit_propagation_inner_loop_wl_loop_pre_def prod.simps
unit_propagation_inner_loop_wl_loop_inv_def
by fast+
then obtain T' where
S_T: ‹(S, T) ∈ state_wl_l (Some (L, w))› and
‹j ≤ w› and
‹correct_watching_except j w L S› and
‹w ≤ length (watched_by S L)› and
T_T': ‹(T, T') ∈ twl_st_l (Some L)› and
struct_invs: ‹twl_struct_invs T'› and
‹twl_stgy_invs T'› and
‹twl_list_invs T› and
uL: ‹- L ∈ lits_of_l (get_trail_l T)› and
confl: ‹clauses_to_update T' ≠ {#} ∨ 0 < remaining_nondom_wl w L S ⟶ get_conflict T' = None›
unfolding unit_propagation_inner_loop_l_inv_def prod.case
by metis
have confl: ‹get_conflict T' = None›
using S_T w_le T_T' confl_S
by (cases S; cases T') (auto simp: state_wl_l_def twl_st_l_def)
have
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T')› and
dup: ‹no_duplicate_queued T'› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T')› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of T')›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by blast+
have n_d: ‹no_dup (trail (state⇩W_of T'))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by auto
have 1: ‹C ∈# clauses_to_update T' ⟹
add_mset (fst C) (literals_to_update T') ⊆#
uminus `# lit_of `# mset (get_trail T')› for C
using dup unfolding no_duplicate_queued_alt_def
by blast
have uL_M: ‹-L ∈ lits_of_l (get_trail T')›
using uL T_T'
by (auto simp: lits_of_def)
have L: ‹L ∈# all_lits_of_mm
(mset `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)›
using alien uL_M twl_st_l(1-8)[OF T_T'] S_S' S_T
init_clss_state_to_l[OF T_T']
unit_init_clauses_get_unit_init_clauses_l[OF T_T']
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: in_all_lits_of_mm_ain_atms_of_iff twl_st_wl twl_st twl_st_l)
then have alien':
‹L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S)›
apply (rule set_rev_mp)
apply (rule all_lits_of_mm_mono)
by (cases S) auto
have ‹watched_by S L ! w ∈ set (drop w (watched_by S L))›
using corr_w alien' SLw S_S' inv pre
by (cases S; cases ‹watched_by S L ! w›)
(auto simp: correct_watching_except.simps Ball_def all_conj_distrib state_wl_l_def
unit_propagation_inner_loop_wl_loop_pre_def in_set_drop_conv_nth
intro!: bex_geI[of _ w]
simp del: Un_iff
dest!: multi_member_split[of L])
then have H: ‹x1 ∈# dom_m (get_clauses_wl S) ∧ bL ∈ set (get_clauses_wl S ∝ C') ∧
bL ≠ L ∧ correctly_marked_as_binary (get_clauses_wl S) (C', bL, bin) ∧
filter_mset (λi. i ∈# dom_m (get_clauses_wl S))
(fst `# mset (take j (watched_by S L) @ drop w (watched_by S L))) =
clause_to_update L (get_trail_wl S, get_clauses_wl S, get_conflict_wl S,
get_unit_init_clss_wl S, get_unit_learned_clss_wl S, {#}, {#})›
using corr_w alien' S_S' bin SLw' unfolding SLw st
by (cases S)
(auto simp: correct_watching_except.simps Ball_def all_conj_distrib state_wl_l_def
simp del:
dest!: multi_member_split[of L])
then show ‹False = (x1 ∉# dom_m (get_clauses_wl (keep_watch L j w S)))›
by auto
have dom: ‹C' ∈# dom_m (get_clauses_wl S)› and
filter: ‹filter_mset (λi. i ∈# dom_m (get_clauses_wl S))
(fst `# mset (take j (watched_by S L) @ drop w (watched_by S L))) =
clause_to_update L (get_trail_wl S, get_clauses_wl S, get_conflict_wl S,
get_unit_init_clss_wl S, get_unit_learned_clss_wl S, {#}, {#})›
using ‹watched_by S L ! w ∈ set (drop w (watched_by S L))› H SLw' unfolding SLw st
by auto
have x1c: ‹x1c = bL› and x1: ‹x1 = x1b›
using SLw' SLw'' unfolding st SLw
by auto
have ‹C' ∈# filter_mset (λi. i ∈# dom_m (get_clauses_wl S))
(fst `# mset (take j (watched_by S L) @ drop w (watched_by S L)))›
using ‹watched_by S L ! w ∈ set (drop w (watched_by S L))› dom
by auto
then have L_in: ‹L ∈ set (watched_l (get_clauses_wl S ∝ C'))›
using L_watched S_T SLw' bin unfolding filter
by (auto simp: clause_to_update_def)
moreover have le2: ‹length (get_clauses_wl S ∝ C') = 2›
using H SLw' bin unfolding SLw st
by (auto simp: correctly_marked_as_binary.simps)
ultimately have lit: ‹(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) = bL› and
[simp]: ‹unwatched_l (get_clauses_wl S ∝ x1) = []› and
lit': ‹(get_clauses_wl (keep_watch L j w S) ∝ x1b !
((if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0 else 1))) = L›
using H SLw' bin unfolding SLw st length_list_2 x1
by (auto simp del: simp del: C'_def)
show ‹False =
(polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) =
Some True)›
using that(8)
unfolding x1c lit
by auto
show ‹propagate_proper_bin_case L x1c (keep_watch L j w S) x1›
using H le2 SLw' L_in unfolding propagate_proper_bin_case_def x1 SLw length_list_2 x1 x1c
by auto
show ‹RETURN None ≤ ⇓ {(f, f'). f = f' ∧ f' = None}
(find_unwatched_l (get_trail_wl (keep_watch L j w S)) (get_clauses_wl (keep_watch L j w S) ∝ x1))›
by (auto simp: find_unwatched_l_def RETURN_RES_refine_iff)
show
‹(polarity (get_trail_wl (keep_watch L j w S)) x1c = Some False) =
(polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) =
Some False)›
unfolding x1c lit ..
show
bin_prop:
‹(let i = if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0 else 1
in RETURN (j + 1, w + 1, propagate_lit_wl_bin x1c x1b i (keep_watch L j w S)))
≤ SPEC (λc. (c, j + 1, w + 1,
propagate_lit_wl_general
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)))
x1 (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)
(keep_watch L j w S))
∈ Id)›
using le2 SLw''
unfolding x1c lit Let_def unfolding x1 propagate_lit_wl_bin_def propagate_lit_wl_general_def
by (cases S)
(auto intro!: RETURN_RES_refine simp: keep_watch_def)
qed
have find_unwatched_l:
‹find_unwatched_l (get_trail_wl (keep_watch L j w S)) (get_clauses_wl (keep_watch L j w S) ∝ x1b)
≤ ⇓ Id
(find_unwatched_l (get_trail_wl (keep_watch L j w S)) (get_clauses_wl (keep_watch L j w S) ∝ x1))›
if
‹x2 = (x1a, x2a)› and
‹watched_by S L ! w = (x1, x2)› and
‹x2b = (x1c, x2c)› and
‹watched_by S L ! w = (x1b, x2b)›
for x1 x2 x1a x2a x1b x2b x1c x2c
proof -
show ?thesis
using that
by auto
qed
have propagate_lit_wl: ‹((j + 1, w + 1,
propagate_lit_wl
(get_clauses_wl (keep_watch L j w S) ∝ x1b !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0
else 1)))
x1b
(if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0 else 1)
(keep_watch L j w S)),
j + 1, w + 1,
propagate_lit_wl_general
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)))
x1 (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)
(keep_watch L j w S))
∈ Id›
if
pre: ‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
st: ‹x2 = (x1a, x2a)›‹x2b = (x1c, x2c)› and
SLw: ‹watched_by S L ! w = (x1, x2)› and
SLw': ‹watched_by S L ! w = (x1b, x2b)› and
inv: ‹unit_prop_body_wl_inv (keep_watch L j w S) j w L› and
‹polarity (get_trail_wl (keep_watch L j w S)) x1c ≠ Some True› and
‹polarity (get_trail_wl (keep_watch L j w S)) x1a ≠ Some True› and
bin: ‹¬ x2c› ‹¬ x2a› and
dom: ‹¬ x1b ∉# dom_m (get_clauses_wl (keep_watch L j w S))›
‹¬ x1 ∉# dom_m (get_clauses_wl (keep_watch L j w S))› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1b !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0 else 1))) ≠
Some True› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) ≠
Some True› and
‹(f, fa) ∈ Id› and
‹unit_prop_body_wl_find_unwatched_inv fa x1 (keep_watch L j w S)› and
‹unit_prop_body_wl_find_unwatched_inv f x1b (keep_watch L j w S)› and
‹f = None› and
‹fa = None› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1b !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1b ! 0 = L then 0 else 1))) ≠
Some False› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) ≠
Some False›
for x1 x2 x1a x2a x1b x2b x1c x2c f fa
proof -
obtain T where
S_T: ‹(S, T) ∈ state_wl_l (Some (L, w))› and
‹j ≤ w› and
w_le: ‹w < length (watched_by S L)›
‹unit_propagation_inner_loop_l_inv L (T, remaining_nondom_wl w L S)› and
‹correct_watching_except j w L S ∧ w ≤ length (watched_by S L)›
using pre unfolding unit_propagation_inner_loop_wl_loop_pre_def prod.simps
unit_propagation_inner_loop_wl_loop_inv_def
by fast+
then obtain T' where
S_T: ‹(S, T) ∈ state_wl_l (Some (L, w))› and
‹j ≤ w› and
‹correct_watching_except j w L S› and
‹w ≤ length (watched_by S L)› and
T_T': ‹(T, T') ∈ twl_st_l (Some L)› and
struct_invs: ‹twl_struct_invs T'› and
‹twl_stgy_invs T'› and
‹twl_list_invs T› and
uL: ‹- L ∈ lits_of_l (get_trail_l T)› and
confl: ‹clauses_to_update T' ≠ {#} ∨ 0 < remaining_nondom_wl w L S ⟶ get_conflict T' = None›
unfolding unit_propagation_inner_loop_l_inv_def prod.case
by metis
have confl: ‹get_conflict T' = None›
using S_T w_le T_T' confl_S
by (cases S; cases T') (auto simp: state_wl_l_def twl_st_l_def)
have
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T')› and
dup: ‹no_duplicate_queued T'› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T')› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of T')› and
twl_st_inv: ‹twl_st_inv T'›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
twl_st_inv.simps
by blast+
have n_d: ‹no_dup (trail (state⇩W_of T'))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by auto
have 1: ‹C ∈# clauses_to_update T' ⟹
add_mset (fst C) (literals_to_update T') ⊆#
uminus `# lit_of `# mset (get_trail T')› for C
using dup unfolding no_duplicate_queued_alt_def
by blast
have uL_M: ‹-L ∈ lits_of_l (get_trail T')›
using uL T_T'
by (auto simp: lits_of_def)
have L: ‹L ∈# all_lits_of_mm
(mset `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)›
using alien uL_M twl_st_l(1-8)[OF T_T'] S_S' S_T
init_clss_state_to_l[OF T_T']
unit_init_clauses_get_unit_init_clauses_l[OF T_T']
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: in_all_lits_of_mm_ain_atms_of_iff twl_st_wl twl_st twl_st_l)
then have alien':
‹L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S)›
apply (rule set_rev_mp)
apply (rule all_lits_of_mm_mono)
by (cases S) auto
have ‹watched_by S L ! w ∈ set (drop w (watched_by S L))›
using corr_w alien' SLw S_S' inv pre
by (cases S; cases ‹watched_by S L ! w›)
(auto simp: correct_watching_except.simps Ball_def all_conj_distrib state_wl_l_def
unit_propagation_inner_loop_wl_loop_pre_def in_set_drop_conv_nth
intro!: bex_geI[of _ w]
simp del: Un_iff
dest!: multi_member_split[of L])
then have H: ‹correctly_marked_as_binary (get_clauses_wl S) (x1b, x1c, False)›
using corr_w alien' S_S' SLw'[unfolded SLw] SLw bin dom unfolding st
by (cases S)
(auto simp: correct_watching_except.simps Ball_def all_conj_distrib state_wl_l_def
simp del:
dest!: multi_member_split[of L])
have ‹∀C∈# (dom_m (get_clauses_wl S)). length (get_clauses_wl S ∝ C) ≥ 2›
using twl_st_inv S_T T_T'
by (cases T; cases T'; cases S)
(auto simp: state_wl_l_def twl_st_l_def twl_st_inv.simps
image_Un[symmetric])
then have le2: ‹length (get_clauses_wl S ∝ C') > 2›
using H SLw' bin dom unfolding SLw st
by (auto simp: correctly_marked_as_binary.simps SLw)
then show ?thesis
using that
by (cases S)
(auto simp: propagate_lit_wl_def
propagate_lit_wl_general_def keep_watch_def)
qed
show ?thesis
unfolding unit_propagation_inner_loop_body_wl_int_alt_def2
unit_propagation_inner_loop_body_wl_alt_def
apply refine_rcg
subgoal by auto
subgoal by auto
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c
by (rule bin_in_dom)
subgoal by (rule bin_pol_not_True)
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c
by fast
apply (rule bin_cannot_find_new; assumption)
apply (rule f'; assumption)
subgoal
by (rule bin_dom)
subgoal
by (rule bin_pol_False)
subgoal by auto
subgoal
by (rule bin_prop)
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c
by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rule find_unwatched_l; assumption)
subgoal by auto
apply (rule f''; assumption)
subgoal by auto
subgoal by auto
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c f fa
by (rule propagate_lit_wl)
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma
fixes S :: ‹'v twl_st_wl› and S' :: ‹'v twl_st_l› and L :: ‹'v literal› and w :: nat
defines [simp]: ‹C' ≡ fst (watched_by S L ! w)›
defines
[simp]: ‹T ≡ remove_one_lit_from_wq C' S'›
defines
[simp]: ‹C'' ≡ get_clauses_l S' ∝ C'›
assumes
S_S': ‹(S, S') ∈ state_wl_l (Some (L, w))› and
w_le: ‹w < length (watched_by S L)› and
j_w: ‹j ≤ w› and
corr_w: ‹correct_watching_except j w L S› and
inner_loop_inv: ‹unit_propagation_inner_loop_wl_loop_inv L (j, w, S)› and
n: ‹n = size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl S)) (mset (drop w (watched_by S L))))› and
confl_S: ‹get_conflict_wl S = None›
shows unit_propagation_inner_loop_body_wl_int_spec: ‹unit_propagation_inner_loop_body_wl_int L j w S ≤
⇓{((i, j, T'), (T, n)).
(T', T) ∈ state_wl_l (Some (L, j)) ∧
correct_watching_except i j L T' ∧
j ≤ length (watched_by T' L) ∧
length (watched_by S L) = length (watched_by T' L) ∧
i ≤ j ∧
(get_conflict_wl T' = None ⟶
n = size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl T')) (mset (drop j (watched_by T' L))))) ∧
(get_conflict_wl T' ≠ None ⟶ n = 0)}
(unit_propagation_inner_loop_body_l_with_skip L (S', n))› (is ‹?propa› is ‹_ ≤ ⇓ ?unit _›)and
unit_propagation_inner_loop_body_wl_update:
‹unit_propagation_inner_loop_body_l_inv L C' T ⟹
mset `# (ran_mf ((get_clauses_wl S) (C'↪ (swap (get_clauses_wl S ∝ C') 0
(1 - (if (get_clauses_wl S)∝C' ! 0 = L then 0 else 1)))))) =
mset `# (ran_mf (get_clauses_wl S))› (is ‹_ ⟹ ?eq›)
proof -
obtain bL where SLw: ‹watched_by S L ! w = (C', bL)›
using C'_def by (cases ‹watched_by S L ! w›) auto
have val: ‹(polarity a b, polarity a' b') ∈ Id›
if ‹a = a'› and ‹b = b'› for a a' :: ‹('a, 'b) ann_lits› and b b' :: ‹'a literal›
by (auto simp: that)
let ?M = ‹get_trail_wl S›
have f: ‹find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝ C')
≤ ⇓ {(found, found'). found = 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))
}
(find_unwatched_l (get_trail_l T) (get_clauses_l T ∝ C'))›
(is ‹_ ≤ ⇓ ?find _›)
using S_S' by (auto simp: find_unwatched_l_def intro!: RES_refine)
define i :: nat where
‹i ≡ (if get_clauses_wl S ∝ C' ! 0 = L then 0 else 1)›
have
l_wl_inv: ‹unit_prop_body_wl_inv S j w L› (is ?inv) and
clause_ge_0: ‹0 < length (get_clauses_l T ∝ C')› (is ?ge) and
L_def: ‹defined_lit (get_trail_wl S) L› ‹-L ∈ lits_of_l (get_trail_wl S)›
‹L ∉ lits_of_l (get_trail_wl S)› (is ?L_def) and
i_le: ‹i < length (get_clauses_wl S ∝ C')› (is ?i_le) and
i_le2: ‹1-i < length (get_clauses_wl S ∝ C')› (is ?i_le2) and
C'_dom: ‹C' ∈# dom_m (get_clauses_l T)› (is ?C'_dom) and
L_watched: ‹L ∈ set (watched_l (get_clauses_l T ∝ C'))› (is ?L_w) and
dist_clss: ‹distinct_mset_mset (mset `# ran_mf (get_clauses_wl S))› and
confl: ‹get_conflict_l T = None› (is ?confl) and
alien_L:
‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)›
(is ?alien) and
alien_L':
‹L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S)›
(is ?alien') and
alien_L'':
‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_clauses_wl S)›
(is ?alien'') and
correctly_marked_as_binary: ‹correctly_marked_as_binary (get_clauses_wl S) (C', bL)›
if
‹unit_propagation_inner_loop_body_l_inv L C' T›
proof -
have ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that unfolding unit_prop_body_wl_inv_def by fast+
then obtain T' where
T_T': ‹(set_clauses_to_update_l (clauses_to_update_l T + {#C'#}) T, T') ∈ twl_st_l (Some L)› and
struct_invs: ‹twl_struct_invs T'› and
‹twl_stgy_invs T'› and
C'_dom: ‹C' ∈# dom_m (get_clauses_l T)› and
‹0 < C'› and
ge_0: ‹0 < length (get_clauses_l T ∝ C')› and
‹no_dup (get_trail_l T)› and
i_le: ‹(if get_clauses_l T ∝ C' ! 0 = L then 0 else 1)
< length (get_clauses_l T ∝ C')› and
i_le2: ‹1 - (if get_clauses_l T ∝ C' ! 0 = L then 0 else 1)
< length (get_clauses_l T ∝ C')› and
L_watched: ‹L ∈ set (watched_l (get_clauses_l T ∝ C'))› and
confl: ‹get_conflict_l T = None›
unfolding unit_propagation_inner_loop_body_l_inv_def by blast
show ?i_le and ?C'_dom and ?L_w and ?i_le2
using S_S' i_le C'_dom L_watched i_le2 unfolding i_def by auto
have
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T')› and
dup: ‹no_duplicate_queued T'› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T')› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of T')›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by blast+
have n_d: ‹no_dup (trail (state⇩W_of T'))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by auto
have 1: ‹C ∈# clauses_to_update T' ⟹
add_mset (fst C) (literals_to_update T') ⊆#
uminus `# lit_of `# mset (get_trail T')› for C
using dup unfolding no_duplicate_queued_alt_def
by blast
have H: ‹(L, twl_clause_of C'') ∈# clauses_to_update T'›
using twl_st_l(5)[OF T_T']
by (auto simp: twl_st_l)
have uL_M: ‹-L ∈ lits_of_l (get_trail T')›
using mset_le_add_mset_decr_left2[OF 1[OF H]]
by (auto simp: lits_of_def)
then show ‹defined_lit (get_trail_wl S) L› ‹-L ∈ lits_of_l (get_trail_wl S)›
‹L ∉ lits_of_l (get_trail_wl S)›
using S_S' T_T' n_d by (auto simp: Decided_Propagated_in_iff_in_lits_of_l twl_st
dest: no_dup_consistentD)
show L: ?alien
using alien uL_M twl_st_l(1-8)[OF T_T'] S_S'
init_clss_state_to_l[OF T_T']
unit_init_clauses_get_unit_init_clauses_l[OF T_T']
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: in_all_lits_of_mm_ain_atms_of_iff twl_st_wl twl_st twl_st_l)
then show alien': ?alien'
apply (rule set_rev_mp)
apply (rule all_lits_of_mm_mono)
by (cases S) auto
show ?alien''
using L
apply (rule set_rev_mp)
apply (rule all_lits_of_mm_mono)
by (cases S) auto
then have l_wl_inv: ‹(S, S') ∈ state_wl_l (Some (L, w)) ∧
unit_propagation_inner_loop_body_l_inv L (fst (watched_by S L ! w))
(remove_one_lit_from_wq (fst (watched_by S L ! w)) S') ∧
L ∈# all_lits_of_mm
(mset `# init_clss_lf (get_clauses_wl S) +
get_unit_clauses_wl S) ∧
correct_watching_except j w L S ∧
w < length (watched_by S L) ∧ get_conflict_wl S = None›
using that assms L unfolding unit_prop_body_wl_inv_def unit_propagation_inner_loop_body_l_inv_def
by (auto simp: twl_st)
then show ?inv
using that assms unfolding unit_prop_body_wl_inv_def unit_propagation_inner_loop_body_l_inv_def
by blast
show ?ge
by (rule ge_0)
show ‹distinct_mset_mset (mset `# ran_mf (get_clauses_wl S))›
using dist S_S' twl_st_l(1-8)[OF T_T'] T_T' unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_alt_def
by (auto simp: twl_st)
show ?confl
using confl .
have ‹watched_by S L ! w ∈ set (take j (watched_by S L)) ∪ set (drop w (watched_by S L))›
using L alien' C'_dom SLw w_le
by (cases S)
(auto simp: in_set_drop_conv_nth)
then show ‹correctly_marked_as_binary (get_clauses_wl S) (C', bL)›
using corr_w alien' C'_dom SLw S_S'
by (cases S; cases ‹watched_by S L ! w›)
(clarsimp simp: correct_watching_except.simps Ball_def all_conj_distrib state_wl_l_def
simp del: Un_iff
dest!: multi_member_split[of L])
qed
have f': ‹(f, f') ∈ ⟨Id⟩option_rel›
if ‹f = f'› for f f'
using that by auto
have i_def': ‹i = (if get_clauses_l T ∝ C' ! 0 = L then 0 else 1)›
using S_S' unfolding i_def by auto
have [refine0]: ‹RETURN (C', bL) ≤ ⇓ {((C', bL), b). (b ⟷ C'∉# dom_m (get_clauses_wl S)) ∧
(b ⟶ 0 < n) ∧ (¬b ⟶ clauses_to_update_l S' ≠ {#})}
(SPEC (λb. (b ⟶ 0 < n) ∧ (¬b ⟶ clauses_to_update_l S' ≠ {#})))›
(is ‹_ ≤ ⇓ ?blit _›)
if ‹unit_propagation_inner_loop_l_inv L (S', n)› and
‹clauses_to_update_l S' ≠ {#} ∨ 0 < n › ‹unit_propagation_inner_loop_l_inv L (S', n)›
‹unit_propagation_inner_loop_wl_loop_inv L (j, w, S)›
proof -
have 1: ‹(C', bL) ∈# {#(i, _) ∈# mset (drop w (watched_by S L)). i ∉# dom_m (get_clauses_wl S)#}›
if ‹fst (watched_by S L ! w) ∉# dom_m (get_clauses_wl S) ›
using that w_le unfolding SLw apply -
apply (auto simp add: in_set_drop_conv_nth intro!: ex_geI[of _ w])
unfolding SLw
apply auto
done
have ‹fst (watched_by S L ! w) ∈# dom_m (get_clauses_wl S) ⟹
clauses_to_update_l S' = {#} ⟹ False›
using S_S' w_le that n 1 unfolding SLw unit_propagation_inner_loop_l_inv_def apply -
by (cases S; cases S')
(auto simp add: state_wl_l_def in_set_drop_conv_nth twl_st_l_def
Cons_nth_drop_Suc[symmetric]
intro: ex_geI[of _ w]
split: if_splits)
with multi_member_split[OF 1] show ?thesis
apply (intro RETURN_SPEC_refine)
apply (rule exI[of _ ‹C' ∉# dom_m (get_clauses_wl S)›])
using n
by auto
qed
have [simp]: ‹length (watched_by (keep_watch L j w S) L) = length (watched_by S L)› for S j w L
by (cases S) (auto simp: keep_watch_def)
have S_removal: ‹(S, set_clauses_to_update_l
(remove1_mset (fst (watched_by S L ! w)) (clauses_to_update_l S')) S')
∈ state_wl_l (Some (L, Suc w))›
using S_S' w_le by (cases S; cases S')
(auto simp: state_wl_l_def Cons_nth_drop_Suc[symmetric])
have K:
‹RETURN (get_clauses_wl (keep_watch L j w S) ∝ C')
≤ ⇓ {(_, (U, C)). C = C' ∧ (S, U) ∈ state_wl_l (Some (L, Suc w))} (select_from_clauses_to_update S')›
if ‹unit_propagation_inner_loop_wl_loop_inv L (j, w, S)› and
‹fst (watched_by S L ! w) ∈# clauses_to_update_l S'›
unfolding select_from_clauses_to_update_def
apply (rule RETURN_RES_refine)
apply (rule exI[of _ ‹(T, C')›])
by (auto simp: remove_one_lit_from_wq_def S_removal that)
have keep_watch_state_wl: ‹fst (watched_by S L ! w) ∉# dom_m (get_clauses_wl S) ⟹
(keep_watch L j w S, S') ∈ state_wl_l (Some (L, Suc w))›
using S_S' w_le j_w by (cases S; cases S')
(auto simp: state_wl_l_def keep_watch_def Cons_nth_drop_Suc[symmetric]
drop_map)
have [simp]: ‹drop (Suc w) (watched_by (keep_watch L j w S) L) = drop (Suc w) (watched_by S L)›
using j_w w_le by (cases S) (auto simp: keep_watch_def)
have [simp]: ‹get_clauses_wl (keep_watch L j w S) = get_clauses_wl S› for L j w S
by (cases S) (auto simp: keep_watch_def)
have keep_watch:
‹RETURN (keep_watch L j w S) ≤ ⇓ {(T, (T', C)). (T, T') ∈ state_wl_l (Some (L, Suc w)) ∧
C = C' ∧ T' = set_clauses_to_update_l (clauses_to_update_l S' - {#C#}) S'}
(select_from_clauses_to_update S')›
(is ‹_ ≤ ⇓ ?keep_watch _›)
if
cond: ‹clauses_to_update_l S' ≠ {#} ∨ 0 < n› and
inv: ‹unit_propagation_inner_loop_l_inv L (S', n)› and
‹unit_propagation_inner_loop_wl_loop_inv L (j, w, S)› and
‹¬ C' ∉# dom_m (get_clauses_wl S)› and
clss: ‹clauses_to_update_l S' ≠ {#}›
proof -
have ‹get_conflict_l S' = None›
using clss inv unfolding unit_propagation_inner_loop_l_inv_def twl_struct_invs_def prod.case
apply -
apply normalize_goal+
by auto
then show ?thesis
using S_S' that w_le j_w
unfolding select_from_clauses_to_update_def keep_watch_def
by (cases S)
(auto intro!: RETURN_RES_refine simp: state_wl_l_def drop_map
Cons_nth_drop_Suc[symmetric])
qed
have trail_keep_w: ‹get_trail_wl (keep_watch L j w S) = get_trail_wl S› for L j w S
by (cases S) (auto simp: keep_watch_def)
have unit_prop_body_wl_inv: ‹unit_prop_body_wl_inv (keep_watch L j w S) j w L›
if
‹clauses_to_update_l S' ≠ {#} ∨ 0 < n› and
loop_l: ‹unit_propagation_inner_loop_l_inv L (S', n)› and
loop_wl: ‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
‹((C', bL), b) ∈ ?blit› and
‹(C', bL) = (x1, x2)› and
‹¬ x1 ∉# dom_m (get_clauses_wl S)› and
‹¬ b› and
‹clauses_to_update_l S' ≠ {#}› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
inv: ‹unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2)›
for x1 b X2 x2
proof -
have corr_w':
‹correct_watching_except j w L S ⟹ correct_watching_except j w L (keep_watch L j w S)›
using j_w w_le
apply (cases S)
apply (simp only: correct_watching_except.simps keep_watch_def prod.case)
apply (cases ‹j = w›)
by simp_all
have [simp]:
‹(keep_watch L j w S, S') ∈ state_wl_l (Some (L, w)) ⟷ (S, S') ∈ state_wl_l (Some (L, w))›
using j_w
by (cases S ; cases ‹j=w›)
(auto simp: state_wl_l_def keep_watch_def drop_map)
have [simp]: ‹watched_by (keep_watch L j w S) L ! w = watched_by S L ! w›
using j_w
by (cases S ; cases ‹j=w›)
(auto simp: state_wl_l_def keep_watch_def drop_map)
have [simp]: ‹get_conflict_wl S = None›
using S_S' inv X2 unfolding unit_propagation_inner_loop_body_l_inv_def apply -
apply normalize_goal+
by auto
have ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that by (auto simp: remove_one_lit_from_wq_def)
then have ‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_clauses_wl S)›
using alien_L'' by fast
then show ?thesis
using j_w w_le
unfolding unit_prop_body_wl_inv_def
apply (intro impI conjI)
subgoal using w_le by auto
subgoal using j_w by auto
subgoal
apply (rule exI[of _ S'])
using inv X2 w_le S_S'
by (auto simp: corr_w' corr_w remove_one_lit_from_wq_def)
done
qed
have [refine0]: ‹SPEC ((=) x2) ≤ SPEC (λK. K ∈ set (get_clauses_l (fst X2) ∝ snd X2))›
if
‹clauses_to_update_l S' ≠ {#} ∨ 0 < n› and
‹unit_propagation_inner_loop_l_inv L (S', n)› and
‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
bL: ‹((C', bL), b) ∈ ?blit› and
x: ‹(C', bL) = (x1, x2')› and
x2': ‹x2' =(x2, x3)› and
x1: ‹¬ x1 ∉# dom_m (get_clauses_wl S)› and
‹¬ b› and
‹clauses_to_update_l S' ≠ {#}› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
‹unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2)› and
‹unit_prop_body_wl_inv (keep_watch L j w S) j w L›
for x1 x2 X2 b x3 x2'
proof -
have [simp]: ‹x2' = bL› ‹x1 = C'›
using x by simp_all
have ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that by (auto simp: remove_one_lit_from_wq_def)
from alien_L'[OF this]
have ‹L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S)›
.
from correct_watching_exceptD[OF corr_w this w_le]
have ‹fst bL ∈ set (get_clauses_wl S ∝ fst (watched_by S L ! w))›
using x1 SLw
by (cases S; cases ‹watched_by S L ! w›) (auto simp add: )
then show ?thesis
using bL X2 S_S' x1 x2'
by auto
qed
have find_unwatched_l: ‹find_unwatched_l (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1)
≤ ⇓ {(k, k'). k = k' ∧ get_clauses_wl S ∝ x1 ≠ [] ∧
(k ≠ None ⟶ (the k ≥ 2 ∧ the k < length (get_clauses_wl (keep_watch L j w S) ∝ x1) ∧
(undefined_lit (get_trail_wl S) (get_clauses_wl (keep_watch L j w S) ∝ x1!(the k))
∨ get_clauses_wl (keep_watch L j w S) ∝ x1!(the k) ∈ lits_of_l (get_trail_wl S)))) ∧
((k = None) ⟷
(∀La∈#mset (unwatched_l (get_clauses_wl (keep_watch L j w S) ∝ x1)).
- La ∈ lits_of_l (get_trail_wl (keep_watch L j w S))))}
(find_unwatched_l (get_trail_l (fst X2))
(get_clauses_l (fst X2) ∝ snd X2))›
(is ‹_ ≤ ⇓ ?find_unw _›)
if
C': ‹(C', bL) = (x1, x2)› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
x: ‹x ∈ {K. K ∈ set (get_clauses_l (fst X2) ∝ snd X2)}› and
‹(keep_watch L j w S, X2) ∈ ?keep_watch›
for x1 x2 X2 x
proof -
show ?thesis
using S_S' X2 SLw that unfolding C'
by (auto simp: twl_st_wl find_unwatched_l_def intro!: SPEC_refine)
qed
have blit_final:
‹(if polarity (get_trail_wl (keep_watch L j w S)) x2 = Some True
then RETURN (j + 1, w + 1, keep_watch L j w S)
else RETURN (j, w + 1, keep_watch L j w S))
≤ ⇓ ?unit
(RETURN (S', n - 1))›
if
‹((C', bL), b) ∈ ?blit› and
‹(C', bL) = (x1, x2')› and
x2': ‹x2' =(x2, x3)› and
‹x1 ∉# dom_m (get_clauses_wl S)› and
‹unit_prop_body_wl_inv (keep_watch L j w S) j w L›
for b x1 x2 x2' x3
using S_S' w_le j_w n that confl_S
by (auto simp: keep_watch_state_wl assert_bind_spec_conv Let_def twl_st_wl
Cons_nth_drop_Suc[symmetric] correct_watching_except_correct_watching_except_Suc_Suc_keep_watch
corr_w correct_watching_except_correct_watching_except_Suc_notin
split: if_splits)
have conflict_final: ‹((j + 1, w + 1,
set_conflict_wl (get_clauses_wl (keep_watch L j w S) ∝ x1)
(keep_watch L j w S)),
set_conflict_l (get_clauses_l (fst X2) ∝ snd X2) (fst X2),
if get_conflict_l
(set_conflict_l (get_clauses_l (fst X2) ∝ snd X2) (fst X2)) =
None
then n else 0)
∈ ?unit›
if
C'_bl: ‹(C', bL) = (x1, x2')› and
x2': ‹x2' =(x2, x3)› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch›
for b x1 x2 X2 K x f x' x2' x3
proof -
have [simp]: ‹get_conflict_l (set_conflict_l C S) ≠ None›
‹get_conflict_wl (set_conflict_wl C S') = Some (mset C)›
‹watched_by (set_conflict_wl C S') L = watched_by S' L› for C S S' L
apply (cases S; auto simp: set_conflict_l_def; fail)
apply (cases S'; auto simp: set_conflict_wl_def; fail)
apply (cases S'; auto simp: set_conflict_wl_def; fail)
done
have [simp]: ‹correct_watching_except j w L (set_conflict_wl C S) ⟷
correct_watching_except j w L S› for j w L C S
apply (cases S)
by (simp only: correct_watching_except.simps
set_conflict_wl_def prod.case clause_to_update_def get_clauses_l.simps)
have ‹(set_conflict_wl (get_clauses_wl S ∝ x1) (keep_watch L j w S),
set_conflict_l (get_clauses_l (fst X2) ∝ snd X2) (fst X2))
∈ state_wl_l (Some (L, Suc w))›
using S_S' X2 SLw C'_bl by (cases S; cases S') (auto simp: state_wl_l_def
set_conflict_wl_def set_conflict_l_def keep_watch_def
clauses_to_update_wl.simps)
then show ?thesis
using S_S' w_le j_w n
by (auto simp: keep_watch_state_wl
correct_watching_except_correct_watching_except_Suc_Suc_keep_watch
corr_w correct_watching_except_correct_watching_except_Suc_notin
split: if_splits)
qed
have propa_final: ‹((j + 1, w + 1,
propagate_lit_wl_general
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)))
x1 (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)
(keep_watch L j w S)),
propagate_lit_l
(get_clauses_l (fst X2) ∝ snd X2 !
(1 - (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)))
(snd X2) (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)
(fst X2),
if get_conflict_l
(propagate_lit_l
(get_clauses_l (fst X2) ∝ snd X2 !
(1 - (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)))
(snd X2) (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)
(fst X2)) =
None
then n else 0)
∈ ?unit›
if
C': ‹(C', bL) = (x1, x2)› and
x1_dom: ‹¬ x1 ∉# dom_m (get_clauses_wl S)› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
l_inv: ‹unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2)›
for b x1 x2 X2 K x f x'
proof -
have [simp]: ‹get_conflict_l (propagate_lit_l C L w S) = get_conflict_l S›
‹watched_by (propagate_lit_wl_general C L w S') L' = watched_by S' L'›
‹get_conflict_wl (propagate_lit_wl_general C L w S') = get_conflict_wl S'›
‹L ∈# dom_m (get_clauses_wl S') ⟹
dom_m (get_clauses_wl (propagate_lit_wl_general C L w S')) = dom_m (get_clauses_wl S')›
‹dom_m (get_clauses_wl (keep_watch L' i j S')) = dom_m (get_clauses_wl S')›
for C L w S S' L' i j
apply (cases S; auto simp: propagate_lit_l_def; fail)
apply (cases S'; auto simp: propagate_lit_wl_general_def; fail)
apply (cases S'; auto simp: propagate_lit_wl_general_def; fail)
apply (cases S'; auto simp: propagate_lit_wl_general_def; fail)
apply (cases S'; auto simp: propagate_lit_wl_general_def; fail)
done
define i :: nat where ‹i ≡ if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1›
have i_alt_def: ‹i = (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)›
using X2 S_S' SLw unfolding i_def C' by auto
have x1_dom[simp]: ‹x1 ∈# dom_m (get_clauses_wl S)›
using x1_dom by fast
have [simp]: ‹get_clauses_wl S ∝ x1 ! 0 ≠ L ⟹ get_clauses_wl S ∝ x1 ! Suc 0 = L› and
‹Suc 0 < length (get_clauses_wl S ∝ x1)›
using l_inv X2 S_S' SLw unfolding unit_propagation_inner_loop_body_l_inv_def C'
apply - apply normalize_goal+
by (cases ‹get_clauses_wl S ∝ x1›; cases ‹tl (get_clauses_wl S ∝ x1)›)
auto
have n: ‹n = size {#(i, _) ∈# mset (drop (Suc w) (watched_by S L)).
i ∉# dom_m (get_clauses_wl S)#}›
using n
apply (subst (asm) Cons_nth_drop_Suc[symmetric])
subgoal using w_le by simp
subgoal using n SLw X2 S_S' unfolding i_def C' by auto
done
have [simp]: ‹get_conflict_l (fst X2) = get_conflict_wl S›
using X2 S_S' by auto
have
‹(propagate_lit_wl_general (get_clauses_wl S ∝ x1 ! (Suc 0 - i)) x1 i (keep_watch L j w S),
propagate_lit_l (get_clauses_l (fst X2) ∝ snd X2 ! (Suc 0 - i)) (snd X2) i (fst X2))
∈ state_wl_l (Some (L, Suc w))›
using X2 S_S' SLw j_w w_le multi_member_split[OF x1_dom] unfolding C'
by (cases S; cases S')
(auto simp: state_wl_l_def propagate_lit_wl_general_def keep_watch_def
propagate_lit_l_def drop_map)
moreover have ‹correct_watching_except (Suc j) (Suc w) L (keep_watch L j w S) ⟹
correct_watching_except (Suc j) (Suc w) L
(propagate_lit_wl_general (get_clauses_wl S ∝ x1 ! (Suc 0 - i)) x1 i (keep_watch L j w S))›
apply (rule correct_watching_except_correct_watching_except_propagate_lit_wl)
using w_le j_w ‹Suc 0 < length (get_clauses_wl S ∝ x1)› by auto
moreover have ‹correct_watching_except (Suc j) (Suc w) L (keep_watch L j w S)›
by (simp add: corr_w correct_watching_except_correct_watching_except_Suc_Suc_keep_watch j_w w_le)
ultimately show ?thesis
using w_le unfolding i_def[symmetric] i_alt_def[symmetric]
by (auto simp: twl_st_wl j_w n)
qed
have update_blit_wl_final:
‹update_blit_wl L x1 x3 j w (get_clauses_wl (keep_watch L j w S) ∝ x1 ! xa) (keep_watch L j w S)
≤ ⇓ ?unit
(RETURN (fst X2, if get_conflict_l (fst X2) = None then n else 0))›
if
cond: ‹clauses_to_update_l S' ≠ {#} ∨ 0 < n› and
loop_inv: ‹unit_propagation_inner_loop_l_inv L (S', n)› and
‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
C'bl: ‹((C', bL), b) ∈ ?blit› and
C'_bl: ‹(C', bL) = (x1, x2')› and
x2': ‹x2' =(x2, x3)› and
dom: ‹¬ x1 ∉# dom_m (get_clauses_wl S)› and
‹¬ b› and
‹clauses_to_update_l S' ≠ {#}› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
pre: ‹unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2)› and
‹unit_prop_body_wl_inv (keep_watch L j w S) j w L› and
‹(K, x) ∈ Id› and
‹K ∈ Collect ((=) x2)› and
‹x ∈ {K. K ∈ set (get_clauses_l (fst X2) ∝ snd X2)}› and
fx': ‹(f, x') ∈ ?find_unw x1› and
‹unit_prop_body_wl_find_unwatched_inv f x1 (keep_watch L j w S)› and
f: ‹f = Some xa› and
x': ‹x' = Some x'a› and
xa: ‹(xa, x'a) ∈ nat_rel› and
‹x'a < length (get_clauses_l (fst X2) ∝ snd X2)› and
‹polarity (get_trail_wl (keep_watch L j w S)) (get_clauses_wl (keep_watch L j w S) ∝ x1 ! xa) =
Some True› and
pol: ‹polarity (get_trail_l (fst X2)) (get_clauses_l (fst X2) ∝ snd X2 ! x'a) = Some True›
for b x1 x2 X2 K x f x' xa x'a x2' x3
proof -
have confl: ‹get_conflict_wl S = None›
using S_S' loop_inv cond unfolding unit_propagation_inner_loop_l_inv_def prod.case apply -
by normalize_goal+ auto
have unit_T: ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that by (auto simp: remove_one_lit_from_wq_def)
have ‹correct_watching_except (Suc j) (Suc w) L (keep_watch L j w S)›
by (simp add: corr_w correct_watching_except_correct_watching_except_Suc_Suc_keep_watch
j_w w_le)
moreover have ‹correct_watching_except (Suc j) (Suc w) L
(a, b, None, d, e, f, ga(L := (ga L)[j := (x1, b ∝ x1 ! xa, x3)]))›
if
corr: ‹correct_watching_except (Suc j) (Suc w) L
(a, b, None, d, e, f, ga(L := (ga L)[j := (x1, x2, x3)]))› and
‹ga L ! w = (x1, x2, x3)› and
S[simp]: ‹S = (a, b, None, d, e, f, ga)› and
‹X2 = (set_clauses_to_update_l (remove1_mset x1 (clauses_to_update_l S')) S', x1)› and
‹(a, b, None, d, e,
{#i ∈# mset (drop (Suc w) (map fst ((ga L)[j := (x1, x2, x3)]))). i ∈# dom_m b#}, f) =
set_clauses_to_update_l (remove1_mset x1 (clauses_to_update_l S')) S'›
for a :: ‹('v literal, 'v literal,nat) annotated_lit list› and
b :: ‹(nat, 'v literal list × bool) fmap› and
d :: ‹'v literal multiset multiset› and
e :: ‹'v literal multiset multiset› and
f :: ‹'v literal multiset› and
ga :: ‹'v literal ⇒ (nat × 'v literal × bool) list›
proof -
have ‹b ∝ x1 ! xa ∈# all_lits_of_mm (mset `# ran_mf b + (d + e))›
using dom fx' by (auto simp: ran_m_def all_lits_of_mm_add_mset x' f twl_st_wl
dest!: multi_member_split
intro!: in_clause_in_all_lits_of_m)
moreover have ‹b ∝ x1 ! xa ∈ set (b ∝ x1)›
using dom fx' by (auto simp: ran_m_def all_lits_of_mm_add_mset x' f twl_st_wl
dest!: multi_member_split
intro!: in_clause_in_all_lits_of_m)
moreover have ‹b ∝ x1 ! xa ≠ L›
using pol X2 L_def[OF unit_T] S_S' SLw fx' x' f' xa unfolding C'_bl
by (auto simp: polarity_def split: if_splits)
moreover have ‹correctly_marked_as_binary b (x1, b ∝ x1 ! xa, x3)›
using correctly_marked_as_binary unit_T C'_bl x2' C'bl dom SLw by (auto simp: correctly_marked_as_binary.simps)
ultimately show ?thesis
by (rule correct_watching_except_update_blit[OF corr ])
qed
ultimately have ‹update_blit_wl L x1 x3 j w (get_clauses_wl (keep_watch L j w S) ∝ x1 ! xa) (keep_watch L j w S)
≤ SPEC(λ(i, j, T'). correct_watching_except i j L T')›
using X2 confl SLw unfolding C'_bl
apply (cases S)
by (auto simp: keep_watch_def state_wl_l_def x2'
update_blit_wl_def)
moreover have ‹get_conflict_wl S = None›
using S_S' loop_inv cond unfolding unit_propagation_inner_loop_l_inv_def prod.case apply -
by normalize_goal+ auto
moreover have ‹n = size {#(i, _) ∈# mset (drop (Suc w) (watched_by S L)). i ∉# dom_m (get_clauses_wl S)#}›
using n dom X2 w_le S_S' SLw unfolding C'_bl
by (auto simp: Cons_nth_drop_Suc[symmetric])
ultimately show ?thesis
using j_w w_le S_S' X2
by (cases S)
(auto simp: update_blit_wl_def keep_watch_def state_wl_l_def drop_map)
qed
have update_clss_final: ‹update_clause_wl L x1 x3 j w
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1) xa
(keep_watch L j w S)
≤ ⇓ ?unit
(update_clause_l (snd X2)
(if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1) x'a (fst X2) ⤜
(λT. RETURN (T, if get_conflict_l T = None then n else 0)))›
if
cond: ‹clauses_to_update_l S' ≠ {#} ∨ 0 < n› and
loop_inv: ‹unit_propagation_inner_loop_l_inv L (S', n)› and
‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
‹((C', bL), b) ∈ ?blit› and
C'_bl: ‹(C', bL) = (x1, x2')› and
x2': ‹x2' =(x2, x3)› and
dom: ‹¬ x1 ∉# dom_m (get_clauses_wl S)› and
‹¬ b› and
‹clauses_to_update_l S' ≠ {#}› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
wl_inv: ‹unit_prop_body_wl_inv (keep_watch L j w S) j w L› and
‹(K, x) ∈ Id› and
‹K ∈ Collect ((=) x2)› and
‹x ∈ {K. K ∈ set (get_clauses_l (fst X2) ∝ snd X2)}› and
‹polarity (get_trail_wl (keep_watch L j w S)) K ≠ Some True› and
‹polarity (get_trail_l (fst X2)) x ≠ Some True› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 - (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) ≠
Some True› and
‹polarity (get_trail_l (fst X2))
(get_clauses_l (fst X2) ∝ snd X2 !
(1 - (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1))) ≠
Some True› and
fx': ‹(f, x') ∈ ?find_unw x1› and
‹unit_prop_body_wl_find_unwatched_inv f x1 (keep_watch L j w S)› and
f: ‹f = Some xa› and
x': ‹x' = Some x'a› and
xa: ‹(xa, x'a) ∈ nat_rel› and
‹x'a < length (get_clauses_l (fst X2) ∝ snd X2)› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 ! xa) ≠
Some True› and
pol: ‹polarity (get_trail_l (fst X2)) (get_clauses_l (fst X2) ∝ snd X2 ! x'a) ≠ Some True› and
‹unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2)›
for b x1 x2 X2 K x f x' xa x'a x2' x3
proof -
have confl: ‹get_conflict_wl S = None›
using S_S' loop_inv cond unfolding unit_propagation_inner_loop_l_inv_def prod.case apply -
by normalize_goal+ auto
then obtain M N NE UE Q W where
S: ‹S = (M, N, None, NE, UE, Q, W)›
by (cases S) (auto simp: twl_st_l)
have dom': ‹x1 ∈# dom_m (get_clauses_wl (keep_watch L j w S)) ⟷ True›
using dom by auto
moreover have watch_by_S_w: ‹watched_by (keep_watch L j w S) L ! w = (x1, x2, x3)›
using j_w w_le SLw x2' unfolding i_def C'_bl
by (cases S) (auto simp: keep_watch_def)
ultimately have C'_dom: ‹fst (watched_by (keep_watch L j w S) L ! w) ∈# dom_m (get_clauses_wl (keep_watch L j w S)) ⟷ True›
using SLw unfolding C'_bl by (auto simp: twl_st_wl)
obtain x where
S_x: ‹(keep_watch L j w S, x) ∈ state_wl_l (Some (L, w))› and
unit_loop_inv:
‹unit_propagation_inner_loop_body_l_inv L (fst (watched_by (keep_watch L j w S) L ! w))
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w)) x)› and
L: ‹L ∈# all_lits_of_mm
(mset `# init_clss_lf (get_clauses_wl (keep_watch L j w S)) +
get_unit_clauses_wl (keep_watch L j w S))› and
‹correct_watching_except j w L (keep_watch L j w S)› and
‹w < length (watched_by (keep_watch L j w S) L)› and
‹get_conflict_wl (keep_watch L j w S) = None›
using wl_inv unfolding unit_prop_body_wl_inv_alt_def C'_dom simp_thms apply -
by blast
obtain x' where
x_x': ‹(set_clauses_to_update_l
(clauses_to_update_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) +
{#fst (watched_by (keep_watch L j w S) L ! w)#})
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w)) x),
x') ∈ twl_st_l (Some L)› and
‹twl_struct_invs x'› and
‹twl_stgy_invs x'› and
‹fst (watched_by (keep_watch L j w S) L ! w)
∈# dom_m
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x))› and
‹0 < fst (watched_by (keep_watch L j w S) L ! w)› and
‹0 < length
(get_clauses_l
(remove_one_lit_from_wq
(fst (watched_by (keep_watch L j w S) L ! w)) x) ∝
fst (watched_by (keep_watch L j w S) L ! w))› and
‹no_dup
(get_trail_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x))› and
ge0: ‹(if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w) !
0 =
L
then 0 else 1)
< length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w))› and
ge1i: ‹1 -
(if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w) !
0 =
L
then 0 else 1)
< length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w))› and
L_watched: ‹L ∈ set (watched_l
(get_clauses_l
(remove_one_lit_from_wq
(fst (watched_by (keep_watch L j w S) L ! w)) x) ∝
fst (watched_by (keep_watch L j w S) L ! w)))› and
‹get_conflict_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w)) x) =
None›
using unit_loop_inv
unfolding unit_propagation_inner_loop_body_l_inv_def
by blast
have [simp]: ‹x'a = xa›
using xa by auto
have unit_T: ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that
by (auto simp: remove_one_lit_from_wq_def)
have corr: ‹correct_watching_except (Suc j) (Suc w) L (keep_watch L j w S)›
by (simp add: corr_w correct_watching_except_correct_watching_except_Suc_Suc_keep_watch
j_w w_le)
have i:
‹i = (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)›
‹i = (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)›
using SLw X2 S_S' unfolding i_def C'_bl apply (cases X2; auto simp add: twl_st_wl; fail)
using SLw X2 S_S' unfolding i_def C'_bl apply (cases X2; auto simp add: twl_st_wl; fail)
done
have i': ‹i = (if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w) !
0 =
L
then 0 else 1)›
using j_w w_le S_x unfolding i_def
by (cases S) (auto simp: keep_watch_def)
have ‹twl_st_inv x'›
using ‹twl_struct_invs x'› unfolding twl_struct_invs_def by fast
then have ‹∃x. twl_st_inv
(x, {#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#},
None, NE, UE,
add_mset
(L, TWL_Clause (mset (watched_l (N ∝ fst ((W L)[j := W L ! w] ! w))))
(mset (unwatched_l (N ∝ fst ((W L)[j := W L ! w] ! w)))))
{#(L, TWL_Clause (mset (watched_l (N ∝ x)))
(mset (unwatched_l (N ∝ x))))
. x ∈# remove1_mset (fst ((W L)[j := W L ! w] ! w))
{#i ∈# mset (drop w (map fst ((W L)[j := W L ! w]))).
i ∈# dom_m N#}#},
Q)›
using x_x' S_x
apply (cases x)
apply (auto simp: S twl_st_l_def state_wl_l_def keep_watch_def
simp del: struct_wf_twl_cls.simps)
done
then have ‹Multiset.Ball
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# ran_m N#})
struct_wf_twl_cls›
unfolding twl_st_inv.simps image_mset_union[symmetric] all_clss_l_ran_m
by blast
then have distinct_N_x1: ‹distinct (N ∝ x1)›
using dom
by (auto simp: S ran_m_def mset_take_mset_drop_mset' dest!: multi_member_split)
then have L_i: ‹L = N ∝ x1 ! i›
using watch_by_S_w L_watched ge0 ge1i SLw S_x unfolding i_def C'_bl
by (auto simp: take_2_if twl_st_wl S split: if_splits)
have i_le: ‹i < length (N ∝ x1)› ‹1-i < length (N ∝ x1)›
using watch_by_S_w ge0 ge1i S_x unfolding i'[symmetric]
by (auto simp: S)
have X2: ‹X2 = (set_clauses_to_update_l (remove1_mset x1 (clauses_to_update_l S')) S', x1)›
using SLw X2 S_S' unfolding i_def C'_bl by (cases X2; auto simp add: twl_st_wl)
have ‹n = size {#(i, _) ∈# mset (drop (Suc w) (watched_by S L)).
i ≠ x1 ∧ i ∉# remove1_mset x1 (dom_m (get_clauses_wl S))#}›
using dom n w_le SLw unfolding C'_bl
by (auto simp: Cons_nth_drop_Suc[symmetric] dest!: multi_member_split)
moreover have ‹L ≠ get_clauses_wl S ∝ x1 ! xa›
using pol X2 L_def[OF unit_T] S_S' SLw xa fx' unfolding C'_bl f x'
by (auto simp: polarity_def twl_st_wl split: if_splits)
moreover have ‹remove1_mset x1 {#i ∈# mset (drop w (map fst (watched_by S L))). i ∈# dom_m (get_clauses_wl S)#} =
{#i ∈# mset (drop (Suc w) (map fst ((watched_by S L)[j := (x1, x2, x3)]))). i = x1 ∨ i ∈# remove1_mset x1 (dom_m (get_clauses_wl S))#}›
using dom n w_le SLw j_w unfolding C'_bl
by (auto simp: Cons_nth_drop_Suc[symmetric] drop_map dest!: multi_member_split)
moreover have ‹correct_watching_except j (Suc w) L
(M, N(x1 ↪ swap (N ∝ x1) i xa), None, NE, UE, Q, W
(L := (W L)[j := (x1, x2, x3)],
N ∝ x1 ! xa := W (N ∝ x1 ! xa) @ [(x1, L, x3)]))›
apply (rule correct_watching_except_correct_watching_except_update_clause)
subgoal
using corr j_w w_le unfolding S
by (auto simp: keep_watch_def)
subgoal using j_w .
subgoal using w_le by (auto simp: S)
subgoal using alien_L'[OF unit_T] by (auto simp: S twl_st_wl)
subgoal using i_le unfolding L_i by auto
subgoal using L by (subst all_clss_l_ran_m[symmetric], subst image_mset_union)
(auto simp: S all_lits_of_mm_union)
subgoal using distinct_N_x1 i_le fx' xa i_le unfolding L_i x'
by (auto simp: S nth_eq_iff_index_eq i_def)
subgoal using dom by (simp add: S)
subgoal using i_le by simp
subgoal using xa fx' unfolding f xa by (auto simp: S)
subgoal using SLw unfolding C'_bl by (auto simp: S x2')
subgoal unfolding L_i ..
subgoal using distinct_N_x1 i_le unfolding L_i
by (auto simp: nth_eq_iff_index_eq i_def)
subgoal using distinct_N_x1 i_le fx' xa i_le unfolding L_i x'
by (auto simp: S nth_eq_iff_index_eq i_def)
subgoal using distinct_N_x1 i_le fx' xa i_le unfolding L_i x'
by (auto simp: S nth_eq_iff_index_eq i_def)
subgoal using distinct_N_x1 i_le fx' xa i_le unfolding L_i x'
by (auto simp: S nth_eq_iff_index_eq i_def)
subgoal using i_def by (auto simp: S split: if_splits)
subgoal using xa fx' unfolding f xa by (auto simp: S)
subgoal using distinct_N_x1 i_le fx' xa i_le unfolding L_i x'
by (auto simp: S nth_eq_iff_index_eq i_def)
done
ultimately show ?thesis
using S_S' w_le j_w SLw confl
unfolding update_clause_wl_def update_clause_l_def i[symmetric] C'_bl
by (cases S')
(auto simp: Let_def X2 keep_watch_def state_wl_l_def S x2')
qed
have blit_final_in_dom: ‹update_blit_wl L x1 x3 j w
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)))
(keep_watch L j w S)
≤ ⇓ ?unit
(RETURN (fst X2, if get_conflict_l (fst X2) = None then n else 0))›
if
cond: ‹clauses_to_update_l S' ≠ {#} ∨ 0 < n› and
loop_inv: ‹unit_propagation_inner_loop_l_inv L (S', n)› and
‹unit_propagation_inner_loop_wl_loop_pre L (j, w, S)› and
‹((C', bL), b) ∈ ?blit› and
C'_bl: ‹(C', bL) = (x1, x2')› and
x2': ‹x2' =(x2, x3)› and
dom: ‹¬ x1 ∉# dom_m (get_clauses_wl S)› and
‹¬ b› and
‹clauses_to_update_l S' ≠ {#}› and
X2: ‹(keep_watch L j w S, X2) ∈ ?keep_watch› and
l_inv: ‹unit_propagation_inner_loop_body_l_inv L (snd X2) (fst X2)› and
wl_inv: ‹unit_prop_body_wl_inv (keep_watch L j w S) j w L› and
‹(K, x) ∈ Id› and
‹K ∈ Collect ((=) x2)› and
‹x ∈ {K. K ∈ set (get_clauses_l (fst X2) ∝ snd X2)}› and
‹polarity (get_trail_wl (keep_watch L j w S)) K ≠ Some True› and
‹polarity (get_trail_l (fst X2)) x ≠ Some True› and
‹polarity (get_trail_wl (keep_watch L j w S))
(get_clauses_wl (keep_watch L j w S) ∝ x1 !
(1 -
(if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1))) =
Some True› and
‹polarity (get_trail_l (fst X2))
(get_clauses_l (fst X2) ∝ snd X2 !
(1 - (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1))) =
Some True›
for b x1 x2 X2 K x x2' x3
proof -
have confl: ‹get_conflict_wl S = None›
using S_S' loop_inv cond unfolding unit_propagation_inner_loop_l_inv_def prod.case apply -
by normalize_goal+ auto
then obtain M N NE UE Q W where
S: ‹S = (M, N, None, NE, UE, Q, W)›
by (cases S) (auto simp: twl_st_l)
have dom': ‹x1 ∈# dom_m (get_clauses_wl (keep_watch L j w S)) ⟷ True›
using dom by auto
then have SLW_dom': ‹fst (watched_by (keep_watch L j w S) L ! w)
∈# dom_m (get_clauses_wl (keep_watch L j w S))›
using SLw w_le unfolding C'_bl by auto
have bin: ‹correctly_marked_as_binary N (x1, N ∝ x1 ! (Suc 0 - i), x3)›
using X2 correctly_marked_as_binary l_inv x2' C'_bl
by (cases bL)
(auto simp: S remove_one_lit_from_wq_def correctly_marked_as_binary.simps)
obtain x where
S_x: ‹(keep_watch L j w S, x) ∈ state_wl_l (Some (L, w))› and
unit_loop_inv:
‹unit_propagation_inner_loop_body_l_inv L (fst (watched_by (keep_watch L j w S) L ! w))
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w)) x)› and
L: ‹L ∈# all_lits_of_mm
(mset `# init_clss_lf (get_clauses_wl (keep_watch L j w S)) +
get_unit_clauses_wl (keep_watch L j w S))› and
‹correct_watching_except j w L (keep_watch L j w S)› and
‹w < length (watched_by (keep_watch L j w S) L)› and
‹get_conflict_wl (keep_watch L j w S) = None›
using wl_inv SLW_dom' unfolding unit_prop_body_wl_inv_alt_def
by blast
obtain x' where
x_x': ‹(set_clauses_to_update_l
(clauses_to_update_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) +
{#fst (watched_by (keep_watch L j w S) L ! w)#})
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w)) x),
x') ∈ twl_st_l (Some L)› and
‹twl_struct_invs x'› and
‹twl_stgy_invs x'› and
‹fst (watched_by (keep_watch L j w S) L ! w)
∈# dom_m
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x))› and
‹0 < fst (watched_by (keep_watch L j w S) L ! w)› and
‹0 < length
(get_clauses_l
(remove_one_lit_from_wq
(fst (watched_by (keep_watch L j w S) L ! w)) x) ∝
fst (watched_by (keep_watch L j w S) L ! w))› and
‹no_dup
(get_trail_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x))› and
ge0: ‹(if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w) !
0 =
L
then 0 else 1)
< length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w))› and
ge1i: ‹1 -
(if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w) !
0 =
L
then 0 else 1)
< length
(get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w))› and
L_watched: ‹L ∈ set (watched_l
(get_clauses_l
(remove_one_lit_from_wq
(fst (watched_by (keep_watch L j w S) L ! w)) x) ∝
fst (watched_by (keep_watch L j w S) L ! w)))› and
‹get_conflict_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w)) x) =
None›
using unit_loop_inv
unfolding unit_propagation_inner_loop_body_l_inv_def
by blast
have unit_T: ‹unit_propagation_inner_loop_body_l_inv L C' T›
using that
by (auto simp: remove_one_lit_from_wq_def)
have corr: ‹correct_watching_except (Suc j) (Suc w) L (keep_watch L j w S)›
by (simp add: corr_w correct_watching_except_correct_watching_except_Suc_Suc_keep_watch
j_w w_le)
have i:
‹i = (if get_clauses_wl (keep_watch L j w S) ∝ x1 ! 0 = L then 0 else 1)›
‹i = (if get_clauses_l (fst X2) ∝ snd X2 ! 0 = L then 0 else 1)›
using SLw X2 S_S' unfolding i_def C'_bl apply (cases X2; auto simp add: twl_st_wl; fail)
using SLw X2 S_S' unfolding i_def C'_bl apply (cases X2; auto simp add: twl_st_wl; fail)
done
have i': ‹i = (if get_clauses_l
(remove_one_lit_from_wq (fst (watched_by (keep_watch L j w S) L ! w))
x) ∝
fst (watched_by (keep_watch L j w S) L ! w) !
0 =
L
then 0 else 1)›
using j_w w_le S_x unfolding i_def
by (cases S) (auto simp: keep_watch_def)
have ‹twl_st_inv x'›
using ‹twl_struct_invs x'› unfolding twl_struct_invs_def by fast
then have ‹∃x. twl_st_inv
(x, {#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#},
None, NE, UE,
add_mset
(L, TWL_Clause (mset (watched_l (N ∝ fst ((W L)[j := W L ! w] ! w))))
(mset (unwatched_l (N ∝ fst ((W L)[j := W L ! w] ! w)))))
{#(L, TWL_Clause (mset (watched_l (N ∝ x)))
(mset (unwatched_l (N ∝ x))))
. x ∈# remove1_mset (fst ((W L)[j := W L ! w] ! w))
{#i ∈# mset (drop w (map fst ((W L)[j := W L ! w]))).
i ∈# dom_m N#}#},
Q)›
using x_x' S_x
apply (cases x)
apply (auto simp: S twl_st_l_def state_wl_l_def keep_watch_def
simp del: struct_wf_twl_cls.simps)
done
have ‹twl_st_inv x'›
using ‹twl_struct_invs x'› unfolding twl_struct_invs_def by fast
then have ‹∃x. twl_st_inv
(x, {#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#},
None, NE, UE,
add_mset
(L, TWL_Clause (mset (watched_l (N ∝ fst ((W L)[j := W L ! w] ! w))))
(mset (unwatched_l (N ∝ fst ((W L)[j := W L ! w] ! w)))))
{#(L, TWL_Clause (mset (watched_l (N ∝ x)))
(mset (unwatched_l (N ∝ x))))
. x ∈# remove1_mset (fst ((W L)[j := W L ! w] ! w))
{#i ∈# mset (drop w (map fst ((W L)[j := W L ! w]))).
i ∈# dom_m N#}#},
Q)›
using x_x' S_x
apply (cases x)
apply (auto simp: S twl_st_l_def state_wl_l_def keep_watch_def
simp del: struct_wf_twl_cls.simps)
done
then have ‹Multiset.Ball
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# ran_m N#})
struct_wf_twl_cls›
unfolding twl_st_inv.simps image_mset_union[symmetric] all_clss_l_ran_m
by blast
then have distinct_N_x1: ‹distinct (N ∝ x1)›
using dom
by (auto simp: S ran_m_def mset_take_mset_drop_mset' dest!: multi_member_split)
have watch_by_S_w: ‹watched_by (keep_watch L j w S) L ! w = (x1, x2, x3)›
using j_w w_le SLw unfolding i_def C'_bl x2'
by (cases S)
(auto simp: keep_watch_def split: if_splits)
then have L_i: ‹L = N ∝ x1 ! i›
using L_watched ge0 ge1i SLw S_x unfolding i_def C'_bl
by (auto simp: take_2_if twl_st_wl S split: if_splits)
have i_le: ‹i < length (N ∝ x1)› ‹1-i < length (N ∝ x1)›
using watch_by_S_w ge0 ge1i S_x unfolding i'[symmetric]
by (auto simp: S)
have X2: ‹X2 = (set_clauses_to_update_l (remove1_mset x1 (clauses_to_update_l S')) S', x1)›
using SLw X2 S_S' unfolding i_def C'_bl by (cases X2; auto simp add: twl_st_wl)
have N_x1_in_L: ‹N ∝ x1 ! (Suc 0 - i)
∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE))›
using dom i_le by (auto simp: ran_m_def S all_lits_of_mm_add_mset
intro!: in_clause_in_all_lits_of_m
dest!: multi_member_split)
have ‹((M, N, None, NE, UE, Q, W (L := (W L)[j := (x1, N ∝ x1 ! (Suc 0 - i), x3)])),
fst X2) ∈ state_wl_l (Some (L, Suc w))›
using S_S' X2 j_w w_le SLw unfolding C'_bl
apply (auto simp: state_wl_l_def S keep_watch_def drop_map)
apply (subst Cons_nth_drop_Suc[symmetric])
apply auto[]
apply (subst (asm)Cons_nth_drop_Suc[symmetric])
apply auto[]
unfolding mset.simps image_mset_add_mset filter_mset_add_mset
subgoal premises p
using p(1-5)
by (auto simp: L_i)
done
moreover have ‹n = size {#(i, _) ∈# mset (drop (Suc w) (watched_by S L)).
i ∉# dom_m (get_clauses_wl S)#}›
using dom n w_le SLw unfolding C'_bl
by (auto simp: Cons_nth_drop_Suc[symmetric] dest!: multi_member_split)
moreover {
have ‹Suc 0 - i ≠ i›
by (auto simp: i_def split: if_splits)
then have ‹correct_watching_except (Suc j) (Suc w) L
(M, N, None, NE, UE, Q, W(L := (W L)[j := (x1, N ∝ x1 ! (Suc 0 - i), x3)]))›
using SLw unfolding C'_bl apply -
apply (rule correct_watching_except_update_blit)
using N_x1_in_L corr i_le distinct_N_x1 i_le bin x2' unfolding S
by (auto simp: keep_watch_def L_i nth_eq_iff_index_eq)
}
ultimately show ?thesis
using j_w w_le
unfolding i[symmetric]
by (auto simp: S update_blit_wl_def keep_watch_def)
qed
show 1: ?propa
(is ‹_ ≤ ⇓ ?unit _›)
supply trail_keep_w[simp]
unfolding unit_propagation_inner_loop_body_wl_int_alt_def
i_def[symmetric] i_def'[symmetric] unit_propagation_inner_loop_body_l_with_skip_alt_def
unit_propagation_inner_loop_body_l_def
apply (rewrite at "let _ = keep_watch _ _ _ _ in _" Let_def)
unfolding i_def[symmetric] SLw prod.case
apply (rewrite at "let _ = _ in let _ = get_clauses_l _ ∝ _ ! _ in _" Let_def)
apply (rewrite in ‹if (¬_) then ASSERT _ >>= _ else _› if_not_swap)
supply RETURN_as_SPEC_refine[refine2 del]
supply [[goals_limit=50]]
apply (refine_rcg val f f' keep_watch find_unwatched_l)
subgoal using inner_loop_inv w_le j_w
unfolding unit_propagation_inner_loop_wl_loop_pre_def by auto
subgoal using assms by auto
subgoal using w_le unfolding unit_prop_body_wl_inv_def by auto
subgoal using w_le j_w unfolding unit_prop_body_wl_inv_def by auto
subgoal by (rule blit_final)
subgoal unfolding unit_propagation_inner_loop_wl_loop_pre_def by fast
subgoal by auto
subgoal by (rule unit_prop_body_wl_inv)
apply assumption+
subgoal
using S_S' by auto
subgoal
using S_S' w_le j_w n confl_S
by (auto simp: correct_watching_except_correct_watching_except_Suc_Suc_keep_watch
Cons_nth_drop_Suc[symmetric] corr_w twl_st_wl)
subgoal
using S_S' by auto
subgoal for b x1 x2 X2 K x
by (rule blit_final_in_dom)
apply assumption+
subgoal for b x1 x2 X2 K x
unfolding unit_prop_body_wl_find_unwatched_inv_def
by auto
subgoal by auto
subgoal using S_S' by (auto simp: twl_st_wl)
subgoal for b x1 x2 X2 K x f x'
by (rule conflict_final)
subgoal for b x1 x2 X2 K x
by (rule propa_final)
subgoal
using S_S' by auto
subgoal for b x1 x2 X2 K x f x' xa x'a
by (rule update_blit_wl_final)
subgoal for b x1 x2 X2 K x f x' xa x'a
by (rule update_clss_final)
done
have [simp]: ‹add_mset a (remove1_mset a M) = M ⟷ a ∈# M› for a M
by (metis ab_semigroup_add_class.add.commute add.left_neutral multi_self_add_other_not_self
remove1_mset_eqE union_mset_add_mset_left)
show ?eq if inv: ‹unit_propagation_inner_loop_body_l_inv L C' T›
using i_le[OF inv] i_le2[OF inv] C'_dom[OF inv] S_S'
unfolding i_def[symmetric]
by (auto simp: ran_m_clause_upd image_mset_remove1_mset_if)
qed
lemma
fixes S :: ‹'v twl_st_wl› and S' :: ‹'v twl_st_l› and L :: ‹'v literal› and w :: nat
defines [simp]: ‹C' ≡ fst (watched_by S L ! w)›
defines
[simp]: ‹T ≡ remove_one_lit_from_wq C' S'›
defines
[simp]: ‹C'' ≡ get_clauses_l S' ∝ C'›
assumes
S_S': ‹(S, S') ∈ state_wl_l (Some (L, w))› and
w_le: ‹w < length (watched_by S L)› and
j_w: ‹j ≤ w› and
corr_w: ‹correct_watching_except j w L S› and
inner_loop_inv: ‹unit_propagation_inner_loop_wl_loop_inv L (j, w, S)› and
n: ‹n = size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl S)) (mset (drop w (watched_by S L))))› and
confl_S: ‹get_conflict_wl S = None›
shows unit_propagation_inner_loop_body_wl_spec: ‹unit_propagation_inner_loop_body_wl L j w S ≤
⇓{((i, j, T'), (T, n)).
(T', T) ∈ state_wl_l (Some (L, j)) ∧
correct_watching_except i j L T' ∧
j ≤ length (watched_by T' L) ∧
length (watched_by S L) = length (watched_by T' L) ∧
i ≤ j ∧
(get_conflict_wl T' = None ⟶
n = size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl T')) (mset (drop j (watched_by T' L))))) ∧
(get_conflict_wl T' ≠ None ⟶ n = 0)}
(unit_propagation_inner_loop_body_l_with_skip L (S', n))›
apply (rule order_trans)
apply (rule unit_propagation_inner_loop_body_wl_wl_int[OF S_S' w_le j_w corr_w inner_loop_inv n
confl_S])
apply (subst Down_id_eq)
apply (rule unit_propagation_inner_loop_body_wl_int_spec[OF S_S' w_le j_w corr_w inner_loop_inv n
confl_S])
done
definition unit_propagation_inner_loop_wl_loop
:: ‹'v literal ⇒ 'v twl_st_wl ⇒ (nat × nat × 'v twl_st_wl) nres› where
‹unit_propagation_inner_loop_wl_loop L S⇩0 = do {
let n = length (watched_by S⇩0 L);
WHILE⇩T⇗unit_propagation_inner_loop_wl_loop_inv L⇖
(λ(j, w, S). w < n ∧ get_conflict_wl S = None)
(λ(j, w, S). do {
unit_propagation_inner_loop_body_wl L j w S
})
(0, 0, S⇩0)
}›
lemma correct_watching_except_correct_watching_cut_watch:
assumes corr: ‹correct_watching_except j w L (a, b, c, d, e, f, g)›
shows ‹correct_watching (a, b, c, d, e, f, g(L := take j (g L) @ drop w (g L)))›
proof -
have
Heq:
‹⋀La i K b'. La ∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
(La = L ⟶
distinct_watched (take j (g La) @ drop w (g La)) ∧
((i, K, b')∈#mset (take j (g La) @ drop w (g La)) ⟶
i ∈# dom_m b ⟶ K ∈ set (b ∝ i) ∧ K ≠ La ∧ correctly_marked_as_binary b (i, K, b')) ∧
((i, K, b')∈#mset (take j (g La) @ drop w (g La)) ⟶
b' ⟶ i ∈# dom_m b) ∧
{#i ∈# fst `# mset (take j (g La) @ drop w (g La)). i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#}))› and
Hneq:
‹⋀La i K b'. La∈#all_lits_of_mm (mset `# ran_mf b + (d + e)) ⟹
(La ≠ L ⟶
distinct_watched (g La) ∧
((i, K, b')∈#mset (g La) ⟶ i ∈# dom_m b ⟶ K ∈ set (b ∝ i) ∧ K ≠ La
∧ correctly_marked_as_binary b (i, K, b')) ∧
((i, K, b')∈#mset (g La) ⟶ b' ⟶ i ∈# dom_m b) ∧
{#i ∈# fst `# mset (g La). i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#}))›
using corr
unfolding correct_watching.simps correct_watching_except.simps
by fast+
have
‹((i, K, b')∈#mset ((g(L := take j (g L) @ drop w (g L))) La) ⟹
i ∈# dom_m b ⟶ K ∈ set (b ∝ i) ∧ K ≠ La ∧ correctly_marked_as_binary b (i, K, b'))› and
‹(i, K, b')∈#mset ((g(L := take j (g L) @ drop w (g L))) La) ⟹
b' ⟶ i ∈# dom_m b› and
‹{#i ∈# fst `# mset ((g(L := take j (g L) @ drop w (g L))) La).
i ∈# dom_m b#} =
clause_to_update La (a, b, c, d, e, {#}, {#})›and
‹distinct_watched ((g(L := take j (g L) @ drop w (g L))) La)›
if ‹La∈#all_lits_of_mm (mset `# ran_mf b + (d + e))›
for La i K b'
apply (cases ‹La = L›)
subgoal
using Heq[of La i K] that by auto
subgoal
using Hneq[of La i K] that by auto
apply (cases ‹La = L›)
subgoal
using Heq[of La i K] that by auto
subgoal
using Hneq[of La i K] that by auto
apply (cases ‹La = L›)
subgoal
using Heq[of La i K] that by auto
subgoal
using Hneq[of La i K] that by auto
apply (cases ‹La = L›)
subgoal
using Heq[of La i K] that by auto
subgoal
using Hneq[of La i K] that by auto
done
then show ?thesis
unfolding correct_watching.simps
by blast
qed
lemma unit_propagation_inner_loop_wl_loop_alt_def:
‹unit_propagation_inner_loop_wl_loop L S⇩0 = do {
let (_ :: nat) = (if get_conflict_wl S⇩0 = None then remaining_nondom_wl 0 L S⇩0 else 0);
let n = length (watched_by S⇩0 L);
WHILE⇩T⇗unit_propagation_inner_loop_wl_loop_inv L⇖
(λ(j, w, S). w < n ∧ get_conflict_wl S = None)
(λ(j, w, S). do {
unit_propagation_inner_loop_body_wl L j w S
})
(0, 0, S⇩0)
}
›
unfolding unit_propagation_inner_loop_wl_loop_def Let_def by auto
definition cut_watch_list :: ‹nat ⇒ nat ⇒ 'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹cut_watch_list j w L =(λ(M, N, D, NE, UE, Q, W). do {
ASSERT(j ≤ w ∧ j ≤ length (W L) ∧ w ≤ length (W L));
RETURN (M, N, D, NE, UE, Q, W(L := take j (W L) @ drop w (W L)))
})›
definition unit_propagation_inner_loop_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹unit_propagation_inner_loop_wl L S⇩0 = do {
(j, w, S) ← unit_propagation_inner_loop_wl_loop L S⇩0;
ASSERT(j ≤ w ∧ w ≤ length (watched_by S L));
cut_watch_list j w L S
}›
lemma correct_watching_correct_watching_except00:
‹correct_watching S ⟹ correct_watching_except 0 0 L S›
apply (cases S)
apply (simp only: correct_watching.simps correct_watching_except.simps
take0 drop0 append.left_neutral)
by fast
lemma unit_propagation_inner_loop_wl_spec:
shows ‹(uncurry unit_propagation_inner_loop_wl, uncurry unit_propagation_inner_loop_l) ∈
{((L', T'::'v twl_st_wl), (L, T::'v twl_st_l)). L = L' ∧ (T', T) ∈ state_wl_l (Some (L, 0)) ∧
correct_watching T'} →
⟨{(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'}⟩ nres_rel
› (is ‹?fg ∈ ?A → ⟨?B⟩nres_rel› is ‹?fg ∈ ?A → ⟨{(T', T). _ ∧ ?P T T'}⟩nres_rel›)
proof -
{
fix L :: ‹'v literal› and S :: ‹'v twl_st_wl› and S' :: ‹'v twl_st_l›
assume
corr_w: ‹correct_watching S› and
SS': ‹(S, S') ∈ state_wl_l (Some (L, 0))›
text ‹To ease the finding the correspondence between the body of the loops, we introduce
following function:›
let ?R' = ‹{((i, j, T'), (T, n)).
(T', T) ∈ state_wl_l (Some (L, j)) ∧
correct_watching_except i j L T' ∧
j ≤ length (watched_by T' L) ∧
length (watched_by S L) = length (watched_by T' L) ∧
i ≤ j ∧
(get_conflict_wl T' = None ⟶
n = size (filter_mset (λ(i, _). i ∉# dom_m (get_clauses_wl T')) (mset (drop j (watched_by T' L))))) ∧
(get_conflict_wl T' ≠ None ⟶ n = 0)}›
have inv: ‹unit_propagation_inner_loop_wl_loop_inv L iT'›
if
iT'_Tn: ‹(iT', Tn) ∈ ?R'› and
‹unit_propagation_inner_loop_l_inv L Tn›
for Tn iT'
proof -
obtain i j :: nat and T' where iT': ‹iT' = (i, j, T')› by (cases iT')
obtain T n where Tn[simp]: ‹Tn = (T, n)› by (cases Tn)
have ‹unit_propagation_inner_loop_l_inv L (T, 0::nat)›
if ‹unit_propagation_inner_loop_l_inv L (T, n)› and ‹get_conflict_l T ≠ None›
using that iT'_Tn
unfolding unit_propagation_inner_loop_l_inv_def iT' prod.case
apply - apply normalize_goal+
apply (rule_tac x=x in exI)
by auto
then show ?thesis
unfolding unit_propagation_inner_loop_wl_loop_inv_def iT' prod.simps apply -
apply (rule exI[of _ T])
using that by (auto simp: iT')
qed
have cond: ‹(j < length (watched_by S L) ∧ get_conflict_wl T' = None) =
(clauses_to_update_l T ≠ {#} ∨ n > 0)›
if
iT'_T: ‹(ijT', Tn) ∈ ?R'› and
[simp]: ‹ijT' = (i, jT')› ‹jT' = (j, T')› ‹Tn = (T, n)›
for ijT' Tn i j T' n T jT'
proof -
have [simp]: ‹size {#(i, _) ∈# mset (drop j xs). i ∉# dom_m b#} =
size {#i ∈# fst `# mset (drop j xs). i ∉# dom_m b#}› for xs b
apply (induction ‹xs› arbitrary: j)
subgoal by auto
subgoal premises p for a xs j
using p[of 0] p
by (cases j) auto
done
have [simp]: ‹size (filter_mset (λi. (i ∈# (dom_m b))) (fst `# (mset (drop j (g L))))) +
size {#i ∈# fst `# mset (drop j (g L)). i ∉# dom_m b#} =
length (g L) - j› for g j b
apply (subst size_union[symmetric])
apply (subst multiset_partition[symmetric])
by auto
have [simp]: ‹A ≠ {#} ⟹ size A > 0› for A
by (auto dest!: multi_member_split)
have ‹length (watched_by T' L) = size (clauses_to_update_wl T' L j) + n + j›
if ‹get_conflict_wl T' = None›
using that iT'_T
by (cases ‹get_conflict_wl T'›; cases T')
(auto simp add: state_wl_l_def drop_map)
then show ?thesis
using iT'_T
by (cases ‹get_conflict_wl T' = None›) auto
qed
have remaining: ‹RETURN (if get_conflict_wl S = None then remaining_nondom_wl 0 L S else 0) ≤ SPEC (λ_. True)›
by auto
have unit_propagation_inner_loop_l_alt_def: ‹unit_propagation_inner_loop_l L S' = do {
n ← SPEC (λ_::nat. True);
(S, n) ← WHILE⇩T⇗unit_propagation_inner_loop_l_inv L⇖
(λ(S, n). clauses_to_update_l S ≠ {#} ∨ 0 < n)
(unit_propagation_inner_loop_body_l_with_skip L) (S', n);
RETURN S}› for L S'
unfolding unit_propagation_inner_loop_l_def by auto
have unit_propagation_inner_loop_wl_alt_def: ‹unit_propagation_inner_loop_wl L S = do {
let (n::nat) = (if get_conflict_wl S = None then remaining_nondom_wl 0 L S else 0);
(j, w, S) ← WHILE⇩T⇗unit_propagation_inner_loop_wl_loop_inv L⇖
(λ(j, w, T). w < length (watched_by S L) ∧ get_conflict_wl T = None)
(λ(j, x, y). unit_propagation_inner_loop_body_wl L j x y) (0, 0, S);
ASSERT (j ≤ w ∧ w ≤ length (watched_by S L));
cut_watch_list j w L S}›
unfolding unit_propagation_inner_loop_wl_loop_alt_def unit_propagation_inner_loop_wl_def
by auto
have ‹unit_propagation_inner_loop_wl L S ≤
⇓ {((T'), T). (T', T) ∈ state_wl_l None ∧ ?P T T'}
(unit_propagation_inner_loop_l L S')›
(is ‹_ ≤ ⇓ ?R _›)
unfolding unit_propagation_inner_loop_l_alt_def uncurry_def
unit_propagation_inner_loop_wl_alt_def
apply (refine_vcg WHILEIT_refine_genR[where
R' = ‹?R'› and
R = ‹{((i, j, T'), (T, n)). ((i, j, T'), (T, n)) ∈ ?R' ∧ i ≤ j ∧
length (watched_by S L) = length (watched_by T' L) ∧
(j ≥ length (watched_by T' L) ∨ get_conflict_wl T' ≠ None)}›]
remaining)
subgoal using corr_w SS' by (auto simp: correct_watching_correct_watching_except00)
subgoal by (rule inv)
subgoal by (rule cond)
subgoal for n i'w'T' Tn i' w'T' w' T'
apply (cases Tn)
apply (rule order_trans)
apply (rule unit_propagation_inner_loop_body_wl_spec[of _ ‹fst Tn›])
apply (simp only: prod.case in_pair_collect_simp)
apply normalize_goal+
by (auto simp del: twl_st_of_wl.simps)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for n i'w'T' Tn i' w'T' j L' w' T'
apply (cases T')
by (auto simp: state_wl_l_def cut_watch_list_def
dest!: correct_watching_except_correct_watching_cut_watch)
done
}
note H = this
show ?thesis
unfolding fref_param1
apply (intro frefI nres_relI)
by (auto simp: intro!: H)
qed
subsubsection ‹Outer loop›
definition select_and_remove_from_literals_to_update_wl :: ‹'v twl_st_wl ⇒ ('v twl_st_wl × 'v literal) nres› where
‹select_and_remove_from_literals_to_update_wl S = SPEC(λ(S', L). L ∈# literals_to_update_wl S ∧
S' = set_literals_to_update_wl (literals_to_update_wl S - {#L#}) S)›
definition unit_propagation_outer_loop_wl_inv where
‹unit_propagation_outer_loop_wl_inv S ⟷
(∃S'. (S, S') ∈ state_wl_l None ∧
correct_watching S ∧
unit_propagation_outer_loop_l_inv S')›
definition unit_propagation_outer_loop_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹unit_propagation_outer_loop_wl S⇩0 =
WHILE⇩T⇗unit_propagation_outer_loop_wl_inv⇖
(λS. literals_to_update_wl S ≠ {#})
(λS. do {
ASSERT(literals_to_update_wl S ≠ {#});
(S', L) ← select_and_remove_from_literals_to_update_wl S;
ASSERT(L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S') + get_unit_clauses_wl S'));
unit_propagation_inner_loop_wl L S'
})
(S⇩0 :: 'v twl_st_wl)
›
lemma unit_propagation_outer_loop_wl_spec:
‹(unit_propagation_outer_loop_wl, unit_propagation_outer_loop_l)
∈ {(T'::'v twl_st_wl, T).
(T', T) ∈ state_wl_l None ∧
correct_watching T'} →⇩f
⟨{(T', T).
(T', T) ∈ state_wl_l None ∧
correct_watching T'}⟩nres_rel›
(is ‹?u ∈ ?A →⇩f ⟨?B⟩ nres_rel›)
proof -
have inv: ‹unit_propagation_outer_loop_wl_inv T'›
if
‹(T', T) ∈ {(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'}› and
‹unit_propagation_outer_loop_l_inv T›
for T T'
unfolding unit_propagation_outer_loop_wl_inv_def
apply (rule exI[of _ T])
using that by auto
have select_and_remove_from_literals_to_update_wl:
‹select_and_remove_from_literals_to_update_wl S' ≤
⇓ {((T', L'), (T, L)). L = L' ∧ (T', T) ∈ state_wl_l (Some (L, 0)) ∧
T' = set_literals_to_update_wl (literals_to_update_wl S' - {#L#}) S' ∧ L ∈# literals_to_update_wl S' ∧
L ∈# all_lits_of_mm (mset `# ran_mf (get_clauses_wl S') + get_unit_clauses_wl S')
}
(select_and_remove_from_literals_to_update S)›
if S: ‹(S', S) ∈ state_wl_l None› and ‹get_conflict_wl S' = None› and
corr_w: ‹correct_watching S'› and
inv_l: ‹unit_propagation_outer_loop_l_inv S›
for S :: ‹'v twl_st_l› and S' :: ‹'v twl_st_wl›
proof -
obtain M N D NE UE W Q where
S': ‹S' = (M, N, D, NE, UE, Q, W)›
by (cases S') auto
obtain R where
S_R: ‹(S, R) ∈ twl_st_l None› and
struct_invs: ‹twl_struct_invs R›
using inv_l unfolding unit_propagation_outer_loop_l_inv_def by blast
have [simp]:
‹init_clss (state⇩W_of R) = mset `# (init_clss_lf N) + NE›
using S_R S by (auto simp: twl_st S' twl_st_wl)
have
no_dup_q: ‹no_duplicate_queued R› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of R)›
using struct_invs that by (auto simp: twl_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
then have H1: ‹L ∈# all_lits_of_mm (mset `# ran_mf N + NE + UE)› if LQ: ‹L ∈# Q› for L
proof -
have [simp]: ‹(f o g) ` I = f ` g ` I› for f g I
by auto
obtain K where ‹L = - lit_of K› and ‹K ∈# mset (trail (state⇩W_of R))›
using that no_dup_q LQ S_R S
mset_le_add_mset_decr_left2[of L ‹remove1_mset L Q› Q]
by (fastforce simp: S' cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
all_lits_of_mm_def atms_of_ms_def twl_st_l_def state_wl_l_def uminus_lit_swap
convert_lit.simps
dest!: multi_member_split[of L Q] mset_subset_eq_insertD in_convert_lits_lD2)
from imageI[OF this(2), of ‹atm_of o lit_of›]
have ‹atm_of L ∈ atm_of ` lits_of_l (get_trail_wl S')› and
[simp]: ‹atm_of ` lits_of_l (trail (state⇩W_of R)) = atm_of ` lits_of_l (get_trail_wl S')›
using S_R S S ‹L = - lit_of K›
by (simp_all add: twl_st image_image[symmetric]
lits_of_def[symmetric])
then have ‹atm_of L ∈ atm_of ` lits_of_l M›
using S' by auto
moreover {
have ‹atm_of ` lits_of_l M
⊆ (⋃x∈set_mset (init_clss_lf N). atm_of ` set x) ∪
(⋃x∈set_mset NE. atms_of x) ›
using that alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: S' cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
all_lits_of_mm_def atms_of_ms_def)
then have ‹atm_of ` lits_of_l M ⊆ (⋃x∈set_mset (init_clss_lf N). atm_of ` set x) ∪
(⋃x∈set_mset NE. atms_of x)›
unfolding image_Un[symmetric]
set_append[symmetric]
append_take_drop_id
.
then have ‹atm_of ` lits_of_l M ⊆ atms_of_mm (mset `# init_clss_lf N + NE)›
by (smt UN_Un Un_iff append_take_drop_id atms_of_ms_def atms_of_ms_mset_unfold set_append
set_image_mset set_mset_mset set_mset_union subset_eq)
}
ultimately have ‹atm_of L ∈ atms_of_mm (mset `# ran_mf N + NE)›
using that
unfolding all_lits_of_mm_union atms_of_ms_union all_clss_lf_ran_m[symmetric]
image_mset_union set_mset_union
by auto
then show ?thesis
using that by (auto simp: in_all_lits_of_mm_ain_atms_of_iff)
qed
have H: ‹clause_to_update L S = {#i ∈# fst `# mset (W L). i ∈# dom_m N#}› and
‹L ∈# all_lits_of_mm (mset `# ran_mf N + NE + UE)›
if ‹L ∈# Q› for L
using corr_w that S H1[OF that] by (auto simp: correct_watching.simps S' clause_to_update_def
Ball_def ac_simps all_conj_distrib
dest!: multi_member_split)
show ?thesis
unfolding select_and_remove_from_literals_to_update_wl_def select_and_remove_from_literals_to_update_def
apply (rule RES_refine)
unfolding Bex_def
apply (rule_tac x=‹(set_clauses_to_update_l (clause_to_update (snd s) S)
(set_literals_to_update_l
(remove1_mset (snd s) (literals_to_update_l S)) S), snd s)› in exI)
using that S' S by (auto 5 5 simp: correct_watching.simps clauses_def state_wl_l_def
mset_take_mset_drop_mset' cdcl⇩W_restart_mset_state all_lits_of_mm_union
dest: H H1)
qed
have conflict_None: ‹get_conflict_wl T = None›
if
‹literals_to_update_wl T ≠ {#}› and
inv1: ‹unit_propagation_outer_loop_wl_inv T›
for T
proof -
obtain T' where
2: ‹(T, T') ∈ state_wl_l None› and
inv2: ‹unit_propagation_outer_loop_l_inv T'›
using inv1 unfolding unit_propagation_outer_loop_wl_inv_def by blast
obtain T'' where
3: ‹(T', T'') ∈ twl_st_l None› and
‹twl_struct_invs T''›
using inv2 unfolding unit_propagation_outer_loop_l_inv_def by blast
then have ‹get_conflict T'' ≠ None ⟶
clauses_to_update T'' = {#} ∧ literals_to_update T'' = {#}›
unfolding twl_struct_invs_def by fast
then show ?thesis
using that 2 3 by (auto simp: twl_st_wl twl_st twl_st_l)
qed
show ?thesis
unfolding unit_propagation_outer_loop_wl_def unit_propagation_outer_loop_l_def
apply (intro frefI nres_relI)
apply (refine_rcg select_and_remove_from_literals_to_update_wl
unit_propagation_inner_loop_wl_spec[unfolded fref_param1, THEN fref_to_Down_curry])
subgoal by (rule inv)
subgoal by auto
subgoal by auto
subgoal by (rule conflict_None)
subgoal for T' T by (auto simp: )
subgoal by (auto simp: twl_st_wl)
subgoal by auto
done
qed
subsubsection ‹Decide or Skip›
definition find_unassigned_lit_wl :: ‹'v twl_st_wl ⇒ 'v literal option nres› where
‹find_unassigned_lit_wl = (λ(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_wl_or_skip_pre where
‹decide_wl_or_skip_pre S ⟷
(∃S'. (S, S') ∈ state_wl_l None ∧
decide_l_or_skip_pre S'
)›
definition decide_lit_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹decide_lit_wl = (λL' (M, N, D, NE, UE, Q, W).
(Decided L' # M, N, D, NE, UE, {#- L'#}, W))›
definition decide_wl_or_skip :: ‹'v twl_st_wl ⇒ (bool × 'v twl_st_wl) nres› where
‹decide_wl_or_skip S = (do {
ASSERT(decide_wl_or_skip_pre S);
L ← find_unassigned_lit_wl S;
case L of
None ⇒ RETURN (True, S)
| Some L ⇒ RETURN (False, decide_lit_wl L S)
})
›
lemma decide_wl_or_skip_spec:
‹(decide_wl_or_skip, decide_l_or_skip)
∈ {(T':: 'v twl_st_wl, T).
(T', T) ∈ state_wl_l None ∧
correct_watching T' ∧
get_conflict_wl T' = None} →
⟨{((b', T'), (b, T)). b' = b ∧
(T', T) ∈ state_wl_l None ∧
correct_watching T'}⟩nres_rel›
proof -
have find_unassigned_lit_wl: ‹find_unassigned_lit_wl S'
≤ ⇓ Id
(find_unassigned_lit_l S)›
if ‹(S', S) ∈ state_wl_l None›
for S :: ‹'v twl_st_l› and S' :: ‹'v twl_st_wl›
using that
by (cases S') (auto simp: find_unassigned_lit_wl_def find_unassigned_lit_l_def
mset_take_mset_drop_mset' state_wl_l_def)
have option: ‹(x, x') ∈ ⟨Id⟩option_rel› if ‹x = x'› for x x'
using that by (auto)
show ?thesis
unfolding decide_wl_or_skip_def decide_l_or_skip_def
apply (refine_vcg find_unassigned_lit_wl option)
subgoal unfolding decide_wl_or_skip_pre_def by fast
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S S'
by (cases S) (auto simp: correct_watching.simps clause_to_update_def
decide_lit_l_def decide_lit_wl_def state_wl_l_def)
done
qed
subsubsection ‹Skip or Resolve›
definition tl_state_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
‹tl_state_wl = (λ(M, N, D, NE, UE, WS, Q). (tl M, N, D, NE, UE, WS, Q))›
definition resolve_cls_wl' :: ‹'v twl_st_wl ⇒ nat ⇒ 'v literal ⇒ 'v clause› where
‹resolve_cls_wl' S C L =
remove1_mset L (remove1_mset (-L) (the (get_conflict_wl S) ∪# (mset (get_clauses_wl S ∝ C))))›
definition update_confl_tl_wl :: ‹nat ⇒ 'v literal ⇒ 'v twl_st_wl ⇒ bool × 'v twl_st_wl› where
‹update_confl_tl_wl = (λC L (M, N, D, NE, UE, WS, Q).
let D = resolve_cls_wl' (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_wl_inv :: ‹'v twl_st_wl ⇒ bool ⇒ 'v twl_st_wl ⇒ bool› where
‹skip_and_resolve_loop_wl_inv S⇩0 brk S ⟷
(∃S' S'⇩0. (S, S') ∈ state_wl_l None ∧
(S⇩0, S'⇩0) ∈ state_wl_l None ∧
skip_and_resolve_loop_inv_l S'⇩0 brk S' ∧
correct_watching S)›
definition skip_and_resolve_loop_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹skip_and_resolve_loop_wl S⇩0 =
do {
ASSERT(get_conflict_wl S⇩0 ≠ None);
(_, S) ←
WHILE⇩T⇗λ(brk, S). skip_and_resolve_loop_wl_inv S⇩0 brk S⇖
(λ(brk, S). ¬brk ∧ ¬is_decided (hd (get_trail_wl S)))
(λ(_, S).
do {
let D' = the (get_conflict_wl S);
let (L, C) = lit_and_ann_of_propagated (hd (get_trail_wl S));
if -L ∉# D' then
do {RETURN (False, tl_state_wl S)}
else
if get_maximum_level (get_trail_wl S) (remove1_mset (-L) D') = count_decided (get_trail_wl S)
then
do {RETURN (update_confl_tl_wl C L S)}
else
do {RETURN (True, S)}
}
)
(False, S⇩0);
RETURN S
}
›
lemma tl_state_wl_tl_state_l:
‹(S, S') ∈ state_wl_l None ⟹ (tl_state_wl S, tl_state_l S') ∈ state_wl_l None›
by (cases S) (auto simp: state_wl_l_def tl_state_wl_def tl_state_l_def)
lemma skip_and_resolve_loop_wl_spec:
‹(skip_and_resolve_loop_wl, skip_and_resolve_loop_l)
∈ {(T'::'v twl_st_wl, T).
(T', T) ∈ state_wl_l None ∧
correct_watching T' ∧
0 < count_decided (get_trail_wl T')} →
⟨{(T', T).
(T', T) ∈ state_wl_l None ∧
correct_watching T'}⟩nres_rel›
(is ‹?s ∈ ?A → ⟨?B⟩nres_rel›)
proof -
have get_conflict_wl: ‹((False, S'), False, S)
∈ Id ×⇩r {(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'}›
(is ‹_ ∈ ?B›)
if ‹(S', S) ∈ state_wl_l None› and ‹correct_watching S'›
for S :: ‹'v twl_st_l› and S' :: ‹'v twl_st_wl›
using that by (cases S') (auto simp: state_wl_l_def)
have [simp]: ‹correct_watching (tl_state_wl S) = correct_watching S› for S
by (cases S) (auto simp: correct_watching.simps tl_state_wl_def clause_to_update_def)
have [simp]: ‹correct_watching (tl aa, ca, da, ea, fa, ha, h) ⟷
correct_watching (aa, ca, None, ea, fa, ha, h)›
for aa ba ca L da ea fa ha h
by (auto simp: correct_watching.simps tl_state_wl_def clause_to_update_def)
have [simp]: ‹NO_MATCH None da ⟹ correct_watching (aa, ca, da, ea, fa, ha, h) ⟷
correct_watching (aa, ca, None, ea, fa, ha, h)›
for aa ba ca L da ea fa ha h
by (auto simp: correct_watching.simps tl_state_wl_def clause_to_update_def)
have update_confl_tl_wl: ‹
(brkT, brkT') ∈ bool_rel ×⇩f {(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'} ⟹
case brkT' of (brk, S) ⇒ skip_and_resolve_loop_inv_l S' brk S ⟹
brkT' = (brk', T') ⟹
brkT = (brk, T) ⟹
lit_and_ann_of_propagated (hd (get_trail_l T')) = (L', C') ⟹
lit_and_ann_of_propagated (hd (get_trail_wl T)) = (L, C) ⟹
(update_confl_tl_wl C L T, update_confl_tl_l C' L' T') ∈ bool_rel ×⇩f {(T', T).
(T', T) ∈ state_wl_l None ∧ correct_watching T'}›
for T' brkT brk brkT' brk' T C C' L L' S'
unfolding update_confl_tl_wl_def update_confl_tl_l_def resolve_cls_wl'_def resolve_cls_l'_def
by (cases T; cases T')
(auto simp: Let_def state_wl_l_def)
have inv: ‹skip_and_resolve_loop_wl_inv S' b' T'›
if
‹(S', S) ∈ ?A› and
‹get_conflict_wl S' ≠ None› and
bt_inv: ‹case bT of (x, xa) ⇒ skip_and_resolve_loop_inv_l S x xa› and
‹(b'T', bT) ∈ ?B› and
b'T': ‹b'T' = (b', T')›
for S' S b'T' bT b' T'
proof -
obtain b T where bT: ‹bT = (b, T)› by (cases bT)
show ?thesis
unfolding skip_and_resolve_loop_wl_inv_def
apply (rule exI[of _ T])
apply (rule exI[of _ S])
using that by (auto simp: bT b'T')
qed
show H: ‹?s ∈ ?A → ⟨{(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'}⟩nres_rel›
unfolding skip_and_resolve_loop_wl_def skip_and_resolve_loop_l_def
apply (refine_rcg get_conflict_wl)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule inv)
subgoal by auto
subgoal by auto
subgoal by (auto intro!: tl_state_wl_tl_state_l)
subgoal for S' S b'T' bT b' T' by (cases T') (auto simp: correct_watching.simps)
subgoal by auto
subgoal by (rule update_confl_tl_wl) assumption+
subgoal by auto
subgoal by (auto simp: correct_watching.simps clause_to_update_def)
done
qed
subsubsection ‹Backtrack›
definition find_decomp_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹find_decomp_wl = (λL (M, N, D, NE, UE, Q, W).
SPEC(λS. ∃K M2 M1. S = (M1, N, D, NE, UE, Q, W) ∧ (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (the D - {#-L#}) + 1))›
definition find_lit_of_max_level_wl :: ‹'v twl_st_wl ⇒ 'v literal ⇒ 'v literal nres› where
‹find_lit_of_max_level_wl = (λ(M, N, D, NE, UE, Q, W) L.
SPEC(λL'. L' ∈# remove1_mset (-L) (the D) ∧ get_level M L' = get_maximum_level M (the D - {#-L#})))›
fun extract_shorter_conflict_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹extract_shorter_conflict_wl (M, N, D, NE, UE, Q, W) = SPEC(λS.
∃D'. D' ⊆# the D ∧ S = (M, N, Some D', NE, UE, Q, W) ∧
clause `# twl_clause_of `# ran_mf N + NE + UE ⊨pm D' ∧ -(lit_of (hd M)) ∈# D')›
declare extract_shorter_conflict_wl.simps[simp del]
lemmas extract_shorter_conflict_wl_def = extract_shorter_conflict_wl.simps
definition backtrack_wl_inv where
‹backtrack_wl_inv S ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ backtrack_l_inv S' ∧ correct_watching S)
›
text ‹Rougly: we get a fresh index that has not yet been used.›
definition get_fresh_index_wl :: ‹'v clauses_l ⇒ _ ⇒ _ ⇒ nat nres› where
‹get_fresh_index_wl N NUE W = SPEC(λi. i > 0 ∧ i ∉# dom_m N ∧
(∀L ∈# all_lits_of_mm (mset `# ran_mf N + NUE) . i ∉ fst ` set (W L)))›
definition propagate_bt_wl :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹propagate_bt_wl = (λL L' (M, N, D, NE, UE, Q, W). do {
D'' ← list_of_mset (the D);
i ← get_fresh_index_wl N (NE + UE) W;
let b = (length ([-L, L'] @ (remove1 (-L) (remove1 L' D''))) = 2);
RETURN (Propagated (-L) i # M,
fmupd i ([-L, L'] @ (remove1 (-L) (remove1 L' D'')), False) N,
None, NE, UE, {#L#}, W(-L:= W (-L) @ [(i, L', b)], L':= W L' @ [(i, -L, b)]))
})›
definition propagate_unit_bt_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹propagate_unit_bt_wl = (λL (M, N, D, NE, UE, Q, W).
(Propagated (-L) 0 # M, N, None, NE, add_mset (the D) UE, {#L#}, W))›
definition backtrack_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹backtrack_wl S =
do {
ASSERT(backtrack_wl_inv S);
let L = lit_of (hd (get_trail_wl S));
S ← extract_shorter_conflict_wl S;
S ← find_decomp_wl L S;
if size (the (get_conflict_wl S)) > 1
then do {
L' ← find_lit_of_max_level_wl S L;
propagate_bt_wl L L' S
}
else do {
RETURN (propagate_unit_bt_wl L S)
}
}›
lemma correct_watching_learn:
assumes
L1: ‹atm_of L1 ∈ atms_of_mm (mset `# ran_mf N + NE)› and
L2: ‹atm_of L2 ∈ atms_of_mm (mset `# ran_mf N + NE)› and
UW: ‹atms_of (mset UW) ⊆ atms_of_mm (mset `# ran_mf N + NE)› and
i_dom: ‹i ∉# dom_m N› and
fresh: ‹⋀L. L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹ i ∉ fst ` set (W L)› and
[iff]: ‹L1 ≠ L2› and
b: ‹b ⟷ length (L1 # L2 # UW) = 2›
shows
‹correct_watching (K # M, fmupd i (L1 # L2 # UW, b') N,
D, NE, UE, Q, W (L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) ⟷
correct_watching (M, N, D, NE, UE, Q', W)›
(is ‹?l ⟷ ?c› is ‹correct_watching (_, ?N, _) = _›)
proof -
have [iff]: ‹L2 ≠ L1›
using ‹L1 ≠ L2› by (subst eq_commute)
have [simp]: ‹clause_to_update L1 (M, fmupd i (L1 # L2 # UW, b') N, D, NE, UE, {#}, {#}) =
add_mset i (clause_to_update L1 (M, N, D, NE, UE, {#}, {#}))› for L2 UW
using i_dom
by (auto simp: clause_to_update_def intro: filter_mset_cong)
have [simp]: ‹clause_to_update L2 (M, fmupd i (L1 # L2 # UW, b') N, D, NE, UE, {#}, {#}) =
add_mset i (clause_to_update L2 (M, N, D, NE, UE, {#}, {#}))› for L1 UW
using i_dom
by (auto simp: clause_to_update_def intro: filter_mset_cong)
have [simp]: ‹x ≠ L1 ⟹ x ≠ L2 ⟹
clause_to_update x (M, fmupd i (L1 # L2 # UW, b') N, D, NE, UE, {#}, {#}) =
clause_to_update x (M, N, D, NE, UE, {#}, {#})› for x UW
using i_dom
by (auto simp: clause_to_update_def intro: filter_mset_cong)
have [simp]: ‹L1 ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE))›
‹L2 ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE))›
using i_dom L1 L2 UW
by (fastforce simp: ran_m_mapsto_upd_notin
all_lits_of_mm_add_mset all_lits_of_m_add_mset in_all_lits_of_m_ain_atms_of_iff
in_all_lits_of_mm_ain_atms_of_iff)+
have H':
‹{#ia ∈# fst `# mset (W x). ia = i ∨ ia ∈# dom_m N#} = {#ia ∈# fst `# mset (W x). ia ∈# dom_m N#}›
if ‹x ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE))› for x
using i_dom fresh[of x] that
by (auto simp: clause_to_update_def intro!: filter_mset_cong)
have [simp]:
‹clause_to_update L1 (K # M, N, D, NE, UE, {#}, {#}) = clause_to_update L1 (M, N, D, NE, UE, {#}, {#})›
for L1 N D NE UE M K
by (auto simp: clause_to_update_def)
have [simp]: ‹set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m ?N#} + (NE + UE))) =
set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE + UE)))›
using i_dom L1 L2 UW
by (fastforce simp: ran_m_mapsto_upd_notin
all_lits_of_mm_add_mset all_lits_of_m_add_mset in_all_lits_of_m_ain_atms_of_iff
in_all_lits_of_mm_ain_atms_of_iff)
show ?thesis
proof (rule iffI)
assume corr: ?l
have
H: ‹⋀L ia K' b''. (L∈#all_lits_of_mm
(mset `# ran_mf (fmupd i (L1 # L2 # UW, b') N) + (NE + UE)) ⟹
distinct_watched ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) L) ∧
((ia, K', b'')∈#mset ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) L) ⟶
ia ∈# dom_m (fmupd i (L1 # L2 # UW, b') N) ⟶
K' ∈ set (fmupd i (L1 # L2 # UW, b') N ∝ ia) ∧ K' ≠ L ∧
correctly_marked_as_binary (fmupd i (L1 # L2 # UW, b') N) (ia, K', b'') ) ∧
((ia, K', b'')∈#mset ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) L) ⟶
b'' ⟶ ia ∈# dom_m (fmupd i (L1 # L2 # UW, b') N)) ∧
{#ia ∈# fst `#
mset ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) L).
ia ∈# dom_m (fmupd i (L1 # L2 # UW, b') N)#} =
clause_to_update L
(K # M, fmupd i (L1 # L2 # UW, b') N, D, NE, UE, {#}, {#}))›
using corr unfolding correct_watching.simps
by fast+
have ‹x ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE)) ⟹
distinct_watched (W x) ∧
(xa ∈# mset (W x) ⟶ (((case xa of (i, K, b'') ⇒ i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ x ∧
correctly_marked_as_binary N (i, K, b'')) ∧
(case xa of (i, K, b'') ⇒ b'' ⟶ i ∈# dom_m N)))) ∧
{#i ∈# fst `# mset (W x). i ∈# dom_m N#} = clause_to_update x (M, N, D, NE, UE, {#}, {#})›
for x xa
supply correctly_marked_as_binary.simps[simp]
using H[of x ‹fst xa› ‹fst (snd xa)› ‹snd (snd xa)›] fresh[of x] i_dom
apply (cases ‹x = L1›; cases ‹x = L2›)
subgoal
by (cases xa)
(auto dest!: multi_member_split simp: H')
subgoal
by (cases xa) (force simp add: H' split: if_splits)
subgoal
by (cases xa)
(force simp add: H' split: if_splits)
subgoal
by (cases xa)
(force simp add: H' split: if_splits)
done
then show ?c
unfolding correct_watching.simps Ball_def
by (auto 5 5 simp add: all_lits_of_mm_add_mset all_lits_of_m_add_mset
all_conj_distrib all_lits_of_mm_union dest: multi_member_split)
next
assume corr: ?c
have
H: ‹⋀L ia K' b''. (L∈#all_lits_of_mm
(mset `# ran_mf N + (NE + UE)) ⟹
distinct_watched (W L) ∧
((ia, K', b'')∈#mset (W L) ⟶
ia ∈# dom_m N ⟶
K' ∈ set (N ∝ ia) ∧ K' ≠ L ∧ correctly_marked_as_binary N (ia, K', b'')) ∧
((ia, K', b'')∈#mset (W L) ⟶ b'' ⟶ ia ∈# dom_m N) ∧
{#ia ∈# fst `# mset (W L). ia ∈# dom_m N#} = clause_to_update L (M, N, D, NE, UE, {#}, {#}))›
using corr unfolding correct_watching.simps
by blast+
have ‹x ∈# all_lits_of_mm (mset `# ran_mf (fmupd i (L1 # L2 # UW, b') N) + (NE + UE)) ⟶
distinct_watched ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) x) ∧
(xa ∈# mset ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) x) ⟶
(case xa of (ia, K, b'') ⇒ ia ∈# dom_m (fmupd i (L1 # L2 # UW, b') N) ⟶
K ∈ set (fmupd i (L1 # L2 # UW, b') N ∝ ia) ∧ K ≠ x ∧
correctly_marked_as_binary (fmupd i (L1 # L2 # UW, b') N) (ia, K, b''))) ∧
(xa ∈# mset ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) x) ⟶
(case xa of (ia, K, b'') ⇒ b'' ⟶ ia ∈# dom_m (fmupd i (L1 # L2 # UW, b') N))) ∧
{#ia ∈# fst `# mset ((W(L1 := W L1 @ [(i, L2, b)], L2 := W L2 @ [(i, L1, b)])) x). ia ∈# dom_m (fmupd i (L1 # L2 # UW, b') N)#} =
clause_to_update x (K # M, fmupd i (L1 # L2 # UW, b') N, D, NE, UE, {#}, {#})›
for x :: ‹'a literal› and xa
supply correctly_marked_as_binary.simps[simp]
using H[of x ‹fst xa› ‹fst (snd xa)› ‹snd (snd xa)›] fresh[of x] i_dom b
apply (cases ‹x = L1›; cases ‹x = L2›)
subgoal
by (cases xa)
(auto dest!: multi_member_split simp: H')
subgoal
by (cases xa)
(auto dest!: multi_member_split simp: H')
subgoal
by (cases xa)
(auto dest!: multi_member_split simp: H')
subgoal
by (cases xa)
(auto dest!: multi_member_split simp: H')
done
then show ?l
unfolding correct_watching.simps Ball_def
by auto
qed
qed
fun equality_except_conflict_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl ⇒ bool› where
‹equality_except_conflict_wl (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'›
fun equality_except_trail_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl ⇒ bool› where
‹equality_except_trail_wl (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'›
lemma equality_except_conflict_wl_get_clauses_wl:
‹equality_except_conflict_wl S Y ⟹ get_clauses_wl S = get_clauses_wl Y›
by (cases S; cases Y) (auto simp:)
lemma equality_except_trail_wl_get_clauses_wl:
‹equality_except_trail_wl S Y⟹ get_clauses_wl S = get_clauses_wl Y›
by (cases S; cases Y) (auto simp:)
lemma backtrack_wl_spec:
‹(backtrack_wl, backtrack_l)
∈ {(T'::'v twl_st_wl, T).
(T', T) ∈ state_wl_l None ∧
correct_watching T' ∧
get_conflict_wl T' ≠ None ∧
get_conflict_wl T' ≠ Some {#}} →
⟨{(T', T).
(T', T) ∈ state_wl_l None ∧
correct_watching T'}⟩nres_rel›
(is ‹?bt ∈ ?A → ⟨?B⟩nres_rel›)
proof -
have extract_shorter_conflict_wl: ‹extract_shorter_conflict_wl S'
≤ ⇓ {(U'::'v twl_st_wl, U).
(U', U) ∈ state_wl_l None ∧ equality_except_conflict_wl U' S' ∧
the (get_conflict_wl U') ⊆# the (get_conflict_wl S') ∧
get_conflict_wl U' ≠ None} (extract_shorter_conflict_l S)›
(is ‹_ ≤ ⇓ ?extract _›)
if ‹(S', S) ∈ ?A›
for S' S
apply (cases S'; cases S)
apply clarify
unfolding extract_shorter_conflict_wl_def extract_shorter_conflict_l_def
apply (rule RES_refine)
using that
by (auto simp: extract_shorter_conflict_wl_def extract_shorter_conflict_l_def
mset_take_mset_drop_mset state_wl_l_def)
have find_decomp_wl: ‹find_decomp_wl L T'
≤ ⇓ {(U'::'v twl_st_wl, U).
(U', U) ∈ state_wl_l None ∧ equality_except_trail_wl U' T' ∧
(∃M. get_trail_wl T' = M @ get_trail_wl U') } (find_decomp L' T)›
(is ‹_ ≤ ⇓ ?find _›)
if ‹(S', S) ∈ ?A› ‹L = L'› ‹(T', T) ∈ ?extract S'›
for S' S T T' L L'
using that
apply (cases T; cases T')
apply clarify
unfolding find_decomp_wl_def find_decomp_def prod.case
apply (rule RES_refine)
apply (auto 5 5 simp add: state_wl_l_def find_decomp_wl_def find_decomp_def)
done
have find_lit_of_max_level_wl: ‹find_lit_of_max_level_wl T' LLK'
≤ ⇓ {(L', L). L = L' ∧ L' ∈# the (get_conflict_wl T') ∧ L' ∈# the (get_conflict_wl T') - {#-LLK'#}}
(find_lit_of_max_level T L)›
(is ‹_ ≤ ⇓ ?find_lit _›)
if ‹L = LLK'› ‹(T', T) ∈ ?find S'›
for S' S T T' L LLK'
using that
apply (cases T; cases T'; cases S')
apply clarify
unfolding find_lit_of_max_level_wl_def find_lit_of_max_level_def prod.case
apply (rule RES_refine)
apply (auto simp add: find_lit_of_max_level_wl_def find_lit_of_max_level_def state_wl_l_def
dest: in_diffD)
done
have empty: ‹literals_to_update_wl S' = {#}› if bt: ‹backtrack_wl_inv S'› for S'
using bt apply -
unfolding backtrack_wl_inv_def backtrack_l_inv_def
apply normalize_goal+
apply (auto simp: twl_struct_invs_def)
done
have propagate_bt_wl: ‹propagate_bt_wl (lit_of (hd (get_trail_wl S'))) L' U'
≤ ⇓ {(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'}
(propagate_bt_l (lit_of (hd (get_trail_l S))) L U)›
(is ‹_ ≤ ⇓ ?propa _›)
if SS': ‹(S', S) ∈ ?A› and
UU': ‹(U', U) ∈ ?find T'› and
LL': ‹(L', L) ∈ ?find_lit U' (lit_of (hd (get_trail_wl S')))› and
TT': ‹(T', T) ∈ ?extract S'› and
bt: ‹backtrack_wl_inv S'›
for S' S T T' L L' U U'
proof -
note empty = empty[OF bt]
define K' where ‹K' = lit_of (hd (get_trail_l S))›
obtain MS NS DS NES UES W where
S': ‹S' = (MS, NS, Some DS, NES, UES, {#}, W)›
using SS' empty by (cases S'; cases ‹get_conflict_wl S'›) auto
then obtain DT where
T': ‹T' = (MS, NS, Some DT, NES, UES, {#}, W)› and
‹DT ⊆# DS›
using TT' by (cases T'; cases ‹get_conflict_wl T'›) auto
then obtain MU MU' where
U': ‹U' = (MU, NS, Some DT, NES, UES, {#}, W)› and
MU: ‹MS = MU' @ MU› and
U'U: ‹(U', U) ∈ state_wl_l None›
using UU' by (cases U') auto
then have U: ‹U = (MU, NS, Some DT, NES, UES, {#}, {#})›
by (cases U) (auto simp: state_wl_l_def)
have MS: ‹MS ≠ []›
using bt unfolding backtrack_wl_inv_def backtrack_l_inv_def S' by (auto simp: state_wl_l_def)
have ‹correct_watching S'›
using SS' by fast
then have corr: ‹correct_watching (MU, NS, None, NES, UES, {#K'#}, W)›
unfolding S' correct_watching.simps clause_to_update_def get_clauses_l.simps
by simp
have K_hd[simp]: ‹lit_of (hd MS) = K'›
using SS' unfolding K'_def by (auto simp: S')
have [simp]: ‹L = L'›
using LL' by auto
have trail_no_alien:
‹atm_of ` lits_of_l (get_trail_wl S')
⊆ atms_of_ms
((λx. mset (fst x)) `
{a. a ∈# ran_m (get_clauses_wl S') ∧ snd a}) ∪
atms_of_mm (get_unit_init_clss_wl S')› and
no_alien: ‹atms_of DS ⊆ atms_of_ms
((λx. mset (fst x)) `
{a. a ∈# ran_m (get_clauses_wl S') ∧ snd a}) ∪
atms_of_mm (get_unit_init_clss_wl S')› and
dist: ‹distinct_mset DS›
using SS' bt unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
backtrack_wl_inv_def backtrack_l_inv_def cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
apply -
apply normalize_goal+
apply (simp add: twl_st twl_st_l twl_st_wl)
apply normalize_goal+
apply (simp add: twl_st twl_st_l twl_st_wl S')
apply normalize_goal+
apply (simp add: twl_st twl_st_l twl_st_wl S')
done
moreover have ‹L' ∈# DS›
using LL' TT' by (auto simp: T' S' U' mset_take_mset_drop_mset)
ultimately have
atm_L': ‹atm_of L' ∈ atms_of_mm (mset `# init_clss_lf NS + NES)› and
atm_confl: ‹∀L∈#DS. atm_of L ∈ atms_of_mm (mset `# init_clss_lf NS + NES)›
by (auto simp: cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state S'
mset_take_mset_drop_mset dest!: atm_of_lit_in_atms_of)
have atm_K': ‹atm_of K' ∈ atms_of_mm (mset `# init_clss_lf NS + NES)›
using trail_no_alien K_hd MS
by (cases MS) (auto simp: S'
mset_take_mset_drop_mset simp del: K_hd dest!: atm_of_lit_in_atms_of)
have dist: ‹distinct_mset DT›
using ‹DT ⊆# DS› dist by (rule distinct_mset_mono)
have fresh: ‹get_fresh_index_wl N (NUE) W ≤
⇓ {(i, i'). i = i' ∧ i ∉# dom_m N ∧ (∀L ∈# all_lits_of_mm (mset `# ran_mf N + NUE). i ∉ fst ` set (W L))} (get_fresh_index N')›
if ‹N = N'› for N N' NUE W
unfolding that get_fresh_index_def get_fresh_index_wl_def
by (auto intro: RES_refine)
have [refine0]: ‹SPEC (λD'. the D = mset D') ≤ ⇓ {(D', E'). D' = E' ∧ the D = mset D'}
(SPEC (λD'. the E = mset D'))›
if ‹D = E› for D E
using that by (auto intro!: RES_refine)
show ?thesis
unfolding propagate_bt_wl_def propagate_bt_l_def S' T' U' U st_l_of_wl.simps get_trail_wl.simps
list_of_mset_def K'_def[symmetric] Let_def
apply (refine_vcg fresh; remove_dummy_vars)
apply (subst in_pair_collect_simp)
apply (intro conjI)
subgoal using SS' by (auto simp: corr state_wl_l_def S')
subgoal
apply simp
apply (subst correct_watching_learn)
subgoal using atm_K' unfolding all_clss_lf_ran_m[symmetric] image_mset_union by auto
subgoal using atm_L' unfolding all_clss_lf_ran_m[symmetric] image_mset_union by auto
subgoal using atm_confl TT' unfolding all_clss_lf_ran_m[symmetric] image_mset_union
by (fastforce simp: S' T' dest!: in_atms_of_minusD)
subgoal by auto
subgoal by auto
subgoal using dist LL' by (auto simp: U' S' distinct_mset_remove1_All)
subgoal by auto
apply (rule corr)
done
done
qed
have propagate_unit_bt_wl: ‹(propagate_unit_bt_wl (lit_of (hd (get_trail_wl S'))) U',
propagate_unit_bt_l (lit_of (hd (get_trail_l S))) U)
∈ {(T', T). (T', T) ∈ state_wl_l None ∧ correct_watching T'} ›
(is ‹(_, _) ∈ ?propagate_unit_bt_wl _›)
if
SS': ‹(S', S) ∈ ?A› and
TT': ‹(T', T) ∈ ?extract S'› and
UU': ‹(U', U) ∈ ?find T'› and
bt: ‹backtrack_wl_inv S'›
for S' S T T' L L' U U' K'
proof -
obtain MS NS DS NES UES W where
S': ‹S' = (MS, NS, Some DS, NES, UES, {#}, W)›
using SS' UU' empty[OF bt] by (cases S'; cases ‹get_conflict_wl S'›) auto
then obtain DT where
T': ‹T' = (MS, NS, Some DT, NES, UES, {#}, W)› and
DT_DS: ‹DT ⊆# DS›
using TT' by (cases T'; cases ‹get_conflict_wl T'›) auto
have T: ‹T = (MS, NS, Some DT, NES, UES, {#}, {#})›
using TT' by (auto simp: S' T' state_wl_l_def)
obtain MU MU' where
U': ‹U' = (MU, NS, Some DT, NES, UES, {#}, W)› and
MU: ‹MS = MU' @ MU› and
U: ‹(U', U) ∈ state_wl_l None›
using UU' T' by (cases U') auto
have U: ‹U = (MU, NS, Some DT, NES, UES, {#}, {#})›
using UU' by (auto simp: U' state_wl_l_def)
obtain S1 S2 where
S1: ‹(S', S1) ∈ state_wl_l None› and
S2: ‹(S1, S2) ∈ twl_st_l None› and
struct_invs: ‹twl_struct_invs S2›
using bt unfolding backtrack_wl_inv_def backtrack_l_inv_def
by blast
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of S2)›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
then have K: ‹set_mset (all_lits_of_mm (mset `# ran_mf NS + NES + add_mset (the (Some DT)) UES)) =
set_mset (all_lits_of_mm (mset `# ran_mf NS + (NES + UES)))›
apply (subst all_clss_lf_ran_m[symmetric])+
apply (subst image_mset_union)+
using S1 S2 atms_of_subset_mset_mono[OF DT_DS]
by (fastforce simp: all_lits_of_mm_union all_lits_of_mm_add_mset state_wl_l_def
twl_st_l_def S' cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
mset_take_mset_drop_mset' in_all_lits_of_mm_ain_atms_of_iff
in_all_lits_of_m_ain_atms_of_iff)
then have K': ‹set_mset (all_lits_of_mm (mset `# ran_mf NS + (NES + add_mset (the (Some DT)) UES))) =
set_mset (all_lits_of_mm (mset `# ran_mf NS + (NES + UES)))›
by (auto simp: ac_simps)
have ‹correct_watching S'›
using SS' by fast
then have corr: ‹correct_watching (Propagated (- lit_of (hd MS)) 0 # MU, NS, None, NES,
add_mset (the (Some DT)) UES, unmark (hd MS), W)›
unfolding S' correct_watching.simps clause_to_update_def get_clauses_l.simps K
K' .
show ?thesis
unfolding propagate_unit_bt_wl_def propagate_unit_bt_l_def S' T' U U'
st_l_of_wl.simps get_trail_wl.simps list_of_mset_def
apply clarify
apply (refine_rcg)
subgoal using SS' by (auto simp: S' state_wl_l_def)
subgoal by (rule corr)
done
qed
show ?thesis
unfolding st_l_of_wl.simps get_trail_wl.simps list_of_mset_def
backtrack_wl_def backtrack_l_def
apply (refine_vcg find_decomp_wl find_lit_of_max_level_wl extract_shorter_conflict_wl
propagate_bt_wl propagate_unit_bt_wl;
remove_dummy_vars)
subgoal using backtrack_wl_inv_def by blast
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
subsubsection ‹Backtrack, Skip, Resolve or Decide›
definition cdcl_twl_o_prog_wl_pre where
‹cdcl_twl_o_prog_wl_pre S ⟷
(∃S'. (S, S') ∈ state_wl_l None ∧
correct_watching S ∧
cdcl_twl_o_prog_l_pre S')›
definition cdcl_twl_o_prog_wl :: ‹'v twl_st_wl ⇒ (bool × 'v twl_st_wl) nres› where
‹cdcl_twl_o_prog_wl S =
do {
ASSERT(cdcl_twl_o_prog_wl_pre S);
do {
if get_conflict_wl S = None
then decide_wl_or_skip S
else do {
if count_decided (get_trail_wl S) > 0
then do {
T ← skip_and_resolve_loop_wl S;
ASSERT(get_conflict_wl T ≠ None ∧ get_conflict_wl T ≠ Some {#});
U ← backtrack_wl T;
RETURN (False, U)
}
else do {RETURN (True, S)}
}
}
}
›
lemma cdcl_twl_o_prog_wl_spec:
‹(cdcl_twl_o_prog_wl, cdcl_twl_o_prog_l) ∈ {(S::'v twl_st_wl, S'::'v twl_st_l).
(S, S') ∈ state_wl_l None ∧
correct_watching S} →⇩f
⟨{((brk::bool, T::'v twl_st_wl), brk'::bool, T'::'v twl_st_l).
(T, T') ∈ state_wl_l None ∧
brk = brk' ∧
correct_watching T}⟩nres_rel›
(is ‹?o ∈ ?A →⇩f ⟨?B⟩ nres_rel›)
proof -
have find_unassigned_lit_wl: ‹find_unassigned_lit_wl S ≤ ⇓ Id (find_unassigned_lit_l S')›
if ‹(S, S') ∈ state_wl_l None›
for S :: ‹'v twl_st_wl› and S' :: ‹'v twl_st_l›
unfolding find_unassigned_lit_wl_def find_unassigned_lit_l_def
using that
by (cases S; cases S') (auto simp: state_wl_l_def)
have [iff]: ‹correct_watching (decide_lit_wl L S) ⟷ correct_watching S› for L S
by (cases S; auto simp: decide_lit_wl_def correct_watching.simps clause_to_update_def)
have [iff]: ‹(decide_lit_wl L S, decide_lit_l L S') ∈ state_wl_l None›
if ‹(S, S') ∈ state_wl_l None›
for L S S'
using that by (cases S; auto simp: decide_lit_wl_def decide_lit_l_def state_wl_l_def)
have option_id: ‹x = x' ⟹ (x,x') ∈ ⟨Id⟩option_rel› for x x' by auto
show cdcl_o: ‹?o ∈ ?A →⇩f
⟨{((brk::bool, T::'v twl_st_wl), brk'::bool, T'::'v twl_st_l).
(T, T') ∈ state_wl_l None ∧
brk = brk' ∧
correct_watching T}⟩nres_rel›
unfolding cdcl_twl_o_prog_wl_def cdcl_twl_o_prog_l_def decide_wl_or_skip_def
decide_l_or_skip_def fref_param1[symmetric]
apply (refine_vcg skip_and_resolve_loop_wl_spec["to_⇓"] backtrack_wl_spec["to_⇓"]
find_unassigned_lit_wl option_id)
subgoal unfolding cdcl_twl_o_prog_wl_pre_def by blast
subgoal by auto
subgoal unfolding decide_wl_or_skip_pre_def by blast
subgoal by (auto simp:)
subgoal unfolding decide_wl_or_skip_pre_def by auto
subgoal by auto
subgoal by (auto simp: )
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: )
subgoal by (auto simp: )
subgoal by auto
done
qed
subsubsection ‹Full Strategy›
definition cdcl_twl_stgy_prog_wl_inv :: ‹'v twl_st_wl ⇒ bool × 'v twl_st_wl ⇒ bool› where
‹cdcl_twl_stgy_prog_wl_inv S⇩0 ≡ λ(brk, T).
(∃ T' S⇩0'. (T, T') ∈ state_wl_l None ∧
(S⇩0, S⇩0') ∈ state_wl_l None ∧
cdcl_twl_stgy_prog_l_inv S⇩0' (brk, T'))›
definition cdcl_twl_stgy_prog_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹cdcl_twl_stgy_prog_wl S⇩0 =
do {
(brk, T) ← WHILE⇩T⇗cdcl_twl_stgy_prog_wl_inv S⇩0⇖
(λ(brk, _). ¬brk)
(λ(brk, S). do {
T ← unit_propagation_outer_loop_wl S;
cdcl_twl_o_prog_wl T
})
(False, S⇩0);
RETURN T
}›
theorem cdcl_twl_stgy_prog_wl_spec:
‹(cdcl_twl_stgy_prog_wl, cdcl_twl_stgy_prog_l) ∈ {(S::'v twl_st_wl, S').
(S, S') ∈ state_wl_l None ∧
correct_watching S} →
⟨state_wl_l None⟩nres_rel›
(is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›)
proof -
have H: ‹((False, S'), False, S) ∈ {((brk', T'), (brk, T)). (T', T) ∈ state_wl_l None ∧ brk' = brk ∧
correct_watching T'}›
if ‹(S', S) ∈ state_wl_l None› and
‹correct_watching S'›
for S' :: ‹'v twl_st_wl› and S :: ‹'v twl_st_l›
using that by auto
show ?thesis
unfolding cdcl_twl_stgy_prog_wl_def cdcl_twl_stgy_prog_l_def
apply (refine_rcg H unit_propagation_outer_loop_wl_spec[THEN fref_to_Down]
cdcl_twl_o_prog_wl_spec[THEN fref_to_Down])
subgoal for S' S by (cases S') auto
subgoal by auto
subgoal unfolding cdcl_twl_stgy_prog_wl_inv_def by blast
subgoal by auto
subgoal by auto
subgoal for S' S brk'T' brkT brk' T' by auto
subgoal by fast
subgoal by auto
done
qed
theorem cdcl_twl_stgy_prog_wl_spec':
‹(cdcl_twl_stgy_prog_wl, cdcl_twl_stgy_prog_l) ∈ {(S::'v twl_st_wl, S').
(S, S') ∈ state_wl_l None ∧ correct_watching S} →
⟨{(S::'v twl_st_wl, S').
(S, S') ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel›
(is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›)
proof -
have H: ‹((False, S'), False, S) ∈ {((brk', T'), (brk, T)). (T', T) ∈ state_wl_l None ∧ brk' = brk ∧
correct_watching T'}›
if ‹(S', S) ∈ state_wl_l None› and
‹correct_watching S'›
for S' :: ‹'v twl_st_wl› and S :: ‹'v twl_st_l›
using that by auto
thm unit_propagation_outer_loop_wl_spec[THEN fref_to_Down]
show ?thesis
unfolding cdcl_twl_stgy_prog_wl_def cdcl_twl_stgy_prog_l_def
apply (refine_rcg H unit_propagation_outer_loop_wl_spec[THEN fref_to_Down]
cdcl_twl_o_prog_wl_spec[THEN fref_to_Down])
subgoal for S' S by (cases S') auto
subgoal by auto
subgoal unfolding cdcl_twl_stgy_prog_wl_inv_def by blast
subgoal by auto
subgoal by auto
subgoal for S' S brk'T' brkT brk' T' by auto
subgoal by fast
subgoal by auto
done
qed
definition cdcl_twl_stgy_prog_wl_pre where
‹cdcl_twl_stgy_prog_wl_pre S U ⟷
(∃T. (S, T) ∈ state_wl_l None ∧ cdcl_twl_stgy_prog_l_pre T U ∧ correct_watching S)›
lemma cdcl_twl_stgy_prog_wl_spec_final:
assumes
‹cdcl_twl_stgy_prog_wl_pre S S'›
shows
‹cdcl_twl_stgy_prog_wl S ≤ ⇓ (state_wl_l None O twl_st_l None) (conclusive_TWL_run S')›
proof -
obtain T where T: ‹(S, T) ∈ state_wl_l None› ‹cdcl_twl_stgy_prog_l_pre T S'› ‹correct_watching S›
using assms unfolding cdcl_twl_stgy_prog_wl_pre_def by blast
show ?thesis
apply (rule order_trans[OF cdcl_twl_stgy_prog_wl_spec["to_⇓", of S T]])
subgoal using T by auto
subgoal
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule cdcl_twl_stgy_prog_l_spec_final[of _ S'])
subgoal using T by fast
subgoal unfolding conc_fun_chain by auto
done
done
qed
definition cdcl_twl_stgy_prog_break_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹cdcl_twl_stgy_prog_break_wl S⇩0 =
do {
b ← SPEC(λ_. True);
(b, brk, T) ← WHILE⇩T⇗λ(_, S). cdcl_twl_stgy_prog_wl_inv S⇩0 S⇖
(λ(b, brk, _). b ∧ ¬brk)
(λ(_, brk, S). do {
T ← unit_propagation_outer_loop_wl S;
T ← cdcl_twl_o_prog_wl T;
b ← SPEC(λ_. True);
RETURN (b, T)
})
(b, False, S⇩0);
if brk then RETURN T
else cdcl_twl_stgy_prog_wl T
}›
theorem cdcl_twl_stgy_prog_break_wl_spec':
‹(cdcl_twl_stgy_prog_break_wl, cdcl_twl_stgy_prog_break_l) ∈ {(S::'v twl_st_wl, S').
(S, S') ∈ state_wl_l None ∧ correct_watching S} →⇩f
⟨{(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel›
(is ‹?o ∈ ?A →⇩f ⟨?B⟩ nres_rel›)
proof -
have H: ‹((b', False, S'), b, False, S) ∈ {((b', brk', T'), (b, brk, T)).
(T', T) ∈ state_wl_l None ∧ brk' = brk ∧ b' = b ∧
correct_watching T'}›
if ‹(S', S) ∈ state_wl_l None› and
‹correct_watching S'› and
‹(b', b) ∈ bool_rel›
for S' :: ‹'v twl_st_wl› and S :: ‹'v twl_st_l› and b' b :: bool
using that by auto
show ?thesis
unfolding cdcl_twl_stgy_prog_break_wl_def cdcl_twl_stgy_prog_break_l_def fref_param1[symmetric]
apply (refine_rcg H unit_propagation_outer_loop_wl_spec[THEN fref_to_Down]
cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]
cdcl_twl_stgy_prog_wl_spec'[unfolded fref_param1, THEN fref_to_Down])
subgoal for S' S by (cases S') auto
subgoal by auto
subgoal unfolding cdcl_twl_stgy_prog_wl_inv_def by blast
subgoal by auto
subgoal by auto
subgoal for S' S brk'T' brkT brk' T' by auto
subgoal by fast
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by fast
subgoal by auto
done
qed
theorem cdcl_twl_stgy_prog_break_wl_spec:
‹(cdcl_twl_stgy_prog_break_wl, cdcl_twl_stgy_prog_break_l) ∈ {(S::'v twl_st_wl, S').
(S, S') ∈ state_wl_l None ∧
correct_watching S} →⇩f
⟨state_wl_l None⟩nres_rel›
(is ‹?o ∈ ?A →⇩f ⟨?B⟩ nres_rel›)
using cdcl_twl_stgy_prog_break_wl_spec'
apply -
apply (rule mem_set_trans)
prefer 2 apply assumption
apply (match_fun_rel, solves simp)
apply (match_fun_rel; solves auto)
done
lemma cdcl_twl_stgy_prog_break_wl_spec_final:
assumes
‹cdcl_twl_stgy_prog_wl_pre S S'›
shows
‹cdcl_twl_stgy_prog_break_wl S ≤ ⇓ (state_wl_l None O twl_st_l None) (conclusive_TWL_run S')›
proof -
obtain T where T: ‹(S, T) ∈ state_wl_l None› ‹cdcl_twl_stgy_prog_l_pre T S'› ‹correct_watching S›
using assms unfolding cdcl_twl_stgy_prog_wl_pre_def by blast
show ?thesis
apply (rule order_trans[OF cdcl_twl_stgy_prog_break_wl_spec[unfolded fref_param1[symmetric], "to_⇓", of S T]])
subgoal using T by auto
subgoal
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule cdcl_twl_stgy_prog_break_l_spec_final[of _ S'])
subgoal using T by fast
subgoal unfolding conc_fun_chain by auto
done
done
qed
end