Theory IsaSAT_Inner_Propagation
theory IsaSAT_Inner_Propagation
imports IsaSAT_Setup
IsaSAT_Clauses IsaSAT_VMTF IsaSAT_LBD
IsaSAT_Inner_Propagation_Defs
begin
chapter ‹Propagation: Inner Loop›
declare all_atms_def[symmetric,simp]
lemma map_fun_rel_def2:
‹⟨R⟩map_fun_rel (D⇩0 (all_atms_st u)) =
{(m, f). ∀(i, j)∈(λL. (nat_of_lit L, L)) ` set_mset (all_lits_st u). i < length m ∧ (m ! i, f j) ∈ R}›
unfolding map_fun_rel_def[of ‹D⇩0 (all_atms_st u)› R] unfolding all_lits_st_alt_def[symmetric] ..
section ‹Find replacement›
lemma literals_are_in_ℒ⇩i⇩n_nth2:
fixes C :: nat
assumes dom: ‹C ∈# dom_m (get_clauses_wl S)›
shows ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset (get_clauses_wl S ∝ C))›
proof -
let ?N = ‹get_clauses_wl S›
have ‹?N ∝ C ∈# ran_mf ?N›
using dom by (auto simp: ran_m_def)
then have ‹mset (?N ∝ C) ∈# mset `# (ran_mf ?N)›
by blast
from all_lits_of_m_subset_all_lits_of_mmD[OF this] show ?thesis
unfolding is_ℒ⇩a⇩l⇩l_def literals_are_in_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n_def
all_lits_st_alt_def[symmetric]
by (auto simp add: all_lits_st_def all_lits_of_mm_union all_lits_def)
qed
lemma isa_find_unwatched_between_find_in_list_between_spec:
assumes ‹a ≤ length (N ∝ C)› and ‹b ≤ length (N ∝ C)› and ‹a ≤ b› and
‹valid_arena arena N vdom› and ‹C ∈# dom_m N› and eq: ‹a' = a› ‹b' = b› ‹C' = C› and
‹⋀L. L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ P' L = P L› and
M'M: ‹(M', M) ∈ trail_pol 𝒜›
assumes lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ C))›
shows
‹isa_find_unwatched_between P' M' arena a' b' C' ≤ ⇓ Id (find_in_list_between P a b (N ∝ C))›
proof -
have find_in_list_between_alt:
‹find_in_list_between P a b C = do {
(x, _) ← WHILE⇩T⇗λ(found, i). i ≥ a ∧ i ≤ length C ∧ i ≤ b ∧ (∀j∈{a..<i}. ¬P (C!j)) ∧
(∀j. found = Some j ⟶ (i = j ∧ P (C ! j) ∧ j < b ∧ j ≥ a))⇖
(λ(found, i). found = None ∧ i < b)
(λ(_, i). do {
ASSERT(i < length C);
let L = C!i;
if P L then RETURN (Some i, i) else RETURN (None, i+1)
})
(None, a);
RETURN x
}› for P a b c C
by (auto simp: find_in_list_between_def)
have [refine0]: ‹((None, x2m + a), None, a) ∈ ⟨Id⟩option_rel ×⇩r {(n', n). n' = x2m + n}›
for x2m
by auto
have [simp]: ‹arena_lit arena (C + x2) ∈# ℒ⇩a⇩l⇩l 𝒜› if ‹x2 < length (N ∝ C)› for x2
using that lits assms by (auto simp: arena_lifting
dest!: literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[of 𝒜 _ x2])
have arena_lit_pre: ‹arena_lit_pre arena x2a›
if
‹(x, x') ∈ ⟨nat_rel⟩option_rel ×⇩f {(n', n). n' = C + n}› and
‹case x of (found, i) ⇒ found = None ∧ i < C + b› and
‹case x' of (found, i) ⇒ found = None ∧ i < b› and
‹case x of (found, i) ⇒ True› and
‹case x' of
(found, i) ⇒
a ≤ i ∧
i ≤ length (N ∝ C) ∧
i ≤ b ∧
(∀j∈{a..<i}. ¬ P (N ∝ C ! j)) ∧
(∀j. found = Some j ⟶ i = j ∧ P (N ∝ C ! j) ∧ j < b ∧ a ≤ j)› and
‹x' = (x1, x2)› and
‹x = (x1a, x2a)› and
‹x2 < length (N ∝ C)› and
‹x2a < C + (arena_length arena C)› and
‹C ≤ x2a›
for x x' x1 x2 x1a x2a
proof -
show ?thesis
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
apply (rule bex_leI[of _ C])
apply (rule exI[of _ N])
apply (rule exI[of _ vdom])
using assms that by auto
qed
show ?thesis
unfolding isa_find_unwatched_between_def find_in_list_between_alt eq
apply (refine_vcg mop_arena_lit)
subgoal using assms by (auto dest!: arena_lifting(10))
subgoal using assms by (auto dest!: arena_lifting(10))
subgoal by auto
subgoal by auto
subgoal using assms by (auto simp: arena_lifting)
subgoal using assms by (auto simp: arena_lifting)
subgoal by auto
subgoal by (rule arena_lit_pre)
apply (rule assms)
subgoal using assms by (auto simp: arena_lifting)
subgoal using assms by (auto simp: arena_lifting)
subgoal
by (rule polarity_pol_pre[OF M'M]) (use assms in ‹auto simp: arena_lifting›)
subgoal using assms by (auto simp: arena_lifting)
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
definition isa_find_non_false_literal_between where
‹isa_find_non_false_literal_between M arena a b C =
isa_find_unwatched_between (λL. polarity_pol M L ≠ Some False) M arena a b C›
definition find_unwatched
:: ‹(nat literal ⇒ bool) ⇒ (nat, nat literal list × bool) fmap ⇒ nat ⇒ (nat option) nres› where
‹find_unwatched M N C = do {
ASSERT(C ∈# dom_m N);
b ← SPEC(λb::bool. True);
if b then find_in_list_between M 2 (length (N ∝ C)) (N ∝ C)
else do {
pos ← SPEC (λi. i ≤ length (N ∝ C) ∧ i ≥ 2);
n ← find_in_list_between M pos (length (N ∝ C)) (N ∝ C);
if n = None then find_in_list_between M 2 pos (N ∝ C)
else RETURN n
}
}
›
definition find_unwatched_wl_st_heur_pre where
‹find_unwatched_wl_st_heur_pre =
(λ(S, i). arena_is_valid_clause_idx (get_clauses_wl_heur S) i)›
definition find_unwatched_wl_st'
:: ‹nat twl_st_wl ⇒ nat ⇒ nat option nres› where
‹find_unwatched_wl_st' = (λ(M, N, D, Q, W, vm, φ) i. do {
find_unwatched (λL. polarity M L ≠ Some False) N i
})›
lemma find_unwatched_alt_def:
‹find_unwatched M N C = do {
ASSERT(C ∈# dom_m N);
_ ← RETURN(length (N ∝ C));
b ← SPEC(λb::bool. True);
if b then find_in_list_between M 2 (length (N ∝ C)) (N ∝ C)
else do {
pos ← SPEC (λi. i ≤ length (N ∝ C) ∧ i ≥ 2);
n ← find_in_list_between M pos (length (N ∝ C)) (N ∝ C);
if n = None then find_in_list_between M 2 pos (N ∝ C)
else RETURN n
}
}
›
unfolding find_unwatched_def by auto
lemma isa_find_unwatched_find_unwatched:
assumes valid: ‹valid_arena arena N vdom› and
‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ C))› and
ge2: ‹2 ≤ length (N ∝ C)› and
M'M: ‹(M', M) ∈ trail_pol 𝒜›
shows ‹isa_find_unwatched P M' arena C ≤ ⇓ Id (find_unwatched P N C)›
proof -
have [refine0]:
‹C ∈# dom_m N ⟹ (l, l') ∈ {(l, l'). (l, l') ∈ nat_rel ∧ l' = length (N ∝ C)} ⟹ RETURN(l ≤ MAX_LENGTH_SHORT_CLAUSE) ≤
⇓ {(b,b'). b = b' ∧ (b ⟷ is_short_clause (N∝C))}
(SPEC (λ_. True))›
for l l'
using assms
by (auto simp: RETURN_RES_refine_iff is_short_clause_def arena_lifting)
have [refine]: ‹C ∈# dom_m N ⟹ mop_arena_length arena C ≤ SPEC (λc. (c, length (N ∝ C)) ∈ {(l, l'). (l, l') ∈ nat_rel ∧ l' = length (N ∝ C)})›
using assms unfolding mop_arena_length_def
by refine_vcg (auto simp: arena_lifting arena_is_valid_clause_idx_def)
show ?thesis
unfolding isa_find_unwatched_def find_unwatched_alt_def
apply (refine_vcg isa_find_unwatched_between_find_in_list_between_spec[of _ _ _ _ _ vdom _ _ _ 𝒜 _ _ ])
apply assumption
subgoal by auto
subgoal using ge2 .
subgoal by auto
subgoal using ge2 .
subgoal using valid .
subgoal by fast
subgoal using assms by (auto simp: arena_lifting)
subgoal using assms by auto
subgoal using assms by (auto simp: arena_lifting)
apply (rule M'M)
subgoal using assms by auto
subgoal using assms unfolding get_saved_pos_pre_def arena_is_valid_clause_idx_def
by (auto simp: arena_lifting)
subgoal using assms arena_lifting[OF valid] unfolding get_saved_pos_pre_def
mop_arena_pos_def
by (auto simp: arena_lifting arena_pos_def)
subgoal by (auto simp: arena_pos_def)
subgoal using assms arena_lifting[OF valid] by auto
subgoal using assms by auto
subgoal using assms arena_lifting[OF valid] by auto
subgoal using assms by auto
subgoal using assms by (auto simp: arena_lifting)
subgoal using assms by auto
subgoal using assms arena_lifting[OF valid] by auto
apply (rule M'M)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms arena_lifting[OF valid] by auto
subgoal by (auto simp: arena_pos_def)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
apply (rule M'M)
subgoal using assms by auto
done
qed
lemma find_unwatched:
assumes n_d: ‹no_dup M› and ‹length (N ∝ C) ≥ 2› and ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ C))›
shows ‹find_unwatched (λL. polarity M L ≠ Some False) N C ≤ ⇓ Id (find_unwatched_l M N C)›
proof -
have [refine0]: ‹find_in_list_between (λL. polarity M L ≠ Some False) 2 (length (N ∝ C)) (N ∝ C)
≤ SPEC
(λfound.
(found = None) = (∀L∈set (unwatched_l (N ∝ C) ). - L ∈ lits_of_l M) ∧
(∀j. found = Some j ⟶
j < length (N ∝ C) ∧
(undefined_lit M ((N ∝ C) ! j) ∨ (N ∝ C) ! j ∈ lits_of_l M) ∧ 2 ≤ j))›
proof -
show ?thesis
apply (rule order_trans)
apply (rule find_in_list_between_spec)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal
using n_d
by (auto simp add: polarity_def in_set_drop_conv_nth Ball_def
Decided_Propagated_in_iff_in_lits_of_l split: if_splits dest: no_dup_consistentD)
done
qed
have [refine0]: ‹find_in_list_between (λL. polarity M L ≠ Some False) xa (length (N ∝ C)) (N ∝ C)
≤ SPEC
(λn. (if n = None
then find_in_list_between (λL. polarity M L ≠ Some False) 2 xa (N ∝ C)
else RETURN n)
≤ SPEC
(λfound.
(found = None) =
(∀L∈set (unwatched_l (N ∝ C)). - L ∈ lits_of_l M) ∧
(∀j. found = Some j ⟶
j < length (N ∝ C) ∧
(undefined_lit M ((N ∝ C) ! j) ∨ (N ∝ C) ! j ∈ lits_of_l M) ∧
2 ≤ j)))›
if
‹xa ≤ length (N ∝ C) ∧ 2 ≤ xa›
for xa
proof -
show ?thesis
apply (rule order_trans)
apply (rule find_in_list_between_spec)
subgoal using that by auto
subgoal using assms by auto
subgoal using that by auto
subgoal
apply (rule SPEC_rule)
subgoal for x
apply (cases ‹x = None›; simp only: if_True if_False refl)
subgoal
apply (rule order_trans)
apply (rule find_in_list_between_spec)
subgoal using that by auto
subgoal using that by auto
subgoal using that by auto
subgoal
apply (rule SPEC_rule)
apply (intro impI conjI iffI ballI)
unfolding in_set_drop_conv_nth Ball_def
apply normalize_goal
subgoal for x L xaa
apply (cases ‹xaa ≥ xa›)
subgoal
using n_d
by (auto simp add: polarity_def Ball_def all_conj_distrib
Decided_Propagated_in_iff_in_lits_of_l split: if_splits dest: no_dup_consistentD)
subgoal
using n_d
by (auto simp add: polarity_def Ball_def all_conj_distrib
Decided_Propagated_in_iff_in_lits_of_l split: if_splits dest: no_dup_consistentD)
done
subgoal for x
using n_d that assms
apply (auto simp add: polarity_def Ball_def all_conj_distrib
Decided_Propagated_in_iff_in_lits_of_l split: if_splits dest: no_dup_consistentD,
force)
by (blast intro: dual_order.strict_trans1 dest: no_dup_consistentD)
subgoal
using n_d assms that
by (auto simp add: polarity_def Ball_def all_conj_distrib
Decided_Propagated_in_iff_in_lits_of_l
split: if_splits dest: no_dup_consistentD)
done
done
subgoal
using n_d that assms le_trans
by (auto simp add: polarity_def Ball_def all_conj_distrib in_set_drop_conv_nth
Decided_Propagated_in_iff_in_lits_of_l split: if_splits dest: no_dup_consistentD)
(use le_trans no_dup_consistentD in blast)+
done
done
done
qed
show ?thesis
unfolding find_unwatched_def find_unwatched_l_def
apply (refine_vcg)
subgoal by blast
subgoal by blast
subgoal by blast
done
qed
definition find_unwatched_wl_st_pre where
‹find_unwatched_wl_st_pre = (λ(S, i).
i ∈# dom_m (get_clauses_wl S) ∧ 2 ≤ length (get_clauses_wl S ∝ i) ∧
literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset (get_clauses_wl S ∝ i))
)›
theorem find_unwatched_wl_st_heur_find_unwatched_wl_s:
‹(uncurry isa_find_unwatched_wl_st_heur, uncurry find_unwatched_wl_st')
∈ [find_unwatched_wl_st_pre]⇩f
twl_st_heur ×⇩f nat_rel → ⟨Id⟩nres_rel›
proof -
have [refine0]: ‹((None, x2m + 2), None, 2) ∈ ⟨Id⟩option_rel ×⇩r {(n', n). n' = x2m + n}›
for x2m
by auto
have [refine0]:
‹(polarity M (arena_lit arena i'), polarity M' (N ∝ C' ! j)) ∈ ⟨Id⟩option_rel›
if ‹∃vdom. valid_arena arena N vdom› and
‹C' ∈# dom_m N› and
‹i' = C' + j ∧ j < length (N ∝ C')› and
‹M = M'›
for M arena i i' N j M' C'
using that by (auto simp: arena_lifting)
have [refine0]: ‹RETURN (arena_pos arena C) ≤ ⇓ {(pos, pos'). pos = pos' ∧ pos ≥ 2 ∧ pos ≤ length (N ∝ C)}
(SPEC (λi. i ≤ length (N ∝ C') ∧ 2 ≤ i))›
if valid: ‹valid_arena arena N vdom› and C: ‹C ∈# dom_m N› and ‹C = C'› and
‹is_long_clause (N ∝ C')›
for arena N vdom C C'
using that arena_lifting[OF valid C] by (auto simp: RETURN_RES_refine_iff
arena_pos_def)
have [refine0]:
‹RETURN (arena_length arena C ≤ MAX_LENGTH_SHORT_CLAUSE) ≤ ⇓ {(b, b'). b = b' ∧ (b ⟷ is_short_clause (N ∝ C))}
(SPEC(λ_. True))›
if valid: ‹valid_arena arena N vdom› and C: ‹C ∈# dom_m N›
for arena N vdom C
using that arena_lifting[OF valid C] by (auto simp: RETURN_RES_refine_iff is_short_clause_def)
have [refine0]:
‹C ∈# dom_m N ⟹ (l, l') ∈ {(l, l'). (l, l') ∈ nat_rel ∧ l' = length (N ∝ C)} ⟹ RETURN(l ≤ MAX_LENGTH_SHORT_CLAUSE) ≤
⇓ {(b,b'). b = b' ∧ (b ⟷ is_short_clause (N∝C))}
(SPEC (λ_. True))›
for l l' C N
by (auto simp: RETURN_RES_refine_iff is_short_clause_def arena_lifting)
have [refine]: ‹C ∈# dom_m N ⟹ valid_arena arena N vdom ⟹
mop_arena_length arena C ≤ SPEC (λc. (c, length (N ∝ C)) ∈ {(l, l'). (l, l') ∈ nat_rel ∧ l' = length (N ∝ C)})›
for N C arena vdom
unfolding mop_arena_length_def
by refine_vcg (auto simp: arena_lifting arena_is_valid_clause_idx_def)
have H: ‹isa_find_unwatched P M' arena C ≤ ⇓ Id (find_unwatched P' N C')›
if ‹valid_arena arena N vdom›
‹⋀L. L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ P L = P' L› and
‹C = C'› and
‹2 ≤ length (N ∝ C')› and ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ C'))› and
‹(M', M) ∈ trail_pol 𝒜›
for arena P N C vdom P' C' 𝒜 M' M
using that unfolding isa_find_unwatched_def find_unwatched_alt_def supply [[goals_limit=1]]
apply (refine_vcg isa_find_unwatched_between_find_in_list_between_spec[of _ _ _ _ _ vdom, where 𝒜=𝒜])
unfolding that apply assumption+
subgoal by simp
subgoal by auto
subgoal using that by (simp add: arena_lifting)
subgoal using that by auto
subgoal using that by (auto simp: arena_lifting)
apply assumption
subgoal using that by (auto simp: arena_lifting get_saved_pos_pre_def
arena_is_valid_clause_idx_def)
subgoal using arena_lifting[OF ‹valid_arena arena N vdom›] unfolding get_saved_pos_pre_def
mop_arena_pos_def
by (auto simp: arena_lifting arena_pos_def)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
apply assumption
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
subgoal using that by (auto simp: arena_lifting)
apply assumption
done
show ?thesis
unfolding isa_find_unwatched_wl_st_heur_def find_unwatched_wl_st'_def
uncurry_def twl_st_heur_def
find_unwatched_wl_st_pre_def
apply (intro frefI nres_relI)
apply refine_vcg
subgoal for x y
apply (case_tac x, case_tac y)
by (rule H[where 𝒜3 = ‹all_atms_st (fst y)›, of _ _ ‹set (get_vdom (fst x))›])
(auto simp: polarity_pol_polarity[of ‹all_atms_st (fst y)›,
unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id]
all_atms_def[symmetric] literals_are_in_ℒ⇩i⇩n_nth2)
done
qed
lemma isa_save_pos_is_Id:
assumes
‹(S, T) ∈ twl_st_heur›
‹C ∈# dom_m (get_clauses_wl T)› and
‹i ≤ length (get_clauses_wl T ∝ C)› and
‹i ≥ 2›
shows ‹isa_save_pos C i S ≤ ⇓ {(S', T'). (S', T') ∈ twl_st_heur ∧ length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S) ∧
get_watched_wl_heur S' = get_watched_wl_heur S ∧ get_vdom S' = get_vdom S ∧ get_learned_count S' = get_learned_count S}
(RETURN T)›
proof -
have ‹isa_update_pos_pre ((C, i), get_clauses_wl_heur S)› if ‹is_long_clause (get_clauses_wl T ∝ C)›
unfolding isa_update_pos_pre_def
using assms that
by (cases S; cases T)
(auto simp: isa_save_pos_def twl_st_heur_def arena_update_pos_alt_def
isa_update_pos_pre_def arena_is_valid_clause_idx_def arena_lifting)
then show ?thesis
using assms
by (cases S; cases T)
(auto simp: isa_save_pos_def twl_st_heur_def arena_update_pos_alt_def
isa_update_pos_pre_def arena_is_valid_clause_idx_def arena_lifting
intro!: valid_arena_update_pos ASSERT_leI)
qed
section ‹Updates›
lemma isa_vmtf_bump_to_rescore_also_reasons_cl_isa_vmtf:
assumes ‹(M,M')∈trail_pol 𝒜› ‹isasat_input_bounded 𝒜› and vm: ‹vm ∈ bump_heur 𝒜 M'› and
valid: ‹valid_arena N N' vd› and
C: ‹C ∈# dom_m N'› and
H:‹ ∀L∈set (N' ∝ C). L ∈# ℒ⇩a⇩l⇩l 𝒜›
‹∀L∈set (N' ∝ C).
∀C. Propagated (- L) C ∈ set M' ⟶
C ≠ 0 ⟶ C ∈# dom_m N' ∧ (∀C∈set [C..<C + arena_length N C]. arena_lit N C ∈# ℒ⇩a⇩l⇩l 𝒜)› and
bound: ‹isasat_input_bounded 𝒜›
shows
‹isa_vmtf_bump_to_rescore_also_reasons_cl M N C L vm ≤ RES (bump_heur 𝒜 M')›
proof -
show ?thesis
apply (rule order_trans)
apply (rule isa_vmtf_bump_to_rescore_also_reasons_cl_vmtf_mark_to_rescore_also_reasons_cl[
where 𝒜 = 𝒜,
THEN fref_to_Down_curry4,
of _ _ _ _ _ ‹M'› ‹N› C L vm])
subgoal using assms by auto
subgoal using assms by auto
subgoal
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule vmtf_mark_to_rescore_also_reasons_cl_spec[OF vm valid C bound H])
subgoal by (auto simp: conc_fun_RES)
done
done
qed
lemma mark_conflict_to_rescore:
assumes ‹(S,T)∈twl_st_heur_up'' 𝒟 r s K lcount›
‹set_conflict_wl_pre C T›
shows ‹mark_conflict_to_rescore C S ≤ SPEC(λS'. (S', T)∈ twl_st_heur_up'' 𝒟 r s K lcount)›
proof -
obtain U V b where
TU: ‹(T, U) ∈ state_wl_l b› and
C: ‹C ∈# dom_m (get_clauses_wl T)› and
list: ‹twl_list_invs U›
using assms(2) unfolding set_conflict_wl_pre_def set_conflict_l_pre_def apply -
apply normalize_goal+
by auto
have valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))› and
vm: ‹get_vmtf_heur S ∈ bump_heur (all_atms_st T) (get_trail_wl T)› and
bounded: ‹isasat_input_bounded (all_atms_st T)› and
trail: ‹ (get_trail_wl_heur S, get_trail_wl T) ∈ trail_pol (all_atms_st T)›
using assms unfolding arena_is_valid_clause_idx_def unfolding twl_st_heur'_def
twl_st_heur_def by auto
have H:‹ ∀L∈set (get_clauses_wl T ∝ C). L ∈# ℒ⇩a⇩l⇩l (all_atms_st T)›
‹∀L∈set (get_clauses_wl T ∝ C).
∀C. Propagated (- L) C ∈ set (get_trail_wl T) ⟶
C ≠ 0 ⟶ C ∈# dom_m (get_clauses_wl T) ∧ (∀C∈set [C..<C + arena_length (get_clauses_wl_heur S) C]. arena_lit (get_clauses_wl_heur S) C ∈# ℒ⇩a⇩l⇩l (all_atms_st T))›
subgoal
using valid C by (auto simp: arena_lifting in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
all_atms_st_def all_atms_def all_lits_def all_lits_of_mm_union ran_m_def all_lits_of_mm_add_mset image_Un
atm_of_all_lits_of_m(2)
dest!: multi_member_split[of C]
simp del: all_atms_def[symmetric])[]
apply (intro ballI allI)
subgoal for L D
apply (intro conjI ballI impI)
subgoal
using TU list by (auto simp: twl_list_invs_def dest!: spec[of _ ‹-L›] spec[of _ ‹D›])
subgoal for C
apply (subgoal_tac ‹C - D < length (get_clauses_wl T ∝ D)›)
using TU list arena_lifting(5)[OF valid, of D ‹C - D›,symmetric]
apply (auto simp: twl_list_invs_def dest!: spec[of _ ‹-L›] spec[of _ ‹D›])
using valid
apply (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
all_atms_st_def all_atms_def all_lits_def all_lits_of_mm_union ran_m_def all_lits_of_mm_add_mset image_Un
atm_of_all_lits_of_m(2) arena_lifting
dest!: multi_member_split[of D] spec[of _ ‹-L›] spec[of _ ‹D›]
simp del: all_atms_def[symmetric])
apply (metis (no_types, opaque_lifting) ‹⟦D ∈# dom_m (get_clauses_wl T); C - D < length (get_clauses_wl T ∝ D)⟧ ⟹ arena_lit (get_clauses_wl_heur S) (D + (C - D)) = get_clauses_wl T ∝ D ! (C - D)› add.commute add.right_neutral add_diff_inverse_nat arena_lifting(4) imageI less_diff_conv2 less_nat_zero_code member_add_mset nth_mem)
apply (metis (no_types, opaque_lifting) ‹⟦D ∈# dom_m (get_clauses_wl T); C - D < length (get_clauses_wl T ∝ D)⟧ ⟹ arena_lit (get_clauses_wl_heur S) (D + (C - D)) = get_clauses_wl T ∝ D ! (C - D)› add.commute add.right_neutral add_diff_inverse_nat arena_lifting(4) imageI less_diff_conv2 less_nat_zero_code member_add_mset nth_mem)
done
done
done
have H': ‹literals_are_in_ℒ⇩i⇩n (all_atms_st T) (mset (get_clauses_wl T ∝ C))›
by (simp add: C literals_are_in_ℒ⇩i⇩n_nth2)
show ?thesis
unfolding mark_conflict_to_rescore_def mop_arena_length_def nres_monad3 mop_arena_lit2_def
apply (refine_vcg WHILET_rule[where Φ = ‹λ(i,vm). vm ∈ bump_heur (all_atms_st T) (get_trail_wl T)› and
I = ‹λ(i,vm). i ≤ length (get_clauses_wl T ∝ C) ∧ vm ∈ bump_heur (all_atms_st T) (get_trail_wl T)› and
R = ‹measure (λ(i,vm). length (get_clauses_wl T ∝ C) -i)›] trail bounded valid
isa_vmtf_bump_to_rescore_also_reasons_cl_isa_vmtf[THEN order_trans]
calculate_LBD_heur_st_calculate_LBD_st[where
vdom = ‹set (get_vdom (S))› and 𝒜 = ‹all_atms_st T› and C'=C, unfolded calculate_LBD_st_def conc_fun_RES RETURN_def, THEN order_trans])
subgoal using C valid unfolding arena_is_valid_clause_idx_def by auto
subgoal using valid C arena_lifting(7)[OF valid C, of ‹length (get_clauses_wl T ∝ C) - 1›] by (auto simp: arena_lifting)
subgoal by auto
subgoal by auto
subgoal using vm by auto
subgoal by auto
subgoal using valid C by (auto simp:arena_lifting arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def intro!: exI[of _ C] exI[of _ ‹get_clauses_wl T›])
subgoal by auto
subgoal using C by auto
subgoal by (rule H)
subgoal by (rule H)
subgoal using valid C by (auto simp: arena_lifting)
subgoal by auto
subgoal using valid C by (auto simp: arena_lifting)
subgoal by auto
subgoal using C by auto
subgoal by (rule H')
subgoal by auto
subgoal using assms unfolding twl_st_heur'_def twl_st_heur_def by auto
done
qed
definition set_conflict_wl_heur_pre where
‹set_conflict_wl_heur_pre =
(λ(C, S). True)›
definition update_clause_wl_pre where
‹update_clause_wl_pre K r = (λ((((((((L, L'), C), b), j), w), i), f), S).
L = K)›
lemma arena_lit_pre:
‹valid_arena NU N vdom ⟹ C ∈# dom_m N ⟹ i < length (N ∝ C) ⟹ arena_lit_pre NU (C + i)›
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by (rule bex_leI[of _ C], rule exI[of _ N], rule exI[of _ vdom]) auto
lemma all_atms_swap[simp]:
‹C ∈# dom_m N ⟹ i < length (N ∝ C) ⟹ j < length (N ∝ C) ⟹
all_atms (N(C ↪ swap (N ∝ C) i j)
) = all_atms N›
unfolding all_atms_def
by (auto simp del: all_atms_def[symmetric] simp: all_atms_def intro!: ext)
lemma mop_arena_swap[mop_arena_lit]:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹(C, C') ∈ nat_rel› ‹(i, i') ∈ nat_rel› ‹(j, j') ∈ nat_rel›
shows
‹mop_arena_swap C i j arena ≤ ⇓{(N'', N'). valid_arena N'' N' vdom ∧ N'' = swap_lits C' i' j' arena
∧ N' = op_clauses_swap N C' i' j' ∧ all_atms N' = all_atms N ∧ i' < length (N ∝ C') ∧
j' < length (N ∝ C')} (mop_clauses_swap N C' i' j')›
using assms unfolding mop_clauses_swap_def mop_arena_swap_def swap_lits_pre_def
by refine_rcg
(auto simp: arena_lifting valid_arena_swap_lits op_clauses_swap_def)
lemma update_clause_wl_alt_def:
‹update_clause_wl = (λ(L::'v literal) L' C b j w i f (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
ASSERT(C ∈# dom_m N ∧ j ≤ w ∧ w < length (W L) ∧
correct_watching_except (Suc j) (Suc w) L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
ASSERT(L ∈# all_lits_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
ASSERT(L' ∈# all_lits_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
K' ← mop_clauses_at N C f;
ASSERT(K' ∈# all_lits_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ∧ L ≠ K');
N' ← mop_clauses_swap N C i f;
RETURN (j, w+1, (M, N', D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W(K' := W K' @ [(C, L, b)])))
})›
unfolding update_clause_wl_def by (auto intro!: ext bind_cong[OF refl] simp flip: all_lits_alt_def2)
lemma all_atms_st_simps[simp]:
‹all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W(K := WK)) =
all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
‹all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, add_mset K Q, W) =
all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
‹x1 ∈# dom_m x1aa ⟹ n < length (x1aa ∝ x1) ⟹ n' < length (x1aa ∝ x1) ⟹
all_atms_st (x1b, x1aa(x1 ↪ WB_More_Refinement_List.swap (x1aa ∝ x1) n n'), D, x1c, x1d, NEk, UEk, NS, US, N0, U0, x1e,
x2e) =
all_atms_st
(x1b, x1aa, D, x1c, x1d, NEk, UEk, NS, US, N0, U0, x1e,
x2e)›
‹all_atms_st (L # M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) =
all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
‹NO_MATCH {#} Q ⟹ all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) =
all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, W)›
‹NO_MATCH [] M ⟹ all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) =
all_atms_st ([], N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
‹NO_MATCH None D ⟹ all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) =
all_atms_st (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
‹all_atms_st (set_literals_to_update_wl WS S) = all_atms_st S›
by (cases S; auto simp: all_atms_st_def all_atms_def ran_m_clause_upd
image_mset_remove1_mset_if simp del: all_atms_def[symmetric]; fail)+
lemma update_clause_wl_heur_update_clause_wl:
‹(uncurry8 update_clause_wl_heur, uncurry8 (update_clause_wl)) ∈
[update_clause_wl_pre K r]⇩f
Id ×⇩f Id ×⇩f nat_rel ×⇩f bool_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K lcount⟩nres_rel›
unfolding update_clause_wl_heur_def update_clause_wl_alt_def uncurry_def
update_clause_wl_pre_def all_lits_of_all_atms_of all_lits_of_all_atms_of Let_def
apply (intro frefI nres_relI, case_tac x, case_tac y)
apply (refine_rcg)
apply (rule mop_arena_lit2')
subgoal by (auto 0 0 simp: update_clause_wl_heur_def update_clause_wl_def twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_pre_def arena_lifting arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def swap_lits_pre_def
intro!: ASSERT_refine_left valid_arena_swap_lits
intro!: bex_leI exI)
subgoal by auto
subgoal by auto
subgoal by
(auto 0 0 simp: update_clause_wl_heur_def update_clause_wl_def twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_pre_def arena_lifting arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def swap_lits_pre_def
intro!: ASSERT_refine_left valid_arena_swap_lits
intro!: bex_leI exI)
apply (rule_tac vdom= ‹set (get_vdom ((λ(((((((L,C),b),j),w),_),_),x). x) x))› in mop_arena_swap)
subgoal
by (auto 0 0 simp: twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_pre_def arena_lifting arena_lit_pre_def
intro!: ASSERT_refine_left valid_arena_swap_lits dest!: multi_member_split[of ‹arena_lit _ _›])
subgoal
by (auto 0 0 simp: twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_def arena_lifting arena_lit_pre_def
intro!: ASSERT_refine_left valid_arena_swap_lits dest!: multi_member_split[of ‹arena_lit _ _›])
subgoal
by (auto 0 0 simp: twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_def arena_lifting arena_lit_pre_def
intro!: ASSERT_refine_left valid_arena_swap_lits dest!: multi_member_split[of ‹arena_lit _ _›])
subgoal
by (auto 0 0 simp: twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_pre_def arena_lifting arena_lit_pre_def
intro!: ASSERT_refine_left valid_arena_swap_lits dest!: multi_member_split[of ‹arena_lit _ _›])
subgoal
by (auto simp: twl_st_heur_def Let_def add_mset_eq_add_mset all_lits_of_all_atms_of ac_simps
twl_st_heur'_def update_clause_wl_pre_def arena_lifting arena_lit_pre_def map_fun_rel_def2
dest: multi_member_split simp flip: all_lits_def all_lits_alt_def2
intro!: ASSERT_refine_left valid_arena_swap_lits)
subgoal for x y a b aa ba c d e f g h i j k l m n x1 x1a x1b x1c x1d x1e x1f x2 x2a x2b x2c x2d x2e x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m
x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x1t x1u x1v x1w x1x x1y x2s x2t x2u x2v x2w x2x x2y _ _ _ _ K' K'a N' N'a
by (auto dest!: length_watched_le2[of _ _ _ _ ‹b› 𝒟 r lcount K'a])
(simp_all add: twl_st_heur'_def twl_st_heur_def map_fun_rel_def2)
subgoal
by
(clarsimp simp: twl_st_heur_def Let_def
map_fun_rel_def2 twl_st_heur'_def update_clause_wl_pre_def
op_clauses_swap_def)
done
definition propagate_lit_wl_heur_pre where
‹propagate_lit_wl_heur_pre =
(λ((L, C), S). C ≠ DECISION_REASON)›
definition propagate_lit_wl_pre where
‹propagate_lit_wl_pre = (λ(((L, C), i), S).
undefined_lit (get_trail_wl S) L ∧ get_conflict_wl S = None ∧
C ∈# dom_m (get_clauses_wl S) ∧ L ∈# all_lits_st S ∧
1 - i < length (get_clauses_wl S ∝ C) ∧
0 < length (get_clauses_wl S ∝ C))›
lemma propagate_lit_wl_heur_propagate_lit_wl:
‹(uncurry3 propagate_lit_wl_heur, uncurry3 (propagate_lit_wl)) ∈
[λ_. True]⇩f
Id ×⇩f nat_rel ×⇩f nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount → ⟨twl_st_heur_up'' 𝒟 r s K lcount⟩nres_rel›
supply [[goals_limit=1]]
unfolding propagate_lit_wl_heur_def propagate_lit_wl_def Let_def
apply (intro frefI nres_relI) unfolding uncurry_def mop_save_phase_heur_def
nres_monad3
apply (refine_rcg)
subgoal by auto
apply (rule_tac 𝒜 = ‹all_atms_st (snd y)› in cons_trail_Propagated_tr2)
subgoal by (auto 4 3 simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def atms_of_def save_phase_def
ac_simps
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal
by (auto simp: twl_st_heur_def twl_st_heur'_def all_lits_st_alt_def[symmetric]
ac_simps)
subgoal by (auto 4 3 simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def atms_of_def save_phase_def
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
apply (rule_tac vdom = ‹set (get_vdom (snd x))› in mop_arena_swap)
subgoal by (auto 4 3 simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def atms_of_def save_phase_def
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal by (auto 4 3 simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def atms_of_def save_phase_def
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal by (auto 4 3 simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def atms_of_def save_phase_def
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal by (auto simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def atms_of_def save_phase_def
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal by (auto simp: twl_st_heur_def propagate_lit_wl_heur_def propagate_lit_wl_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_pre_def swap_lits_pre_def
valid_arena_swap_lits arena_lifting phase_saving_def
all_lits_st_alt_def[symmetric] ac_simps
intro!: save_phase_heur_preI)
subgoal for x y
by (cases x; cases y; hypsubst)
(clarsimp simp add: twl_st_heur_def twl_st_heur'_def isa_vmtf_consD
op_clauses_swap_def ac_simps)
done
definition propagate_lit_wl_bin_pre where
‹propagate_lit_wl_bin_pre = (λ(((L, C), i), S).
undefined_lit (get_trail_wl S) L ∧ get_conflict_wl S = None ∧
C ∈# dom_m (get_clauses_wl S) ∧ L ∈# all_lits_st S)›
lemma propagate_lit_wl_bin_heur_propagate_lit_wl_bin:
‹(uncurry2 propagate_lit_wl_bin_heur, uncurry2 (propagate_lit_wl_bin)) ∈
[λ_. True]⇩f
nat_lit_lit_rel ×⇩f nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount → ⟨twl_st_heur_up'' 𝒟 r s K lcount⟩nres_rel›
supply [[goals_limit=1]]
unfolding propagate_lit_wl_bin_heur_def propagate_lit_wl_bin_def Let_def
apply (intro frefI nres_relI) unfolding uncurry_def mop_save_phase_heur_def nres_monad3
apply (refine_rcg)
apply (rule_tac 𝒜 = ‹all_atms_st (snd y)› in cons_trail_Propagated_tr2)
subgoal by (auto 4 3 simp: twl_st_heur_def propagate_lit_wl_bin_heur_def propagate_lit_wl_bin_def
isa_vmtf_consD twl_st_heur'_def propagate_lit_wl_bin_pre_def swap_lits_pre_def
arena_lifting phase_saving_def atms_of_def save_phase_def ℒ⇩a⇩l⇩l_all_atms_all_lits
all_lits_def ac_simps
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal by (auto 4 3 simp: twl_st_heur_def twl_st_heur'_def propagate_lit_wl_bin_pre_def swap_lits_pre_def
arena_lifting phase_saving_def atms_of_def save_phase_def all_lits_st_alt_def[symmetric]
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON
intro!: save_phase_heur_preI)
subgoal by (auto 4 3 simp: twl_st_heur_def twl_st_heur'_def propagate_lit_wl_bin_pre_def swap_lits_pre_def
arena_lifting phase_saving_def atms_of_def save_phase_def all_lits_st_alt_def[symmetric] ac_simps
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON)
subgoal by (auto 4 3 simp: twl_st_heur_def twl_st_heur'_def propagate_lit_wl_bin_pre_def swap_lits_pre_def
arena_lifting phase_saving_def atms_of_def save_phase_def all_lits_st_alt_def[symmetric]
intro!: ASSERT_refine_left cons_trail_Propagated_tr2 cons_trail_Propagated_tr_pre
dest: multi_member_split valid_arena_DECISION_REASON
intro!: save_phase_heur_preI)
subgoal for x y
by (cases x; cases y; hypsubst)
(clarsimp simp add: ac_simps twl_st_heur_def twl_st_heur'_def isa_vmtf_consD
op_clauses_swap_def)
done
lemma pos_of_watched_alt:
‹pos_of_watched N C L = do {
ASSERT(length (N ∝ C) > 0 ∧ C ∈# dom_m N);
let L' = (N ∝ C) ! 0;
RETURN (if L' = L then 0 else 1)
}›
unfolding pos_of_watched_def Let_def by auto
lemma pos_of_watched_heur:
‹(S, S') ∈ {(T, T'). get_vdom T = get_vdom x2e ∧ (T, T') ∈ twl_st_heur_up'' 𝒟 r s t lcount} ⟹
((C, L), (C', L')) ∈ Id ×⇩r Id ⟹
pos_of_watched_heur S C L ≤ ⇓ nat_rel (pos_of_watched (get_clauses_wl S') C' L')›
unfolding pos_of_watched_heur_def pos_of_watched_alt mop_access_lit_in_clauses_heur_def
by (refine_rcg mop_arena_lit[where vdom = ‹set (get_vdom S)›])
(auto simp: twl_st_heur'_def twl_st_heur_def)
lemma other_watched_heur:
‹(S, S') ∈ {(T, T'). get_vdom T = get_vdom x2e ∧ (T, T') ∈ twl_st_heur_up'' 𝒟 r s t lcount} ⟹
((L, C, i), (L', C', i')) ∈ Id ×⇩r Id ⟹
other_watched_wl_heur S L C i ≤ ⇓ Id (other_watched_wl S' L' C' i')›
using arena_lifting(5,7)[of ‹get_clauses_wl_heur S› ‹get_clauses_wl S'› _ C i]
unfolding other_watched_wl_heur_def other_watched_wl_def
mop_access_lit_in_clauses_heur_def
by (refine_rcg mop_arena_lit[where vdom = ‹set (get_vdom S)›])
(auto simp: twl_st_heur'_def twl_st_heur_def
arena_lit_pre2_def
intro!: exI[of _ ‹get_clauses_wl S'›])
section ‹Full inner loop›
declare RETURN_as_SPEC_refine[refine2 del]
definition set_conflict_wl'_pre where
‹set_conflict_wl'_pre i S ⟷
get_conflict_wl S = None ∧ i ∈# dom_m (get_clauses_wl S) ∧
literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf (get_clauses_wl S)) ∧
¬ tautology (mset (get_clauses_wl S ∝ i)) ∧
distinct (get_clauses_wl S ∝ i) ∧
literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) (get_trail_wl S)›
lemma literals_are_in_ℒ⇩i⇩n_mm_clauses[simp]: ‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf (get_clauses_wl S))›
‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) ((λx. mset (fst x)) `# ran_m (get_clauses_wl S))›
apply (auto simp: ℒ⇩a⇩l⇩l_all_atms_all_lits literals_are_in_ℒ⇩i⇩n_mm_def all_lits_st_alt_def[symmetric]
all_lits_st_def all_lits_def all_lits_of_mm_union)
done
lemma set_conflict_wl_alt_def:
‹set_conflict_wl = (λC S. do {
ASSERT(set_conflict_wl_pre C S);
let (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) = S;
let D = Some (mset (N ∝ C));
j ← RETURN (length M);
RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, W)
})›
unfolding set_conflict_wl_def Let_def by (auto simp: ac_simps)
lemma set_conflict_wl_pre_set_conflict_wl'_pre:
assumes ‹set_conflict_wl_pre C S›
shows ‹set_conflict_wl'_pre C S›
proof -
obtain S' T b b' where
SS': ‹(S, S') ∈ state_wl_l b› and
‹blits_in_ℒ⇩i⇩n S› and
confl: ‹get_conflict_l S'= None› and
dom: ‹C ∈# dom_m (get_clauses_l S')› and
tauto: ‹¬ tautology (mset (get_clauses_l S' ∝ C))› and
dist: ‹distinct (get_clauses_l S' ∝ C)› and
‹get_trail_l S' ⊨as CNot (mset (get_clauses_l S' ∝ C))› and
T: ‹(set_clauses_to_update_l (clauses_to_update_l S' + {#C#}) S', T)
∈ twl_st_l b'› and
struct: ‹twl_struct_invs T› and
‹twl_stgy_invs T›
using assms
unfolding set_conflict_wl_pre_def set_conflict_l_pre_def apply -
by blast
have lits_trail: ‹lits_of_l (get_trail T) ⊆ set_mset (all_lits_of_st T)›
using twl_struct_invs_no_alien_in_trail[OF struct] by auto
then have ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) (get_trail_wl S)›
using T SS'
by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_atm_of lits_of_def all_lits_st_alt_def)
then show ?thesis
using SS' T dom tauto dist confl unfolding set_conflict_wl'_pre_def
by (auto simp: literals_are_in_ℒ⇩i⇩n_def twl_st_l
mset_take_mset_drop_mset' simp del: all_atms_def[symmetric])
qed
lemma set_conflict_wl_heur_set_conflict_wl':
‹(uncurry set_conflict_wl_heur, uncurry (set_conflict_wl)) ∈
[λ_. True]⇩f
nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K lcount → ⟨twl_st_heur_up'' 𝒟 r s K lcount⟩nres_rel›
proof -
have H:
‹isa_set_lookup_conflict_aa x y z a b d
≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩f (nat_rel ×⇩f Id))
(set_conflict_m x' y' z' a' b' d')›
if
‹(((((((x, y), z), a), b)), d), (((((x', y'), z'), a'), b')), d')
∈ trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f
nat_rel ×⇩f
option_lookup_clause_rel 𝒜 ×⇩f
nat_rel ×⇩f Id› and
‹z' ∈# dom_m y' ∧ a' = None ∧ distinct (y' ∝ z') ∧
literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf y') ∧
¬ tautology (mset (y' ∝ z')) ∧ b' = 0 ∧ out_learned x' None d' ∧
isasat_input_bounded 𝒜›
for x x' y y' z z' a a' b b' c c' d d' vdom 𝒜
by (rule isa_set_lookup_conflict[THEN fref_to_Down_curry5,
unfolded prod.case, OF that(2,1)])
have [refine0]: ‹isa_set_lookup_conflict_aa (get_trail_wl_heur x2g) (get_clauses_wl_heur x2g) x1g
(get_conflict_wl_heur x2g) 0 (get_outlearned_heur x2g)
≤ ⇓ {((C, n, outl), D). (C, D) ∈ option_lookup_clause_rel (all_atms_st x2) ∧
n = card_max_lvl x1a (the D) ∧ out_learned x1a D outl}
(RETURN (Some (mset (x1b ∝ x1))))›
if
‹(x, y) ∈ nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount› and
‹x2i' = (x1j', x2j')› and
‹x2h' = (x1i', x2i')› and
‹x2g' = (x1h', x2h')› and
‹x2f = (x1g', x2g')› and
‹x2e = (x1f, x2f)› and
‹x2d = (x1e, x2e)› and
‹x2c = (x1d, x2d)› and
‹x2b = (x1c, x2c)› and
‹x2a = (x1b, x2b)› and
‹x2 = (x1a, x2a)› and
‹y = (x1, x2)› and
‹x = (x1g, S)› and
‹(x2g, x2) ∈ twl_st_heur_up'' 𝒟 r s K lcount›
‹case y of (x, xa) ⇒ set_conflict_wl'_pre x xa›
for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h
x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q x2q
x1r x2r x1s x2s x1t x2t x1g' x2g' x1h' x2h' x1i' x2i' x1j' x2j' S
proof -
have [iff]: ‹literals_are_in_ℒ⇩i⇩n_mm
(all_atms_st ([], x1b, None, x1d, x1e, x1f, xaa, af, ag, ah, ai, {#}, bb))
{#mset (fst x). x ∈# ran_m x1b#}› for xaa af ag ah ai bb
by (auto simp: literals_are_in_ℒ⇩i⇩n_mm_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n all_atms_st_def
in_all_lits_of_mm_ain_atms_of_iff all_atms_def all_lits_def
simp del: all_atms_def[symmetric])
show ?thesis
apply (rule order_trans)
apply (rule H[of _ _ _ _ _ _ x1a x1b x1g x1c 0 ‹get_outlearned_heur x2g› ‹all_atms_st x2›
‹set (get_vdom (x2g))›])
subgoal
using that
by (auto simp: twl_st_heur'_def twl_st_heur_def get_clauses_wl.simps ac_simps)
subgoal
using that apply auto
by (auto 0 0 simp add: RETURN_def conc_fun_RES set_conflict_m_def twl_st_heur'_def
twl_st_heur_def set_conflict_wl'_pre_def ac_simps)
subgoal
using that
by (auto 0 0 simp add: RETURN_def conc_fun_RES set_conflict_m_def twl_st_heur'_def
twl_st_heur_def)
done
qed
have isa_set_lookup_conflict_aa_pre:
‹(x, y) ∈ nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount ⟹
y = (x1, x2) ⟹
x = (x1a, x2a) ⟹
set_conflict_wl'_pre x1 x2 ⟹
(S, x2) ∈ twl_st_heur_up'' 𝒟 r s K lcount ⟹
curry2 (curry2 (curry isa_set_lookup_conflict_aa_pre)) (get_trail_wl_heur S)
(get_clauses_wl_heur S) x1a (get_conflict_wl_heur S) 0 (get_outlearned_heur S)›
for x1 x2 x1a x2a S y x
unfolding isa_set_lookup_conflict_aa_pre_def set_conflict_wl'_pre_def
twl_st_heur'_def twl_st_heur_def
by (auto simp: arena_lifting)
have set_conflict_wl_heur_alt_def: ‹set_conflict_wl_heur = (λC S. do {
let S = S;
let n = 0;
let M = get_trail_wl_heur S;
let N = get_clauses_wl_heur S;
let D = get_conflict_wl_heur S;
let outl = get_outlearned_heur S;
ASSERT(curry5 isa_set_lookup_conflict_aa_pre M N C D n outl);
(D, clvls, outl) ← isa_set_lookup_conflict_aa M N C D n outl;
j ← mop_isa_length_trail M;
let S = IsaSAT_Setup.set_conflict_wl_heur D S;
let S = set_outl_wl_heur outl S;
let S = set_count_max_wl_heur clvls S;
let S = set_literals_to_update_wl_heur j S;
RETURN S})›
unfolding set_conflict_wl_heur_def by auto
show ?thesis
supply [[goals_limit=1]]
apply (intro nres_relI frefI)
subgoal for x y
unfolding uncurry_def RES_RETURN_RES4 set_conflict_wl_alt_def set_conflict_wl_heur_alt_def
apply (rewrite at ‹let _ = 0 in _› Let_def)
apply (rewrite at ‹let _ = get_trail_wl_heur _ in _› Let_def)
apply (rewrite at ‹let _ = get_clauses_wl_heur _ in _› Let_def)
apply (rewrite at ‹let _ = get_conflict_wl_heur _ in _› Let_def)
apply (rewrite at ‹let _ = get_outlearned_heur _ in _› Let_def)
apply (refine_vcg mop_isa_length_trail_length_u[of ‹all_atms_st (snd y)›, THEN fref_to_Down_Id_keep, unfolded length_uint32_nat_def
comp_def] mark_conflict_to_rescore[where 𝒟 = 𝒟 and r=r and s=s and K=K and lcount=lcount, unfolded conc_fun_RETURN[symmetric]])
subgoal for x1 x2 x1a x2a
by (rule isa_set_lookup_conflict_aa_pre) (auto dest!: set_conflict_wl_pre_set_conflict_wl'_pre)
apply assumption+
subgoal by auto
subgoal by (auto dest!: set_conflict_wl_pre_set_conflict_wl'_pre)
subgoal for x y
unfolding arena_is_valid_clause_idx_def
by (auto simp: twl_st_heur'_def twl_st_heur_def)
subgoal
by (auto simp: twl_st_heur'_def twl_st_heur_def counts_maximum_level_def ac_simps
set_conflict_wl'_pre_def dest!: set_conflict_wl_pre_set_conflict_wl'_pre
intro!: valid_arena_mark_used)
done
done
qed
lemma in_Id_in_Id_option_rel[refine]:
‹(f, f') ∈ Id ⟹ (f, f') ∈ ⟨Id⟩ option_rel›
by auto
text ‹The assumption that that accessed clause is active has not been checked at this point!›
definition keep_watch_heur_pre where
‹keep_watch_heur_pre =
(λ(((L, j), w), S).
L ∈# ℒ⇩a⇩l⇩l (all_atms_st S))›
lemma vdom_m_update_subset':
‹fst C ∈ vdom_m 𝒜 bh N ⟹ vdom_m 𝒜 (bh(ap := (bh ap)[bf := C])) N ⊆ vdom_m 𝒜 bh N›
unfolding vdom_m_def
by (fastforce split: if_splits elim!: in_set_upd_cases)
lemma vdom_m_update_subset:
‹bg < length (bh ap) ⟹ vdom_m 𝒜 (bh(ap := (bh ap)[bf := bh ap ! bg])) N ⊆ vdom_m 𝒜 bh N›
unfolding vdom_m_def
by (fastforce split: if_splits elim!: in_set_upd_cases)
lemma keep_watch_heur_keep_watch:
‹(uncurry3 keep_watch_heur, uncurry3 (mop_keep_watch)) ∈
[λ_. True]⇩f
Id ×⇩f nat_rel ×⇩f nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount → ⟨twl_st_heur_up'' 𝒟 r s K lcount⟩ nres_rel›
unfolding keep_watch_heur_def mop_keep_watch_def uncurry_def
ℒ⇩a⇩l⇩l_all_atms_all_lits[symmetric]
apply (intro frefI nres_relI)
apply refine_rcg
subgoal
by (auto 5 4 simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def
intro!: ASSERT_leI
dest: vdom_m_update_subset)
subgoal
by (auto 5 4 simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def watched_by_alt_def
intro!: ASSERT_leI
dest: vdom_m_update_subset)
subgoal
by (auto 5 4 simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def watched_by_alt_def
intro!: ASSERT_leI
dest: vdom_m_update_subset)
subgoal
by (clarsimp simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def watched_by_alt_def
intro!: ASSERT_leI split: prod.splits)
(auto dest!: vdom_m_update_subset)
done
text ‹This is a slightly stronger version of the previous lemma:›
lemma keep_watch_heur_keep_watch':
‹((((L', j'), w'), S'), ((L, j), w), S)
∈ nat_lit_lit_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount ⟹
keep_watch_heur L' j' w' S' ≤ ⇓ {(T, T'). get_vdom T = get_vdom S' ∧
(T, T') ∈ twl_st_heur_up'' 𝒟 r s K lcount}
(mop_keep_watch L j w S)›
unfolding keep_watch_heur_def mop_keep_watch_def uncurry_def
ℒ⇩a⇩l⇩l_all_atms_all_lits[symmetric]
apply refine_rcg
subgoal
by (auto 5 4 simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def
intro!: ASSERT_leI
dest: vdom_m_update_subset)
subgoal
by (auto 5 4 simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def watched_by_alt_def
intro!: ASSERT_leI
dest: vdom_m_update_subset)
subgoal
by (auto 5 4 simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def watched_by_alt_def
intro!: ASSERT_leI
dest: vdom_m_update_subset)
subgoal
by (clarsimp simp: keep_watch_heur_def keep_watch_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 all_atms_def[symmetric] mop_keep_watch_def watched_by_alt_def
intro!: ASSERT_leI split: prod.splits
dest: vdom_m_update_subset)
(auto dest!: vdom_m_update_subset)
done
definition update_blit_wl_heur_pre where
‹update_blit_wl_heur_pre r K' = (λ((((((L, C), b), j), w), K), S). L = K')›
lemma update_blit_wl_heur_update_blit_wl:
‹(uncurry6 update_blit_wl_heur, uncurry6 update_blit_wl) ∈
[update_blit_wl_heur_pre r K]⇩f
nat_lit_lit_rel ×⇩f nat_rel ×⇩f bool_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f Id ×⇩f
twl_st_heur_up'' 𝒟 r s K lcount →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K lcount⟩ nres_rel›
apply (intro frefI nres_relI)
apply (auto simp: update_blit_wl_heur_def update_blit_wl_def twl_st_heur'_def keep_watch_heur_pre_def
twl_st_heur_def map_fun_rel_def2 update_blit_wl_heur_pre_def all_atms_def[symmetric]
ℒ⇩a⇩l⇩l_all_atms_all_lits
simp flip: all_lits_alt_def2
intro!: ASSERT_leI ASSERT_refine_right
simp: vdom_m_update_subset)
subgoal for aa ab ac ad ae be af ag ah bf aj ak al am an bg ao bh ap
apply (subgoal_tac ‹vdom_m (all_atms_st ([], ag, None, ah, bf, aj, ak, al, am, an, bg, {#}, ao)) (ao(K := (ao K)[ac := (aa, ae, ab)])) ag ⊆
vdom_m (all_atms_st ([], ag, None, ah, bf, aj, ak, al, am, an, bg, {#}, ao)) ao ag›)
apply fast
apply (rule vdom_m_update_subset')
apply auto
done
subgoal for aa ab ac ad ae be af ag ah bf aj ak al am an bg ao bh ap
apply (subgoal_tac ‹vdom_m (all_atms_st ([], ag, None, bf, aj, ak, al, am, an, bg, ao, {#}, bh)) (bh(K := (bh K)[ac := (aa, ae, ab)])) ag ⊆
vdom_m (all_atms_st ([], ag, None, bf, aj, ak, al, am, an, bg, ao, {#}, bh)) bh ag ›)
apply fast
apply (rule vdom_m_update_subset')
apply auto
done
done
lemma mop_access_lit_in_clauses_heur:
‹(S, T) ∈ twl_st_heur ⟹ (i, i') ∈ Id ⟹ (j, j') ∈ Id ⟹ mop_access_lit_in_clauses_heur S i j
≤ ⇓ Id
(mop_clauses_at (get_clauses_wl T) i' j')›
unfolding mop_access_lit_in_clauses_heur_def
by (rule mop_arena_lit2[where vdom=‹set (get_vdom S)›])
(auto simp: twl_st_heur_def intro!: mop_arena_lit2)
lemma isa_find_unwatched_wl_st_heur_find_unwatched_wl_st:
‹isa_find_unwatched_wl_st_heur x' y'
≤ ⇓ Id (find_unwatched_l (get_trail_wl x) (get_clauses_wl x) y)›
if
xy: ‹((x', y'), x, y) ∈ twl_st_heur ×⇩f nat_rel›
for x y x' y'
proof -
have find_unwatched_l_alt_def: ‹find_unwatched_l M N C = do {
ASSERT(C ∈# dom_m N ∧ length (N ∝ C) ≥ 2 ∧ distinct (N ∝ C) ∧ no_dup M);
find_unwatched_l M N C
}› for M N C
unfolding find_unwatched_l_def by (auto simp: summarize_ASSERT_conv)
have K: ‹find_unwatched_wl_st' x y ≤ find_unwatched_l (get_trail_wl x) (get_clauses_wl x) y›
unfolding find_unwatched_wl_st'_def
apply (subst find_unwatched_l_alt_def)
unfolding le_ASSERT_iff
apply (cases x)
apply clarify
apply (rule order_trans)
apply (rule find_unwatched[of _ _ _ ‹all_atms_st x›])
subgoal
by simp
subgoal
by auto
subgoal
using literals_are_in_ℒ⇩i⇩n_nth2[of y x]
by simp
subgoal by auto
done
show ?thesis
apply (subst find_unwatched_l_alt_def)
apply (intro ASSERT_refine_right)
apply (rule order_trans)
apply (rule find_unwatched_wl_st_heur_find_unwatched_wl_s[THEN fref_to_Down_curry,
OF _ that(1)])
by (simp_all add: K find_unwatched_wl_st_pre_def literals_are_in_ℒ⇩i⇩n_nth2)
qed
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));
(C, K, b) ← mop_watched_by_at S L w;
S ← mop_keep_watch L j w S;
ASSERT(is_nondeleted_clause_pre C L S);
val_K ← mop_polarity_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 do {S ← set_conflict_wl C S;
RETURN (j+1, w+1, S)}
else do {
S ← propagate_lit_wl_bin K C S;
RETURN (j+1, w+1, S)}
}
else if C ∉# dom_m (get_clauses_wl S)
then RETURN (j, w+1, S)
else do {
ASSERT(unit_prop_body_wl_inv S j w L);
i ← pos_of_watched (get_clauses_wl S) C L;
ASSERT(i ≤ 1);
L' ← other_watched_wl S L C i;
val_L' ← mop_polarity_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 {S ← set_conflict_wl C S;
RETURN (j+1, w+1, S)}
else do {S ← propagate_lit_wl L' C i S; RETURN (j+1, w+1, S)}
}
| Some f ⇒ do {
ASSERT(C ∈# dom_m (get_clauses_wl S) ∧ f < length (get_clauses_wl S ∝ C) ∧ f ≥ 2);
let S = S;
K ← mop_clauses_at (get_clauses_wl S) C f;
val_L' ← mop_polarity_wl S K;
if val_L' = Some True
then update_blit_wl L C b j w K S
else update_clause_wl L L' C b j w i f S
}
}
}
}
}›
unfolding unit_propagation_inner_loop_body_wl_def Let_def by auto
lemma fref_to_Down_curry8:
‹(uncurry8 ff, uncurry8 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z' a a' b b' c c' d d' e e' f f'. P ((((((((x', y'), z'), a'), b'), c'), d'), e'), f') ⟹
(((((((((x, y), z), a), b), c), d), e), f), ((((((((x', y'), z'), a'), b'), c'), d'), e'), f')) ∈ A ⟹
ff x y z a b c d e f ≤ ⇓ B (g x' y' z' a' b' c' d' e' f'))›
unfolding fref_def uncurry_def nres_rel_def by auto
lemma unit_propagation_inner_loop_body_wl_heur_unit_propagation_inner_loop_body_wl_D:
‹(uncurry3 unit_propagation_inner_loop_body_wl_heur,
uncurry3 unit_propagation_inner_loop_body_wl)
∈ [λ(((L, i), j), S). length (watched_by S L) ≤ r - MIN_HEADER_SIZE ∧ L = K ∧
length (watched_by S L) = s]⇩f
nat_lit_lit_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K lcount⟩nres_rel›
proof -
have [refine]: ‹clause_not_marked_to_delete_heur_pre (S', C')›
if ‹is_nondeleted_clause_pre C L S› and ‹((C', S'), (C, S)) ∈ nat_rel ×⇩r twl_st_heur› for C C' S S' L
using that apply -
unfolding clause_not_marked_to_delete_heur_pre_def prod.case arena_is_valid_clause_vdom_def
by (rule exI[of _ ‹get_clauses_wl S›], rule exI[of _ ‹set (get_vdom S')›])
(use that in ‹auto 5 3 simp: is_nondeleted_clause_pre_def twl_st_heur_def vdom_m_def watched_by_alt_def
simp flip: all_lits_st_alt_def dest!: multi_member_split[of L]›)
note [refine] = mop_watched_by_app_heur_mop_watched_by_at''[of 𝒟 r lcount K s, THEN fref_to_Down_curry2]
keep_watch_heur_keep_watch'[of _ _ _ _ _ _ _ _ 𝒟 r lcount K s]
mop_polarity_st_heur_mop_polarity_wl''[of 𝒟 r lcount K s, THEN fref_to_Down_curry, unfolded comp_def]
set_conflict_wl_heur_set_conflict_wl'[of 𝒟 r lcount K s, THEN fref_to_Down_curry, unfolded comp_def]
propagate_lit_wl_bin_heur_propagate_lit_wl_bin
[of 𝒟 r lcount K s, THEN fref_to_Down_curry2, unfolded comp_def]
pos_of_watched_heur[of _ _ _ 𝒟 r lcount K s]
mop_access_lit_in_clauses_heur
update_blit_wl_heur_update_blit_wl[of r K 𝒟 lcount s, THEN fref_to_Down_curry6]
isa_find_unwatched_wl_st_heur_find_unwatched_wl_st
propagate_lit_wl_heur_propagate_lit_wl[of 𝒟 r lcount K s, THEN fref_to_Down_curry3, unfolded comp_def]
isa_save_pos_is_Id
update_clause_wl_heur_update_clause_wl[of K r 𝒟 lcount s, THEN fref_to_Down_curry8]
other_watched_heur[of _ _ _ 𝒟 r lcount K s]
have [simp]: ‹is_nondeleted_clause_pre x1f x1b Sa ⟹
clause_not_marked_to_delete_pre (Sa, x1f)› for x1f x1b Sa
unfolding is_nondeleted_clause_pre_def clause_not_marked_to_delete_pre_def vdom_m_def
all_lits_st_alt_def[symmetric] by (cases Sa; auto dest!: multi_member_split)
show ?thesis
supply [[goals_limit=1]] twl_st_heur'_def[simp]
supply RETURN_as_SPEC_refine[refine2 del]
apply (intro frefI nres_relI)
unfolding unit_propagation_inner_loop_body_wl_heur_def
unit_propagation_inner_loop_body_wl_alt_def
uncurry_def clause_not_marked_to_delete_def[symmetric]
watched_by_app_heur_def access_lit_in_clauses_heur_def
apply (refine_rcg )
subgoal unfolding unit_propagation_inner_loop_wl_loop_D_heur_inv0_def twl_st_heur'_def
unit_propagation_inner_loop_wl_loop_pre_def
by fastforce
subgoal by fast
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by fast
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by fast
subgoal by simp
subgoal by simp
subgoal by fast
subgoal by simp
subgoal by simp
apply assumption
subgoal by auto
subgoal
unfolding Not_eq_iff
by (rule clause_not_marked_to_delete_rel[THEN fref_to_Down_unRET_Id_uncurry])
(simp_all add: clause_not_marked_to_delete_rel[THEN fref_to_Down_unRET_Id_uncurry])
subgoal by auto
apply assumption
subgoal by auto
subgoal by auto
apply assumption
subgoal by auto
subgoal by fast
subgoal by simp
subgoal by simp
subgoal
unfolding update_blit_wl_heur_pre_def unit_propagation_inner_loop_wl_loop_D_heur_inv0_def
prod.case unit_propagation_inner_loop_wl_loop_pre_def
by normalize_goal+ simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by force
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by (simp add: clause_not_marked_to_delete_def)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by (simp add: update_blit_wl_heur_pre_def)
subgoal by simp
subgoal by (simp add: update_clause_wl_pre_def)
subgoal by simp
done
qed
lemma unit_propagation_inner_loop_wl_loop_D_heur_unit_propagation_inner_loop_wl_loop_D:
‹(uncurry unit_propagation_inner_loop_wl_loop_D_heur,
uncurry unit_propagation_inner_loop_wl_loop)
∈ [λ(L, S). length (watched_by S L) ≤ r - MIN_HEADER_SIZE ∧ L = K ∧ length (watched_by S L) = s ∧
length (watched_by S L) ≤ r]⇩f
nat_lit_lit_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K lcount⟩nres_rel›
proof -
have unit_propagation_inner_loop_wl_loop_D_heur_inv:
‹unit_propagation_inner_loop_wl_loop_D_heur_inv x2a x1a xa›
if
‹(x, y) ∈ nat_lit_lit_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount› and
‹y = (x1, x2)› and
‹x = (x1a, x2a)› and
‹(xa, x') ∈ nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K lcount› and
H: ‹unit_propagation_inner_loop_wl_loop_inv x1 x'›
for x y x1 x2 x1a x2a xa x'
proof -
obtain w S w' S' j j' where
xa: ‹xa = (j, w, S)› and x': ‹x' = (j', w', S')›
by (cases xa; cases x') auto
show ?thesis
unfolding xa unit_propagation_inner_loop_wl_loop_D_heur_inv_def prod.case
apply (rule exI[of _ x2])
apply (rule exI[of _ S'])
using that xa x' that apply -
unfolding prod.case apply hypsubst
apply (auto simp: twl_st_heur'_def
dest!: twl_struct_invs_no_alien_in_trail[of _ ‹-x1›] simp flip: all_lits_st_alt_def)
unfolding unit_propagation_inner_loop_wl_loop_inv_def unit_propagation_inner_loop_l_inv_def
unfolding prod.case apply normalize_goal+
apply (drule twl_struct_invs_no_alien_in_trail[of _ ‹-x1›])
apply (simp_all only: twl_st_l multiset.map_comp comp_def
clause_twl_clause_of twl_st_wl in_all_lits_of_mm_uminus_iff ac_simps in_all_lits_uminus_iff
flip: all_lits_st_alt_def)
done
qed
have length: ‹⋀x y x1 x2 x1a x2a.
case y of
(L, S) ⇒
length (watched_by S L) ≤ r - MIN_HEADER_SIZE ∧
L = K ∧ length (watched_by S L) = s ∧ length (watched_by S L) ≤ r ⟹
(x, y) ∈ nat_lit_lit_rel ×⇩f twl_st_heur_up'' 𝒟 r s K lcount ⟹ y = (x1, x2) ⟹
x = (x1a, x2a) ⟹
x1 ∈# all_lits_st x2 ⟹
length (watched_by_int x2a x1a) ≤ length (get_clauses_wl_heur x2a) ⟹
mop_length_watched_by_int x2a x1a
≤ ⇓ Id (RETURN (length (watched_by x2 x1)))›
unfolding mop_length_watched_by_int_def
by refine_rcg
(auto simp: twl_st_heur'_def map_fun_rel_def2 twl_st_heur_def
simp flip: ℒ⇩a⇩l⇩l_all_atms_all_lits intro!: ASSERT_leI)
note H[refine] = unit_propagation_inner_loop_body_wl_heur_unit_propagation_inner_loop_body_wl_D
[THEN fref_to_Down_curry3] init
show ?thesis
unfolding unit_propagation_inner_loop_wl_loop_D_heur_def
unit_propagation_inner_loop_wl_loop_def uncurry_def
unit_propagation_inner_loop_wl_loop_inv_def[symmetric]
apply (intro frefI nres_relI)
apply (refine_vcg)
subgoal by (auto simp: twl_st_heur'_def twl_st_heur_state_simp_watched watched_by_alt_def
simp flip: all_lits_st_alt_def)
apply (rule length; assumption)
subgoal by auto
subgoal by (rule unit_propagation_inner_loop_wl_loop_D_heur_inv)
subgoal
by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id])
(auto simp: get_conflict_wl_is_None_heur_get_conflict_wl_is_None twl_st_heur_state_simp_watched twl_st_heur'_def
get_conflict_wl_is_None_def simp flip: ℒ⇩a⇩l⇩l_all_atms_all_lits)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma cut_watch_list_heur2_cut_watch_list_heur:
shows
‹cut_watch_list_heur2 j w L S ≤ ⇓ Id (cut_watch_list_heur j w L S)›
proof -
let ?N = ‹get_clauses_wl_heur S›
let ?W = ‹get_watched_wl_heur S›
define n where n: ‹n = length (?W ! nat_of_lit L)›
let ?R = ‹measure (λ(j'::nat, w' :: nat, _ :: (nat × nat literal × bool) list list). length (?W!nat_of_lit L) - w')›
define I' where
‹I' ≡ λ(j', w', W'). length (W' ! (nat_of_lit L)) = length (?W ! (nat_of_lit L)) ∧ j' ≤ w' ∧ w' ≥ w ∧
w' - w = j' - j ∧ j' ≥ j ∧
drop w' (W' ! (nat_of_lit L)) = drop w' (?W ! (nat_of_lit L)) ∧
w' ≤ length (W' ! (nat_of_lit L)) ∧
W'[nat_of_lit L := take (j + w' - w) (W' ! nat_of_lit L)] =
?W[nat_of_lit L := take (j + w' - w) ((take j (?W!(nat_of_lit L)) @ drop w (?W!(nat_of_lit L))))]›
have cut_watch_list_heur_alt_def:
‹cut_watch_list_heur j w L =(λS. do {
ASSERT(j ≤ length (get_watched_wl_heur S!nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length (get_watched_wl_heur S) ∧
w ≤ length (get_watched_wl_heur S ! (nat_of_lit L)));
let W = (get_watched_wl_heur S)[nat_of_lit L := take j (get_watched_wl_heur S!(nat_of_lit L)) @ drop w (get_watched_wl_heur S!(nat_of_lit L))];
RETURN (set_watched_wl_heur W S)
})›
unfolding cut_watch_list_heur_def Let_def by auto
have REC: ‹ASSERT (x1k < length (x2k ! nat_of_lit L)) ⤜
(λ_. RETURN (x1j + 1, x1k + 1, x2k [nat_of_lit L := (x2k ! nat_of_lit L) [x1j :=
x2k ! nat_of_lit L !
x1k]]))
≤ SPEC (λs'. ∀x1 x2 x1a x2a. x2 = (x1a, x2a) ⟶ s' = (x1, x2) ⟶
(x1 ≤ x1a ∧ nat_of_lit L < length x2a) ∧ I' s' ∧
(s', s) ∈ measure (λ(j', w', _). length (?W ! nat_of_lit L) - w'))›
if
‹j ≤ length (?W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length ?W ∧
w ≤ length (?W ! nat_of_lit L)› and
pre: ‹j ≤ length (?W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length ?W ∧
w ≤ length (?W ! nat_of_lit L)› and
I: ‹case s of (j, w, W) ⇒ j ≤ w ∧ nat_of_lit L < length W› and
I': ‹I' s› and
cond: ‹case s of (j, w, W) ⇒ w < length (W ! nat_of_lit L)› and
[simp]: ‹x2 = (x1k, x2k)› and
[simp]: ‹s = (x1j, x2)›
for s x1j x2 x1k x2k
proof -
have [simp]: ‹x1k < length (x2k ! nat_of_lit L)› and
‹length (?W ! nat_of_lit L) - Suc x1k < length (?W ! nat_of_lit L) - x1k›
using cond I I' unfolding I'_def by auto
moreover have ‹x1j ≤ x1k› ‹nat_of_lit L < length x2k›
using I I' unfolding I'_def by auto
moreover have ‹I' (Suc x1j, Suc x1k, x2k
[nat_of_lit L := (x2k ! nat_of_lit L)[x1j := x2k ! nat_of_lit L ! x1k]])›
proof -
have ball_leI: ‹(⋀x. x < A ⟹ P x) ⟹ (∀x < A. P x)› for A P
by auto
have H: ‹⋀i. x2k[nat_of_lit L := take (j + x1k - w) (x2k ! nat_of_lit L)] ! i = ?W
[nat_of_lit L :=
take (min (j + x1k - w) j) (?W ! nat_of_lit L) @
take (j + x1k - (w + min (length (?W ! nat_of_lit L)) j))
(drop w (?W ! nat_of_lit L))] ! i› and
H': ‹x2k[nat_of_lit L := take (j + x1k - w) (x2k ! nat_of_lit L)] = ?W
[nat_of_lit L :=
take (min (j + x1k - w) j) (?W ! nat_of_lit L) @
take (j + x1k - (w + min (length (?W ! nat_of_lit L)) j))
(drop w (?W ! nat_of_lit L))]› and
‹j < length (?W ! nat_of_lit L)› and
‹(length (?W ! nat_of_lit L) - w) ≥ (Suc x1k - w)› and
‹x1k ≥ w›
‹nat_of_lit L < length ?W› and
‹j + x1k - w = x1j› and
‹x1j - j = x1k - w› and
‹x1j < length (?W ! nat_of_lit L)› and
‹length (x2k ! nat_of_lit L) = length (?W ! nat_of_lit L)› and
‹drop x1k (x2k ! (nat_of_lit L)) = drop x1k (?W ! (nat_of_lit L))›
‹x1j ≥ j› and
‹w + x1j - j = x1k›
using I I' pre cond unfolding I'_def by auto
have
[simp]: ‹min x1j j = j›
using ‹x1j ≥ j› unfolding min_def by auto
have ‹x2k[nat_of_lit L := take (Suc (j + x1k) - w) (x2k[nat_of_lit L := (x2k ! nat_of_lit L)
[x1j := x2k ! nat_of_lit L ! x1k]] ! nat_of_lit L)] =
?W[nat_of_lit L := take j (?W ! nat_of_lit L) @ take (Suc (j + x1k) - (w + min (length (?W ! nat_of_lit L)) j))
(drop w (?W ! nat_of_lit L))]›
using cond I ‹j < length (?W ! nat_of_lit L)› and
‹(length (?W ! nat_of_lit L) - w) ≥ (Suc x1k - w)› and
‹x1k ≥ w›
‹nat_of_lit L < length ?W›
‹j + x1k - w = x1j› ‹x1j < length (?W ! nat_of_lit L)›
apply (subst list_eq_iff_nth_eq)
apply -
apply (intro conjI ball_leI)
subgoal using arg_cong[OF H', of length] by auto
subgoal for k
apply (cases ‹k ≠ nat_of_lit L›)
subgoal using H[of k] by auto
subgoal
using H[of k] ‹x1j < length (?W ! nat_of_lit L)›
‹length (x2k ! nat_of_lit L) = length (?W ! nat_of_lit L)›
arg_cong[OF ‹drop x1k (x2k ! (nat_of_lit L)) = drop x1k (?W ! (nat_of_lit L))›,
of ‹λxs. xs ! 0›] ‹x1j ≥ j›
apply (cases ‹Suc x1j = length (?W ! nat_of_lit L)›)
apply (auto simp add: Suc_diff_le take_Suc_conv_app_nth ‹j + x1k - w = x1j›
‹x1j - j = x1k - w›[symmetric] ‹w + x1j - j = x1k›)
apply (metis (no_types, lifting) append_eq_appendI append_eq_append_conv_if
nat_in_between_eq(1) take_update_last)
by (metis (no_types, lifting) ‹x1j < length (?W ! nat_of_lit L)› append.assoc
take_Suc_conv_app_nth take_update_last)
done
done
then show ?thesis
unfolding I'_def prod.case
using I I' cond unfolding I'_def by (auto simp: Cons_nth_drop_Suc[symmetric])
qed
ultimately show ?thesis
by auto
qed
have step: ‹(s, ?W[nat_of_lit L := take j (?W ! nat_of_lit L) @ drop w (?W ! nat_of_lit L)])
∈ {((i, j, W'), W). (W'[nat_of_lit L := take i (W' ! nat_of_lit L)], W) ∈ Id ∧
i ≤ length (W' ! nat_of_lit L) ∧ nat_of_lit L < length W' ∧
n = length (W' ! nat_of_lit L)}›
if
pre: ‹j ≤ length (?W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length ?W ∧
w ≤ length (?W ! nat_of_lit L)› and
‹j ≤ length (?W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length ?W ∧
w ≤ length (?W ! nat_of_lit L)› and
‹case s of (j, w, W) ⇒ j ≤ w ∧ nat_of_lit L < length W› and
‹I' s› and
‹¬ (case s of (j, w, W) ⇒ w < length (W ! nat_of_lit L))›
for s
proof -
obtain j' w' W' where s: ‹s = (j', w', W')› by (cases s)
have
‹¬ w' < length (W' ! nat_of_lit L)› and
‹j ≤ length (?W ! nat_of_lit L)› and
‹j' ≤ w'› and
‹nat_of_lit L < length W'› and
[simp]: ‹length (W' ! nat_of_lit L) = length (?W ! nat_of_lit L)› and
‹j ≤ w› and
‹j' ≤ w'› and
‹nat_of_lit L < length ?W› and
‹w ≤ length (?W ! nat_of_lit L)› and
‹w ≤ w'› and
‹w' - w = j' - j› and
‹j ≤ j'› and
‹drop w' (W' ! nat_of_lit L) = drop w' (?W ! nat_of_lit L)› and
‹w' ≤ length (W' ! nat_of_lit L)› and
L_le_W: ‹nat_of_lit L < length ?W› and
eq: ‹W'[nat_of_lit L := take (j + w' - w) (W' ! nat_of_lit L)] =
?W[nat_of_lit L := take (j + w' - w) (take j (?W ! nat_of_lit L) @ drop w (?W ! nat_of_lit L))]›
using that unfolding I'_def that prod.case s
by blast+
then have
j_j': ‹j + w' - w = j'› and
j_le: ‹j + w' - w = length (take j (?W ! nat_of_lit L) @ drop w (?W ! nat_of_lit L))› and
w': ‹w' = length (?W ! nat_of_lit L)›
by auto
have [simp]: ‹length ?W = length W'›
using arg_cong[OF eq, of length] by auto
show ?thesis
using eq ‹j ≤ w› ‹w ≤ length (?W ! nat_of_lit L)› ‹j ≤ j'› ‹w' - w = j' - j›
‹w ≤ w'› w' L_le_W
unfolding j_j' j_le s n
by (auto simp: min_def split: if_splits)
qed
have HHH: ‹X ≤ RES (R¯ `` {S}) ⟹ X ≤ ⇓ R (RETURN S)› for X S R
by (auto simp: RETURN_def conc_fun_RES)
show ?thesis
unfolding cut_watch_list_heur2_def cut_watch_list_heur_alt_def prod.case
apply (rewrite at ‹let _ = get_watched_wl_heur _ in _› Let_def)
unfolding n[symmetric]
apply (rewrite at ‹let _ = n in _› Let_def)
apply (refine_vcg WHILEIT_rule_stronger_inv_RES[where R = ?R and
I' = I' and Φ = ‹{((i, j, W'), W). (W'[nat_of_lit L := take i (W' ! nat_of_lit L)], W) ∈ Id ∧
i ≤ length (W' ! nat_of_lit L) ∧ nat_of_lit L < length W' ∧
n = length (W' ! nat_of_lit L)}¯ `` _›] HHH)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: )
subgoal by auto
subgoal by auto
subgoal unfolding I'_def by (auto simp: n)
subgoal unfolding I'_def by (auto simp: n)
subgoal unfolding I'_def by (auto simp: n)
subgoal unfolding I'_def by auto
subgoal unfolding I'_def by auto
subgoal unfolding I'_def by (auto simp: n)
subgoal using REC by (auto simp: n)
subgoal unfolding I'_def by (auto simp: n)
subgoal for s using step[of ‹s›] unfolding I'_def by (auto simp: n)
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma vdom_m_cut_watch_list:
‹set xs ⊆ set (W L) ⟹ vdom_m 𝒜 (W(L := xs)) d ⊆ vdom_m 𝒜 W d›
by (cases ‹L ∈# ℒ⇩a⇩l⇩l 𝒜›)
(force simp: vdom_m_def split: if_splits)+
text ‹The following order allows the rule to be used as a destruction rule, make it more
useful for refinement proofs.›
lemma vdom_m_cut_watch_listD:
‹x ∈ vdom_m 𝒜 (W(L := xs)) d ⟹ set xs ⊆ set (W L) ⟹ x ∈ vdom_m 𝒜 W d›
using vdom_m_cut_watch_list[of xs W L] by auto
lemma cut_watch_list_heur_cut_watch_list_heur:
‹(uncurry3 cut_watch_list_heur, uncurry3 cut_watch_list) ∈
[λ(((j, w), L), S). True]⇩f
nat_rel ×⇩f nat_rel ×⇩f nat_lit_lit_rel ×⇩f twl_st_heur'' 𝒟 r lcount → ⟨twl_st_heur'' 𝒟 r lcount⟩nres_rel›
unfolding cut_watch_list_heur_def cut_watch_list_def uncurry_def
ℒ⇩a⇩l⇩l_all_atms_all_lits[symmetric]
apply (intro frefI nres_relI)
apply refine_vcg
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def2)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def2)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def2)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def2)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def2 vdom_m_cut_watch_list set_take_subset
set_drop_subset dest!: vdom_m_cut_watch_listD
dest!: in_set_dropD in_set_takeD)
done
lemma unit_propagation_inner_loop_wl_D_heur_unit_propagation_inner_loop_wl_D:
‹(uncurry unit_propagation_inner_loop_wl_D_heur, uncurry unit_propagation_inner_loop_wl) ∈
[λ(L, S). length(watched_by S L) ≤ r-MIN_HEADER_SIZE]⇩f
nat_lit_lit_rel ×⇩f twl_st_heur'' 𝒟 r lcount → ⟨twl_st_heur'' 𝒟 r lcount⟩ nres_rel›
proof -
have length_le: ‹length (watched_by x2b x1b) ≤ r - MIN_HEADER_SIZE› and
length_eq: ‹length (watched_by x2b x1b) = length (watched_by (snd y) (fst y))› and
eq: ‹x1b = fst y›
if
‹case y of (L, S) ⇒ length (watched_by S L) ≤ r-MIN_HEADER_SIZE› and
‹(x, y) ∈ nat_lit_lit_rel ×⇩f twl_st_heur'' 𝒟 r lcount› and
‹y = (x1, x2)› and
‹x = (x1a, x2a)› and
‹(x1, x2) = (x1b, x2b)›
for x y x1 x2 x1a x2a x1b x2b r
using that by auto
show ?thesis
unfolding unit_propagation_inner_loop_wl_D_heur_def
unit_propagation_inner_loop_wl_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg cut_watch_list_heur_cut_watch_list_heur[of 𝒟 r, THEN fref_to_Down_curry3]
unit_propagation_inner_loop_wl_loop_D_heur_unit_propagation_inner_loop_wl_loop_D[of r _ _ 𝒟 lcount,
THEN fref_to_Down_curry])
apply (rule length_le; assumption)
apply (rule eq; assumption)
apply (rule length_eq; assumption)
subgoal by auto
subgoal by (auto simp: twl_st_heur'_def twl_st_heur_state_simp_watched)
subgoal
by (auto simp: twl_st_heur'_def twl_st_heur_state_simp_watched watched_by_alt_def
simp flip: all_lits_st_alt_def[symmetric])
apply (rule order.trans)
apply (rule cut_watch_list_heur2_cut_watch_list_heur)
apply (subst Down_id_eq)
apply (rule cut_watch_list_heur_cut_watch_list_heur[of 𝒟, THEN fref_to_Down_curry3])
by auto
qed
lemma select_and_remove_from_literals_to_update_wl_heur_select_and_remove_from_literals_to_update_wl:
‹literals_to_update_wl y ≠ {#} ⟹
(x, y) ∈ twl_st_heur'' 𝒟1 r1 lcount ⟹
select_and_remove_from_literals_to_update_wl_heur x
≤ ⇓{((S, L), (S', L')). ((S, L), (S', L')) ∈ twl_st_heur'' 𝒟1 r1 lcount ×⇩f nat_lit_lit_rel ∧
S' = set_literals_to_update_wl (literals_to_update_wl y - {#L#}) y ∧
get_clauses_wl_heur S = get_clauses_wl_heur x}
(select_and_remove_from_literals_to_update_wl y)›
supply RETURN_as_SPEC_refine[refine2]
unfolding select_and_remove_from_literals_to_update_wl_heur_def
select_and_remove_from_literals_to_update_wl_def
apply (refine_vcg)
subgoal
by (subst trail_pol_same_length[of ‹get_trail_wl_heur x› ‹get_trail_wl y› ‹all_atms_st y›])
(auto simp: twl_st_heur_def twl_st_heur'_def RETURN_RES_refine_iff)
subgoal
by (auto simp: twl_st_heur_def twl_st_heur'_def RETURN_RES_refine_iff trail_pol_alt_def)
subgoal
apply (subst (asm) trail_pol_same_length[of ‹get_trail_wl_heur x› ‹get_trail_wl y› ‹all_atms_st y›])
apply (auto simp: twl_st_heur_def twl_st_heur'_def; fail)[]
apply (rule bind_refine_res)
prefer 2
apply (rule isa_trail_nth_rev_trail_nth[THEN fref_to_Down_curry, unfolded comp_def RETURN_def,
unfolded conc_fun_RES, of ‹get_trail_wl y› _ _ _ ‹all_atms_st y›])
apply ((auto simp: twl_st_heur_def twl_st_heur'_def; fail)+)[2]
subgoal for z
apply (cases x; cases y)
by (auto simp add: Cons_nth_drop_Suc[symmetric] twl_st_heur_def twl_st_heur'_def
RETURN_RES_refine_iff rev_trail_nth_def)
done
done
lemma outer_loop_length_watched_le_length_arena:
assumes
xa_x': ‹(xa, x') ∈ twl_st_heur'' 𝒟 r lcount› and
prop_heur_inv: ‹unit_propagation_outer_loop_wl_D_heur_inv x xa› and
prop_inv: ‹unit_propagation_outer_loop_wl_inv x'› and
xb_x'a: ‹(xb, x'a) ∈ {((S, L), (S', L')). ((S, L), (S', L')) ∈ twl_st_heur'' 𝒟1 r lcount ×⇩f nat_lit_lit_rel ∧
S' = set_literals_to_update_wl (literals_to_update_wl x' - {#L#}) x' ∧
get_clauses_wl_heur S = get_clauses_wl_heur xa}› and
st: ‹x'a = (x1, x2)›
‹xb = (x1a, x2a)› and
x2: ‹x2 ∈# all_lits_st x1› and
st': ‹(x2, x1) = (x1b, x2b)›
shows ‹length (watched_by x2b x1b) ≤ r-MIN_HEADER_SIZE›
proof -
have ‹correct_watching x'›
using prop_inv unfolding unit_propagation_outer_loop_wl_inv_def
unit_propagation_outer_loop_wl_inv_def
by auto
moreover have ‹x2 ∈# all_lits_st x'›
using x2 assms unfolding all_atms_def all_lits_def
by (auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
ultimately have dist: ‹distinct_watched (watched_by x' x2)›
using x2 xb_x'a unfolding all_atms_def all_lits_def
by (cases x'; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps ac_simps)
then have dist: ‹distinct_watched (watched_by x1 x2)›
using xb_x'a unfolding st
by (cases x'; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
have dist_vdom: ‹distinct (get_vdom x1a)›
using xb_x'a
by (cases x')
(auto simp: twl_st_heur_def twl_st_heur'_def st aivdom_inv_dec_alt_def)
have
valid: ‹valid_arena (get_clauses_wl_heur xa) (get_clauses_wl x1) (set (get_vdom x1a))›
using xb_x'a unfolding all_atms_def all_lits_def st
by (cases x')
(auto simp: twl_st_heur'_def twl_st_heur_def)
have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
using xb_x'a
by (cases x')
(auto simp: twl_st_heur_def twl_st_heur'_def st)
then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
using x2 unfolding vdom_m_def st all_lits_st_alt_def[symmetric]
by (cases x1)
(force simp: twl_st_heur'_def twl_st_heur_def
dest!: multi_member_split)
have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
by (rule distinct_subseteq_iff[THEN iffD1])
(use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
‹simp_all flip: distinct_mset_mset_distinct›)
have vdom_incl: ‹set (get_vdom x1a) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur xa)}›
using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto
have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur xa) - MIN_HEADER_SIZE›
by (subst distinct_card[OF dist_vdom, symmetric])
(use card_mono[OF _ vdom_incl] in auto)
then show ?thesis
using size_mset_mono[OF watched_incl] xb_x'a st'
by auto
qed
lemma unit_propagation_outer_loop_wl_D_heur_alt_def:
‹unit_propagation_outer_loop_wl_D_heur S⇩0 = do {
S ← WHILE⇩T⇗unit_propagation_outer_loop_wl_D_heur_inv S⇩0⇖
(λS. literals_to_update_wl_heur S < isa_length_trail (get_trail_wl_heur S))
(λS. do {
ASSERT(literals_to_update_wl_heur S < isa_length_trail (get_trail_wl_heur S));
(S', L) ← select_and_remove_from_literals_to_update_wl_heur S;
ASSERT(length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S));
unit_propagation_inner_loop_wl_D_heur L S'
})
S⇩0;
unit_propagation_update_statistics (of_nat (isa_length_trail (get_trail_wl_heur S⇩0)))
(of_nat (isa_length_trail (get_trail_wl_heur S))) S
} ›
unfolding unit_propagation_outer_loop_wl_D_heur_def IsaSAT_Profile.start_def IsaSAT_Profile.stop_def
Let_def
by auto
lemma unit_propagation_outer_loop_wl_alt_def:
‹unit_propagation_outer_loop_wl S⇩0 = do {
S ← 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_st S');
unit_propagation_inner_loop_wl L S'
})
(S⇩0 :: 'v twl_st_wl);
RETURN S}
›
unfolding unit_propagation_outer_loop_wl_def by auto
lemma unit_propagation_update_statistics_twl_st_heur'':
‹(S, x') ∈ twl_st_heur'' 𝒟 r lcount ⟹
unit_propagation_update_statistics a b S ≤ ⇓(twl_st_heur'' 𝒟 r lcount) (RETURN x')›
unfolding unit_propagation_update_statistics_def Let_def conc_fun_RETURN
apply (refine_vcg trail_height_before_conflict[where 𝒜 = ‹all_atms_st x'›, THEN fref_to_Down, of _ ‹get_trail_wl x'›, THEN order_trans])
subgoal
by (auto simp: twl_st_heur_def twl_st_heur'_def)
subgoal
by (auto simp: twl_st_heur_def twl_st_heur'_def)
subgoal
by (auto simp: twl_st_heur_def twl_st_heur'_def)
subgoal
by (auto simp: twl_st_heur_def twl_st_heur'_def trail_height_before_conflict_spec_def)
done
theorem unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D':
‹(unit_propagation_outer_loop_wl_D_heur, unit_propagation_outer_loop_wl) ∈
twl_st_heur'' 𝒟 r lcount →⇩f ⟨twl_st_heur'' 𝒟 r lcount⟩ nres_rel›
unfolding unit_propagation_outer_loop_wl_D_heur_alt_def
unit_propagation_outer_loop_wl_alt_def all_lits_alt_def2[symmetric]
apply (intro frefI nres_relI)
apply (refine_vcg
unit_propagation_update_statistics_twl_st_heur''
unit_propagation_inner_loop_wl_D_heur_unit_propagation_inner_loop_wl_D[of r 𝒟 lcount, THEN fref_to_Down_curry]
select_and_remove_from_literals_to_update_wl_heur_select_and_remove_from_literals_to_update_wl
[of _ _ 𝒟 r lcount])
subgoal for x y S T
using isa_length_trail_pre[of ‹get_trail_wl_heur S› ‹get_trail_wl T› ‹all_atms_st T›] apply -
unfolding unit_propagation_outer_loop_wl_D_heur_inv_def twl_st_heur'_def
apply (rule_tac x=y in exI)
apply (rule_tac x=T in exI)
by (auto 5 2 simp: twl_st_heur_def twl_st_heur'_def)
subgoal for _ _ x y
by (subst isa_length_trail_length_u[THEN fref_to_Down_unRET_Id, of _ ‹get_trail_wl y› ‹all_atms_st y›])
(auto simp: twl_st_heur_def twl_st_heur'_def simp flip: all_lits_st_alt_def)
subgoal by (auto simp: twl_st_heur'_def)
subgoal for x y xa x' xb x'a x1 x2 x1a x2a x1b x2b
by (rule_tac x=x and xa=xa and 𝒟=𝒟 in outer_loop_length_watched_le_length_arena)
subgoal by (auto simp: twl_st_heur'_def)
done
lemma twl_st_heur'D_twl_st_heurD:
assumes H: ‹(⋀𝒟. f ∈ twl_st_heur' 𝒟 →⇩f ⟨twl_st_heur' 𝒟⟩ nres_rel)›
shows ‹f ∈ twl_st_heur →⇩f ⟨twl_st_heur⟩ nres_rel› (is ‹_ ∈ ?A B›)
proof -
obtain f1 f2 where f: ‹f = (f1, f2)›
by (cases f) auto
show ?thesis
using assms unfolding f
apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
apply (intro conjI impI allI)
subgoal for x y
apply (rule "weaken_⇓'"[of _ ‹twl_st_heur' (dom_m (get_clauses_wl y))›])
apply (fastforce simp: twl_st_heur'_def)+
done
done
qed
lemma watched_by_app_watched_by_app_heur:
‹(uncurry2 (RETURN ooo watched_by_app_heur), uncurry2 (RETURN ooo watched_by_app)) ∈
[λ((S, L), K). L ∈# all_lits_st S ∧ K < length (get_watched_wl S L)]⇩f
twl_st_heur ×⇩f Id ×⇩f Id → ⟨Id⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: watched_by_app_heur_def watched_by_app_def twl_st_heur_def map_fun_rel_def2)
lemma update_clause_wl_heur_pre_le_sint64:
assumes
‹arena_is_valid_clause_idx_and_access (get_clauses_wl_heur S) bf baa› and
‹length (get_clauses_wl_heur S)≤ snat64_max› and
‹arena_lit_pre (get_clauses_wl_heur S) (bf + baa)›
shows ‹bf + baa ≤ snat64_max›
‹length (get_clauses_wl_heur S) ≤ snat64_max›
using assms
by (auto simp: arena_is_valid_clause_idx_and_access_def isasat_fast_def
dest!: arena_lifting(10))
end