theory Watched_Literals_Watch_List_Initialisation
imports Watched_Literals_Watch_List Watched_Literals_Initialisation
begin
subsection ‹Initialisation›
type_synonym 'v twl_st_wl_init' = ‹(('v, nat) ann_lits × 'v clauses_l ×
'v cconflict × 'v clauses × 'v clauses × 'v lit_queue_wl)›
type_synonym 'v twl_st_wl_init = ‹'v twl_st_wl_init' × 'v clauses›
type_synonym 'v twl_st_wl_init_full = ‹'v twl_st_wl × 'v clauses›
fun get_trail_init_wl :: ‹'v twl_st_wl_init ⇒ ('v, nat) ann_lit list› where
‹get_trail_init_wl ((M, _, _, _, _, _), _) = M›
fun get_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses_l› where
‹get_clauses_init_wl ((_, N, _, _, _, _), OC) = N›
fun get_conflict_init_wl :: ‹'v twl_st_wl_init ⇒ 'v cconflict› where
‹get_conflict_init_wl ((_, _, D, _, _, _), _) = D›
fun literals_to_update_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clause› where
‹literals_to_update_init_wl ((_, _, _, _, _, Q), _) = Q›
fun other_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses› where
‹other_clauses_init_wl ((_, _, _, _, _, _), OC) = OC›
fun add_empty_conflict_init_wl :: ‹'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where
add_empty_conflict_init_wl_def[simp del]:
‹add_empty_conflict_init_wl ((M, N, D, NE, UE, Q), OC) =
((M, N, Some {#}, NE, UE, {#}), add_mset {#} OC)›
fun propagate_unit_init_wl :: ‹'v literal ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where
propagate_unit_init_wl_def[simp del]:
‹propagate_unit_init_wl L ((M, N, D, NE, UE, Q), OC) =
((Propagated L 0 # M, N, D, add_mset {#L#} NE, UE, add_mset (-L) Q), OC)›
fun already_propagated_unit_init_wl :: ‹'v clause ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where
already_propagated_unit_init_wl_def[simp del]:
‹already_propagated_unit_init_wl C ((M, N, D, NE, UE, Q), OC) =
((M, N, D, add_mset C NE, UE, Q), OC)›
fun set_conflict_init_wl :: ‹'v literal ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where
set_conflict_init_wl_def[simp del]:
‹set_conflict_init_wl L ((M, N, _, NE, UE, Q), OC) =
((M, N, Some {#L#}, add_mset {#L#} NE, UE, {#}), OC)›
fun add_to_clauses_init_wl :: ‹'v clause_l ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init nres› where
add_to_clauses_init_wl_def[simp del]:
‹add_to_clauses_init_wl C ((M, N, D, NE, UE, Q), OC) = do {
i ← get_fresh_index N;
let b = (length C = 2);
RETURN ((M, fmupd i (C, True) N, D, NE, UE, Q), OC)
}›
definition init_dt_step_wl :: ‹'v clause_l ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init nres› where
‹init_dt_step_wl C S =
(case get_conflict_init_wl S of
None ⇒
if length C = 0
then RETURN (add_empty_conflict_init_wl S)
else if length C = 1
then
let L = hd C in
if undefined_lit (get_trail_init_wl S) L
then RETURN (propagate_unit_init_wl L S)
else if L ∈ lits_of_l (get_trail_init_wl S)
then RETURN (already_propagated_unit_init_wl (mset C) S)
else RETURN (set_conflict_init_wl L S)
else
add_to_clauses_init_wl C S
| Some D ⇒
RETURN (add_to_other_init C S))›
fun st_l_of_wl_init :: ‹'v twl_st_wl_init' ⇒ 'v twl_st_l› where
‹st_l_of_wl_init (M, N, D, NE, UE, Q) = (M, N, D, NE, UE, {#}, Q)›
definition state_wl_l_init' where
‹state_wl_l_init' = {(S ,S'). S' = st_l_of_wl_init S}›
definition init_dt_wl :: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init nres› where
‹init_dt_wl CS = nfoldli CS (λ_. True) init_dt_step_wl›
definition state_wl_l_init :: ‹('v twl_st_wl_init × 'v twl_st_l_init) set› where
‹state_wl_l_init = {(S, S'). (fst S, fst S') ∈ state_wl_l_init' ∧
other_clauses_init_wl S = other_clauses_l_init S'}›
fun all_blits_are_in_problem_init where
[simp del]: ‹all_blits_are_in_problem_init (M, N, D, NE, UE, Q, W) ⟷
(∀L. (∀(i, K, b)∈#mset (W L). K ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE))))›
text ‹We assume that no clause has been deleted during initialisation. The definition is
slightly redundant since \<^term>‹i ∈# dom_m N› is already entailed by
\<^term>‹fst `# mset (W L) = clause_to_update L (M, N, D, NE, UE, {#}, {#})›.›
named_theorems twl_st_wl_init
lemma [twl_st_wl_init]:
assumes ‹(S, S') ∈ state_wl_l_init›
shows
‹get_conflict_l_init S' = get_conflict_init_wl S›
‹get_trail_l_init S' = get_trail_init_wl S›
‹other_clauses_l_init S' = other_clauses_init_wl S›
‹count_decided (get_trail_l_init S') = count_decided (get_trail_init_wl S)›
using assms
by (solves ‹cases S; cases S'; auto simp: state_wl_l_init_def state_wl_l_def
state_wl_l_init'_def›)+
lemma in_clause_to_update_in_dom_mD:
‹bb ∈# clause_to_update L (a, aa, ab, ac, ad, {#}, {#}) ⟹ bb ∈# dom_m aa›
unfolding clause_to_update_def
by force
lemma init_dt_step_wl_init_dt_step:
assumes S_S': ‹(S, S') ∈ state_wl_l_init› and
dist: ‹distinct C›
shows ‹init_dt_step_wl C S ≤ ⇓ state_wl_l_init
(init_dt_step C S')›
(is ‹_ ≤ ⇓ ?A _›)
proof -
have confl: ‹(get_conflict_init_wl S, get_conflict_l_init S') ∈ ⟨Id⟩option_rel›
using S_S' by (auto simp: twl_st_wl_init)
have false: ‹(add_empty_conflict_init_wl S, add_empty_conflict_init_l S') ∈ ?A›
using S_S'
apply (cases S; cases S')
apply (auto simp: add_empty_conflict_init_wl_def add_empty_conflict_init_l_def
all_blits_are_in_problem_init.simps state_wl_l_init'_def
state_wl_l_init_def state_wl_l_def correct_watching.simps clause_to_update_def)
done
have propa_unit:
‹(propagate_unit_init_wl (hd C) S, propagate_unit_init_l (hd C) S') ∈ ?A›
using S_S' apply (cases S; cases S')
apply (auto simp: propagate_unit_init_l_def propagate_unit_init_wl_def state_wl_l_init'_def
state_wl_l_init_def state_wl_l_def clause_to_update_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset all_lits_of_mm_union)
done
have already_propa:
‹(already_propagated_unit_init_wl (mset C) S, already_propagated_unit_init_l (mset C) S') ∈ ?A›
using S_S'
by (cases S; cases S')
(auto simp: already_propagated_unit_init_wl_def already_propagated_unit_init_l_def
state_wl_l_init_def state_wl_l_def clause_to_update_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset state_wl_l_init'_def)
have set_conflict: ‹(set_conflict_init_wl (hd C) S, set_conflict_init_l C S') ∈ ?A›
if ‹C = [hd C]›
using S_S' that
by (cases S; cases S')
(auto simp: set_conflict_init_wl_def set_conflict_init_l_def
state_wl_l_init_def state_wl_l_def clause_to_update_def state_wl_l_init'_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset)
have add_to_clauses_init_wl: ‹add_to_clauses_init_wl C S
≤ ⇓ state_wl_l_init
(add_to_clauses_init_l C S')›
if C: ‹length C ≥ 2› and conf: ‹get_conflict_l_init S' = None›
proof -
have [iff]: ‹C ! Suc 0 ∉ set (watched_l C) ⟷ False›
‹C ! 0 ∉ set (watched_l C) ⟷ False› and
[dest!]: ‹⋀L. L ≠ C ! 0 ⟹ L ≠ C ! Suc 0 ⟹ L ∈ set (watched_l C) ⟹ False›
using C by (cases C; cases ‹tl C›; auto)+
have [dest!]: ‹C ! 0 = C ! Suc 0 ⟹ False›
using C dist by (cases C; cases ‹tl C›; auto)+
show ?thesis
using S_S' conf C
by (cases S; cases S')
(auto 5 5 simp: add_to_clauses_init_wl_def add_to_clauses_init_l_def get_fresh_index_def
state_wl_l_init_def state_wl_l_def clause_to_update_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset state_wl_l_init'_def
RES_RETURN_RES Let_def
intro!: RES_refine filter_mset_cong2)
qed
have add_to_other_init:
‹(add_to_other_init C S, add_to_other_init C S') ∈ ?A›
using S_S'
by (cases S; cases S')
(auto simp: state_wl_l_init_def state_wl_l_def clause_to_update_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset state_wl_l_init'_def)
show ?thesis
unfolding init_dt_step_wl_def init_dt_step_def
apply (refine_vcg confl false propa_unit already_propa set_conflict
add_to_clauses_init_wl add_to_other_init)
subgoal by simp
subgoal by simp
subgoal using S_S' by (simp add: twl_st_wl_init)
subgoal using S_S' by (simp add: twl_st_wl_init)
subgoal using S_S' by (cases C) simp_all
subgoal by linarith
done
qed
lemma init_dt_wl_init_dt:
assumes S_S': ‹(S, S') ∈ state_wl_l_init› and
dist: ‹∀C∈set C. distinct C›
shows ‹init_dt_wl C S ≤ ⇓ state_wl_l_init
(init_dt C S')›
proof -
have C: ‹(C, C) ∈ ⟨{(C, C'). (C, C') ∈ Id ∧ distinct C}⟩list_rel›
using dist
by (auto simp: list_rel_def list.rel_refl_strong)
show ?thesis
unfolding init_dt_wl_def init_dt_def
apply (refine_vcg C S_S')
subgoal using S_S' by fast
subgoal by (auto intro!: init_dt_step_wl_init_dt_step)
done
qed
definition init_dt_wl_pre where
‹init_dt_wl_pre C S ⟷
(∃S'. (S, S') ∈ state_wl_l_init ∧
init_dt_pre C S')›
definition init_dt_wl_spec where
‹init_dt_wl_spec C S T ⟷
(∃S' T'. (S, S') ∈ state_wl_l_init ∧ (T, T') ∈ state_wl_l_init ∧
init_dt_spec C S' T')›
lemma init_dt_wl_init_dt_wl_spec:
assumes ‹init_dt_wl_pre CS S›
shows ‹init_dt_wl CS S ≤ SPEC (init_dt_wl_spec CS S)›
proof -
obtain S' where
SS': ‹(S, S') ∈ state_wl_l_init› and
pre: ‹init_dt_pre CS S'›
using assms unfolding init_dt_wl_pre_def by blast
have dist: ‹∀C∈set CS. distinct C›
using pre unfolding init_dt_pre_def by blast
show ?thesis
apply (rule order.trans)
apply (rule init_dt_wl_init_dt[OF SS' dist])
apply (rule order.trans)
apply (rule ref_two_step')
apply (rule init_dt_full[OF pre])
apply (unfold conc_fun_SPEC)
apply (rule SPEC_rule)
apply normalize_goal+
using SS' pre unfolding init_dt_wl_spec_def
by blast
qed
fun correct_watching_init :: ‹'v twl_st_wl ⇒ bool› where
[simp del]: ‹correct_watching_init (M, N, D, NE, UE, Q, W) ⟷
all_blits_are_in_problem_init (M, N, D, NE, UE, Q, W) ∧
(∀L.
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)) ∧
fst `# mset (W L) = clause_to_update L (M, N, D, NE, UE, {#}, {#}))›
lemma correct_watching_init_correct_watching:
‹correct_watching_init T ⟹ correct_watching T›
by (cases T)
(fastforce simp: correct_watching.simps correct_watching_init.simps filter_mset_eq_conv
all_blits_are_in_problem_init.simps
in_clause_to_update_in_dom_mD)
lemma image_mset_Suc: ‹Suc `# {#C ∈# M. P C#} = {#C ∈# Suc `# M. P (C-1)#}›
by (induction M) auto
lemma correct_watching_init_add_unit:
assumes ‹correct_watching_init (M, N, D, NE, UE, Q, W)›
shows ‹correct_watching_init (M, N, D, add_mset C NE, UE, Q, W)›
proof -
have [intro!]: ‹(a, x) ∈ set (W L) ⟹ a ∈# dom_m N ⟹ b ∈ set (N ∝a) ⟹
b ∉# all_lits_of_mm {#mset (fst x). x ∈# ran_m N#} ⟹ b ∈# all_lits_of_mm NE›
for x b F a L
unfolding ran_m_def
by (auto dest!: multi_member_split simp: all_lits_of_mm_add_mset in_clause_in_all_lits_of_m)
show ?thesis
using assms
unfolding correct_watching_init.simps clause_to_update_def Ball_def
by (fastforce simp: correct_watching.simps all_lits_of_mm_add_mset
all_lits_of_m_add_mset Ball_def all_conj_distrib clause_to_update_def
all_blits_are_in_problem_init.simps all_lits_of_mm_union
dest!: )
qed
lemma correct_watching_init_propagate:
‹correct_watching_init ((L # M, N, D, NE, UE, Q, W)) ⟷
correct_watching_init ((M, N, D, NE, UE, Q, W))›
‹correct_watching_init ((M, N, D, NE, UE, add_mset C Q, W)) ⟷
correct_watching_init ((M, N, D, NE, UE, Q, W))›
unfolding correct_watching_init.simps clause_to_update_def Ball_def
by (auto simp: correct_watching.simps all_lits_of_mm_add_mset
all_lits_of_m_add_mset Ball_def all_conj_distrib clause_to_update_def
all_blits_are_in_problem_init.simps)
lemma all_blits_are_in_problem_cons[simp]:
‹all_blits_are_in_problem_init (Propagated L i # a, aa, ab, ac, ad, ae, b) ⟷
all_blits_are_in_problem_init (a, aa, ab, ac, ad, ae, b)›
‹all_blits_are_in_problem_init (Decided L # a, aa, ab, ac, ad, ae, b) ⟷
all_blits_are_in_problem_init (a, aa, ab, ac, ad, ae, b)›
‹all_blits_are_in_problem_init (a, aa, ab, ac, ad, add_mset L ae, b) ⟷
all_blits_are_in_problem_init (a, aa, ab, ac, ad, ae, b)›
‹NO_MATCH None y ⟹ all_blits_are_in_problem_init (a, aa, y, ac, ad, ae, b) ⟷
all_blits_are_in_problem_init (a, aa, None, ac, ad, ae, b)›
‹NO_MATCH {#} ae ⟹ all_blits_are_in_problem_init (a, aa, y, ac, ad, ae, b) ⟷
all_blits_are_in_problem_init (a, aa, y, ac, ad, {#}, b)›
by (auto simp: all_blits_are_in_problem_init.simps)
lemma correct_watching_init_cons[simp]:
‹NO_MATCH None y ⟹ correct_watching_init ((a, aa, y, ac, ad, ae, b)) ⟷
correct_watching_init ((a, aa, None, ac, ad, ae, b))›
‹NO_MATCH {#} ae ⟹ correct_watching_init ((a, aa, y, ac, ad, ae, b)) ⟷
correct_watching_init ((a, aa, y, ac, ad, {#}, b))›
apply (auto simp: correct_watching_init.simps clause_to_update_def)
apply (subst (asm) all_blits_are_in_problem_cons(4))
apply auto
apply (subst all_blits_are_in_problem_cons(4))
apply auto
apply (subst (asm) all_blits_are_in_problem_cons(5))
apply auto
apply (subst all_blits_are_in_problem_cons(5))
apply auto
done
lemma clause_to_update_mapsto_upd_notin:
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 (clause_to_update L (M, N, C, NE, UE, WS, Q))
else (clause_to_update L (M, N, C, NE, UE, WS, Q)))›
‹clause_to_update L (M, fmupd i (C', b) N, C, NE, UE, WS, Q) =
(if L ∈ set (watched_l C')
then add_mset i (clause_to_update L (M, N, C, NE, UE, WS, Q))
else (clause_to_update L (M, N, C, NE, UE, WS, Q)))›
using assms
by (auto simp: clause_to_update_def intro!: filter_mset_cong)
lemma correct_watching_init_add_clause:
assumes
corr: ‹correct_watching_init ((a, aa, None, ac, ad, Q, b))› and
leC: ‹2 ≤ length C› and
i_notin[simp]: ‹i ∉# dom_m aa› and
dist[iff]: ‹C ! 0 ≠ C ! Suc 0›
shows ‹correct_watching_init
((a, fmupd i (C, red) aa, None, ac, ad, Q, b
(C ! 0 := b (C ! 0) @ [(i, C ! Suc 0, length C = 2)],
C ! Suc 0 := b (C ! Suc 0) @ [(i, C ! 0, length C = 2)])))›
proof -
have [iff]: ‹C ! Suc 0 ≠ C ! 0›
using ‹C ! 0 ≠ C ! Suc 0› by argo
have [iff]: ‹C ! Suc 0 ∈# all_lits_of_m (mset C)› ‹C ! 0 ∈# all_lits_of_m (mset C)›
‹C ! Suc 0 ∈ set C› ‹ C ! 0 ∈ set C› ‹C ! 0 ∈ set (watched_l C)› ‹C ! Suc 0 ∈ set (watched_l C)›
using leC by (force intro!: in_clause_in_all_lits_of_m nth_mem simp: in_set_conv_iff
intro: exI[of _ 0] exI[of _ ‹Suc 0›])+
have [dest!]: ‹⋀L. L ≠ C ! 0 ⟹ L ≠ C ! Suc 0 ⟹ L ∈ set (watched_l C) ⟹ False›
by (cases C; cases ‹tl C›; auto)+
have i: ‹i ∉ fst ` set (b L)› for L
using corr i_notin unfolding correct_watching_init.simps
by force
have [iff]: ‹(i,c, d) ∉ set (b L)› for L c d
using i[of L] by (auto simp: image_iff)
then show ?thesis
using corr
by (force simp: correct_watching_init.simps all_blits_are_in_problem_init.simps ran_m_mapsto_upd_notin
all_lits_of_mm_add_mset all_lits_of_mm_union clause_to_update_mapsto_upd_notin correctly_marked_as_binary.simps
split: if_splits)
qed
definition rewatch
:: ‹'v clauses_l ⇒ ('v literal ⇒ 'v watched) ⇒ ('v literal ⇒ 'v watched) nres›
where
‹rewatch N W = do {
xs ← SPEC(λxs. set_mset (dom_m N) ⊆ set xs ∧ distinct xs);
nfoldli
xs
(λ_. True)
(λi W. do {
if i ∈# dom_m N
then do {
ASSERT(i ∈# dom_m N);
ASSERT(length (N ∝ i) ≥ 2);
let L1 = N ∝ i ! 0;
let L2 = N ∝ i ! 1;
let b = (length (N ∝ i) = 2);
ASSERT(L1 ≠ L2);
ASSERT(length (W L1) < size (dom_m N));
let W = W(L1 := W L1 @ [(i, L2, b)]);
ASSERT(length (W L2) < size (dom_m N));
let W = W(L2 := W L2 @ [(i, L1, b)]);
RETURN W
}
else RETURN W
})
W
}›
lemma rewatch_correctness:
assumes [simp]: ‹W = (λ_. [])› and
H[dest]: ‹⋀x. x ∈# dom_m N ⟹ distinct (N ∝ x) ∧ length (N ∝ x) ≥ 2›
shows
‹rewatch N W ≤ SPEC(λW. correct_watching_init (M, N, C, NE, UE, Q, W))›
proof -
define I where
‹I ≡ λ(a :: nat list) (b :: nat list) W.
correct_watching_init ((M, fmrestrict_set (set a) N, C, NE, UE, Q, W))›
have I0: ‹set_mset (dom_m N) ⊆ set x ∧ distinct x ⟹ I [] x W› for x
unfolding I_def by (auto simp: correct_watching_init.simps
all_blits_are_in_problem_init.simps clause_to_update_def)
have le: ‹length (σ L) < size (dom_m N)›
if ‹correct_watching_init (M, fmrestrict_set (set l1) N, C, NE, UE, Q, σ)› and
‹set_mset (dom_m N) ⊆ set x ∧ distinct x› and
‹x = l1 @ xa # l2› ‹xa ∈# dom_m N›
for L l1 σ xa l2 x
proof -
have 1: ‹card (set l1) ≤ length l1›
by (auto simp: card_length)
have ‹distinct_watched (σ L)› and ‹fst ` set (σ L) ⊆ set l1 ∩ set_mset (dom_m N)›
using that by (fastforce simp: correct_watching_init.simps dom_m_fmrestrict_set')+
then have ‹length (map fst (σ L)) ≤ card (set l1 ∩ set_mset (dom_m N))›
using 1 by (subst distinct_card[symmetric])
(auto simp: distinct_watched_alt_def intro!: card_mono intro: order_trans)
also have ‹... < card (set_mset (dom_m N))›
using that by (auto intro!: psubset_card_mono)
also have ‹... = size (dom_m N)›
by (simp add: distinct_mset_dom distinct_mset_size_eq_card)
finally show ?thesis by simp
qed
show ?thesis
unfolding rewatch_def
apply (refine_vcg
nfoldli_rule[where I = ‹I›])
subgoal by (rule I0)
subgoal using assms unfolding I_def by auto
subgoal for x xa l1 l2 σ using H[of xa] unfolding I_def apply -
by (rule, subst (asm)nth_eq_iff_index_eq)
linarith+
subgoal for x xa l1 l2 σ unfolding I_def by (rule le)
subgoal for x xa l1 l2 σ unfolding I_def by (drule le[where L = ‹N ∝ xa ! 1›]) (auto simp: I_def dest!: le)
subgoal for x xa l1 l2 σ
unfolding I_def
by (cases ‹the (fmlookup N xa)›)
(auto simp: dom_m_fmrestrict_set' intro!: correct_watching_init_add_clause)
subgoal
unfolding I_def by auto
subgoal by auto
subgoal unfolding I_def
by (auto simp: fmlookup_restrict_set_id')
done
qed
definition state_wl_l_init_full :: ‹('v twl_st_wl_init_full × 'v twl_st_l_init) set› where
‹state_wl_l_init_full = {(S, S'). (fst S, fst S') ∈ state_wl_l None ∧
snd S = snd S'}›
definition added_only_watched :: ‹('v twl_st_wl_init_full × 'v twl_st_wl_init) set› where
‹added_only_watched = {(((M, N, D, NE, UE, Q, W), OC), ((M', N', D', NE', UE', Q'), OC')).
(M, N, D, NE, UE, Q) = (M', N', D', NE', UE', Q') ∧ OC = OC'}›
definition init_dt_wl_spec_full
:: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init_full ⇒ bool›
where
‹init_dt_wl_spec_full C S T'' ⟷
(∃S' T T'. (S, S') ∈ state_wl_l_init ∧ (T :: 'v twl_st_wl_init, T') ∈ state_wl_l_init ∧
init_dt_spec C S' T' ∧ correct_watching_init (fst T'') ∧ (T'', T) ∈ added_only_watched)›
definition init_dt_wl_full :: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init_full nres› where
‹init_dt_wl_full CS S = do{
((M, N, D, NE, UE, Q), OC) ← init_dt_wl CS S;
W ← rewatch N (λ_. []);
RETURN ((M, N, D, NE, UE, Q, W), OC)
}›
lemma init_dt_wl_spec_rewatch_pre:
assumes ‹init_dt_wl_spec CS S T› and ‹N = get_clauses_init_wl T› and ‹C ∈# dom_m N›
shows ‹distinct (N ∝ C) ∧ length (N ∝ C) ≥ 2›
proof -
obtain x xa xb where
‹N = get_clauses_init_wl T› and
Sx: ‹(S, x) ∈ state_wl_l_init› and
Txa: ‹(T, xa) ∈ state_wl_l_init› and
xa_xb: ‹(xa, xb) ∈ twl_st_l_init› and
struct_invs: ‹twl_struct_invs_init xb› and
‹clauses_to_update_l_init xa = {#}› and
‹∀s∈set (get_trail_l_init xa). ¬ is_decided s› and
‹get_conflict_l_init xa = None ⟶
literals_to_update_l_init xa = uminus `# lit_of `# mset (get_trail_l_init xa)› and
‹mset `# mset CS + mset `# ran_mf (get_clauses_l_init x) + other_clauses_l_init x +
get_unit_clauses_l_init x =
mset `# ran_mf (get_clauses_l_init xa) + other_clauses_l_init xa +
get_unit_clauses_l_init xa› and
‹learned_clss_lf (get_clauses_l_init x) =
learned_clss_lf (get_clauses_l_init xa)› and
‹get_learned_unit_clauses_l_init xa = get_learned_unit_clauses_l_init x› and
‹twl_list_invs (fst xa)› and
‹twl_stgy_invs (fst xb)› and
‹other_clauses_l_init xa ≠ {#} ⟶ get_conflict_l_init xa ≠ None› and
‹{#} ∈# mset `# mset CS ⟶ get_conflict_l_init xa ≠ None› and
‹get_conflict_l_init x ≠ None ⟶ get_conflict_l_init x = get_conflict_l_init xa›
using assms
unfolding init_dt_wl_spec_def init_dt_spec_def apply -
by normalize_goal+ presburger
have ‹twl_st_inv (fst xb)›
using struct_invs unfolding twl_struct_invs_init_def by fast
then have ‹Multiset.Ball (get_clauses (fst xb)) struct_wf_twl_cls›
by (cases xb) (auto simp: twl_st_inv.simps)
with ‹C ∈# dom_m N› show ?thesis
using Txa xa_xb assms by (cases T; cases ‹fmlookup N C›; cases ‹snd (the(fmlookup N C))›)
(auto simp: state_wl_l_init_def twl_st_l_init_def conj_disj_distribR Collect_disj_eq
Collect_conv_if mset_take_mset_drop_mset'
state_wl_l_init'_def ran_m_def dest!: multi_member_split)
qed
lemma init_dt_wl_full_init_dt_wl_spec_full:
assumes ‹init_dt_wl_pre CS S›
shows ‹init_dt_wl_full CS S ≤ SPEC (init_dt_wl_spec_full CS S)›
proof -
show ?thesis
unfolding init_dt_wl_full_def
apply (rule specify_left)
apply (rule init_dt_wl_init_dt_wl_spec)
subgoal by (rule assms)
apply clarify
apply (rule specify_left)
apply (rule_tac M =a and N=aa and C=ab and NE=ac and UE=ad and Q=b in
rewatch_correctness[OF _ init_dt_wl_spec_rewatch_pre])
subgoal by rule
apply assumption
subgoal by simp
subgoal by simp
subgoal for a aa ab ac ad b ba W
using assms
unfolding init_dt_wl_spec_full_def init_dt_wl_pre_def init_dt_wl_spec_def
by (auto simp: added_only_watched_def state_wl_l_init_def state_wl_l_init'_def)
done
qed
end