theory IsaSAT_Inner_Propagation
imports IsaSAT_Setup
IsaSAT_Clauses
begin
chapter ‹Propagation: Inner Loop›
declare all_atms_def[symmetric,simp]
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
by (auto simp add: all_lits_of_mm_union all_lits_def ℒ⇩a⇩l⇩l_all_atms_all_lits)
qed
definition find_non_false_literal_between where
‹find_non_false_literal_between M a b C =
find_in_list_between (λL. polarity M L ≠ Some False) a b C›
definition isa_find_unwatched_between
:: ‹_ ⇒ trail_pol ⇒ arena ⇒ nat ⇒ nat ⇒ nat ⇒ (nat option) nres› where
‹isa_find_unwatched_between P M' NU a b C = do {
ASSERT(C+a ≤ length NU);
ASSERT(C+b ≤ length NU);
(x, _) ← WHILE⇩T⇗λ(found, i). True⇖
(λ(found, i). found = None ∧ i < C + b)
(λ(_, i). do {
ASSERT(i < C + (arena_length NU C));
ASSERT(i ≥ C);
ASSERT(i < C + b);
ASSERT(arena_lit_pre NU i);
L ← mop_arena_lit NU i;
ASSERT(polarity_pol_pre M' L);
if P L then RETURN (Some (i - C), i) else RETURN (None, i+1)
})
(None, C+a);
RETURN x
}
›
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); ― ‹non-deterministic between full iteration (used in minisat),
or starting in the middle (use in cadical)›
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
})›
definition isa_find_unwatched
:: ‹(nat literal ⇒ bool) ⇒ trail_pol ⇒ arena ⇒ nat ⇒ (nat option) nres›
where
‹isa_find_unwatched P M' arena C = do {
l ← mop_arena_length arena C;
b ← RETURN(l ≤ MAX_LENGTH_SHORT_CLAUSE);
if b then isa_find_unwatched_between P M' arena 2 l C
else do {
ASSERT(get_saved_pos_pre arena C);
pos ← mop_arena_pos arena C;
n ← isa_find_unwatched_between P M' arena pos l C;
if n = None then isa_find_unwatched_between P M' arena 2 pos C
else RETURN n
}
}
›
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); ― ‹non-deterministic between full iteration (used in minisat),
or starting in the middle (use in cadical)›
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
definition isa_find_unwatched_wl_st_heur
:: ‹twl_st_wl_heur ⇒ nat ⇒ nat option nres› where
‹isa_find_unwatched_wl_st_heur = (λ(M, N, D, Q, W, vm, φ) i. do {
isa_find_unwatched (λL. polarity_pol M L ≠ Some False) M N i
})›
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
definition isa_save_pos :: ‹nat ⇒ nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹isa_save_pos C i = (λ(M, N, oth). do {
ASSERT(arena_is_valid_clause_idx N C);
if arena_length N C > MAX_LENGTH_SHORT_CLAUSE then do {
ASSERT(isa_update_pos_pre ((C, i), N));
RETURN (M, arena_update_pos C i N, oth)
} else RETURN (M, N, oth)
})
›
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} (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›
definition set_conflict_wl_heur_pre where
‹set_conflict_wl_heur_pre =
(λ(C, S). True)›
definition set_conflict_wl_heur
:: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹set_conflict_wl_heur = (λC (M, N, D, Q, W, vmtf, clvls, cach, lbd, outl, stats, fema, sema). do {
let n = 0;
ASSERT(curry6 isa_set_lookup_conflict_aa_pre M N C D n lbd outl);
(D, clvls, lbd, outl) ← isa_set_lookup_conflict_aa M N C D n lbd outl;
ASSERT(isa_length_trail_pre M);
ASSERT(arena_act_pre N C);
RETURN (M, arena_incr_act N C, D, isa_length_trail M, W, vmtf, clvls, cach, lbd, outl,
incr_conflict stats, fema, sema)})›
definition update_clause_wl_code_pre where
‹update_clause_wl_code_pre = (λ(((((((L, C), b), j), w), i), f), S).
w < length (get_watched_wl_heur S ! nat_of_lit L) )›
definition update_clause_wl_heur
:: ‹nat literal ⇒ nat ⇒ bool ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ twl_st_wl_heur ⇒
(nat × nat × twl_st_wl_heur) nres›
where
‹update_clause_wl_heur = (λ(L::nat literal) C b j w i f (M, N, D, Q, W, vm). do {
K' ← mop_arena_lit2' (set (get_vdom (M, N, D, Q, W, vm))) N C f;
ASSERT(w < length N);
N' ← mop_arena_swap C i f N;
ASSERT(nat_of_lit K' < length W);
ASSERT(length (W ! (nat_of_lit K')) < length N);
let W = W[nat_of_lit K':= W ! (nat_of_lit K') @ [(C, L, b)]];
RETURN (j, w+1, (M, N', D, Q, W, vm))
})›
definition update_clause_wl_pre where
‹update_clause_wl_pre K r = (λ(((((((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} (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) C b j w i f (M, N, D, NE, UE, NS, US, 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, NS, US, Q, W));
ASSERT(L ∈# all_lits_st (M, N, D, NE, UE, NS, US, Q, W));
K' ← mop_clauses_at N C f;
ASSERT(K' ∈# all_lits_st (M, N, D, NE, UE, NS, US, Q, W) ∧ L ≠ K');
N' ← mop_clauses_swap N C i f;
RETURN (j, w+1, (M, N', D, NE, UE, NS, US, Q, W(K' := W K' @ [(C, L, b)])))
})›
unfolding update_clause_wl_def by (auto intro!: ext simp flip: all_lits_alt_def2)
lemma update_clause_wl_heur_update_clause_wl:
‹(uncurry7 update_clause_wl_heur, uncurry7 (update_clause_wl)) ∈
[update_clause_wl_pre K r]⇩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 →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K⟩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
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_def 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_def 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_def 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_def 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_def 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_def 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
map_fun_rel_def twl_st_heur'_def update_clause_wl_pre_def arena_lifting arena_lit_pre_def
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 c d e f g h i j k l m n p q ra t aa ba ca da ea fa ga ha ia
ja 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 x1p x1q x1r
x1s x1t x1u x2o x2p x2q x2r x2s x2t x2u x1v x2v x1w x2w x1x x2x x1y
x2y x1z x2z K' K'a N' K'a'
supply[[goals_limit=1]]
by (auto dest!: length_watched_le2[of _ _ _ _ x2u 𝒟 r K'a])
(simp_all add: twl_st_heur'_def twl_st_heur_def map_fun_rel_def ac_simps)
subgoal
by
(clarsimp simp: twl_st_heur_def Let_def
map_fun_rel_def 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_heur
:: ‹nat literal ⇒ nat ⇒ nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹propagate_lit_wl_heur = (λL' C i (M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats,
heur, sema). do {
ASSERT(i ≤ 1);
M ← cons_trail_Propagated_tr L' C M;
N' ← mop_arena_swap C 0 (1 - i) N;
let stats = incr_propagation (if count_decided_pol M = 0 then incr_uset stats else stats);
heur ← mop_save_phase_heur (atm_of L') (is_pos L') heur;
RETURN (M, N', D, Q, W, vm, clvls, cach, lbd, outl,
stats, heur, sema)
})›
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 ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧
1 - i < length (get_clauses_wl S ∝ C) ∧
0 < length (get_clauses_wl S ∝ C))›
lemma isa_vmtf_consD:
assumes vmtf: ‹((ns, m, fst_As, lst_As, next_search), remove) ∈ isa_vmtf 𝒜 M›
shows ‹((ns, m, fst_As, lst_As, next_search), remove) ∈ isa_vmtf 𝒜 (L # M)›
using vmtf_consD[of ns m fst_As lst_As next_search _ 𝒜 M L] assms
by (auto simp: isa_vmtf_def)
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 → ⟨twl_st_heur_up'' 𝒟 r s K⟩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_def ℒ⇩a⇩l⇩l_all_atms_all_lits
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 atms_of_def ℒ⇩a⇩l⇩l_all_atms_all_lits
all_lits_def 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_consD2
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 ∈# ℒ⇩a⇩l⇩l (all_atms_st S))›
definition propagate_lit_wl_bin_heur
:: ‹nat literal ⇒ nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹propagate_lit_wl_bin_heur = (λL' C (M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats,
heur, sema). do {
M ← cons_trail_Propagated_tr L' C M;
let stats = incr_propagation (if count_decided_pol M = 0 then incr_uset stats else stats);
heur ← mop_save_phase_heur (atm_of L') (is_pos L') heur;
RETURN (M, N, D, Q, W, vm, clvls, cach, lbd, outl,
stats, heur, sema)
})›
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 → ⟨twl_st_heur_up'' 𝒟 r s K⟩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 ℒ⇩a⇩l⇩l_all_atms_all_lits ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm
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 ℒ⇩a⇩l⇩l_all_atms_all_lits
all_lits_def ℒ⇩a⇩l⇩l_all_atms_all_lits ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm 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 ℒ⇩a⇩l⇩l_all_atms_all_lits ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm
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_consD2
op_clauses_swap_def)
done
definition unit_prop_body_wl_heur_inv where
‹unit_prop_body_wl_heur_inv S j w L ⟷
(∃S'. (S, S') ∈ twl_st_heur ∧ unit_prop_body_wl_inv S' j w L)›
definition unit_prop_body_wl_D_find_unwatched_heur_inv where
‹unit_prop_body_wl_D_find_unwatched_heur_inv f C S ⟷
(∃S'. (S, S') ∈ twl_st_heur ∧ unit_prop_body_wl_find_unwatched_inv f C S')›
definition keep_watch_heur where
‹keep_watch_heur = (λL i j (M, N, D, Q, W, vm). do {
ASSERT(nat_of_lit L < length W);
ASSERT(i < length (W ! nat_of_lit L));
ASSERT(j < length (W ! nat_of_lit L));
RETURN (M, N, D, Q, W[nat_of_lit L := (W!(nat_of_lit L))[i := W ! (nat_of_lit L) ! j]], vm)
})›
definition update_blit_wl_heur
:: ‹nat literal ⇒ nat ⇒ bool ⇒ nat ⇒ nat ⇒ nat literal ⇒ twl_st_wl_heur ⇒
(nat × nat × twl_st_wl_heur) nres›
where
‹update_blit_wl_heur = (λ(L::nat literal) C b j w K (M, N, D, Q, W, vm). do {
ASSERT(nat_of_lit L < length W);
ASSERT(j < length (W ! nat_of_lit L));
ASSERT(j < length N);
ASSERT(w < length N);
RETURN (j+1, w+1, (M, N, D, Q, W[nat_of_lit L := (W!nat_of_lit L)[j:= (C, K, b)]], vm))
})›
definition pos_of_watched_heur :: ‹twl_st_wl_heur ⇒ nat ⇒ nat literal ⇒ nat nres› where
‹pos_of_watched_heur S C L = do {
L' ← mop_access_lit_in_clauses_heur S C 0;
RETURN (if L = L' then 0 else 1)
} ›
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} ⟹
((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)
definition unit_propagation_inner_loop_wl_loop_D_heur_inv0 where
‹unit_propagation_inner_loop_wl_loop_D_heur_inv0 L =
(λ(j, w, S'). ∃S. (S', S) ∈ twl_st_heur ∧ unit_propagation_inner_loop_wl_loop_inv L (j, w, S) ∧
length (watched_by S L) ≤ length (get_clauses_wl_heur S') - 4)›
definition other_watched_wl_heur :: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat ⇒ nat ⇒ nat literal nres› where
‹other_watched_wl_heur S L C i = do {
ASSERT(i < 2 ∧ arena_lit_pre2 (get_clauses_wl_heur S) C i ∧
arena_lit (get_clauses_wl_heur S) (C + i) = L ∧ arena_lit_pre2 (get_clauses_wl_heur S) C (1 - i));
mop_access_lit_in_clauses_heur S C (1 - i)
}›
lemma other_watched_heur:
‹(S, S') ∈ {(T, T'). get_vdom T = get_vdom x2e ∧ (T, T') ∈ twl_st_heur_up'' 𝒟 r s t} ⟹
((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›
definition unit_propagation_inner_loop_body_wl_heur
:: ‹nat literal ⇒ nat ⇒ nat ⇒ twl_st_wl_heur ⇒ (nat × nat × twl_st_wl_heur) nres›
where
‹unit_propagation_inner_loop_body_wl_heur L j w (S0 :: twl_st_wl_heur) = do {
ASSERT(unit_propagation_inner_loop_wl_loop_D_heur_inv0 L (j, w, S0));
(C, K, b) ← mop_watched_by_app_heur S0 L w;
S ← keep_watch_heur L j w S0;
ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0));
val_K ← mop_polarity_st_heur S K;
if val_K = Some True
then RETURN (j+1, w+1, S)
else do {
if b then do {
if val_K = Some False
then do {
S ← set_conflict_wl_heur C S;
RETURN (j+1, w+1, S)}
else do {
S ← propagate_lit_wl_bin_heur K C S;
RETURN (j+1, w+1, S)}
}
else do {
―‹Now the costly operations:›
ASSERT(clause_not_marked_to_delete_heur_pre (S, C));
if ¬clause_not_marked_to_delete_heur S C
then RETURN (j, w+1, S)
else do {
i ← pos_of_watched_heur S C L;
ASSERT(i ≤ 1);
L' ← other_watched_wl_heur S L C i;
val_L' ← mop_polarity_st_heur S L';
if val_L' = Some True
then update_blit_wl_heur L C b j w L' S
else do {
f ← isa_find_unwatched_wl_st_heur S C;
case f of
None ⇒ do {
if val_L' = Some False
then do {
S ← set_conflict_wl_heur C S;
RETURN (j+1, w+1, S)}
else do {
S ← propagate_lit_wl_heur L' C i S;
RETURN (j+1, w+1, S)}
}
| Some f ⇒ do {
S ← isa_save_pos C f S;
ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0));
K ← mop_access_lit_in_clauses_heur S C f;
val_L' ← mop_polarity_st_heur S K;
if val_L' = Some True
then update_blit_wl_heur L C b j w K S
else do {
update_clause_wl_heur L C b j w i f S
}
}
}
}
}
}
}›
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)
apply (auto simp: all_lits_def all_lits_of_mm_union)
done
lemma set_conflict_wl_alt_def:
‹set_conflict_wl = (λC (M, N, D, NE, UE, NS, US, Q, W). do {
ASSERT(set_conflict_wl_pre C (M, N, D, NE, UE, NS, US, Q, W));
let D = Some (mset (N ∝ C));
RETURN (M, N, D, NE, UE, NS, US, {#}, 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
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T)›
using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have lits_trail: ‹atm_of ` lits_of_l (get_trail T) ⊆ atms_of_mm (clause `# get_clauses T + unit_clss T +
subsumed_clauses T)›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (cases T) (auto
simp del: all_clss_l_ran_m union_filter_mset_complement
simp: twl_st twl_st_l twl_st_wl all_lits_of_mm_union lits_of_def
convert_lits_l_def image_image in_all_lits_of_mm_ain_atms_of_iff
get_unit_clauses_wl_alt_def image_subset_iff)
moreover have ‹atms_of_mm (clause `# get_clauses T + unit_clss T +
subsumed_clauses T) = set_mset (all_atms_st S)›
using SS' T unfolding all_atms_st_alt_def all_lits_def
by (auto simp: mset_take_mset_drop_mset' twl_st_l atm_of_all_lits_of_mm)
ultimately show ?thesis
using SS' T dom tauto dist confl unfolding set_conflict_wl'_pre_def
by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_atm_of 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 → ⟨twl_st_heur_up'' 𝒟 r s K⟩nres_rel›
proof -
have H:
‹isa_set_lookup_conflict_aa x y z a b c d
≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩f (nat_rel ×⇩f (Id ×⇩f Id)))
(set_conflict_m x' y' z' a' b' c' d')›
if
‹(((((((x, y), z), a), b), c), d), (((((x', y'), z'), a'), b'), c'), d')
∈ trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f
nat_rel ×⇩f
option_lookup_clause_rel 𝒜 ×⇩f
nat_rel ×⇩f
Id ×⇩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_curry6,
unfolded prod.case, OF that(2,1)])
have [refine0]: ‹isa_set_lookup_conflict_aa x1h x1i x1g x1j 0 x1q x1r
≤ ⇓ {((C, n, lbd, 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› 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
‹x2s = (x1t, x2t)› and
‹x2r = (x1s, x2s)› and
‹x2q = (x1r, x2r)› and
‹x2p = (x1q, x2q)› and
‹x2n = (x1o, x2p)› and
‹x2m = (x1n, x2n)› and
‹x2l = (x1m, x2m)› and
‹x2k = (x1l, x2l)› and
‹x2j = (x1k, x2k)› and
‹x2i = (x1j, x2j)› and
‹x2h = (x1i, x2i)› and
‹x2g = (x1h, x2h)› and
‹x = (x1g, x2g)› and
‹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
proof -
show ?thesis
apply (rule order_trans)
apply (rule H[of _ _ _ _ _ _ _ x1a x1b x1g x1c 0 x1q x1r ‹all_atms_st x2›
‹set (get_vdom (snd x))›])
subgoal
using that
by (auto simp: twl_st_heur'_def twl_st_heur_def 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:
‹curry6 isa_set_lookup_conflict_aa_pre x1h x1i x1g x1j 0 x1q x1r›
if
‹case y of (x, xa) ⇒ set_conflict_wl'_pre x xa› and
‹(x, y) ∈ nat_rel ×⇩f twl_st_heur_up'' 𝒟 r s K› 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
‹x2s = (x1t, x2t)› and
‹x2r = (x1s, x2s)› and
‹x2q = (x1r, x2r)› and
‹x2p = (x1q, x2q)› and
‹x2n = (x1o, x2p)› and
‹x2m = (x1n, x2n)› and
‹x2l = (x1m, x2m)› and
‹x2k = (x1l, x2l)› and
‹x2j = (x1k, x2k)› and
‹x2i = (x1j, x2j)› and
‹x2h = (x1i, x2i)› and
‹x2g = (x1h, x2h)› and
‹x = (x1g, x2g)›
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
proof -
show ?thesis
using that 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)
qed
show ?thesis
supply [[goals_limit=1]]
apply (intro nres_relI frefI)
unfolding uncurry_def RES_RETURN_RES4 set_conflict_wl_alt_def set_conflict_wl_heur_def
apply (rewrite at ‹let _ = 0 in _› Let_def)
apply (refine_vcg)
subgoal by (rule isa_set_lookup_conflict_aa_pre) (auto dest!: set_conflict_wl_pre_set_conflict_wl'_pre)
apply assumption+
subgoal by (auto dest!: set_conflict_wl_pre_set_conflict_wl'_pre)
subgoal for x y
unfolding arena_act_pre_def arena_is_valid_clause_idx_def
by (rule isa_length_trail_pre)
(auto simp: twl_st_heur'_def twl_st_heur_def)
subgoal for x y
unfolding arena_act_pre_def arena_is_valid_clause_idx_def
by (rule exI[of _ ‹get_clauses_wl (snd y)›], rule exI[of _ ‹set (get_vdom (snd x))›])
(auto simp: twl_st_heur'_def twl_st_heur_def set_conflict_wl'_pre_def dest!: set_conflict_wl_pre_set_conflict_wl'_pre)
subgoal
by (subst isa_length_trail_length_u[THEN fref_to_Down_unRET_Id])
(auto simp: twl_st_heur'_def twl_st_heur_def counts_maximum_level_def ac_simps
set_conflict_wl'_pre_def all_atms_def[symmetric] dest!: set_conflict_wl_pre_set_conflict_wl'_pre
intro!: valid_arena_arena_incr_act valid_arena_mark_used)
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 → ⟨twl_st_heur_up'' 𝒟 r s K⟩ 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_def 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_def 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_def 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_def all_atms_def[symmetric] mop_keep_watch_def keep_watch_def
intro!: ASSERT_leI
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 ⟹
keep_watch_heur L' j' w' S' ≤ ⇓ {(T, T'). get_vdom T = get_vdom S' ∧
(T, T') ∈ twl_st_heur_up'' 𝒟 r s K}
(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_def 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_def 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_def 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_def all_atms_def[symmetric] mop_keep_watch_def keep_watch_def
intro!: ASSERT_leI
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→
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K⟩ 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_def 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 aq ar bi at bl
bm bn bo bp bq br bs bt bu bv bw bx _ _ _ _ _ _ _ _ "by" bz ca cb ci cj ck cl cm cn co
cq cr cs ct cv y x
apply (subgoal_tac ‹vdom_m (all_atms co (cq + cr + cs + ct))
(cv(K := (cv K)[ck := (ci, cm, cj)])) co ⊆
vdom_m (all_atms co (cq + cr + cs + ct)) cv co›)
apply fast
apply (rule vdom_m_update_subset')
apply auto
done
subgoal for aa ab ac ad ae be af ag ah bf ai aj ak al am an bg ao bh ap aq ar bi at
bl bm bn bo bp bq br bs bt bu bv bw bx _ _ _ _ _ _ _ _ "by" bz ca cb ci cj ck cl cm cn
co cp cq cr cs ct cv x
apply (subgoal_tac ‹vdom_m (all_atms co (cq + cr + cs + ct))
(cv(K := (cv K)[ck := (ci, cm, cj)])) co ⊆
vdom_m (all_atms co (cq + cr + cs + ct)) cv co›)
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)}
} ―‹Now the costly operations:›
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; ― ‹position saving›
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 C b j w i f S
}
}
}
}
}›
unfolding unit_propagation_inner_loop_body_wl_def Let_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 - 4 ∧ 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 →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K⟩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
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 ‹force simp: is_nondeleted_clause_pre_def twl_st_heur_def vdom_m_def
ℒ⇩a⇩l⇩l_all_atms_all_lits dest!: multi_member_split[of L]›)
note [refine] = mop_watched_by_app_heur_mop_watched_by_at''[of 𝒟 r K s, THEN fref_to_Down_curry2]
keep_watch_heur_keep_watch'[of _ _ _ _ _ _ _ _ 𝒟 r K s]
mop_polarity_st_heur_mop_polarity_wl''[of 𝒟 r K s, THEN fref_to_Down_curry, unfolded comp_def]
set_conflict_wl_heur_set_conflict_wl'[of 𝒟 r K s, THEN fref_to_Down_curry, unfolded comp_def]
propagate_lit_wl_bin_heur_propagate_lit_wl_bin
[of 𝒟 r K s, THEN fref_to_Down_curry2, unfolded comp_def]
pos_of_watched_heur[of _ _ _ 𝒟 r K s]
mop_access_lit_in_clauses_heur
update_blit_wl_heur_update_blit_wl[of r K 𝒟 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 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 𝒟 s, THEN fref_to_Down_curry7]
other_watched_heur[of _ _ _ 𝒟 r 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
ℒ⇩a⇩l⇩l_all_atms_all_lits 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
definition unit_propagation_inner_loop_wl_loop_D_heur_inv where
‹unit_propagation_inner_loop_wl_loop_D_heur_inv S⇩0 L =
(λ(j, w, S'). ∃S⇩0' S. (S⇩0, S⇩0') ∈ twl_st_heur ∧ (S', S) ∈ twl_st_heur ∧ unit_propagation_inner_loop_wl_loop_inv L (j, w, S) ∧
L ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧ dom_m (get_clauses_wl S) = dom_m (get_clauses_wl S⇩0') ∧
length (get_clauses_wl_heur S⇩0) = length (get_clauses_wl_heur S'))›
definition mop_length_watched_by_int :: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat nres› where
‹mop_length_watched_by_int S L = do {
ASSERT(nat_of_lit L < length (get_watched_wl_heur S));
RETURN (length (watched_by_int S L))
}›
lemma mop_length_watched_by_int_alt_def:
‹mop_length_watched_by_int = (λ(M, N, D, Q, W, _) L. do {
ASSERT(nat_of_lit L < length (W));
RETURN (length (W ! nat_of_lit L))
})›
unfolding mop_length_watched_by_int_def by (auto intro!: ext)
definition unit_propagation_inner_loop_wl_loop_D_heur
:: ‹nat literal ⇒ twl_st_wl_heur ⇒ (nat × nat × twl_st_wl_heur) nres›
where
‹unit_propagation_inner_loop_wl_loop_D_heur L S⇩0 = do {
ASSERT(length (watched_by_int S⇩0 L) ≤ length (get_clauses_wl_heur S⇩0));
n ← mop_length_watched_by_int S⇩0 L;
WHILE⇩T⇗unit_propagation_inner_loop_wl_loop_D_heur_inv S⇩0 L⇖
(λ(j, w, S). w < n ∧ get_conflict_wl_is_None_heur S)
(λ(j, w, S). do {
unit_propagation_inner_loop_body_wl_heur L j w S
})
(0, 0, S⇩0)
}›
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 - 4 ∧ 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 →
⟨nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K⟩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› and
‹y = (x1, x2)› and
‹x = (x1a, x2a)› and
‹(xa, x') ∈ nat_rel ×⇩r nat_rel ×⇩r twl_st_heur_up'' 𝒟 r s K› 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: ℒ⇩a⇩l⇩l_all_atms_all_lits all_lits_def twl_st_heur'_def dest!: twl_struct_invs_no_alien_in_trail[of _ ‹-x1›])
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 ℒ⇩a⇩l⇩l_all_atms_all_lits all_lits_def multiset.map_comp comp_def
clause_twl_clause_of twl_st_wl in_all_lits_of_mm_uminus_iff ac_simps)
done
qed
have length: ‹⋀x y x1 x2 x1a x2a.
case y of
(L, S) ⇒
length (watched_by S L) ≤ r - 4 ∧
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 ⟹ 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_def 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 simp flip: ℒ⇩a⇩l⇩l_all_atms_all_lits)
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
definition cut_watch_list_heur
:: ‹nat ⇒ nat ⇒ nat literal ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹cut_watch_list_heur j w L =(λ(M, N, D, Q, W, oth). do {
ASSERT(j ≤ length (W!nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length W ∧
w ≤ length (W ! (nat_of_lit L)));
RETURN (M, N, D, Q,
W[nat_of_lit L := take j (W!(nat_of_lit L)) @ drop w (W!(nat_of_lit L))], oth)
})›
definition cut_watch_list_heur2
:: ‹nat ⇒ nat ⇒ nat literal ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹cut_watch_list_heur2 = (λj w L (M, N, D, Q, W, oth). do {
ASSERT(j ≤ length (W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length W ∧
w ≤ length (W ! (nat_of_lit L)));
let n = length (W!(nat_of_lit L));
(j, w, W) ← WHILE⇩T⇗λ(j, w, W). j ≤ w ∧ w ≤ n ∧ nat_of_lit L < length W⇖
(λ(j, w, W). w < n)
(λ(j, w, W). do {
ASSERT(w < length (W!(nat_of_lit L)));
RETURN (j+1, w+1, W[nat_of_lit L := (W!(nat_of_lit L))[j := W!(nat_of_lit L)!w]])
})
(j, w, W);
ASSERT(j ≤ length (W ! nat_of_lit L) ∧ nat_of_lit L < length W);
let W = W[nat_of_lit L := take j (W ! nat_of_lit L)];
RETURN (M, N, D, Q, W, oth)
})›
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 -
obtain M N D Q W oth where S: ‹S = (M, N, D, Q, W, oth)›
by (cases 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 =(λ(M, N, D, Q, W, oth). do {
ASSERT(j ≤ length (W!nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length W ∧
w ≤ length (W ! (nat_of_lit L)));
let W = W[nat_of_lit L := take j (W!(nat_of_lit L)) @ drop w (W!(nat_of_lit L))];
RETURN (M, N, D, Q, W, oth)
})›
unfolding cut_watch_list_heur_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 append.assoc le_neq_implies_less list_update_id nat_in_between_eq(1)
not_less_eq take_Suc_conv_app_nth take_all)
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 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 S 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: S)
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 → ⟨twl_st_heur'' 𝒟 r⟩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_def)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def)
subgoal
by (auto simp: cut_watch_list_heur_def cut_watch_list_def twl_st_heur'_def
twl_st_heur_def map_fun_rel_def 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
definition unit_propagation_inner_loop_wl_D_heur
:: ‹nat literal ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹unit_propagation_inner_loop_wl_D_heur L S⇩0 = do {
(j, w, S) ← unit_propagation_inner_loop_wl_loop_D_heur L S⇩0;
ASSERT(length (watched_by_int S L) ≤ length (get_clauses_wl_heur S⇩0) - 4);
cut_watch_list_heur2 j w L S
}›
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-4]⇩f
nat_lit_lit_rel ×⇩f twl_st_heur'' 𝒟 r → ⟨twl_st_heur'' 𝒟 r⟩ nres_rel›
proof -
have length_le: ‹length (watched_by x2b x1b) ≤ r - 4› 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-4› and
‹(x, y) ∈ nat_lit_lit_rel ×⇩f twl_st_heur'' 𝒟 r› 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 _ _ 𝒟,
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
simp flip: ℒ⇩a⇩l⇩l_all_atms_all_lits)
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
definition select_and_remove_from_literals_to_update_wl_heur
:: ‹twl_st_wl_heur ⇒ (twl_st_wl_heur × nat literal) nres›
where
‹select_and_remove_from_literals_to_update_wl_heur S = do {
ASSERT(literals_to_update_wl_heur S < length (fst (get_trail_wl_heur S)));
ASSERT(literals_to_update_wl_heur S + 1 ≤ uint32_max);
L ← isa_trail_nth (get_trail_wl_heur S) (literals_to_update_wl_heur S);
RETURN (set_literals_to_update_wl_heur (literals_to_update_wl_heur S + 1) S, -L)
}›
definition unit_propagation_outer_loop_wl_D_heur_inv
:: ‹twl_st_wl_heur ⇒ twl_st_wl_heur ⇒ bool›
where
‹unit_propagation_outer_loop_wl_D_heur_inv S⇩0 S' ⟷
(∃S⇩0' S. (S⇩0, S⇩0') ∈ twl_st_heur ∧ (S', S) ∈ twl_st_heur ∧
unit_propagation_outer_loop_wl_inv S ∧
dom_m (get_clauses_wl S) = dom_m (get_clauses_wl S⇩0') ∧
length (get_clauses_wl_heur S') = length (get_clauses_wl_heur S⇩0) ∧
isa_length_trail_pre (get_trail_wl_heur S'))›
definition unit_propagation_outer_loop_wl_D_heur
:: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹unit_propagation_outer_loop_wl_D_heur S⇩0 =
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›
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 ⟹
select_and_remove_from_literals_to_update_wl_heur x
≤ ⇓{((S, L), (S', L')). ((S, L), (S', L')) ∈ twl_st_heur'' 𝒟1 r1 ×⇩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 (simp_all 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› 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 ×⇩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-4›
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)
have x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
using x2 xb_x'a unfolding st ℒ⇩a⇩l⇩l_all_atms_all_lits
by auto
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
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) ⊆ {4..< 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) - 4›
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
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 →⇩f ⟨twl_st_heur'' 𝒟 r⟩ nres_rel›
unfolding unit_propagation_outer_loop_wl_D_heur_def
unit_propagation_outer_loop_wl_def all_lits_alt_def2[symmetric]
apply (intro frefI nres_relI)
apply (refine_vcg
unit_propagation_inner_loop_wl_D_heur_unit_propagation_inner_loop_wl_D[of r 𝒟, THEN fref_to_Down_curry]
select_and_remove_from_literals_to_update_wl_heur_select_and_remove_from_literals_to_update_wl
[of _ _ 𝒟 r])
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)
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 ∈# ℒ⇩a⇩l⇩l (all_atms_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_def)
lemma case_tri_bool_If:
‹(case a of
None ⇒ f1
| Some v ⇒
(if v then f2 else f3)) =
(let b = a in if b = UNSET
then f1
else if b = SET_TRUE then f2 else f3)›
by (auto split: option.splits)
definition isa_find_unset_lit :: ‹trail_pol ⇒ arena ⇒ nat ⇒ nat ⇒ nat ⇒ nat option nres› where
‹isa_find_unset_lit M = isa_find_unwatched_between (λL. polarity_pol M L ≠ Some False) M›
lemma update_clause_wl_heur_pre_le_sint64:
assumes
‹arena_is_valid_clause_idx_and_access a1'a bf baa› and
‹length (get_clauses_wl_heur
(a1', a1'a, (da, db, dc), a1'c, a1'd, ((eu, ev, ew, ex, ey), ez), fa, fb,
fc, fd, fe, (ff, fg, fh, fi), fj, fk, fl, fm, fn)) ≤ sint64_max› and
‹arena_lit_pre a1'a (bf + baa)›
shows ‹bf + baa ≤ sint64_max›
‹length a1'a ≤ sint64_max›
using assms
by (auto simp: arena_is_valid_clause_idx_and_access_def isasat_fast_def
dest!: arena_lifting(10))
end