theory IsaSAT_Lookup_Conflict
imports
IsaSAT_Literals
Watched_Literals.CDCL_Conflict_Minimisation
LBD
IsaSAT_Clauses
IsaSAT_Watch_List
IsaSAT_Trail
begin
chapter ‹Clauses Encoded as Positions›
text ‹We use represent the conflict in two data structures close to the one used by the most SAT
solvers: We keep an array that represent the clause (for efficient iteration on the clause) and a
``hash-table'' to efficiently test if a literal belongs to the clause.
The first data structure is simply an array to represent the clause. This theory is only about
the second data structure. We refine it from the clause (seen as a multiset) in two steps:
▸ First, we represent the clause as a ``hash-table'', where the \<^term>‹i›-th position indicates
\<^term>‹Some True› (respectively \<^term>‹Some False›, \<^term>‹None›) if \<^term>‹Pos i› is present in the
clause (respectively \<^term>‹Neg i›, not at all). This allows to represent every not-tautological
clause whose literals fits in the underlying array.
▸ Then we refine it to an array of booleans indicating if the atom is present or not. This
information is redundant because we already know that a literal can only appear negated
compared to the trail.
The first step makes it easier to reason about the clause (since we have the full clause), while the
second step should generate (slightly) more efficient code.
Most solvers also merge the underlying array with the array used to cache information for the
conflict minimisation (see theory \<^theory>‹Watched_Literals.CDCL_Conflict_Minimisation›,
where we only test if atoms appear in the clause, not literals).
As far as we know, versat stops at the first refinement (stating that there is no significant
overhead, which is probably true, but the second refinement is not much additional work anyhow and
we don't have to rely on the ability of the compiler to not represent the option type on booleans
as a pointer, which it might be able to or not).
›
text ‹This is the first level of the refinement. We tried a few different definitions (including a
direct one, i.e., mapping a position to the inclusion in the set) but the inductive version turned out
to the easiest one to use.
›
inductive mset_as_position :: ‹bool option list ⇒ nat literal multiset ⇒ bool› where
empty:
‹mset_as_position (replicate n None) {#}› |
add:
‹mset_as_position xs' (add_mset L P)›
if ‹mset_as_position xs P› and ‹atm_of L < length xs› and ‹L ∉# P› and ‹-L ∉# P› and
‹xs' = xs[atm_of L := Some (is_pos L)]›
lemma mset_as_position_distinct_mset:
‹mset_as_position xs P ⟹ distinct_mset P›
by (induction rule: mset_as_position.induct) auto
lemma mset_as_position_atm_le_length:
‹mset_as_position xs P ⟹ L ∈# P ⟹ atm_of L < length xs›
by (induction rule: mset_as_position.induct) (auto simp: nth_list_update' atm_of_eq_atm_of)
lemma mset_as_position_nth:
‹mset_as_position xs P ⟹ L ∈# P ⟹ xs ! (atm_of L) = Some (is_pos L)›
by (induction rule: mset_as_position.induct)
(auto simp: nth_list_update' atm_of_eq_atm_of dest: mset_as_position_atm_le_length)
lemma mset_as_position_in_iff_nth:
‹mset_as_position xs P ⟹ atm_of L < length xs ⟹ L ∈# P ⟷ xs ! (atm_of L) = Some (is_pos L)›
by (induction rule: mset_as_position.induct)
(auto simp: nth_list_update' atm_of_eq_atm_of is_pos_neg_not_is_pos
dest: mset_as_position_atm_le_length)
lemma mset_as_position_tautology: ‹mset_as_position xs C ⟹ ¬tautology C›
by (induction rule: mset_as_position.induct) (auto simp: tautology_add_mset)
lemma mset_as_position_right_unique:
assumes
map: ‹mset_as_position xs D› and
map': ‹mset_as_position xs D'›
shows ‹D = D'›
proof (rule distinct_set_mset_eq)
show ‹distinct_mset D›
using mset_as_position_distinct_mset[OF map] .
show ‹distinct_mset D'›
using mset_as_position_distinct_mset[OF map'] .
show ‹set_mset D = set_mset D'›
using mset_as_position_in_iff_nth[OF map] mset_as_position_in_iff_nth[OF map']
mset_as_position_atm_le_length[OF map] mset_as_position_atm_le_length[OF map']
by blast
qed
lemma mset_as_position_mset_union:
fixes P xs
defines ‹xs' ≡ fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs›
assumes
mset: ‹mset_as_position xs P'› and
atm_P_xs: ‹∀L ∈ set P. atm_of L < length xs› and
uL_P: ‹∀L ∈ set P. -L ∉# P'› and
dist: ‹distinct P› and
tauto: ‹¬tautology (mset P)›
shows ‹mset_as_position xs' (mset P ∪# P')›
using atm_P_xs uL_P dist tauto unfolding xs'_def
proof (induction P)
case Nil
show ?case using mset by auto
next
case (Cons L P) note IH = this(1) and atm_P_xs = this(2) and uL_P = this(3) and dist = this(4)
and tauto = this(5)
then have mset:
‹mset_as_position (fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs) (mset P ∪# P')›
by (auto simp: tautology_add_mset)
show ?case
proof (cases ‹L ∈# P'›)
case True
then show ?thesis
using mset dist
by (metis (no_types, lifting) add_mset_union assms(2) distinct.simps(2) fold_simps(2)
insert_DiffM list_update_id mset.simps(2) mset_as_position_nth set_mset_mset
sup_union_right1)
next
case False
have [simp]: ‹length (fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs) = length xs›
by (induction P arbitrary: xs) auto
moreover have ‹- L ∉ set P›
using tauto by (metis list.set_intros(1) list.set_intros(2) set_mset_mset tautology_minus)
moreover have
‹fold (λL xs. xs[atm_of L := Some (is_pos L)]) P (xs[atm_of L := Some (is_pos L)]) =
(fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs) [atm_of L := Some (is_pos L)]›
using uL_P dist tauto
apply (induction P arbitrary: xs)
subgoal by auto
subgoal for L' P
by (cases ‹atm_of L = atm_of L'›)
(auto simp: tautology_add_mset list_update_swap atm_of_eq_atm_of)
done
ultimately show ?thesis
using mset atm_P_xs dist uL_P False by (auto intro!: mset_as_position.add)
qed
qed
lemma mset_as_position_empty_iff: ‹mset_as_position xs {#} ⟷ (∃n. xs = replicate n None)›
apply (rule iffI)
subgoal
by (cases rule: mset_as_position.cases, assumption) auto
subgoal
by (auto intro: mset_as_position.intros)
done
type_synonym (in -) lookup_clause_rel = ‹nat × bool option list›
definition lookup_clause_rel :: ‹nat multiset ⇒ (lookup_clause_rel × nat literal multiset) set› where
‹lookup_clause_rel 𝒜 = {((n, xs), C). n = size C ∧ mset_as_position xs C ∧
(∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs)}›
lemma lookup_clause_rel_empty_iff: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜 ⟹ n = 0 ⟷ C = {#}›
by (auto simp: lookup_clause_rel_def)
lemma conflict_atm_le_length: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜 ⟹ L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜) ⟹
L < length xs›
by (auto simp: lookup_clause_rel_def)
lemma conflict_le_length:
assumes
c_rel: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜› and
L_ℒ⇩a⇩l⇩l: ‹L ∈# ℒ⇩a⇩l⇩l 𝒜›
shows ‹atm_of L < length xs›
proof -
have
size: ‹n = size C› and
mset_pos: ‹mset_as_position xs C› and
atms_le: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs›
using c_rel unfolding lookup_clause_rel_def by blast+
have ‹atm_of L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
using L_ℒ⇩a⇩l⇩l by (simp add: atms_of_def)
then show ?thesis
using atms_le by blast
qed
lemma lookup_clause_rel_atm_in_iff:
‹((n, xs), C) ∈ lookup_clause_rel 𝒜 ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ L ∈# C ⟷ xs!(atm_of L) = Some (is_pos L)›
by (rule mset_as_position_in_iff_nth)
(auto simp: lookup_clause_rel_def atms_of_def)
lemma
assumes
c: ‹((n,xs), C) ∈ lookup_clause_rel 𝒜› and
bounded: ‹isasat_input_bounded 𝒜›
shows
lookup_clause_rel_not_tautolgy: ‹¬tautology C› and
lookup_clause_rel_distinct_mset: ‹distinct_mset C› and
lookup_clause_rel_size: ‹literals_are_in_ℒ⇩i⇩n 𝒜 C ⟹ size C ≤ 1 + uint32_max div 2›
proof -
have mset: ‹mset_as_position xs C› and ‹n = size C› and ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs›
using c unfolding lookup_clause_rel_def by fast+
show ‹¬tautology C›
using mset
apply (induction rule: mset_as_position.induct)
subgoal by (auto simp: literals_are_in_ℒ⇩i⇩n_def)
subgoal by (auto simp: tautology_add_mset)
done
show ‹distinct_mset C›
using mset mset_as_position_distinct_mset by blast
then show ‹literals_are_in_ℒ⇩i⇩n 𝒜 C ⟹ size C ≤ 1 + uint32_max div 2›
using simple_clss_size_upper_div2[of 𝒜 ‹C›] ‹¬tautology C› bounded by auto
qed
definition option_bool_rel :: ‹(bool × 'a option) set› where
‹option_bool_rel = {(b, x). b ⟷ ¬(is_None x)}›
definition NOTIN :: ‹bool option› where
[simp]: ‹NOTIN = None›
definition ISIN :: ‹bool ⇒ bool option› where
[simp]: ‹ISIN b = Some b›
definition is_NOTIN :: ‹bool option ⇒ bool› where
[simp]: ‹is_NOTIN x ⟷ x = NOTIN›
lemma is_NOTIN_alt_def:
‹is_NOTIN x ⟷ is_None x›
by (auto split: option.splits)
definition option_lookup_clause_rel where
‹option_lookup_clause_rel 𝒜 = {((b,(n,xs)), C). b = (C = None) ∧
(C = None ⟶ ((n,xs), {#}) ∈ lookup_clause_rel 𝒜) ∧
(C ≠ None ⟶ ((n,xs), the C) ∈ lookup_clause_rel 𝒜)}
›
lemma option_lookup_clause_rel_lookup_clause_rel_iff:
‹((False, (n, xs)), Some C) ∈ option_lookup_clause_rel 𝒜 ⟷
((n, xs), C) ∈ lookup_clause_rel 𝒜›
unfolding option_lookup_clause_rel_def by auto
type_synonym (in -) conflict_option_rel = ‹bool × nat × bool option list›
definition (in -) lookup_clause_assn_is_None :: ‹_ ⇒ bool› where
‹lookup_clause_assn_is_None = (λ(b, _, _). b)›
lemma lookup_clause_assn_is_None_is_None:
‹(RETURN o lookup_clause_assn_is_None, RETURN o is_None) ∈
option_lookup_clause_rel 𝒜 →⇩f ⟨bool_rel⟩nres_rel›
by (intro nres_relI frefI)
(auto simp: option_lookup_clause_rel_def lookup_clause_assn_is_None_def split: option.splits)
definition (in -) lookup_clause_assn_is_empty :: ‹_ ⇒ bool› where
‹lookup_clause_assn_is_empty = (λ(_, n, _). n = 0)›
lemma lookup_clause_assn_is_empty_is_empty:
‹(RETURN o lookup_clause_assn_is_empty, RETURN o (λD. Multiset.is_empty(the D))) ∈
[λD. D ≠ None]⇩f option_lookup_clause_rel 𝒜 → ⟨bool_rel⟩nres_rel›
by (intro nres_relI frefI)
(auto simp: option_lookup_clause_rel_def lookup_clause_assn_is_empty_def lookup_clause_rel_def
Multiset.is_empty_def split: option.splits)
definition size_lookup_conflict :: ‹_ ⇒ nat› where
‹size_lookup_conflict = (λ(_, n, _). n)›
definition size_conflict_wl_heur :: ‹_ ⇒ nat› where
‹size_conflict_wl_heur = (λ(M, N, U, D, _, _, _, _). size_lookup_conflict D)›
lemma (in -) mset_as_position_length_not_None:
‹mset_as_position x2 C ⟹ size C = length (filter ((≠) None) x2)›
proof (induction rule: mset_as_position.induct)
case (empty n)
then show ?case by auto
next
case (add xs P L xs') note m_as_p = this(1) and atm_L = this(2)
have xs_L: ‹xs ! (atm_of L) = None›
proof -
obtain bb :: ‹bool option ⇒ bool› where
f1: ‹∀z. z = None ∨ z = Some (bb z)›
by (metis option.exhaust)
have f2: ‹xs ! atm_of L ≠ Some (is_pos L)›
using add.hyps(1) add.hyps(2) add.hyps(3) mset_as_position_in_iff_nth by blast
have f3: ‹∀z b. ((Some b = z ∨ z = None) ∨ bb z) ∨ b›
using f1 by blast
have f4: ‹∀zs. (zs ! atm_of L ≠ Some (is_pos (- L)) ∨ ¬ atm_of L < length zs)
∨ ¬ mset_as_position zs P›
by (metis add.hyps(4) atm_of_uminus mset_as_position_in_iff_nth)
have ‹∀z b. ((Some b = z ∨ z = None) ∨ ¬ bb z) ∨ ¬ b›
using f1 by blast
then show ?thesis
using f4 f3 f2 by (metis add.hyps(1) add.hyps(2) is_pos_neg_not_is_pos)
qed
obtain xs1 xs2 where
xs_xs12: ‹xs = xs1 @ None # xs2› and
xs1: ‹length xs1 = atm_of L›
using atm_L upd_conv_take_nth_drop[of ‹atm_of L› xs ‹None›] apply -
apply (subst(asm)(2) xs_L[symmetric])
by (force simp del: append_take_drop_id)+
then show ?case
using add by (auto simp: list_update_append)
qed
definition (in -) is_in_lookup_conflict where
‹is_in_lookup_conflict = (λ(n, xs) L. ¬is_None (xs ! atm_of L))›
lemma mset_as_position_remove:
‹mset_as_position xs D ⟹ L < length xs ⟹
mset_as_position (xs[L := None]) (remove1_mset (Pos L) (remove1_mset (Neg L) D))›
proof (induction rule: mset_as_position.induct)
case (empty n)
then have [simp]: ‹(replicate n None)[L := None] = replicate n None›
using list_update_id[of ‹replicate n None› L] by auto
show ?case by (auto intro: mset_as_position.intros)
next
case (add xs P K xs')
show ?case
proof (cases ‹L = atm_of K›)
case True
then show ?thesis
using add by (cases K) auto
next
case False
have map: ‹mset_as_position (xs[L := None]) (remove1_mset (Pos L) (remove1_mset (Neg L) P))›
using add by auto
have ‹K ∉# P - {#Pos L, Neg L#}› ‹-K ∉# P - {#Pos L, Neg L#}›
by (auto simp: add.hyps dest!: in_diffD)
then show ?thesis
using mset_as_position.add[OF map, of ‹K› ‹xs[L := None, atm_of K := Some (is_pos K)]›]
add False list_update_swap[of ‹atm_of K› L xs] apply simp
apply (subst diff_add_mset_swap)
by auto
qed
qed
lemma mset_as_position_remove2:
‹mset_as_position xs D ⟹ atm_of L < length xs ⟹
mset_as_position (xs[atm_of L := None]) (D - {#L, -L#})›
using mset_as_position_remove[of xs D ‹atm_of (-L)›]
by (smt add_mset_commute add_mset_diff_bothsides atm_of_uminus insert_DiffM
literal.exhaust_sel minus_notin_trivial2 remove_1_mset_id_iff_notin uminus_not_id')
definition (in -) delete_from_lookup_conflict
:: ‹nat literal ⇒ lookup_clause_rel ⇒ lookup_clause_rel nres› where
‹delete_from_lookup_conflict = (λL (n, xs). do {
ASSERT(n≥1);
ASSERT(atm_of L < length xs);
RETURN (n - 1, xs[atm_of L := None])
})›
lemma delete_from_lookup_conflict_op_mset_delete:
‹(uncurry delete_from_lookup_conflict, uncurry (RETURN oo remove1_mset)) ∈
[λ(L, D). -L ∉# D ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ L ∈# D]⇩f Id ×⇩f lookup_clause_rel 𝒜 →
⟨lookup_clause_rel 𝒜⟩nres_rel›
apply (intro frefI nres_relI)
subgoal for x y
using mset_as_position_remove[of ‹snd (snd x)› ‹snd y› ‹atm_of (fst y)›]
apply (cases x; cases y; cases ‹fst y›)
by (auto simp: delete_from_lookup_conflict_def lookup_clause_rel_def
dest!: multi_member_split
intro!: ASSERT_refine_left)
done
definition delete_from_lookup_conflict_pre where
‹delete_from_lookup_conflict_pre 𝒜 = (λ(a, b). - a ∉# b ∧ a ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ a ∈# b)›
definition set_conflict_m
:: ‹(nat, nat) ann_lits ⇒ nat clauses_l ⇒ nat ⇒ nat clause option ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (nat clause option × nat × lbd × out_learned) nres›
where
‹set_conflict_m M N i _ _ _ _ =
SPEC (λ(C, n, lbd, outl). C = Some (mset (N∝i)) ∧ n = card_max_lvl M (mset (N∝i)) ∧
out_learned M C outl)›
definition merge_conflict_m
:: ‹(nat, nat) ann_lits ⇒ nat clauses_l ⇒ nat ⇒ nat clause option ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (nat clause option × nat × lbd × out_learned) nres›
where
‹merge_conflict_m M N i D _ _ _ =
SPEC (λ(C, n, lbd, outl). C = Some (mset (tl (N∝i)) ∪# the D) ∧
n = card_max_lvl M (mset (tl (N∝i)) ∪# the D) ∧
out_learned M C outl)›
definition merge_conflict_m_g
:: ‹nat ⇒ (nat, nat) ann_lits ⇒ nat clause_l ⇒ nat clause option ⇒
(nat clause option × nat × lbd × out_learned) nres›
where
‹merge_conflict_m_g init M Ni D =
SPEC (λ(C, n, lbd, outl). C = Some (mset (drop init (Ni)) ∪# the D) ∧
n = card_max_lvl M (mset (drop init (Ni)) ∪# the D) ∧
out_learned M C outl)›
definition add_to_lookup_conflict :: ‹nat literal ⇒ lookup_clause_rel ⇒ lookup_clause_rel› where
‹add_to_lookup_conflict = (λL (n, xs). (if xs ! atm_of L = NOTIN then n + 1 else n,
xs[atm_of L := ISIN (is_pos L)]))›
definition lookup_conflict_merge'_step
:: ‹nat multiset ⇒ nat ⇒ (nat, nat) ann_lits ⇒ nat ⇒ nat ⇒ lookup_clause_rel ⇒ nat clause_l ⇒
nat clause ⇒ out_learned ⇒ bool›
where
‹lookup_conflict_merge'_step 𝒜 init M i clvls zs D C outl = (
let D' = mset (take (i - init) (drop init D));
E = remdups_mset (D' + C) in
((False, zs), Some E) ∈ option_lookup_clause_rel 𝒜 ∧
out_learned M (Some E) outl ∧
literals_are_in_ℒ⇩i⇩n 𝒜 E ∧ clvls = card_max_lvl M E)›
lemma option_lookup_clause_rel_update_None:
assumes ‹((False, (n, xs)), Some D) ∈ option_lookup_clause_rel 𝒜› and L_xs : ‹L < length xs›
shows ‹((False, (if xs!L = None then n else n - 1, xs[L := None])),
Some (D - {# Pos L, Neg L #})) ∈ option_lookup_clause_rel 𝒜›
proof -
have [simp]: ‹L ∉# A ⟹ A - add_mset L' (add_mset L B) = A - add_mset L' B›
for A B :: ‹'a multiset› and L L'
by (metis add_mset_commute minus_notin_trivial)
have ‹n = size D› and map: ‹mset_as_position xs D›
using assms by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def)
have xs_None_iff: ‹xs ! L = None ⟷ Pos L ∉# D ∧ Neg L ∉# D›
using map L_xs mset_as_position_in_iff_nth[of xs D ‹Pos L›]
mset_as_position_in_iff_nth[of xs D ‹Neg L›]
by (cases ‹xs ! L›) auto
have 1: ‹xs ! L = None ⟹ D - {#Pos L, Neg L#} = D›
using assms by (auto simp: xs_None_iff minus_notin_trivial)
have 2: ‹xs ! L = None ⟹ xs[L := None] = xs›
using map list_update_id[of xs L] by (auto simp: 1)
have 3: ‹xs ! L = Some y ⟷ (y ∧ Pos L ∈# D ∧ Neg L ∉# D) ∨ (¬y ∧ Pos L ∉# D ∧ Neg L ∈# D)›
for y
using map L_xs mset_as_position_in_iff_nth[of xs D ‹Pos L›]
mset_as_position_in_iff_nth[of xs D ‹Neg L›]
by (cases ‹xs ! L›) auto
show ?thesis
using assms mset_as_position_remove[of xs D L]
by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def 1 2 3 size_remove1_mset_If
minus_notin_trivial mset_as_position_remove)
qed
lemma add_to_lookup_conflict_lookup_clause_rel:
assumes
confl: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜› and
uL_C: ‹-L ∉# C› and
L_ℒ⇩a⇩l⇩l: ‹L ∈# ℒ⇩a⇩l⇩l 𝒜›
shows ‹(add_to_lookup_conflict L (n, xs), {#L#} ∪# C) ∈ lookup_clause_rel 𝒜›
proof -
have
n: ‹n = size C› and
mset: ‹mset_as_position xs C› and
atm: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs›
using confl unfolding lookup_clause_rel_def by blast+
have ‹distinct_mset C›
using mset by (blast dest: mset_as_position_distinct_mset)
have atm_L_xs: ‹atm_of L < length xs›
using atm L_ℒ⇩a⇩l⇩l by (auto simp: atms_of_def)
then show ?thesis
proof (cases ‹L ∈# C›)
case True
with mset have xs: ‹xs ! atm_of L = Some (is_pos L)› ‹xs ! atm_of L ≠ None›
by (auto dest: mset_as_position_nth)
moreover have ‹{#L#} ∪# C = C›
using True by (simp add: subset_mset.sup.absorb2)
ultimately show ?thesis
using n mset atm True
by (auto simp: lookup_clause_rel_def add_to_lookup_conflict_def xs[symmetric])
next
case False
with mset have ‹xs ! atm_of L = None›
using mset_as_position_in_iff_nth[of xs C L]
mset_as_position_in_iff_nth[of xs C ‹-L›] atm_L_xs uL_C
by (cases L; cases ‹xs ! atm_of L›) auto
then show ?thesis
using n mset atm False atm_L_xs uL_C
by (auto simp: lookup_clause_rel_def add_to_lookup_conflict_def
intro!: mset_as_position.intros)
qed
qed
definition outlearned_add
:: ‹(nat,nat)ann_lits ⇒ nat literal ⇒ nat × bool option list ⇒ out_learned ⇒ out_learned› where
‹outlearned_add = (λM L zs outl.
(if get_level M L < count_decided M ∧ ¬is_in_lookup_conflict zs L then outl @ [L]
else outl))›
definition clvls_add
:: ‹(nat,nat)ann_lits ⇒ nat literal ⇒ nat × bool option list ⇒ nat ⇒ nat› where
‹clvls_add = (λM L zs clvls.
(if get_level M L = count_decided M ∧ ¬is_in_lookup_conflict zs L then clvls + 1
else clvls))›
definition lookup_conflict_merge
:: ‹nat ⇒ (nat,nat)ann_lits ⇒ nat clause_l ⇒ conflict_option_rel ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (conflict_option_rel × nat × lbd × out_learned) nres›
where
‹lookup_conflict_merge init M D = (λ(b, xs) clvls lbd outl. do {
(_, clvls, zs, lbd, outl) ← WHILE⇩T⇗λ(i::nat, clvls :: nat, zs, lbd, outl).
length (snd zs) = length (snd xs) ∧
Suc i ≤ uint32_max ∧ Suc (fst zs) ≤ uint32_max ∧ Suc clvls ≤ uint32_max⇖
(λ(i :: nat, clvls, zs, lbd, outl). i < length_uint32_nat D)
(λ(i :: nat, clvls, zs, lbd, outl). do {
ASSERT(i < length_uint32_nat D);
ASSERT(Suc i ≤ uint32_max);
let lbd = lbd_write lbd (get_level M (D!i));
ASSERT(¬is_in_lookup_conflict zs (D!i) ⟶ length outl < uint32_max);
let outl = outlearned_add M (D!i) zs outl;
let clvls = clvls_add M (D!i) zs clvls;
let zs = add_to_lookup_conflict (D!i) zs;
RETURN(Suc i, clvls, zs, lbd, outl)
})
(init, clvls, xs, lbd, outl);
RETURN ((False, zs), clvls, lbd, outl)
})›
definition resolve_lookup_conflict_aa
:: ‹(nat,nat)ann_lits ⇒ nat clauses_l ⇒ nat ⇒ conflict_option_rel ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (conflict_option_rel × nat × lbd × out_learned) nres›
where
‹resolve_lookup_conflict_aa M N i xs clvls lbd outl =
lookup_conflict_merge 1 M (N ∝ i) xs clvls lbd outl›
definition set_lookup_conflict_aa
:: ‹(nat,nat)ann_lits ⇒ nat clauses_l ⇒ nat ⇒ conflict_option_rel ⇒ nat ⇒ lbd ⇒
out_learned ⇒(conflict_option_rel × nat × lbd × out_learned) nres›
where
‹set_lookup_conflict_aa M C i xs clvls lbd outl =
lookup_conflict_merge 0 M (C∝i) xs clvls lbd outl›
definition isa_outlearned_add
:: ‹trail_pol ⇒ nat literal ⇒ nat × bool option list ⇒ out_learned ⇒ out_learned› where
‹isa_outlearned_add = (λM L zs outl.
(if get_level_pol M L < count_decided_pol M ∧ ¬is_in_lookup_conflict zs L then outl @ [L]
else outl))›
lemma isa_outlearned_add_outlearned_add:
‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹
isa_outlearned_add M' L zs outl = outlearned_add M L zs outl›
by (auto simp: isa_outlearned_add_def outlearned_add_def get_level_get_level_pol
count_decided_trail_ref[THEN fref_to_Down_unRET_Id])
definition isa_clvls_add
:: ‹trail_pol ⇒ nat literal ⇒ nat × bool option list ⇒ nat ⇒ nat› where
‹isa_clvls_add = (λM L zs clvls.
(if get_level_pol M L = count_decided_pol M ∧ ¬is_in_lookup_conflict zs L then clvls + 1
else clvls))›
lemma isa_clvls_add_clvls_add:
‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹
isa_clvls_add M' L zs outl = clvls_add M L zs outl›
by (auto simp: isa_clvls_add_def clvls_add_def get_level_get_level_pol
count_decided_trail_ref[THEN fref_to_Down_unRET_Id])
definition isa_lookup_conflict_merge
:: ‹nat ⇒ trail_pol ⇒ arena ⇒ nat ⇒ conflict_option_rel ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (conflict_option_rel × nat × lbd × out_learned) nres›
where
‹isa_lookup_conflict_merge init M N i = (λ(b, xs) clvls lbd outl. do {
ASSERT( arena_is_valid_clause_idx N i);
(_, clvls, zs, lbd, outl) ← WHILE⇩T⇗λ(i::nat, clvls :: nat, zs, lbd, outl).
length (snd zs) = length (snd xs) ∧
Suc (fst zs) ≤ uint32_max ∧ Suc clvls ≤ uint32_max⇖
(λ(j :: nat, clvls, zs, lbd, outl). j < i + arena_length N i)
(λ(j :: nat, clvls, zs, lbd, outl). do {
ASSERT(j < length N);
ASSERT(arena_lit_pre N j);
ASSERT(get_level_pol_pre (M, arena_lit N j));
ASSERT(get_level_pol M (arena_lit N j) ≤ Suc (uint32_max div 2));
let lbd = lbd_write lbd (get_level_pol M (arena_lit N j));
ASSERT(atm_of (arena_lit N j) < length (snd zs));
ASSERT(¬is_in_lookup_conflict zs (arena_lit N j) ⟶ length outl < uint32_max);
let outl = isa_outlearned_add M (arena_lit N j) zs outl;
let clvls = isa_clvls_add M (arena_lit N j) zs clvls;
let zs = add_to_lookup_conflict (arena_lit N j) zs;
RETURN(Suc j, clvls, zs, lbd, outl)
})
(i+init, clvls, xs, lbd, outl);
RETURN ((False, zs), clvls, lbd, outl)
})›
lemma isa_lookup_conflict_merge_lookup_conflict_merge_ext:
assumes valid: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
bxs: ‹((b, xs), C) ∈ option_lookup_clause_rel 𝒜› and
M'M: ‹(M', M) ∈ trail_pol 𝒜› and
bound: ‹isasat_input_bounded 𝒜›
shows
‹isa_lookup_conflict_merge init M' arena i (b, xs) clvls lbd outl ≤ ⇓ Id
(lookup_conflict_merge init M (N ∝ i) (b, xs) clvls lbd outl)›
proof -
have [refine0]: ‹((i + init, clvls, xs, lbd, outl), init, clvls, xs, lbd, outl) ∈
{(k, l). k = l + i} ×⇩r nat_rel ×⇩r Id ×⇩r Id ×⇩r Id›
by auto
have ‹no_dup M›
using assms by (auto simp: trail_pol_def)
have ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M›
using M'M by (auto simp: trail_pol_def literals_are_in_ℒ⇩i⇩n_trail_def)
from literals_are_in_ℒ⇩i⇩n_trail_get_level_uint32_max[OF bound this ‹no_dup M›]
have lev_le: ‹get_level M L ≤ Suc (uint32_max div 2)› for L .
show ?thesis
unfolding isa_lookup_conflict_merge_def lookup_conflict_merge_def prod.case
apply refine_vcg
subgoal using assms unfolding arena_is_valid_clause_idx_def by fast
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using valid i by (auto simp: arena_lifting)
subgoal using valid i by (auto simp: arena_lifting ac_simps)
subgoal using valid i
by (auto simp: arena_lifting arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
intro!: exI[of _ i])
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g
using i literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of 𝒜 N i x1] lits valid M'M
by (auto simp: arena_lifting ac_simps image_image intro!: get_level_pol_pre)
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g'
using valid i literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of 𝒜 N i x1] lits
by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff arena_lifting ac_simps get_level_get_level_pol[OF M'M, symmetric]
isa_outlearned_add_outlearned_add[OF M'M] isa_clvls_add_clvls_add[OF M'M] lev_le)
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g
using i literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of 𝒜 N i x1] lits valid M'M
using bxs by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff arena_lifting ac_simps)
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g'
using valid i literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of 𝒜 N i x1] lits
by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff arena_lifting ac_simps get_level_get_level_pol[OF M'M]
isa_outlearned_add_outlearned_add[OF M'M] isa_clvls_add_clvls_add[OF M'M])
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g'
using valid i literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of 𝒜 N i x1] lits
by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff arena_lifting ac_simps get_level_get_level_pol[OF M'M]
isa_outlearned_add_outlearned_add[OF M'M] isa_clvls_add_clvls_add[OF M'M])
subgoal using bxs by (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff get_level_get_level_pol[OF M'M])
done
qed
lemma (in -) arena_is_valid_clause_idx_le_uint64_max:
‹arena_is_valid_clause_idx be bd ⟹
length be ≤ uint64_max ⟹
bd + arena_length be bd ≤ uint64_max›
‹arena_is_valid_clause_idx be bd ⟹ length be ≤ uint64_max ⟹
bd ≤ uint64_max›
using arena_lifting(10)[of be _ _ bd]
by (fastforce simp: arena_lifting arena_is_valid_clause_idx_def)+
definition isa_set_lookup_conflict_aa where
‹isa_set_lookup_conflict_aa = isa_lookup_conflict_merge 0›
definition isa_set_lookup_conflict_aa_pre where
‹isa_set_lookup_conflict_aa_pre =
(λ((((((M, N), i), (_, xs)), _), _), out). i < length N)›
lemma lookup_conflict_merge'_spec:
assumes
o: ‹((b, n, xs), Some C) ∈ option_lookup_clause_rel 𝒜› and
dist: ‹distinct D› and
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset D)› and
tauto: ‹¬tautology (mset D)› and
lits_C: ‹literals_are_in_ℒ⇩i⇩n 𝒜 C› and
‹clvls = card_max_lvl M C› and
CD: ‹⋀L. L ∈ set (drop init D) ⟹ -L ∉# C› and
‹Suc init ≤ uint32_max› and
‹out_learned M (Some C) outl› and
bounded: ‹isasat_input_bounded 𝒜›
shows
‹lookup_conflict_merge init M D (b, n, xs) clvls lbd outl ≤
⇓(option_lookup_clause_rel 𝒜 ×⇩r Id ×⇩r Id)
(merge_conflict_m_g init M D (Some C))›
(is ‹_ ≤ ⇓ ?Ref ?Spec›)
proof -
define lbd_upd where
‹lbd_upd lbd i ≡ lbd_write lbd (get_level M (D!i))› for lbd i
let ?D = ‹drop init D›
have le_D_le_upper[simp]: ‹a < length D ⟹ Suc (Suc a) ≤ uint32_max› for a
using simple_clss_size_upper_div2[of 𝒜 ‹mset D›] assms by (auto simp: uint32_max_def)
have Suc_N_uint32_max: ‹Suc n ≤ uint32_max› and
size_C_uint32_max: ‹size C ≤ 1 + uint32_max div 2› and
clvls: ‹clvls = card_max_lvl M C› and
tauto_C: ‹¬ tautology C› and
dist_C: ‹distinct_mset C› and
atms_le_xs: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs› and
map: ‹mset_as_position xs C›
using assms simple_clss_size_upper_div2[of 𝒜 C] mset_as_position_distinct_mset[of xs C]
lookup_clause_rel_not_tautolgy[of n xs C] bounded
unfolding option_lookup_clause_rel_def lookup_clause_rel_def
by (auto simp: uint32_max_def)
then have clvls_uint32_max: ‹clvls ≤ 1 + uint32_max div 2›
using size_filter_mset_lesseq[of ‹λL. get_level M L = count_decided M› C]
unfolding uint32_max_def card_max_lvl_def by linarith
have [intro]: ‹((b, a, ba), Some C) ∈ option_lookup_clause_rel 𝒜 ⟹ literals_are_in_ℒ⇩i⇩n 𝒜 C ⟹
Suc (Suc a) ≤ uint32_max› for b a ba C
using lookup_clause_rel_size[of a ba C, OF _ bounded] by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def uint32_max_def)
have [simp]: ‹remdups_mset C = C›
using o mset_as_position_distinct_mset[of xs C] by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def distinct_mset_remdups_mset_id)
have ‹¬tautology C›
using mset_as_position_tautology o by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def)
have ‹distinct_mset C›
using mset_as_position_distinct_mset[of _ C] o
unfolding option_lookup_clause_rel_def lookup_clause_rel_def by auto
let ?C' = ‹λa. (mset (take (a - init) (drop init D)) + C)›
have tauto_C': ‹¬ tautology (?C' a)› if ‹a ≥ init› for a
using that tauto tauto_C dist dist_C CD unfolding tautology_decomp'
by (force dest: in_set_takeD in_diffD dest: in_set_dropD
simp: distinct_mset_in_diff in_image_uminus_uminus)
define I where
‹I xs = (λ(i, clvls, zs :: lookup_clause_rel, lbd :: lbd, outl :: out_learned).
length (snd zs) =
length (snd xs) ∧
Suc i ≤ uint32_max ∧
Suc (fst zs) ≤ uint32_max ∧
Suc clvls ≤ uint32_max)›
for xs :: lookup_clause_rel
define I' where ‹I' = (λ(i, clvls, zs, lbd :: lbd, outl).
lookup_conflict_merge'_step 𝒜 init M i clvls zs D C outl ∧ i ≥ init)›
have dist_D: ‹distinct_mset (mset D)›
using dist by auto
have dist_CD: ‹distinct_mset (C - mset D - uminus `# mset D)›
using ‹distinct_mset C› by auto
have [simp]: ‹remdups_mset (mset (drop init D) + C) = mset (drop init D) ∪# C›
apply (rule distinct_mset_rempdups_union_mset[symmetric])
using dist_C dist by auto
have ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (take (a - init) (drop init D)) ∪# C)› for a
using lits_C lits by (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_m_def
dest!: in_set_takeD in_set_dropD)
then have size_outl_le: ‹size (mset (take (a - init) (drop init D)) ∪# C) ≤ Suc uint32_max div 2› if ‹a ≥ init› for a
using simple_clss_size_upper_div2[OF bounded, of ‹mset (take (a - init) (drop init D)) ∪# C›]
tauto_C'[OF that] ‹distinct_mset C› dist_D
by (auto simp: uint32_max_def)
have
if_True_I: ‹I x2 (Suc a, clvls_add M (D ! a) baa aa,
add_to_lookup_conflict (D ! a) baa, lbd_upd lbd' a,
outlearned_add M (D ! a) baa outl)› (is ?I) and
if_true_I': ‹I' (Suc a, clvls_add M (D ! a) baa aa,
add_to_lookup_conflict (D ! a) baa, lbd_upd lbd' a,
outlearned_add M (D ! a) baa outl)› (is ?I')
if
I: ‹I x2 s› and
I': ‹I' s› and
cond: ‹case s of (i, clvls, zs, lbd, outl) ⇒ i < length D› and
s: ‹s = (a, ba)› ‹ba = (aa, baa2)› ‹baa2 = (baa, lbdL')› ‹(b, n, xs) = (x1, x2)›
‹lbdL' = (lbd', outl)› and
a_le_D: ‹a < length D› and
a_uint32_max: ‹Suc a ≤ uint32_max›
for x1 x2 s a ba aa baa baa2 lbd' lbdL' outl
proof -
have [simp]:
‹s = (a, aa, baa, lbd', outl)›
‹ba = (aa, baa, lbd', outl)›
‹x2 = (n, xs)›
using s by auto
obtain ab b where baa[simp]: ‹baa = (ab, b)› by (cases baa)
have aa: ‹aa = card_max_lvl M (remdups_mset (?C' a))› and
ocr: ‹((False, ab, b), Some (remdups_mset (?C' a))) ∈ option_lookup_clause_rel 𝒜› and
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (remdups_mset (?C' a))› and
outl: ‹out_learned M (Some (remdups_mset (?C' a))) outl›
using I'
unfolding I'_def lookup_conflict_merge'_step_def Let_def
by auto
have
ab: ‹ab = size (remdups_mset (?C' a))› and
map: ‹mset_as_position b (remdups_mset (?C' a))› and
‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length b› and
cr: ‹((ab, b), remdups_mset (?C' a)) ∈ lookup_clause_rel 𝒜›
using ocr unfolding option_lookup_clause_rel_def lookup_clause_rel_def
by auto
have a_init: ‹a ≥ init›
using I' unfolding I'_def by auto
have ‹size (card_max_lvl M (remdups_mset (?C' a))) ≤ size (remdups_mset (?C' a))›
unfolding card_max_lvl_def
by auto
then have [simp]: ‹Suc (Suc aa) ≤ uint32_max› ‹Suc aa ≤ uint32_max›
using size_C_uint32_max lits a_init
simple_clss_size_upper_div2[of 𝒜 ‹remdups_mset (?C' a)›, OF bounded]
unfolding uint32_max_def aa[symmetric]
by (auto simp: tauto_C')
have [simp]: ‹length b = length xs›
using I unfolding I_def by simp_all
have ab_upper: ‹Suc (Suc ab) ≤ uint32_max›
using simple_clss_size_upper_div2[OF bounded, of ‹remdups_mset (?C' a)›]
lookup_clause_rel_not_tautolgy[OF cr bounded] a_le_D lits mset_as_position_distinct_mset[OF map]
unfolding ab literals_are_in_ℒ⇩i⇩n_remdups uint32_max_def by auto
show ?I
using le_D_le_upper a_le_D ab_upper a_init
unfolding I_def add_to_lookup_conflict_def baa clvls_add_def by auto
have take_Suc_a[simp]: ‹take (Suc a - init) ?D = take (a - init) ?D @ [D ! a]›
by (smt Suc_diff_le a_init a_le_D append_take_drop_id diff_less_mono drop_take_drop_drop
length_drop same_append_eq take_Suc_conv_app_nth take_hd_drop)
have [simp]: ‹D ! a ∉ set (take (a - init) ?D)›
using dist tauto a_le_D apply (subst (asm) append_take_drop_id[symmetric, of _ ‹Suc a - init›],
subst append_take_drop_id[symmetric, of _ ‹Suc a - init›])
apply (subst (asm) distinct_append, subst nth_append)
by (auto simp: in_set_distinct_take_drop_iff)
have [simp]: ‹- D ! a ∉ set (take (a - init) ?D)›
proof
assume ‹- D ! a ∈ set (take (a - init) (drop init D))›
then have "(if is_pos (D ! a) then Neg else Pos) (atm_of (D ! a)) ∈ set D"
by (metis (no_types) in_set_dropD in_set_takeD uminus_literal_def)
then show False
using a_le_D tauto by force
qed
have D_a_notin: ‹D ! a ∉# (mset (take (a - init) ?D) + uminus `# mset (take (a - init) ?D))›
by (auto simp: uminus_lit_swap[symmetric])
have uD_a_notin: ‹-D ! a ∉# (mset (take (a - init) ?D) + uminus `# mset (take (a - init) ?D))›
by (auto simp: uminus_lit_swap[symmetric])
show ?I'
proof (cases ‹(get_level M (D ! a) = count_decided M ∧ ¬ is_in_lookup_conflict baa (D ! a))›)
case if_cond: True
have [simp]: ‹D ! a ∉# C› ‹-D ! a ∉# C› ‹b ! atm_of (D ! a) = None›
using if_cond mset_as_position_nth[OF map, of ‹D ! a›]
if_cond mset_as_position_nth[OF map, of ‹-D ! a›] D_a_notin uD_a_notin
by (auto simp: is_in_lookup_conflict_def split: option.splits bool.splits
dest: in_diffD)
have [simp]: ‹atm_of (D ! a) < length xs› ‹D ! a ∈# ℒ⇩a⇩l⇩l 𝒜›
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[OF ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset D)› a_le_D] atms_le_xs
by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
have ocr: ‹((False, add_to_lookup_conflict (D ! a) (ab, b)), Some (remdups_mset (?C' (Suc a))))
∈ option_lookup_clause_rel 𝒜›
using ocr D_a_notin uD_a_notin
unfolding option_lookup_clause_rel_def lookup_clause_rel_def add_to_lookup_conflict_def
by (auto dest: in_diffD simp: minus_notin_trivial
intro!: mset_as_position.intros)
have ‹out_learned M (Some (remdups_mset (?C' (Suc a)))) (outlearned_add M (D ! a) (ab, b) outl)›
using D_a_notin uD_a_notin ocr lits if_cond a_init outl
unfolding outlearned_add_def out_learned_def
by auto
then show ?I'
using D_a_notin uD_a_notin ocr lits if_cond a_init
unfolding I'_def lookup_conflict_merge'_step_def Let_def clvls_add_def
by (auto simp: minus_notin_trivial literals_are_in_ℒ⇩i⇩n_add_mset
card_max_lvl_add_mset aa)
next
case if_cond: False
have atm_D_a_le_xs: ‹atm_of (D ! a) < length xs› ‹D ! a ∈# ℒ⇩a⇩l⇩l 𝒜›
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[OF ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset D)› a_le_D] atms_le_xs
by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
have [simp]: ‹D ! a ∉# C - add_mset (- D ! a)
(add_mset (D ! a)
(mset (take a D) + uminus `# mset (take a D)))›
using dist_C in_diffD[of ‹D ! a› C ‹add_mset (- D ! a)
(mset (take a D) + uminus `# mset (take a D))›,
THEN multi_member_split]
by (meson distinct_mem_diff_mset member_add_mset)
have a_init: ‹a ≥ init›
using I' unfolding I'_def by auto
have take_Suc_a[simp]: ‹take (Suc a - init) ?D = take (a - init) ?D @ [D ! a]›
by (smt Suc_diff_le a_init a_le_D append_take_drop_id diff_less_mono drop_take_drop_drop
length_drop same_append_eq take_Suc_conv_app_nth take_hd_drop)
have [iff]: ‹D ! a ∉ set (take (a - init) ?D)›
using dist tauto a_le_D
apply (subst (asm) append_take_drop_id[symmetric, of _ ‹Suc a - init›],
subst append_take_drop_id[symmetric, of _ ‹Suc a - init›])
apply (subst (asm) distinct_append, subst nth_append)
by (auto simp: in_set_distinct_take_drop_iff)
have [simp]: ‹- D ! a ∉ set (take (a - init) ?D)›
proof
assume "- D ! a ∈ set (take (a - init) (drop init D))"
then have "(if is_pos (D ! a) then Neg else Pos) (atm_of (D ! a)) ∈ set D"
by (metis (no_types) in_set_dropD in_set_takeD uminus_literal_def)
then show False
using a_le_D tauto by force
qed
have ‹D ! a ∈ set (drop init D)›
using a_init a_le_D by (meson in_set_drop_conv_nth)
from CD[OF this] have [simp]: ‹-D ! a ∉# C› .
consider
(None) ‹b ! atm_of (D ! a) = None› |
(Some_in) i where ‹b ! atm_of (D ! a) = Some i› and
‹(if i then Pos (atm_of (D ! a)) else Neg (atm_of (D ! a))) ∈# C›
using if_cond mset_as_position_in_iff_nth[OF map, of ‹D ! a›]
if_cond mset_as_position_in_iff_nth[OF map, of ‹-D ! a›] atm_D_a_le_xs(1)
by (cases ‹b ! atm_of (D ! a)›) (auto simp: is_pos_neg_not_is_pos)
then have ocr: ‹((False, add_to_lookup_conflict (D ! a) (ab, b)),
Some (remdups_mset (?C' (Suc a)))) ∈ option_lookup_clause_rel 𝒜›
proof cases
case [simp]: None
have [simp]: ‹D ! a ∉# C›
using if_cond mset_as_position_nth[OF map, of ‹D ! a›]
if_cond mset_as_position_nth[OF map, of ‹-D ! a›]
by (auto simp: is_in_lookup_conflict_def split: option.splits bool.splits
dest: in_diffD)
have [simp]: ‹atm_of (D ! a) < length xs› ‹D ! a ∈# ℒ⇩a⇩l⇩l 𝒜›
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[OF ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset D)› a_le_D] atms_le_xs
by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
show ocr: ‹((False, add_to_lookup_conflict (D ! a) (ab, b)),
Some (remdups_mset (?C' (Suc a)))) ∈ option_lookup_clause_rel 𝒜›
using ocr
unfolding option_lookup_clause_rel_def lookup_clause_rel_def add_to_lookup_conflict_def
by (auto dest: in_diffD simp: minus_notin_trivial
intro!: mset_as_position.intros)
next
case Some_in
then have ‹remdups_mset (?C' a) = remdups_mset (?C' (Suc a))›
using if_cond mset_as_position_in_iff_nth[OF map, of ‹D ! a›] a_init
if_cond mset_as_position_in_iff_nth[OF map, of ‹-D ! a›] atm_D_a_le_xs(1)
by (auto simp: is_neg_neg_not_is_neg)
moreover
have 1: ‹Some i = Some (is_pos (D ! a))›
using if_cond mset_as_position_in_iff_nth[OF map, of ‹D ! a›] a_init Some_in
if_cond mset_as_position_in_iff_nth[OF map, of ‹-D ! a›] atm_D_a_le_xs(1)
‹D ! a ∉ set (take (a - init) ?D)› ‹-D ! a ∉# C›
‹- D ! a ∉ set (take (a - init) ?D)›
by (cases ‹D ! a›) (auto simp: is_neg_neg_not_is_neg)
moreover have ‹b[atm_of (D ! a) := Some i] = b›
unfolding 1[symmetric] Some_in(1)[symmetric] by simp
ultimately show ?thesis
using dist_C atms_le_xs Some_in(1) map
unfolding option_lookup_clause_rel_def lookup_clause_rel_def add_to_lookup_conflict_def ab
by (auto simp: distinct_mset_in_diff minus_notin_trivial
intro: mset_as_position.intros
simp del: remdups_mset_singleton_sum)
qed
have notin_lo_in_C: ‹¬is_in_lookup_conflict (ab, b) (D ! a) ⟹ D ! a ∉# C›
using mset_as_position_in_iff_nth[OF map, of ‹Pos (atm_of (D!a))›]
mset_as_position_in_iff_nth[OF map, of ‹Neg (atm_of (D!a))›] atm_D_a_le_xs(1)
‹- D ! a ∉ set (take (a - init) (drop init D))›
‹D ! a ∉ set (take (a - init) (drop init D))›
‹-D ! a ∉# C› a_init
by (cases ‹b ! (atm_of (D ! a))›; cases ‹D ! a›)
(auto simp: is_in_lookup_conflict_def dist_C distinct_mset_in_diff
split: option.splits bool.splits
dest: in_diffD)
have in_lo_in_C: ‹is_in_lookup_conflict (ab, b) (D ! a) ⟹ D ! a ∈# C›
using mset_as_position_in_iff_nth[OF map, of ‹Pos (atm_of (D!a))›]
mset_as_position_in_iff_nth[OF map, of ‹Neg (atm_of (D!a))›] atm_D_a_le_xs(1)
‹- D ! a ∉ set (take (a - init) (drop init D))›
‹D ! a ∉ set (take (a - init) (drop init D))›
‹-D ! a ∉# C› a_init
by (cases ‹b ! (atm_of (D ! a))›; cases ‹D ! a›)
(auto simp: is_in_lookup_conflict_def dist_C distinct_mset_in_diff
split: option.splits bool.splits
dest: in_diffD)
moreover have ‹out_learned M (Some (remdups_mset (?C' (Suc a))))
(outlearned_add M (D ! a) (ab, b) outl)›
using D_a_notin uD_a_notin ocr lits if_cond a_init outl in_lo_in_C notin_lo_in_C
unfolding outlearned_add_def out_learned_def
by auto
ultimately show ?I'
using ocr lits if_cond atm_D_a_le_xs a_init
unfolding I'_def lookup_conflict_merge'_step_def Let_def clvls_add_def
by (auto simp: minus_notin_trivial literals_are_in_ℒ⇩i⇩n_add_mset
card_max_lvl_add_mset aa)
qed
qed
have uL_C_if_L_C: ‹-L ∉# C› if ‹L ∈# C› for L
using tauto_C that unfolding tautology_decomp' by blast
have outl_le: ‹length bc < uint32_max›
if
‹I x2 s› and
‹I' s› and
‹s = (a, ba)› and
‹ba = (aa, baa)› and
‹baa = (ab, bb)› and
‹bb = (ac, bc)› for x1 x2 s a ba aa baa ab bb ac bc
proof -
have ‹mset (tl bc) ⊆# (remdups_mset (mset (take (a -init) (drop init D)) + C))› and ‹init ≤ a›
using that by (auto simp: I_def I'_def lookup_conflict_merge'_step_def Let_def out_learned_def)
from size_mset_mono[OF this(1)] this(2) show ?thesis using size_outl_le[of a] dist_C dist_D
by (auto simp: uint32_max_def distinct_mset_rempdups_union_mset)
qed
show confl: ‹lookup_conflict_merge init M D (b, n, xs) clvls lbd outl
≤ ⇓ ?Ref (merge_conflict_m_g init M D (Some C))›
supply [[goals_limit=1]]
unfolding resolve_lookup_conflict_aa_def lookup_conflict_merge_def
distinct_mset_rempdups_union_mset[OF dist_D dist_CD] I_def[symmetric] conc_fun_SPEC
lbd_upd_def[symmetric] Let_def length_uint32_nat_def merge_conflict_m_g_def
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(j, _). length D - j)› and
I' = I'])
subgoal by auto
subgoal
using clvls_uint32_max Suc_N_uint32_max ‹Suc init ≤ uint32_max›
unfolding uint32_max_def I_def by auto
subgoal using assms
unfolding lookup_conflict_merge'_step_def Let_def option_lookup_clause_rel_def I'_def
by (auto simp add: uint32_max_def lookup_conflict_merge'_step_def option_lookup_clause_rel_def)
subgoal by auto
subgoal unfolding I_def by fast
subgoal for x1 x2 s a ba aa baa ab bb ac bc by (rule outl_le)
subgoal by (rule if_True_I)
subgoal by (rule if_true_I')
subgoal for b' n' s j zs
using dist lits tauto
by (auto simp: option_lookup_clause_rel_def take_Suc_conv_app_nth
literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l)
subgoal using assms by (auto simp: option_lookup_clause_rel_def lookup_conflict_merge'_step_def
Let_def I_def I'_def)
done
qed
lemma literals_are_in_ℒ⇩i⇩n_mm_literals_are_in_ℒ⇩i⇩n:
assumes lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
i: ‹i ∈# dom_m N›
shows ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ i))›
unfolding literals_are_in_ℒ⇩i⇩n_def
proof (standard)
fix L
assume ‹L ∈# all_lits_of_m (mset (N ∝ i))›
then have ‹atm_of L ∈ atms_of_mm (mset `# ran_mf N)›
using i unfolding ran_m_def in_all_lits_of_m_ain_atms_of_iff
by (auto dest!: multi_member_split)
then show ‹L ∈# ℒ⇩a⇩l⇩l 𝒜›
using lits atm_of_notin_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff
unfolding literals_are_in_ℒ⇩i⇩n_mm_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
by blast
qed
lemma isa_set_lookup_conflict:
‹(uncurry6 isa_set_lookup_conflict_aa, uncurry6 set_conflict_m) ∈
[λ((((((M, N), i), xs), clvls), lbd), outl). i ∈# dom_m N ∧ xs = None ∧ distinct (N ∝ i) ∧
literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N) ∧
¬tautology (mset (N ∝ i)) ∧ clvls = 0 ∧
out_learned M None outl ∧
isasat_input_bounded 𝒜]⇩f
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 →
⟨option_lookup_clause_rel 𝒜 ×⇩r nat_rel ×⇩r Id ×⇩r Id ⟩nres_rel›
proof -
have H: ‹set_lookup_conflict_aa M N i (b, n, xs) clvls lbd outl
≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩r Id)
(set_conflict_m M N i None clvls lbd outl)›
if
i: ‹i ∈# dom_m N› and
ocr: ‹((b, n, xs), None) ∈ option_lookup_clause_rel 𝒜› and
dist: ‹distinct (N ∝ i)› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
tauto: ‹¬tautology (mset (N ∝ i))› and
‹clvls = 0› and
out: ‹out_learned M None outl› and
bounded: ‹isasat_input_bounded 𝒜›
for b n xs N i M clvls lbd outl
proof -
have lookup_conflict_merge_normalise:
‹lookup_conflict_merge 0 M C (b, zs) = lookup_conflict_merge 0 M C (False, zs)›
for M C zs
unfolding lookup_conflict_merge_def by auto
have [simp]: ‹out_learned M (Some {#}) outl›
using out by (cases outl) (auto simp: out_learned_def)
have T: ‹((False, n, xs), Some {#}) ∈ option_lookup_clause_rel 𝒜›
using ocr unfolding option_lookup_clause_rel_def by auto
have ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ i))›
using literals_are_in_ℒ⇩i⇩n_mm_literals_are_in_ℒ⇩i⇩n[OF lits i] .
then show ?thesis unfolding set_lookup_conflict_aa_def set_conflict_m_def
using lookup_conflict_merge'_spec[of False n xs ‹{#}› 𝒜 ‹N∝i› 0 _ 0 outl lbd] that dist T
by (auto simp: lookup_conflict_merge_normalise uint32_max_def merge_conflict_m_g_def)
qed
have H: ‹isa_set_lookup_conflict_aa M' arena i (b, n, xs) clvls lbd outl
≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩r Id)
(set_conflict_m M N i None clvls lbd outl)›
if
i: ‹i ∈# dom_m N› and
ocr: ‹((b, n, xs), None) ∈ option_lookup_clause_rel 𝒜› and
dist: ‹distinct (N ∝ i)› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
tauto: ‹¬tautology (mset (N ∝ i))› and
‹clvls = 0› and
out: ‹out_learned M None outl› and
valid: ‹valid_arena arena N vdom› and
M'M: ‹(M', M) ∈ trail_pol 𝒜› and
bounded: ‹isasat_input_bounded 𝒜›
for b n xs N i M clvls lbd outl arena vdom M'
unfolding isa_set_lookup_conflict_aa_def
apply (rule order.trans)
apply (rule isa_lookup_conflict_merge_lookup_conflict_merge_ext[OF valid i lits ocr M'M bounded])
unfolding lookup_conflict_merge_def[symmetric] set_lookup_conflict_aa_def[symmetric]
by (auto intro: H[OF that(1-7,10)])
show ?thesis
unfolding lookup_conflict_merge_def uncurry_def
by (intro nres_relI WB_More_Refinement.frefI) (auto intro!: H)
qed
definition merge_conflict_m_pre where
‹merge_conflict_m_pre 𝒜 =
(λ((((((M, N), i), xs), clvls), lbd), out). i ∈# dom_m N ∧ xs ≠ None ∧ distinct (N ∝ i) ∧
¬tautology (mset (N ∝ i)) ∧
(∀L ∈ set (tl (N ∝ i)). - L ∉# the xs) ∧
literals_are_in_ℒ⇩i⇩n 𝒜 (the xs) ∧ clvls = card_max_lvl M (the xs) ∧
out_learned M xs out ∧ no_dup M ∧
literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N) ∧
isasat_input_bounded 𝒜)›
definition isa_resolve_merge_conflict_gt2 where
‹isa_resolve_merge_conflict_gt2 = isa_lookup_conflict_merge 1›
lemma isa_resolve_merge_conflict_gt2:
‹(uncurry6 isa_resolve_merge_conflict_gt2, uncurry6 merge_conflict_m) ∈
[merge_conflict_m_pre 𝒜]⇩f
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 →
⟨option_lookup_clause_rel 𝒜 ×⇩r nat_rel ×⇩r Id ×⇩r Id ⟩nres_rel›
proof -
have H1: ‹resolve_lookup_conflict_aa M N i (b, n, xs) clvls lbd outl
≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩r Id)
(merge_conflict_m M N i C clvls lbd outl)›
if
i: ‹i ∈# dom_m N› and
ocr: ‹((b, n, xs), C) ∈ option_lookup_clause_rel 𝒜› and
dist: ‹distinct (N ∝ i)› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
lits': ‹literals_are_in_ℒ⇩i⇩n 𝒜 (the C)› and
tauto: ‹¬tautology (mset (N ∝ i))› and
out: ‹out_learned M C outl› and
not_neg: ‹⋀L. L ∈ set (tl (N ∝ i)) ⟹ - L ∉# the C› and
‹clvls = card_max_lvl M (the C)› and
C_None: ‹C ≠ None› and
bounded: ‹isasat_input_bounded 𝒜›
for b n xs N i M clvls lbd outl C
proof -
have lookup_conflict_merge_normalise:
‹lookup_conflict_merge 1 M C (b, zs) = lookup_conflict_merge 1 M C (False, zs)›
for M C zs
unfolding lookup_conflict_merge_def by auto
have ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (N ∝ i))›
using literals_are_in_ℒ⇩i⇩n_mm_literals_are_in_ℒ⇩i⇩n[OF lits i] .
then show ?thesis unfolding resolve_lookup_conflict_aa_def merge_conflict_m_def
using lookup_conflict_merge'_spec[of b n xs ‹the C› 𝒜 ‹N∝i› clvls M 1 outl lbd] that dist
not_neg ocr C_None lits'
by (auto simp: lookup_conflict_merge_normalise uint32_max_def merge_conflict_m_g_def
drop_Suc)
qed
have H2: ‹isa_resolve_merge_conflict_gt2 M' arena i (b, n, xs) clvls lbd outl
≤ ⇓ (Id ×⇩r Id)
(resolve_lookup_conflict_aa M N i (b, n, xs) clvls lbd outl)›
if
i: ‹i ∈# dom_m N› and
ocr: ‹((b, n, xs), C) ∈ option_lookup_clause_rel 𝒜› and
dist: ‹distinct (N ∝ i)› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
lits': ‹literals_are_in_ℒ⇩i⇩n 𝒜 (the C)› and
tauto: ‹¬tautology (mset (N ∝ i))› and
out: ‹out_learned M C outl› and
not_neg: ‹⋀L. L ∈ set (tl (N ∝ i)) ⟹ - L ∉# the C› and
‹clvls = card_max_lvl M (the C)› and
C_None: ‹C ≠ None› and
valid: ‹valid_arena arena N vdom› and
i: ‹i ∈# dom_m N› and
dist: ‹distinct (N ∝ i)› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
tauto: ‹¬tautology (mset (N ∝ i))› and
‹clvls = card_max_lvl M (the C)› and
out: ‹out_learned M C outl› and
bounded: ‹isasat_input_bounded 𝒜› and
M'M: ‹(M', M) ∈ trail_pol 𝒜›
for b n xs N i M clvls lbd outl arena vdom C M'
unfolding isa_resolve_merge_conflict_gt2_def
apply (rule order.trans)
apply (rule isa_lookup_conflict_merge_lookup_conflict_merge_ext[OF valid i lits ocr M'M])
unfolding resolve_lookup_conflict_aa_def[symmetric] set_lookup_conflict_aa_def[symmetric]
using bounded by (auto intro: H1[OF that(1-6)])
show ?thesis
unfolding lookup_conflict_merge_def uncurry_def
apply (intro nres_relI frefI)
apply clarify
subgoal
unfolding merge_conflict_m_pre_def
apply (rule order_trans)
apply (rule H2; auto; auto; fail)
by (auto intro!: H1 simp: merge_conflict_m_pre_def)
done
qed
definition (in -) is_in_conflict :: ‹nat literal ⇒ nat clause option ⇒ bool› where
[simp]: ‹is_in_conflict L C ⟷ L ∈# the C›
definition (in -) is_in_lookup_option_conflict
:: ‹nat literal ⇒ (bool × nat × bool option list) ⇒ bool›
where
‹is_in_lookup_option_conflict = (λL (_, _, xs). xs ! atm_of L = Some (is_pos L))›
lemma is_in_lookup_option_conflict_is_in_conflict:
‹(uncurry (RETURN oo is_in_lookup_option_conflict),
uncurry (RETURN oo is_in_conflict)) ∈
[λ(L, C). C ≠ None ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f Id ×⇩r option_lookup_clause_rel 𝒜 →
⟨Id⟩nres_rel›
apply (intro nres_relI frefI)
subgoal for Lxs LC
using lookup_clause_rel_atm_in_iff[of _ ‹snd (snd (snd Lxs))›]
apply (cases Lxs)
by (auto simp: is_in_lookup_option_conflict_def option_lookup_clause_rel_def)
done
definition conflict_from_lookup where
‹conflict_from_lookup = (λ(n, xs). SPEC(λD. mset_as_position xs D ∧ n = size D))›
lemma Ex_mset_as_position:
‹Ex (mset_as_position xs)›
proof (induction ‹size {#x ∈# mset xs. x ≠ None#}› arbitrary: xs)
case 0
then have xs: ‹xs = replicate (length xs) None›
by (auto simp: filter_mset_empty_conv dest: replicate_length_same)
show ?case
by (subst xs) (auto simp: mset_as_position.empty intro!: exI[of _ ‹{#}›])
next
case (Suc x) note IH = this(1) and xs = this(2)
obtain i where
[simp]: ‹i < length xs› and
xs_i: ‹xs ! i ≠ None›
using xs[symmetric]
by (auto dest!: size_eq_Suc_imp_elem simp: in_set_conv_nth)
let ?xs = ‹xs [i := None]›
have ‹x = size {#x ∈# mset ?xs. x ≠ None#}›
using xs[symmetric] xs_i by (auto simp: mset_update size_remove1_mset_If)
from IH[OF this] obtain D where
map: ‹mset_as_position ?xs D›
by blast
have [simp]: ‹Pos i ∉# D› ‹Neg i ∉# D›
using xs_i mset_as_position_nth[OF map, of ‹Pos i›]
mset_as_position_nth[OF map, of ‹Neg i›]
by auto
have [simp]: ‹xs ! i = a ⟹ xs[i := a] = xs› for a
by auto
have ‹mset_as_position xs (add_mset (if the (xs ! i) then Pos i else Neg i) D)›
using mset_as_position.add[OF map, of ‹if the (xs ! i) then Pos i else Neg i› xs]
xs_i[symmetric]
by (cases ‹xs ! i›) auto
then show ?case by blast
qed
lemma id_conflict_from_lookup:
‹(RETURN o id, conflict_from_lookup) ∈ [λ(n, xs). ∃D. ((n, xs), D) ∈ lookup_clause_rel 𝒜]⇩f Id →
⟨lookup_clause_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: lookup_clause_rel_def conflict_from_lookup_def RETURN_RES_refine_iff)
lemma lookup_clause_rel_exists_le_uint32_max:
assumes ocr: ‹((n, xs), D) ∈ lookup_clause_rel 𝒜› and ‹n > 0› and
le_i: ‹∀k<i. xs ! k = None› and lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 D› and
bounded: ‹isasat_input_bounded 𝒜›
shows
‹∃j. j ≥ i ∧ j < length xs ∧ j < uint32_max ∧ xs ! j ≠ None›
proof -
have
n_D: ‹n = size D› and
map: ‹mset_as_position xs D› and
le_xs: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs›
using ocr unfolding lookup_clause_rel_def by auto
have map_empty: ‹mset_as_position xs {#} ⟷ (xs = [] ∨ set xs = {None})›
by (subst mset_as_position.simps) (auto simp add: list_eq_replicate_iff)
have ex_not_none: ‹∃j. j ≥ i ∧ j < length xs ∧ xs ! j ≠ None›
proof (rule ccontr)
assume ‹¬ ?thesis›
then have ‹xs = [] ∨ set xs = {None}›
using le_i by (fastforce simp: in_set_conv_nth)
then have ‹mset_as_position xs {#}›
using map_empty by auto
then show False
using mset_as_position_right_unique[OF map] ‹n > 0› n_D by (cases D) auto
qed
then obtain j where
j: ‹j ≥ i›‹j < length xs›‹xs ! j ≠ None›
by blast
let ?L = ‹if the (xs ! j) then Pos j else Neg j›
have ‹?L ∈# D›
using j mset_as_position_in_iff_nth[OF map, of ?L] by auto
then have ‹nat_of_lit ?L ≤ uint32_max›
using lits bounded
by (auto 5 5 dest!: multi_member_split[of _ D]
simp: literals_are_in_ℒ⇩i⇩n_add_mset split: if_splits)
then have ‹j < uint32_max›
by (auto simp: uint32_max_def split: if_splits)
then show ?thesis
using j by blast
qed
text ‹During the conflict analysis, the literal of highest level is at the beginning. During the
rest of the time the conflict is \<^term>‹None›.
›
definition highest_lit where
‹highest_lit M C L ⟷
(L = None ⟶ C = {#}) ∧
(L ≠ None ⟶ get_level M (fst (the L)) = snd (the L) ∧
snd (the L) = get_maximum_level M C ∧
fst (the L) ∈# C
)›
paragraph ‹Conflict Minimisation›
definition iterate_over_conflict_inv where
‹iterate_over_conflict_inv M D⇩0' = (λ(D, D'). D ⊆# D⇩0' ∧ D' ⊆# D)›
definition is_literal_redundant_spec where
‹is_literal_redundant_spec K NU UNE D L = SPEC(λb. b ⟶
NU + UNE ⊨pm remove1_mset L (add_mset K D))›
definition iterate_over_conflict
:: ‹'v literal ⇒ ('v, 'mark) ann_lits ⇒ 'v clauses ⇒ 'v clauses ⇒ 'v clause ⇒
'v clause nres›
where
‹iterate_over_conflict K M NU UNE D⇩0' = do {
(D, _) ←
WHILE⇩T⇗iterate_over_conflict_inv M D⇩0'⇖
(λ(D, D'). D' ≠ {#})
(λ(D, D'). do{
x ← SPEC (λx. x ∈# D');
red ← is_literal_redundant_spec K NU UNE D x;
if ¬red
then RETURN (D, remove1_mset x D')
else RETURN (remove1_mset x D, remove1_mset x D')
})
(D⇩0', D⇩0');
RETURN D
}›
definition minimize_and_extract_highest_lookup_conflict_inv where
‹minimize_and_extract_highest_lookup_conflict_inv = (λ(D, i, s, outl).
length outl ≤ uint32_max ∧ mset (tl outl) = D ∧ outl ≠ [] ∧ i ≥ 1)›
type_synonym 'v conflict_highest_conflict = ‹('v literal × nat) option›
definition (in -) atm_in_conflict where
‹atm_in_conflict L D ⟷ L ∈ atms_of D›
definition atm_in_conflict_lookup :: ‹nat ⇒ lookup_clause_rel ⇒ bool› where
‹atm_in_conflict_lookup = (λL (_, xs). xs ! L ≠ None)›
definition atm_in_conflict_lookup_pre :: ‹nat ⇒ lookup_clause_rel ⇒ bool› where
‹atm_in_conflict_lookup_pre L xs ⟷ L < length (snd xs)›
lemma atm_in_conflict_lookup_atm_in_conflict:
‹(uncurry (RETURN oo atm_in_conflict_lookup), uncurry (RETURN oo atm_in_conflict)) ∈
[λ(L, xs). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)]⇩f Id ×⇩f lookup_clause_rel 𝒜 → ⟨bool_rel⟩nres_rel›
apply (intro frefI nres_relI)
subgoal for x y
using mset_as_position_in_iff_nth[of ‹snd (snd x)› ‹snd y› ‹Pos (fst x)›]
mset_as_position_in_iff_nth[of ‹snd (snd x)› ‹snd y› ‹Neg (fst x)›]
by (cases x; cases y)
(auto simp: atm_in_conflict_lookup_def atm_in_conflict_def
lookup_clause_rel_def atm_iff_pos_or_neg_lit
pos_lit_in_atms_of neg_lit_in_atms_of)
done
lemma atm_in_conflict_lookup_pre:
fixes x1 :: ‹nat› and x2 :: ‹nat›
assumes
‹x1n ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹(x2f, x2a) ∈ lookup_clause_rel 𝒜›
shows ‹atm_in_conflict_lookup_pre (atm_of x1n) x2f›
proof -
show ?thesis
using assms
by (auto simp: lookup_clause_rel_def atm_in_conflict_lookup_pre_def atms_of_def)
qed
definition is_literal_redundant_lookup_spec where
‹is_literal_redundant_lookup_spec 𝒜 M NU NUE D' L s =
SPEC(λ(s', b). b ⟶ (∀D. (D', D) ∈ lookup_clause_rel 𝒜 ⟶
(mset `# mset (tl NU)) + NUE ⊨pm remove1_mset L D))›
type_synonym (in -) conflict_min_cach_l = ‹minimize_status list × nat list›
definition (in -) conflict_min_cach_set_removable_l
:: ‹conflict_min_cach_l ⇒ nat ⇒ conflict_min_cach_l nres›
where
‹conflict_min_cach_set_removable_l = (λ(cach, sup) L. do {
ASSERT(L < length cach);
ASSERT(length sup ≤ 1 + uint32_max div 2);
RETURN (cach[L := SEEN_REMOVABLE], if cach ! L = SEEN_UNKNOWN then sup @ [L] else sup)
})›
definition (in -) conflict_min_cach :: ‹nat conflict_min_cach ⇒ nat ⇒ minimize_status› where
[simp]: ‹conflict_min_cach cach L = cach L›
definition lit_redundant_reason_stack2
:: ‹'v literal ⇒ 'v clauses_l ⇒ nat ⇒ (nat × nat × bool)› where
‹lit_redundant_reason_stack2 L NU C' =
(if length (NU ∝ C') > 2 then (C', 1, False)
else if NU ∝ C' ! 0 = L then (C', 1, False)
else (C', 0, True))›
definition ana_lookup_rel
:: ‹nat clauses_l ⇒ ((nat × nat × bool) × (nat × nat × nat × nat)) set›
where
‹ana_lookup_rel NU = {((C, i, b), (C', k', i', len')).
C = C' ∧ k' = (if b then 1 else 0) ∧ i = i' ∧
len' = (if b then 1 else length (NU ∝ C))}›
lemma ana_lookup_rel_alt_def:
‹((C, i, b), (C', k', i', len')) ∈ ana_lookup_rel NU ⟷
C = C' ∧ k' = (if b then 1 else 0) ∧ i = i' ∧
len' = (if b then 1 else length (NU ∝ C))›
unfolding ana_lookup_rel_def
by auto
abbreviation ana_lookups_rel where
‹ana_lookups_rel NU ≡ ⟨ana_lookup_rel NU⟩list_rel›
definition ana_lookup_conv :: ‹nat clauses_l ⇒ (nat × nat × bool) ⇒ (nat × nat × nat × nat)› where
‹ana_lookup_conv NU = (λ(C, i, b). (C, (if b then 1 else 0), i, (if b then 1 else length (NU ∝ C))))›
definition get_literal_and_remove_of_analyse_wl2
:: ‹'v clause_l ⇒ (nat × nat × bool) list ⇒ 'v literal × (nat × nat × bool) list› where
‹get_literal_and_remove_of_analyse_wl2 C analyse =
(let (i, j, b) = last analyse in
(C ! j, analyse[length analyse - 1 := (i, j + 1, b)]))›
definition lit_redundant_rec_wl_inv2 where
‹lit_redundant_rec_wl_inv2 M NU D =
(λ(cach, analyse, b). ∃analyse'. (analyse, analyse') ∈ ana_lookups_rel NU ∧
lit_redundant_rec_wl_inv M NU D (cach, analyse', b))›
definition mark_failed_lits_stack_inv2 where
‹mark_failed_lits_stack_inv2 NU analyse = (λcach.
∃analyse'. (analyse, analyse') ∈ ana_lookups_rel NU ∧
mark_failed_lits_stack_inv NU analyse' cach)›
definition lit_redundant_rec_wl_lookup
:: ‹nat multiset ⇒ (nat,nat)ann_lits ⇒ nat clauses_l ⇒ nat clause ⇒
_ ⇒ _ ⇒ _ ⇒ (_ × _ × bool) nres›
where
‹lit_redundant_rec_wl_lookup 𝒜 M NU D cach analysis lbd =
WHILE⇩T⇗lit_redundant_rec_wl_inv2 M NU D⇖
(λ(cach, analyse, b). analyse ≠ [])
(λ(cach, analyse, b). do {
ASSERT(analyse ≠ []);
ASSERT(length analyse ≤ length M);
let (C,k, i, len) = ana_lookup_conv NU (last analyse);
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) > k); ― ‹ >= 2 would work too ›
ASSERT (NU ∝ C ! k ∈ lits_of_l M);
ASSERT(NU ∝ C ! k ∈# ℒ⇩a⇩l⇩l 𝒜);
ASSERT(literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ C)));
ASSERT(length (NU ∝ C) ≤ Suc (uint32_max div 2));
ASSERT(len ≤ length (NU ∝ C)); ― ‹makes the refinement easier›
let C = NU ∝ C;
if i ≥ len
then
RETURN(cach (atm_of (C ! k) := SEEN_REMOVABLE), butlast analyse, True)
else do {
let (L, analyse) = get_literal_and_remove_of_analyse_wl2 C analyse;
ASSERT(L ∈# ℒ⇩a⇩l⇩l 𝒜);
let b = ¬level_in_lbd (get_level M L) lbd;
if (get_level M L = 0 ∨
conflict_min_cach cach (atm_of L) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of L) D)
then RETURN (cach, analyse, False)
else if b ∨ conflict_min_cach cach (atm_of L) = SEEN_FAILED
then do {
ASSERT(mark_failed_lits_stack_inv2 NU analyse cach);
cach ← mark_failed_lits_wl NU analyse cach;
RETURN (cach, [], False)
}
else do {
ASSERT(- L ∈ lits_of_l M);
C ← get_propagation_reason M (-L);
case C of
Some C ⇒ do {
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) ≥ 2);
ASSERT(literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ C)));
ASSERT(length (NU ∝ C) ≤ Suc (uint32_max div 2));
RETURN (cach, analyse @ [lit_redundant_reason_stack2 (-L) NU C], False)
}
| None ⇒ do {
ASSERT(mark_failed_lits_stack_inv2 NU analyse cach);
cach ← mark_failed_lits_wl NU analyse cach;
RETURN (cach, [], False)
}
}
}
})
(cach, analysis, False)›
lemma lit_redundant_rec_wl_ref_butlast:
‹lit_redundant_rec_wl_ref NU x ⟹ lit_redundant_rec_wl_ref NU (butlast x)›
by (cases x rule: rev_cases)
(auto simp: lit_redundant_rec_wl_ref_def dest: in_set_butlastD)
lemma lit_redundant_rec_wl_lookup_mark_failed_lits_stack_inv:
assumes
‹(x, x') ∈ Id› and
‹case x of (cach, analyse, b) ⇒ analyse ≠ []› and
‹lit_redundant_rec_wl_inv M NU D x'› and
‹¬ snd (snd (snd (last x1a))) ≤ fst (snd (snd (last x1a)))› and
‹get_literal_and_remove_of_analyse_wl (NU ∝ fst (last x1c)) x1c = (x1e, x2e)› and
‹x2 = (x1a, x2a)› and
‹x' = (x1, x2)› and
‹x2b = (x1c, x2c)› and
‹x = (x1b, x2b)›
shows ‹mark_failed_lits_stack_inv NU x2e x1b›
proof -
show ?thesis
using assms
unfolding mark_failed_lits_stack_inv_def lit_redundant_rec_wl_inv_def
lit_redundant_rec_wl_ref_def get_literal_and_remove_of_analyse_wl_def
by (cases ‹x1a› rule: rev_cases)
(auto simp: elim!: in_set_upd_cases)
qed
context
fixes M D 𝒜 NU analysis analysis'
assumes
M_D: ‹M ⊨as CNot D› and
n_d: ‹no_dup M› and
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M› and
ana: ‹(analysis, analysis') ∈ ana_lookups_rel NU› and
lits_NU: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m NU)› and
bounded: ‹isasat_input_bounded 𝒜›
begin
lemma ccmin_rel:
assumes ‹lit_redundant_rec_wl_inv M NU D (cach, analysis', False)›
shows ‹((cach, analysis, False), cach, analysis', False)
∈ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
proof -
show ?thesis using ana assms by auto
qed
context
fixes x :: ‹(nat ⇒ minimize_status) × (nat × nat × bool) list × bool› and
x' :: ‹(nat ⇒ minimize_status) × (nat × nat × nat × nat) list × bool›
assumes x_x': ‹(x, x') ∈ {((cach, ana, b), (cach', ana', b')).
(ana, ana') ∈ ana_lookups_rel NU ∧ b = b' ∧ cach = cach' ∧
lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
begin
lemma ccmin_lit_redundant_rec_wl_inv2:
assumes ‹lit_redundant_rec_wl_inv M NU D x'›
shows ‹lit_redundant_rec_wl_inv2 M NU D x›
using x_x' unfolding lit_redundant_rec_wl_inv2_def
by auto
context
assumes
‹lit_redundant_rec_wl_inv2 M NU D x› and
‹lit_redundant_rec_wl_inv M NU D x'›
begin
lemma ccmin_cond:
fixes x1 :: ‹nat ⇒ minimize_status› and
x2 :: ‹(nat × nat × bool) list × bool› and
x1a :: ‹(nat × nat × bool) list› and
x2a :: ‹bool› and x1b :: ‹nat ⇒ minimize_status› and
x2b :: ‹(nat × nat × nat × nat) list × bool› and
x1c :: ‹(nat × nat × nat × nat) list› and x2c :: ‹bool›
assumes
‹x2 = (x1a, x2a)›
‹x = (x1, x2)›
‹x2b = (x1c, x2c)›
‹x' = (x1b, x2b)›
shows ‹(x1a ≠ []) = (x1c ≠ [])›
using assms x_x'
by auto
end
context
assumes
‹case x of (cach, analyse, b) ⇒ analyse ≠ []› and
‹case x' of (cach, analyse, b) ⇒ analyse ≠ []› and
inv2: ‹lit_redundant_rec_wl_inv2 M NU D x› and
‹lit_redundant_rec_wl_inv M NU D x'›
begin
context
fixes x1 :: ‹nat ⇒ minimize_status› and
x2 :: ‹(nat × nat × nat × nat) list × bool› and
x1a :: ‹(nat × nat × nat × nat) list› and x2a :: ‹bool› and
x1b :: ‹nat ⇒ minimize_status› and
x2b :: ‹(nat × nat × bool) list × bool› and
x1c :: ‹(nat × nat × bool) list› and
x2c :: ‹bool›
assumes st:
‹x2 = (x1a, x2a)›
‹x' = (x1, x2)›
‹x2b = (x1c, x2c)›
‹x = (x1b, x2b)› and
x1a: ‹x1a ≠ []›
begin
private lemma st:
‹x2 = (x1a, x2a)›
‹x' = (x1, x1a, x2a)›
‹x2b = (x1c, x2a)›
‹x = (x1, x1c, x2a)›
‹x1b = x1›
‹x2c = x2a› and
x1c: ‹x1c ≠ []›
using st x_x' x1a by auto
lemma ccmin_nempty:
shows ‹x1c ≠ []›
using x_x' x1a
by (auto simp: st)
context
notes _[simp] = st
fixes x1d :: ‹nat› and x2d :: ‹nat × nat × nat› and
x1e :: ‹nat› and x2e :: ‹nat × nat› and
x1f :: ‹nat› and
x2f :: ‹nat› and x1g :: ‹nat› and
x2g :: ‹nat × nat × nat› and
x1h :: ‹nat› and
x2h :: ‹nat × nat› and
x1i :: ‹nat› and
x2i :: ‹nat›
assumes
ana_lookup_conv: ‹ana_lookup_conv NU (last x1c) = (x1g, x2g)› and
last: ‹last x1a = (x1d, x2d)› and
dom: ‹x1d ∈# dom_m NU› and
le: ‹x1e < length (NU ∝ x1d)› and
in_lits: ‹NU ∝ x1d ! x1e ∈ lits_of_l M› and
st2:
‹x2g = (x1h, x2h)›
‹x2e = (x1f, x2f)›
‹x2d = (x1e, x2e)›
‹x2h = (x1i, x2i)›
begin
private lemma x1g_x1d:
‹x1g = x1d›
‹x1h = x1e›
‹x1i = x1f›
using st2 last ana_lookup_conv x_x' x1a last
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: ana_lookup_conv_def ana_lookup_rel_def
list_rel_append_single_iff; fail)+
private definition j where
‹j = fst (snd (last x1c))›
private definition b where
‹b = snd (snd (last x1c))›
private lemma last_x1c[simp]:
‹last x1c = (x1d, x1f, b)›
using inv2 x1a last x_x' unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def)
private lemma
ana: ‹(x1d, (if b then 1 else 0), x1f, (if b then 1 else length (NU ∝ x1d))) = (x1d, x1e, x1f, x2i)› and
st3:
‹x1e = (if b then 1 else 0)›
‹x1f = j›
‹x2f = (if b then 1 else length (NU ∝ x1d))›
‹x2d = (if b then 1 else 0, j, if b then 1 else length (NU ∝ x1d))› and
‹j ≤ (if b then 1 else length (NU ∝ x1d))› and
‹x1d ∈# dom_m NU› and
‹0 < x1d› and
‹(if b then 1 else length (NU ∝ x1d)) ≤ length (NU ∝ x1d)› and
‹(if b then 1 else 0) < length (NU ∝ x1d)› and
dist: ‹distinct (NU ∝ x1d)› and
tauto: ‹¬ tautology (mset (NU ∝ x1d))›
subgoal
using inv2 x1a last x_x' x1c ana_lookup_conv
unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def ana_lookup_conv_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def st2
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
subgoal
using inv2 x1a last x_x' x1c unfolding x1g_x1d st j_def b_def
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases;
auto simp: lit_redundant_rec_wl_inv2_def list_rel_append_single_iff
lit_redundant_rec_wl_inv_def ana_lookup_rel_def
lit_redundant_rec_wl_ref_def
simp del: x1c)
done
lemma ccmin_in_dom:
shows x1g_dom: ‹x1g ∈# dom_m NU›
using dom unfolding x1g_x1d .
lemma ccmin_in_dom_le_length:
shows ‹x1h < length (NU ∝ x1g)›
using le unfolding x1g_x1d .
lemma ccmin_in_trail:
shows ‹NU ∝ x1g ! x1h ∈ lits_of_l M›
using in_lits unfolding x1g_x1d .
lemma ccmin_literals_are_in_ℒ⇩i⇩n_NU_x1g:
shows ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ x1g))›
using lits_NU multi_member_split[OF x1g_dom]
by (auto simp: ran_m_def literals_are_in_ℒ⇩i⇩n_mm_add_mset)
lemma ccmin_le_uint32_max:
‹length (NU ∝ x1g) ≤ Suc (uint32_max div 2)›
using simple_clss_size_upper_div2[OF bounded ccmin_literals_are_in_ℒ⇩i⇩n_NU_x1g]
dist tauto unfolding x1g_x1d
by auto
lemma ccmin_in_all_lits:
shows ‹NU ∝ x1g ! x1h ∈# ℒ⇩a⇩l⇩l 𝒜›
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[OF ccmin_literals_are_in_ℒ⇩i⇩n_NU_x1g, of x1h]
le unfolding x1g_x1d by auto
lemma ccmin_less_length:
shows ‹x2i ≤ length (NU ∝ x1g)›
using le ana unfolding x1g_x1d st3 by (simp split: if_splits)
lemma ccmin_same_cond:
shows ‹(x2i ≤ x1i) = (x2f ≤ x1f)›
using le ana unfolding x1g_x1d st3 by (simp split: if_splits)
lemma list_rel_butlast:
assumes rel: ‹(xs, ys) ∈ ⟨R⟩list_rel›
shows ‹(butlast xs, butlast ys) ∈ ⟨R⟩list_rel›
proof -
have ‹length xs = length ys›
using assms list_rel_imp_same_length by blast
then show ?thesis
using rel
by (induction xs ys rule: list_induct2) (auto split: nat.splits)
qed
lemma ccmin_set_removable:
assumes
‹x2i ≤ x1i› and
‹x2f ≤ x1f› and ‹lit_redundant_rec_wl_inv2 M NU D x›
shows ‹((x1b(atm_of (NU ∝ x1g ! x1h) := SEEN_REMOVABLE), butlast x1c, True),
x1(atm_of (NU ∝ x1d ! x1e) := SEEN_REMOVABLE), butlast x1a, True)
∈ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
using x_x' by (auto simp: x1g_x1d lit_redundant_rec_wl_ref_butlast lit_redundant_rec_wl_inv_def
dest: list_rel_butlast)
context
assumes
le: ‹¬ x2i ≤ x1i› ‹¬ x2f ≤ x1f›
begin
context
notes _[simp]= x1g_x1d st2 last
fixes x1j :: ‹nat literal› and x2j :: ‹(nat × nat × nat × nat) list› and
x1k :: ‹nat literal› and x2k :: ‹(nat × nat × bool) list›
assumes
rem: ‹get_literal_and_remove_of_analyse_wl (NU ∝ x1d) x1a = (x1j, x2j)› and
rem2:‹get_literal_and_remove_of_analyse_wl2 (NU ∝ x1g) x1c = (x1k, x2k)› and
‹fst (snd (snd (last x2j))) ≠ 0› and
ux1j_M: ‹- x1j ∈ lits_of_l M›
begin
private lemma confl_min_last: ‹(last x1c, last x1a) ∈ ana_lookup_rel NU›
using x1a x1c x_x' rem rem2 last ana_lookup_conv unfolding x1g_x1d st2 b_def st
by (cases x1c rule: rev_cases; cases x1a rule: rev_cases)
(auto simp: list_rel_append_single_iff
get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
private lemma rel: ‹(x1c[length x1c - Suc 0 := (x1d, Suc x1f, b)], x1a
[length x1a - Suc 0 := (x1d, x1e, Suc x1f, x2f)])
∈ ana_lookups_rel NU›
using x1a x1c x_x' rem rem2 confl_min_last unfolding x1g_x1d st2 last b_def st
by (cases x1c rule: rev_cases; cases x1a rule: rev_cases)
(auto simp: list_rel_append_single_iff
ana_lookup_rel_alt_def get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
private lemma x1k_x1j: ‹x1k = x1j› ‹x1j = NU ∝ x1d ! x1f› and
x2k_x2j: ‹(x2k, x2j) ∈ ana_lookups_rel NU›
subgoal
using x1a x1c x_x' rem rem2 confl_min_last unfolding x1g_x1d st2 last b_def st
by (cases x1c rule: rev_cases; cases x1a rule: rev_cases)
(auto simp: list_rel_append_single_iff
ana_lookup_rel_alt_def get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
subgoal
using x1a x1c x_x' rem rem2 confl_min_last unfolding x1g_x1d st2 last b_def st
by (cases x1c rule: rev_cases; cases x1a rule: rev_cases)
(auto simp: list_rel_append_single_iff
ana_lookup_rel_alt_def get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
subgoal
using x1a x1c x_x' rem rem2 confl_min_last unfolding x1g_x1d st2 last b_def st
by (cases x1c rule: rev_cases; cases x1a rule: rev_cases)
(auto simp: list_rel_append_single_iff
ana_lookup_rel_alt_def get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
done
lemma ccmin_x1k_all:
shows ‹x1k ∈# ℒ⇩a⇩l⇩l 𝒜›
unfolding x1k_x1j
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[OF ccmin_literals_are_in_ℒ⇩i⇩n_NU_x1g, of x1f]
literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[OF lits ‹- x1j ∈ lits_of_l M›]
le st3 unfolding x1g_x1d by (auto split: if_splits simp: x1k_x1j uminus_𝒜⇩i⇩n_iff)
context
notes _[simp]= x1k_x1j
fixes b :: ‹bool› and lbd
assumes b: ‹(¬ level_in_lbd (get_level M x1k) lbd, b) ∈ bool_rel›
begin
private lemma in_conflict_atm_in:
‹- x1e' ∈ lits_of_l M ⟹ atm_in_conflict (atm_of x1e') D ⟷ x1e' ∈# D› for x1e'
using M_D n_d
by (auto simp: atm_in_conflict_def true_annots_true_cls_def_iff_negation_in_model
atms_of_def atm_of_eq_atm_of dest!: multi_member_split no_dup_consistentD)
lemma ccmin_already_seen:
shows ‹(get_level M x1k = 0 ∨
conflict_min_cach x1b (atm_of x1k) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of x1k) D) =
(get_level M x1j = 0 ∨ x1 (atm_of x1j) = SEEN_REMOVABLE ∨ x1j ∈# D)›
using in_lits ana ux1j_M
by (auto simp add: in_conflict_atm_in)
private lemma ccmin_lit_redundant_rec_wl_inv: ‹lit_redundant_rec_wl_inv M NU D
(x1, x2j, False)›
using x_x' last ana_lookup_conv rem rem2 x1a x1c le
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases)
(auto simp add: lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def
lit_redundant_reason_stack_def get_literal_and_remove_of_analyse_wl_def
list_rel_append_single_iff get_literal_and_remove_of_analyse_wl2_def)
lemma ccmin_already_seen_rel:
assumes
‹get_level M x1k = 0 ∨
conflict_min_cach x1b (atm_of x1k) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of x1k) D› and
‹get_level M x1j = 0 ∨ x1 (atm_of x1j) = SEEN_REMOVABLE ∨ x1j ∈# D›
shows ‹((x1b, x2k, False), x1, x2j, False)
∈ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
using x2k_x2j ccmin_lit_redundant_rec_wl_inv by auto
context
assumes
‹¬ (get_level M x1k = 0 ∨
conflict_min_cach x1b (atm_of x1k) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of x1k) D)› and
‹¬ (get_level M x1j = 0 ∨ x1 (atm_of x1j) = SEEN_REMOVABLE ∨ x1j ∈# D)›
begin
lemma ccmin_already_failed:
shows ‹(¬ level_in_lbd (get_level M x1k) lbd ∨
conflict_min_cach x1b (atm_of x1k) = SEEN_FAILED) =
(b ∨ x1 (atm_of x1j) = SEEN_FAILED)›
using b by auto
context
assumes
‹¬ level_in_lbd (get_level M x1k) lbd ∨
conflict_min_cach x1b (atm_of x1k) = SEEN_FAILED› and
‹b ∨ x1 (atm_of x1j) = SEEN_FAILED›
begin
lemma ccmin_mark_failed_lits_stack_inv2_lbd:
shows ‹mark_failed_lits_stack_inv2 NU x2k x1b›
using x1a x1c x2k_x2j rem rem2 x_x' le last
unfolding mark_failed_lits_stack_inv_def lit_redundant_rec_wl_inv_def
lit_redundant_rec_wl_ref_def get_literal_and_remove_of_analyse_wl_def
unfolding mark_failed_lits_stack_inv2_def
apply -
apply (rule exI[of _ x2j])
apply (cases ‹x1a› rule: rev_cases; cases ‹x1c› rule: rev_cases)
by (auto simp: mark_failed_lits_stack_inv_def elim!: in_set_upd_cases)
lemma ccmin_mark_failed_lits_wl_lbd:
shows ‹mark_failed_lits_wl NU x2k x1b
≤ ⇓ Id
(mark_failed_lits_wl NU x2j x1)›
by (auto simp: mark_failed_lits_wl_def)
lemma ccmin_rel_lbd:
fixes cach :: ‹nat ⇒ minimize_status› and cacha :: ‹nat ⇒ minimize_status›
assumes ‹(cach, cacha) ∈ Id›
shows ‹((cach, [], False), cacha, [], False) ∈ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
using x_x' assms by (auto simp: lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def)
end
context
assumes
‹¬ (¬ level_in_lbd (get_level M x1k) lbd ∨
conflict_min_cach x1b (atm_of x1k) = SEEN_FAILED)› and
‹¬ (b ∨ x1 (atm_of x1j) = SEEN_FAILED)›
begin
lemma ccmin_lit_in_trail:
‹- x1k ∈ lits_of_l M›
using ‹- x1j ∈ lits_of_l M› x1k_x1j(1) by blast
lemma ccmin_lit_eq:
‹- x1k = - x1j›
by auto
context
fixes xa :: ‹nat option› and x'a :: ‹nat option›
assumes xa_x'a: ‹(xa, x'a) ∈ ⟨nat_rel⟩option_rel›
begin
lemma ccmin_lit_eq2:
‹(xa, x'a) ∈ Id›
using xa_x'a by auto
context
assumes
[simp]: ‹xa = None› ‹x'a = None›
begin
lemma ccmin_mark_failed_lits_stack_inv2_dec:
‹mark_failed_lits_stack_inv2 NU x2k x1b›
using x1a x1c x2k_x2j rem rem2 x_x' le last
unfolding mark_failed_lits_stack_inv_def lit_redundant_rec_wl_inv_def
lit_redundant_rec_wl_ref_def get_literal_and_remove_of_analyse_wl_def
unfolding mark_failed_lits_stack_inv2_def
apply -
apply (rule exI[of _ x2j])
apply (cases ‹x1a› rule: rev_cases; cases ‹x1c› rule: rev_cases)
by (auto simp: mark_failed_lits_stack_inv_def elim!: in_set_upd_cases)
lemma ccmin_mark_failed_lits_stack_wl_dec:
shows ‹mark_failed_lits_wl NU x2k x1b
≤ ⇓ Id
(mark_failed_lits_wl NU x2j x1)›
by (auto simp: mark_failed_lits_wl_def)
lemma ccmin_rel_dec:
fixes cach :: ‹nat ⇒ minimize_status› and cacha :: ‹nat ⇒ minimize_status›
assumes ‹(cach, cacha) ∈ Id›
shows ‹((cach, [], False), cacha, [], False)
∈ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
using assms by (auto simp: lit_redundant_rec_wl_ref_def lit_redundant_rec_wl_inv_def)
end
context
fixes xb :: ‹nat› and x'b :: ‹nat›
assumes H:
‹xa = Some xb›
‹x'a = Some x'b›
‹(xb, x'b) ∈ nat_rel›
‹x'b ∈# dom_m NU›
‹2 ≤ length (NU ∝ x'b)›
‹x'b > 0›
‹distinct (NU ∝ x'b) ∧ ¬ tautology (mset (NU ∝ x'b))›
begin
lemma ccmin_stack_pre:
shows ‹xb ∈# dom_m NU› ‹2 ≤ length (NU ∝ xb)›
using H by auto
lemma ccmin_literals_are_in_ℒ⇩i⇩n_NU_xb:
shows ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ xb))›
using lits_NU multi_member_split[of xb ‹dom_m NU›] H
by (auto simp: ran_m_def literals_are_in_ℒ⇩i⇩n_mm_add_mset)
lemma ccmin_le_uint32_max_xb:
‹length (NU ∝ xb) ≤ Suc (uint32_max div 2)›
using simple_clss_size_upper_div2[OF bounded ccmin_literals_are_in_ℒ⇩i⇩n_NU_xb]
H unfolding x1g_x1d
by auto
private lemma ccmin_lit_redundant_rec_wl_inv3: ‹lit_redundant_rec_wl_inv M NU D
(x1, x2j @ [lit_redundant_reason_stack (- NU ∝ x1d ! x1f) NU x'b], False)›
using ccmin_stack_pre H x_x' last ana_lookup_conv rem rem2 x1a x1c le
by (cases x1a rule: rev_cases; cases x1c rule: rev_cases)
(auto simp add: lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def
lit_redundant_reason_stack_def get_literal_and_remove_of_analyse_wl_def
list_rel_append_single_iff get_literal_and_remove_of_analyse_wl2_def)
lemma ccmin_stack_rel:
shows ‹((x1b, x2k @ [lit_redundant_reason_stack2 (- x1k) NU xb], False), x1,
x2j @ [lit_redundant_reason_stack (- x1j) NU x'b], False)
∈ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}›
using x2k_x2j H ccmin_lit_redundant_rec_wl_inv3
by (auto simp: list_rel_append_single_iff ana_lookup_rel_alt_def
lit_redundant_reason_stack2_def lit_redundant_reason_stack_def)
end
end
end
end
end
end
end
end
end
end
end
end
lemma lit_redundant_rec_wl_lookup_lit_redundant_rec_wl:
assumes
M_D: ‹M ⊨as CNot D› and
n_d: ‹no_dup M› and
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M› and
‹(analysis, analysis') ∈ ana_lookups_rel NU› and
‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m NU)› and
‹isasat_input_bounded 𝒜›
shows
‹lit_redundant_rec_wl_lookup 𝒜 M NU D cach analysis lbd ≤
⇓ (Id ×⇩r (ana_lookups_rel NU) ×⇩r bool_rel) (lit_redundant_rec_wl M NU D cach analysis' lbd)›
proof -
have M: ‹∀a ∈ lits_of_l M. a ∈# ℒ⇩a⇩l⇩l 𝒜›
using literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l lits by blast
have [simp]: ‹- x1e ∈ lits_of_l M ⟹ atm_in_conflict (atm_of x1e) D ⟷ x1e ∈# D› for x1e
using M_D n_d
by (auto simp: atm_in_conflict_def true_annots_true_cls_def_iff_negation_in_model
atms_of_def atm_of_eq_atm_of dest!: multi_member_split no_dup_consistentD)
have [simp, intro]: ‹- x1e ∈ lits_of_l M ⟹ atm_of x1e ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
‹x1e ∈ lits_of_l M ⟹ x1e ∈# (ℒ⇩a⇩l⇩l 𝒜)›
‹- x1e ∈ lits_of_l M ⟹ x1e ∈# (ℒ⇩a⇩l⇩l 𝒜)› for x1e
using lits atm_of_notin_atms_of_iff literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l apply blast
using M uminus_𝒜⇩i⇩n_iff by auto
have [refine_vcg]: ‹(a, b) ∈ Id ⟹ (a, b) ∈ ⟨Id⟩option_rel› for a b by auto
have [refine_vcg]: ‹get_propagation_reason M x
≤ ⇓ (⟨nat_rel⟩option_rel) (get_propagation_reason M y)› if ‹x = y› for x y
by (use that in auto)
have [refine_vcg]:‹RETURN (¬ level_in_lbd (get_level M L) lbd) ≤ ⇓ Id (RES UNIV)› for L
by auto
have [refine_vcg]: ‹mark_failed_lits_wl NU a b
≤ ⇓ Id
(mark_failed_lits_wl NU a' b')› if ‹a = a'› and ‹b = b'› for a a' b b'
unfolding that by auto
have H: ‹lit_redundant_rec_wl_lookup 𝒜 M NU D cach analysis lbd ≤
⇓ {((cach, ana, b), cach', ana', b').
(ana, ana') ∈ ana_lookups_rel NU ∧
b = b' ∧ cach = cach' ∧ lit_redundant_rec_wl_inv M NU D (cach, ana', b)}
(lit_redundant_rec_wl M NU D cach analysis' lbd)›
using assms apply -
unfolding lit_redundant_rec_wl_lookup_def lit_redundant_rec_wl_def WHILET_def
apply (refine_vcg)
subgoal by (rule ccmin_rel)
subgoal by (rule ccmin_lit_redundant_rec_wl_inv2)
subgoal by (rule ccmin_cond)
subgoal by (rule ccmin_nempty)
subgoal by (auto simp: list_rel_imp_same_length)
subgoal by (rule ccmin_in_dom)
subgoal by (rule ccmin_in_dom_le_length)
subgoal by (rule ccmin_in_trail)
subgoal by (rule ccmin_in_all_lits)
subgoal by (rule ccmin_literals_are_in_ℒ⇩i⇩n_NU_x1g)
subgoal by (rule ccmin_le_uint32_max)
subgoal by (rule ccmin_less_length)
subgoal by (rule ccmin_same_cond)
subgoal by (rule ccmin_set_removable)
subgoal by (rule ccmin_x1k_all)
subgoal by (rule ccmin_already_seen)
subgoal by (rule ccmin_already_seen_rel)
subgoal by (rule ccmin_already_failed)
subgoal by (rule ccmin_mark_failed_lits_stack_inv2_lbd)
apply (rule ccmin_mark_failed_lits_wl_lbd; assumption)
subgoal by (rule ccmin_rel_lbd)
subgoal by (rule ccmin_lit_in_trail)
subgoal by (rule ccmin_lit_eq)
subgoal by (rule ccmin_lit_eq2)
subgoal by (rule ccmin_mark_failed_lits_stack_inv2_dec)
apply (rule ccmin_mark_failed_lits_stack_wl_dec; assumption)
subgoal by (rule ccmin_rel_dec)
subgoal by (rule ccmin_stack_pre)
subgoal by (rule ccmin_stack_pre)
subgoal by (rule ccmin_literals_are_in_ℒ⇩i⇩n_NU_xb)
subgoal by (rule ccmin_le_uint32_max_xb)
subgoal by (rule ccmin_stack_rel)
done
show ?thesis
by (rule H[THEN order_trans], rule conc_fun_R_mono)
auto
qed
definition literal_redundant_wl_lookup where
‹literal_redundant_wl_lookup 𝒜 M NU D cach L lbd = do {
ASSERT(L ∈# ℒ⇩a⇩l⇩l 𝒜);
if get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE
then RETURN (cach, [], True)
else if cach (atm_of L) = SEEN_FAILED
then RETURN (cach, [], False)
else do {
ASSERT(-L ∈ lits_of_l M);
C ← get_propagation_reason M (-L);
case C of
Some C ⇒ do {
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) ≥ 2);
ASSERT(literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ C)));
ASSERT(distinct (NU ∝ C) ∧ ¬tautology (mset (NU ∝ C)));
ASSERT(length (NU ∝ C) ≤ Suc (uint32_max div 2));
lit_redundant_rec_wl_lookup 𝒜 M NU D cach [lit_redundant_reason_stack2 (-L) NU C] lbd
}
| None ⇒ do {
RETURN (cach, [], False)
}
}
}›
lemma literal_redundant_wl_lookup_literal_redundant_wl:
assumes ‹M ⊨as CNot D› ‹no_dup M› ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M›
‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m NU)› and
‹isasat_input_bounded 𝒜›
shows
‹literal_redundant_wl_lookup 𝒜 M NU D cach L lbd ≤
⇓ (Id ×⇩f (ana_lookups_rel NU ×⇩f bool_rel)) (literal_redundant_wl M NU D cach L lbd)›
proof -
have M: ‹∀a ∈ lits_of_l M. a ∈# ℒ⇩a⇩l⇩l 𝒜›
using literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l assms by blast
have [simp, intro!]: ‹- x1e ∈ lits_of_l M ⟹ atm_of x1e ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
‹- x1e ∈ lits_of_l M ⟹ x1e ∈# (ℒ⇩a⇩l⇩l 𝒜)› for x1e
using assms atm_of_notin_atms_of_iff literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l apply blast
using M uminus_𝒜⇩i⇩n_iff by auto
have [refine]: ‹(x, x') ∈ Id ⟹ (x, x') ∈ ⟨Id⟩option_rel› for x x'
by auto
have [refine_vcg]: ‹get_propagation_reason M x
≤ ⇓ ({(C, C'). (C, C') ∈ ⟨nat_rel⟩option_rel})
(get_propagation_reason M y)› if ‹x = y› and ‹y ∈ lits_of_l M› for x y
by (use that in ‹auto simp: get_propagation_reason_def intro: RES_refine›)
show ?thesis
unfolding literal_redundant_wl_lookup_def literal_redundant_wl_def
apply (refine_vcg lit_redundant_rec_wl_lookup_lit_redundant_rec_wl)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal
using assms by (auto dest!: multi_member_split simp: ran_m_def literals_are_in_ℒ⇩i⇩n_mm_add_mset)
subgoal by auto
subgoal by auto
subgoal using assms simple_clss_size_upper_div2[of 𝒜 ‹mset (NU ∝ _)›] by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by (auto simp: lit_redundant_reason_stack2_def lit_redundant_reason_stack_def
ana_lookup_rel_def)
subgoal using assms by auto
subgoal using assms by auto
done
qed
definition (in -) lookup_conflict_nth where
[simp]: ‹lookup_conflict_nth = (λ(_, xs) i. xs ! i)›
definition (in -) lookup_conflict_size where
[simp]: ‹lookup_conflict_size = (λ(n, xs). n)›
definition (in -) lookup_conflict_upd_None where
[simp]: ‹lookup_conflict_upd_None = (λ(n, xs) i. (n-1, xs [i :=None]))›
definition minimize_and_extract_highest_lookup_conflict
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ nat clauses_l ⇒ nat clause ⇒ (nat ⇒ minimize_status) ⇒ lbd ⇒
out_learned ⇒ (nat clause × (nat ⇒ minimize_status) × out_learned) nres›
where
‹minimize_and_extract_highest_lookup_conflict 𝒜 = (λM NU nxs s lbd outl. do {
(D, _, s, outl) ←
WHILE⇩T⇗minimize_and_extract_highest_lookup_conflict_inv⇖
(λ(nxs, i, s, outl). i < length outl)
(λ(nxs, x, s, outl). do {
ASSERT(x < length outl);
let L = outl ! x;
ASSERT(L ∈# ℒ⇩a⇩l⇩l 𝒜);
(s', _, red) ← literal_redundant_wl_lookup 𝒜 M NU nxs s L lbd;
if ¬red
then RETURN (nxs, x+1, s', outl)
else do {
ASSERT (delete_from_lookup_conflict_pre 𝒜 (L, nxs));
RETURN (remove1_mset L nxs, x, s', delete_index_and_swap outl x)
}
})
(nxs, 1, s, outl);
RETURN (D, s, outl)
})›
lemma entails_uminus_filter_to_poslev_can_remove:
assumes NU_uL_E: ‹NU ⊨p add_mset (- L) (filter_to_poslev M' L E)› and
NU_E: ‹NU ⊨p E› and L_E: ‹L ∈# E›
shows ‹NU ⊨p remove1_mset L E›
proof -
have ‹filter_to_poslev M' L E ⊆# remove1_mset L E›
by (induction E)
(auto simp add: filter_to_poslev_add_mset remove1_mset_add_mset_If subset_mset_trans_add_mset
intro: diff_subset_eq_self subset_mset.dual_order.trans)
then have ‹NU ⊨p add_mset (- L) (remove1_mset L E)›
using NU_uL_E
by (meson conflict_minimize_intermediate_step mset_subset_eqD)
moreover have ‹NU ⊨p add_mset L (remove1_mset L E)›
using NU_E L_E by auto
ultimately show ?thesis
using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of NU L ‹remove1_mset L E›
‹remove1_mset L E›]
by (auto simp: true_clss_cls_add_self)
qed
lemma minimize_and_extract_highest_lookup_conflict_iterate_over_conflict:
fixes D :: ‹nat clause› and S' :: ‹nat twl_st_l› and NU :: ‹nat clauses_l› and S :: ‹nat twl_st_wl›
and S'' :: ‹nat twl_st›
defines
‹S''' ≡ state⇩W_of S''›
defines
‹M ≡ get_trail_wl S› and
NU: ‹NU ≡ get_clauses_wl S› and
NU'_def: ‹NU' ≡ mset `# ran_mf NU› and
NUE: ‹NUE ≡ get_unit_learned_clss_wl S + get_unit_init_clss_wl S› and
NUS: ‹NUS ≡ get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S› and
M': ‹M' ≡ trail S'''›
assumes
S_S': ‹(S, S') ∈ state_wl_l None› and
S'_S'': ‹(S', S'') ∈ twl_st_l None› and
D'_D: ‹mset (tl outl) = D› and
M_D: ‹M ⊨as CNot D› and
dist_D: ‹distinct_mset D› and
tauto: ‹¬tautology D› and
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M› and
struct_invs: ‹twl_struct_invs S''› and
add_inv: ‹twl_list_invs S'› and
cach_init: ‹conflict_min_analysis_inv M' s' (NU' + NUE + NUS) D› and
NU_P_D: ‹NU' + NUE + NUS ⊨pm add_mset K D› and
lits_D: ‹literals_are_in_ℒ⇩i⇩n 𝒜 D› and
lits_NU: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf NU)› and
K: ‹K = outl ! 0› and
outl_nempty: ‹outl ≠ []› and
bounded: ‹isasat_input_bounded 𝒜›
shows
‹minimize_and_extract_highest_lookup_conflict 𝒜 M NU D s' lbd outl ≤
⇓ ({((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧ outl ! 0 = K ∧
E' ⊆# D ∧ outl ≠ []})
(iterate_over_conflict K M NU' (NUE + NUS) D)›
(is ‹_ ≤ ⇓ ?R _›)
proof -
let ?UE = ‹get_unit_learned_clss_wl S›
let ?NE = ‹get_unit_init_clss_wl S›
let ?US = ‹get_subsumed_learned_clauses_wl S›
let ?NS = ‹get_subsumed_init_clauses_wl S›
define N U where
‹N ≡ mset `# init_clss_lf NU› and
‹U ≡ mset `# learned_clss_lf NU›
obtain E where
S''': ‹S''' = (M', N + ?NE + ?NS, U + ?UE + ?US, E)›
using M' S_S' S'_S'' unfolding S'''_def N_def U_def NU
by (cases S) (auto simp: state_wl_l_def twl_st_l_def
mset_take_mset_drop_mset')
then have NU_N_U: ‹mset `# ran_mf NU = N + U›
using NU S_S' S'_S'' unfolding S'''_def N_def U_def
apply (subst all_clss_l_ran_m[symmetric])
apply (subst image_mset_union[symmetric])
apply (subst image_mset_union[symmetric])
by (auto simp: mset_take_mset_drop_mset')
let ?NU = ‹N + ?NE + ?NS + U + ?UE + ?US›
have NU'_N_U: ‹NU' = N + U›
unfolding NU'_def N_def U_def mset_append[symmetric] image_mset_union[symmetric]
by auto
have NU'_NUE: ‹NU' + NUE = N + get_unit_init_clss_wl S + U + get_unit_learned_clss_wl S›
unfolding NUE NU'_N_U by (auto simp: ac_simps)
have struct_inv_S''': ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M', N + (?NE + ?NS),
U + (?UE + ?US), E)›
using struct_invs unfolding twl_struct_invs_def S'''_def[symmetric] S''' add.assoc
by fast
then have n_d: ‹no_dup M'›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
trail.simps by fast
then have n_d: ‹no_dup M›
using S_S' S'_S'' unfolding M_def M' S'''_def by (auto simp: twl_st_wl twl_st_l twl_st)
define R where
‹R = {((D':: nat clause, i, cach :: nat ⇒ minimize_status, outl' :: out_learned),
(F :: nat clause, E :: nat clause)).
i ≤ length outl' ∧
F ⊆# D ∧
E ⊆# F ∧
mset (drop i outl') = E ∧
mset (tl outl') = F ∧
conflict_min_analysis_inv M' cach (?NU) F ∧
?NU ⊨pm add_mset K F ∧
mset (tl outl') = D' ∧
i > 0 ∧ outl' ≠ [] ∧
outl' ! 0 = K
}›
have [simp]: ‹add_mset K (mset (tl outl)) = mset outl›
using D'_D K
by (cases outl) (auto simp: drop_Suc outl_nempty)
have ‹Suc 0 < length outl ⟹
highest_lit M (mset (take (Suc 0) (tl outl)))
(Some (outl ! Suc 0, get_level M (outl ! Suc 0)))›
using outl_nempty
by (cases outl; cases ‹tl outl›) (auto simp: highest_lit_def get_maximum_level_add_mset)
then have init_args_ref: ‹((D, 1, s', outl), D, D) ∈ R›
using D'_D cach_init NU_P_D dist_D tauto K
unfolding R_def NUE NU'_def NU_N_U NUS
by (auto simp: ac_simps drop_Suc outl_nempty ac_simps)
have init_lo_inv: ‹minimize_and_extract_highest_lookup_conflict_inv s'›
if
‹(s', s) ∈ R› and
‹iterate_over_conflict_inv M D s›
for s' s
proof -
have [dest!]: ‹mset b ⊆# D ⟹ length b ≤ size D› for b
using size_mset_mono by fastforce
show ?thesis
using that simple_clss_size_upper_div2[OF bounded lits_D dist_D tauto]
unfolding minimize_and_extract_highest_lookup_conflict_inv_def
by (auto simp: R_def uint32_max_def)
qed
have cond: ‹(m < length outl') = (D' ≠ {#})›
if
st'_st: ‹(st', st) ∈ R› and
‹minimize_and_extract_highest_lookup_conflict_inv st'› and
‹iterate_over_conflict_inv M D st› and
st:
‹x2b = (j, outl')›
‹x2a = (m, x2b)›
‹st' = (nxs, x2a)›
‹st = (E, D')›
for st' st nxs x2a m x2b j x2c D' E st2 st3 outl'
proof -
show ?thesis
using st'_st unfolding st R_def
by auto
qed
have redundant: ‹literal_redundant_wl_lookup 𝒜 M NU nxs cach
(outl' ! x1d) lbd
≤ ⇓ {((s', a', b'), b). b = b' ∧
(b ⟶ ?NU ⊨pm remove1_mset L (add_mset K E) ∧
conflict_min_analysis_inv M' s' ?NU (remove1_mset L E)) ∧
(¬b ⟶ ?NU ⊨pm add_mset K E ∧ conflict_min_analysis_inv M' s' ?NU E)}
(is_literal_redundant_spec K NU' (NUE+NUS) E L)›
(is ‹_ ≤ ⇓ ?red _›)
if
R: ‹(x, x') ∈ R› and
‹case x' of (D, D') ⇒ D' ≠ {#}› and
‹minimize_and_extract_highest_lookup_conflict_inv x› and
‹iterate_over_conflict_inv M D x'› and
st:
‹x' = (E, x1a)›
‹x2d = (cach, outl')›
‹x2c = (x1d, x2d)›
‹x = (nxs, x2c)› and
L: ‹(outl'!x1d, L) ∈ Id›
‹x1d < length outl'›
for x x' E x2 x1a x2a nxs x2c x1d x2d x1e x2e cach highest L outl' st3
proof -
let ?L = ‹(outl' ! x1d)›
have
‹x1d < length outl'› and
‹x1d ≤ length outl'› and
‹mset (tl outl') ⊆# D› and
‹E = mset (tl outl')› and
cach: ‹conflict_min_analysis_inv M' cach ?NU E› and
NU_P_E: ‹?NU ⊨pm add_mset K (mset (tl outl'))› and
‹nxs = mset (tl outl')› and
‹0 < x1d› and
[simp]: ‹L = outl'!x1d› and
‹E ⊆# D›
‹E = mset (tl outl')› and
‹E = nxs›
using R L unfolding R_def st
by auto
have M_x1: ‹M ⊨as CNot E›
by (metis CNot_plus M_D ‹E ⊆# D› subset_mset.le_iff_add true_annots_union)
then have M'_x1: ‹M' ⊨as CNot E›
using S_S' S'_S'' unfolding M' M_def S'''_def by (auto simp: twl_st twl_st_wl twl_st_l)
have ‹outl' ! x1d ∈# E›
using ‹E = mset (tl outl')› ‹x1d < length outl'› ‹0 < x1d›
by (auto simp: nth_in_set_tl)
have 1:
‹literal_redundant_wl_lookup 𝒜 M NU nxs cach ?L lbd ≤ ⇓ (Id ×⇩f (ana_lookups_rel NU ×⇩f bool_rel)) (literal_redundant_wl M NU nxs cach ?L lbd)›
by (rule literal_redundant_wl_lookup_literal_redundant_wl)
(use lits_NU n_d lits M_x1 struct_invs bounded add_inv ‹outl' ! x1d ∈# E› ‹E = nxs› in auto)
have 2:
‹literal_redundant_wl M NU nxs cach ?L lbd ≤ ⇓
(Id ×⇩r {(analyse, analyse'). analyse' = convert_analysis_list NU analyse ∧
lit_redundant_rec_wl_ref NU analyse} ×⇩r bool_rel)
(literal_redundant M' NU' nxs cach ?L)›
by (rule literal_redundant_wl_literal_redundant[of S S' S'',
unfolded M_def[symmetric] NU[symmetric] M'[symmetric] S'''_def[symmetric]
NU'_def[symmetric], THEN order_trans])
(use bounded S_S' S'_S'' M_x1 struct_invs add_inv ‹outl' ! x1d ∈# E› ‹E = nxs› in
‹auto simp: NU›)
have NU_alt_def: ‹?NU = N + (?NE + ?NS) + U + (?UE + ?US)›
by (auto simp: ac_simps)
have 3:
‹literal_redundant M' (N + U) nxs cach ?L ≤
literal_redundant_spec M' (N + U + (?NE + ?NS) + (?UE + ?US)) nxs ?L›
unfolding ‹E = nxs›[symmetric]
apply (rule literal_redundant_spec)
apply (rule struct_inv_S''')
apply (rule cach[unfolded NU_alt_def])
apply (rule ‹outl' ! x1d ∈# E›)
apply (rule M'_x1)
done
then have 3:
‹literal_redundant M' (NU') nxs cach ?L ≤ literal_redundant_spec M' ?NU nxs ?L›
by (auto simp: ac_simps NU'_N_U)
have ent: ‹?NU ⊨pm add_mset (- L) (filter_to_poslev M' L (add_mset K E))›
if ‹?NU ⊨pm add_mset (- L) (filter_to_poslev M' L E)›
using that by (auto simp: filter_to_poslev_add_mset add_mset_commute)
show ?thesis
apply (rule order.trans)
apply (rule 1)
apply (rule order.trans)
apply (rule ref_two_step')
apply (rule 2)
apply (subst conc_fun_chain)
apply (rule order.trans)
apply (rule ref_two_step'[OF 3])
unfolding literal_redundant_spec_def is_literal_redundant_spec_def
conc_fun_SPEC NU'_NUE[symmetric]
apply (rule SPEC_rule)
apply clarify
using NU_P_E ent ‹E = nxs› ‹E = mset (tl outl')›[symmetric] ‹outl' ! x1d ∈# E› NU'_NUE
apply (auto intro!: entails_uminus_filter_to_poslev_can_remove[of _ _ M'] NUE NUS ac_simps
filter_to_poslev_conflict_min_analysis_inv ac_simps simp del: diff_union_swap2)
apply (smt NU'_NUE NUS add.assoc add.commute set_mset_union)
apply (smt NU'_NUE NUS add.assoc add.commute set_mset_union)
done
qed
have
outl'_F: ‹outl' ! i ∈# F› (is ?out) and
outl'_ℒ⇩a⇩l⇩l: ‹outl' ! i ∈# ℒ⇩a⇩l⇩l 𝒜› (is ?out_L)
if
R: ‹(S, T) ∈ R› and
‹case S of (nxs, i, s, outl) ⇒ i < length outl› and
‹case T of (D, D') ⇒ D' ≠ {#}› and
‹minimize_and_extract_highest_lookup_conflict_inv S› and
‹iterate_over_conflict_inv M D T› and
st:
‹T = (F', F)›
‹S2 = (cach, outl')›
‹S1 = (i, S2)›
‹S = (D', S1)›
‹i < length outl'›
for S T F' T1 F highest' D' S1 i S2 cach S3 highest outl'
proof -
have ?out and ‹F ⊆# D›
using R ‹i < length outl'› unfolding R_def st
by (auto simp: set_drop_conv)
show ?out
using ‹?out› .
then have ‹outl' ! i ∈# D›
using ‹F ⊆# D› by auto
then show ?out_L
using lits_D by (auto dest!: multi_member_split simp: literals_are_in_ℒ⇩i⇩n_add_mset)
qed
have
not_red: ‹¬ red ⟹ ((D', i + 1, cachr, outl'), F',
remove1_mset L F) ∈ R› (is ‹_ ⟹ ?not_red›) and
red: ‹¬ ¬ red ⟹
((remove1_mset (outl' ! i) D', i, cachr, delete_index_and_swap outl' i),
remove1_mset L F', remove1_mset L F) ∈ R› (is ‹_ ⟹ ?red›) and
del: ‹delete_from_lookup_conflict_pre 𝒜 (outl' ! i, D')› (is ?del)
if
R: ‹(S, T) ∈ R› and
‹case S of (nxs, i, s, outl) ⇒ i < length outl› and
‹case T of (D, D') ⇒ D' ≠ {#}› and
‹minimize_and_extract_highest_lookup_conflict_inv S› and
‹iterate_over_conflict_inv M D T› and
st:
‹T = (F', F)›
‹S2 = (cach, outl')›
‹S1 = (i, S2)›
‹S = (D', S1)›
‹cachred1 = (stack, red)›
‹cachred = (cachr, cachred1)› and
‹i < length outl'› and
L: ‹(outl' ! i, L) ∈ Id› and
‹outl' ! i ∈# ℒ⇩a⇩l⇩l 𝒜› and
cach: ‹(cachred, red') ∈ (?red F' L)›
for S T F' T1 F D' S1 i S2 cach S3 highest outl' L cachred red' cachr
cachred1 stack red
proof -
have ‹L = outl' ! i› and
‹i ≤ length outl'› and
‹mset (tl outl') ⊆# D› and
‹mset (drop i outl') ⊆# mset (tl outl')› and
F: ‹F = mset (drop i outl')› and
F': ‹F' = mset (tl outl')› and
‹conflict_min_analysis_inv M' cach ?NU (mset (tl outl'))› and
‹?NU ⊨pm add_mset K (mset (tl outl'))› and
‹D' = mset (tl outl')› and
‹0 < i› and
[simp]: ‹D' = F'› and
F'_D: ‹F' ⊆# D› and
F'_F: ‹F ⊆# F'› and
‹outl' ≠ []› ‹outl' ! 0 = K›
using R L unfolding R_def st
by clarify+
have [simp]: ‹L = outl' ! i›
using L by fast
have L_F: ‹mset (drop (Suc i) outl') = remove1_mset L F›
unfolding F
apply (subst (2) Cons_nth_drop_Suc[symmetric])
using ‹i < length outl'› F'_D
by (auto)
have ‹remove1_mset (outl' ! i) F ⊆# F'›
using ‹F ⊆# F'›
by auto
have ‹red' = red› and
red: ‹red ⟶ ?NU ⊨pm remove1_mset L (add_mset K F') ∧
conflict_min_analysis_inv M' cachr ?NU (remove1_mset L F')› and
not_red: ‹¬ red ⟶ ?NU ⊨pm add_mset K F' ∧ conflict_min_analysis_inv M' cachr ?NU F'›
using cach
unfolding st
by auto
have [simp]: ‹mset (drop (Suc i) (swap outl' (Suc 0) i)) = mset (drop (Suc i) outl')›
by (subst drop_swap_irrelevant) (use ‹0 < i› in auto)
have [simp]: ‹mset (tl (swap outl' (Suc 0) i)) = mset (tl outl')›
apply (cases outl'; cases i)
using ‹i > 0› ‹outl' ≠ []› ‹i < length outl'›
apply (auto simp: WB_More_Refinement_List.swap_def)
unfolding WB_More_Refinement_List.swap_def[symmetric]
by (auto simp: )
have [simp]: ‹mset (take (Suc i) (tl (swap outl' (Suc 0) i))) = mset (take (Suc i) (tl outl'))›
using ‹i > 0› ‹outl' ≠ []› ‹i < length outl'›
by (auto simp: take_tl take_swap_relevant tl_swap_relevant)
have [simp]: ‹mset (take i (tl (swap outl' (Suc 0) i))) = mset (take i (tl outl'))›
using ‹i > 0› ‹outl' ≠ []› ‹i < length outl'›
by (auto simp: take_tl take_swap_relevant tl_swap_relevant)
have [simp]: ‹¬ Suc 0 < a ⟷ a = 0 ∨ a = 1› for a :: nat
by auto
show ?not_red if ‹¬red›
using ‹i < length outl'› F'_D L_F ‹remove1_mset (outl' ! i) F ⊆# F'› not_red that
‹i > 0› ‹outl' ! 0 = K›
by (auto simp: R_def F[symmetric] F'[symmetric] drop_swap_irrelevant)
have [simp]: ‹length (delete_index_and_swap outl' i) = length outl' - 1›
by auto
have last: ‹¬ length outl' ≤ Suc i ⟹last outl' ∈ set (drop (Suc i) outl')›
by (metis List.last_in_set drop_eq_Nil last_drop not_le_imp_less)
then have H: ‹mset (drop i (delete_index_and_swap outl' i)) = mset (drop (Suc i) outl')›
using ‹i < length outl'›
by (cases ‹drop (Suc i) outl' = []›)
(auto simp: butlast_list_update mset_butlast_remove1_mset)
have H': ‹mset (tl (delete_index_and_swap outl' i)) = remove1_mset (outl' ! i) (mset (tl outl'))›
apply (rule mset_tl_delete_index_and_swap)
using ‹i < length outl'› ‹i > 0› by fast+
have [simp]: ‹Suc 0 < i ⟹ delete_index_and_swap outl' i ! Suc 0 = outl' ! Suc 0›
using ‹i < length outl'› ‹i > 0›
by (auto simp: nth_butlast)
have ‹remove1_mset (outl' ! i) F ⊆# remove1_mset (outl' ! i) F'›
using ‹F ⊆# F'›
using mset_le_subtract by blast
have [simp]: ‹delete_index_and_swap outl' i ≠ []›
using ‹outl' ≠ []› ‹i > 0› ‹i < length outl'›
by (cases outl') (auto simp: butlast_update'[symmetric] split: nat.splits)
have [simp]: ‹delete_index_and_swap outl' i ! 0 = outl' ! 0›
using ‹outl' ! 0 = K› ‹i < length outl'› ‹i > 0›
by (auto simp: butlast_update'[symmetric] nth_butlast)
have ‹(outl' ! i) ∈# F'›
using ‹i < length outl'› ‹i > 0› unfolding F' by (auto simp: nth_in_set_tl)
then show ?red if ‹¬¬red›
using ‹i < length outl'› F'_D L_F ‹remove1_mset (outl' ! i) F ⊆# remove1_mset (outl' ! i) F'›
red that ‹i > 0› ‹outl' ! 0 = K› unfolding R_def
by (auto simp: R_def F[symmetric] F'[symmetric] H H' drop_swap_irrelevant
simp del: delete_index_and_swap.simps)
have ‹outl' ! i ∈# ℒ⇩a⇩l⇩l 𝒜› ‹outl' ! i ∈# D›
using ‹(outl' ! i) ∈# F'› F'_D lits_D
by (force simp: literals_are_in_ℒ⇩i⇩n_add_mset
dest!: multi_member_split[of ‹outl' ! i› D])+
then show ?del
using ‹(outl' ! i) ∈# F'› lits_D F'_D tauto
by (auto simp: delete_from_lookup_conflict_pre_def
literals_are_in_ℒ⇩i⇩n_add_mset)
qed
show ?thesis
unfolding minimize_and_extract_highest_lookup_conflict_def iterate_over_conflict_def
apply (refine_vcg WHILEIT_refine[where R = R])
subgoal by (rule init_args_ref)
subgoal for s' s by (rule init_lo_inv)
subgoal by (rule cond)
subgoal by auto
subgoal by (rule outl'_F)
subgoal by (rule outl'_ℒ⇩a⇩l⇩l)
apply (rule redundant; assumption)
subgoal by auto
subgoal by (rule not_red)
subgoal by (rule del)
subgoal
by (rule red)
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c
unfolding R_def by (cases x1b) auto
done
qed
definition cach_refinement_list
:: ‹nat multiset ⇒ (minimize_status list × (nat conflict_min_cach)) set›
where
‹cach_refinement_list 𝒜⇩i⇩n = ⟨Id⟩map_fun_rel {(a, a'). a = a' ∧ a ∈# 𝒜⇩i⇩n}›
definition cach_refinement_nonull
:: ‹nat multiset ⇒ ((minimize_status list × nat list) × minimize_status list) set›
where
‹cach_refinement_nonull 𝒜 = {((cach, support), cach'). cach = cach' ∧
(∀L < length cach. cach ! L ≠ SEEN_UNKNOWN ⟷ L ∈ set support) ∧
(∀L ∈ set support. L < length cach) ∧
distinct support ∧ set support ⊆ set_mset 𝒜}›
definition cach_refinement
:: ‹nat multiset ⇒ ((minimize_status list × nat list) × (nat conflict_min_cach)) set›
where
‹cach_refinement 𝒜⇩i⇩n = cach_refinement_nonull 𝒜⇩i⇩n O cach_refinement_list 𝒜⇩i⇩n›
lemma cach_refinement_alt_def:
‹cach_refinement 𝒜⇩i⇩n = {((cach, support), cach').
(∀L < length cach. cach ! L ≠ SEEN_UNKNOWN ⟷ L ∈ set support) ∧
(∀L ∈ set support. L < length cach) ∧
(∀L ∈# 𝒜⇩i⇩n. L < length cach ∧ cach ! L = cach' L) ∧
distinct support ∧ set support ⊆ set_mset 𝒜⇩i⇩n}›
unfolding cach_refinement_def cach_refinement_nonull_def cach_refinement_list_def
apply (rule; rule)
apply (simp add: map_fun_rel_def split: prod.splits)
apply blast
apply (simp add: map_fun_rel_def split: prod.splits)
apply (rule_tac b=x1a in relcomp.relcompI)
apply blast
apply blast
done
lemma in_cach_refinement_alt_def:
‹((cach, support), cach') ∈ cach_refinement 𝒜⇩i⇩n ⟷
(cach, cach') ∈ cach_refinement_list 𝒜⇩i⇩n ∧
(∀L<length cach. cach ! L ≠ SEEN_UNKNOWN ⟷ L ∈ set support) ∧
(∀L ∈ set support. L < length cach) ∧
distinct support ∧ set support ⊆ set_mset 𝒜⇩i⇩n›
by (auto simp: cach_refinement_def cach_refinement_nonull_def cach_refinement_list_def)
definition (in -) conflict_min_cach_l :: ‹conflict_min_cach_l ⇒ nat ⇒ minimize_status› where
‹conflict_min_cach_l = (λ(cach, sup) L.
(cach ! L)
)›
definition conflict_min_cach_l_pre where
‹conflict_min_cach_l_pre = (λ((cach, sup), L). L < length cach)›
lemma conflict_min_cach_l_pre:
fixes x1 :: ‹nat› and x2 :: ‹nat›
assumes
‹x1n ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹(x1l, x1j) ∈ cach_refinement 𝒜›
shows ‹conflict_min_cach_l_pre (x1l, atm_of x1n)›
proof -
show ?thesis
using assms by (auto simp: cach_refinement_alt_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n conflict_min_cach_l_pre_def)
qed
lemma nth_conflict_min_cach:
‹(uncurry (RETURN oo conflict_min_cach_l), uncurry (RETURN oo conflict_min_cach)) ∈
[λ(cach, L). L ∈# 𝒜⇩i⇩n]⇩f cach_refinement 𝒜⇩i⇩n ×⇩r nat_rel → ⟨Id⟩nres_rel›
by (intro frefI nres_relI) (auto simp: map_fun_rel_def
in_cach_refinement_alt_def cach_refinement_list_def conflict_min_cach_l_def)
definition (in -) conflict_min_cach_set_failed
:: ‹nat conflict_min_cach ⇒ nat ⇒ nat conflict_min_cach›
where
[simp]: ‹conflict_min_cach_set_failed cach L = cach(L := SEEN_FAILED)›
definition (in -) conflict_min_cach_set_failed_l
:: ‹conflict_min_cach_l ⇒ nat ⇒ conflict_min_cach_l nres›
where
‹conflict_min_cach_set_failed_l = (λ(cach, sup) L. do {
ASSERT(L < length cach);
ASSERT(length sup ≤ 1 + uint32_max div 2);
RETURN (cach[L := SEEN_FAILED], if cach ! L = SEEN_UNKNOWN then sup @ [L] else sup)
})›
lemma bounded_included_le:
assumes bounded: ‹isasat_input_bounded 𝒜› and ‹distinct n› and ‹set n ⊆ set_mset 𝒜›
shows ‹length n ≤ Suc (uint32_max div 2)›
proof -
have lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (Pos `# mset n)› and
dist: ‹distinct n›
using assms
by (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def inj_on_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
have dist: ‹distinct_mset (Pos `# mset n)›
by (subst distinct_image_mset_inj)
(use dist in ‹auto simp: inj_on_def›)
have tauto: ‹¬ tautology (poss (mset n))›
by (auto simp: tautology_decomp)
show ?thesis
using simple_clss_size_upper_div2[OF bounded lits dist tauto]
by (auto simp: uint32_max_def)
qed
lemma conflict_min_cach_set_failed:
‹(uncurry conflict_min_cach_set_failed_l, uncurry (RETURN oo conflict_min_cach_set_failed)) ∈
[λ(cach, L). L ∈# 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f cach_refinement 𝒜⇩i⇩n ×⇩r nat_rel → ⟨cach_refinement 𝒜⇩i⇩n⟩nres_rel›
supply isasat_input_bounded_def[simp del]
apply (intro frefI nres_relI)
apply (auto simp: in_cach_refinement_alt_def map_fun_rel_def cach_refinement_list_def
conflict_min_cach_set_failed_l_def cach_refinement_nonull_def
all_conj_distrib intro!: ASSERT_leI bounded_included_le[of 𝒜⇩i⇩n]
dest!: multi_member_split dest: set_mset_mono
dest: subset_add_mset_notin_subset_mset)
by (fastforce dest: subset_add_mset_notin_subset_mset)+
definition (in -) conflict_min_cach_set_removable
:: ‹nat conflict_min_cach ⇒ nat ⇒ nat conflict_min_cach›
where
[simp]: ‹conflict_min_cach_set_removable cach L = cach(L:= SEEN_REMOVABLE)›
lemma conflict_min_cach_set_removable:
‹(uncurry conflict_min_cach_set_removable_l,
uncurry (RETURN oo conflict_min_cach_set_removable)) ∈
[λ(cach, L). L ∈# 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f cach_refinement 𝒜⇩i⇩n ×⇩r nat_rel → ⟨cach_refinement 𝒜⇩i⇩n⟩nres_rel›
supply isasat_input_bounded_def[simp del]
by (intro frefI nres_relI)
(auto 5 5 simp: in_cach_refinement_alt_def map_fun_rel_def cach_refinement_list_def
conflict_min_cach_set_removable_l_def cach_refinement_nonull_def
all_conj_distrib intro!: ASSERT_leI bounded_included_le[of 𝒜⇩i⇩n]
dest!: multi_member_split dest: set_mset_mono
dest: subset_add_mset_notin_subset_mset)
definition isa_mark_failed_lits_stack where
‹isa_mark_failed_lits_stack NU analyse cach = do {
let l = length analyse;
ASSERT(length analyse ≤ 1 + uint32_max div 2);
(_, cach) ← WHILE⇩T⇗λ(_, cach). True⇖
(λ(i, cach). i < l)
(λ(i, cach). do {
ASSERT(i < length analyse);
let (cls_idx, idx, _) = (analyse ! i);
ASSERT(cls_idx + idx ≥ 1);
ASSERT(cls_idx + idx - 1 < length NU);
ASSERT(arena_lit_pre NU (cls_idx + idx - 1));
cach ← conflict_min_cach_set_failed_l cach (atm_of (arena_lit NU (cls_idx + idx - 1)));
RETURN (i+1, cach)
})
(0, cach);
RETURN cach
}›
context
begin
lemma mark_failed_lits_stack_inv_helper1: ‹mark_failed_lits_stack_inv a ba a2' ⟹
a1' < length ba ⟹
(a1'a, a2'a) = ba ! a1' ⟹
a1'a ∈# dom_m a›
using nth_mem[of a1' ba] unfolding mark_failed_lits_stack_inv_def
by (auto simp del: nth_mem)
lemma mark_failed_lits_stack_inv_helper2: ‹mark_failed_lits_stack_inv a ba a2' ⟹
a1' < length ba ⟹
(a1'a, xx, a2'a, yy) = ba ! a1' ⟹
a2'a - Suc 0 < length (a ∝ a1'a)›
using nth_mem[of a1' ba] unfolding mark_failed_lits_stack_inv_def
by (auto simp del: nth_mem)
lemma isa_mark_failed_lits_stack_isa_mark_failed_lits_stack:
assumes ‹isasat_input_bounded 𝒜⇩i⇩n›
shows ‹(uncurry2 isa_mark_failed_lits_stack, uncurry2 (mark_failed_lits_stack 𝒜⇩i⇩n)) ∈
[λ((N, ana), cach). length ana ≤ 1 + uint32_max div 2]⇩f
{(arena, N). valid_arena arena N vdom} ×⇩f ana_lookups_rel NU ×⇩f cach_refinement 𝒜⇩i⇩n →
⟨cach_refinement 𝒜⇩i⇩n⟩nres_rel›
proof -
have subset_mset_add_new: ‹a ∉# A ⟹ a ∈# B ⟹ add_mset a A ⊆# B ⟷ A ⊆# B› for a A B
by (metis insert_DiffM insert_subset_eq_iff subset_add_mset_notin_subset)
have [refine0]: ‹((0, x2c), 0, x2a) ∈ nat_rel ×⇩f cach_refinement 𝒜⇩i⇩n›
if ‹(x2c, x2a) ∈ cach_refinement 𝒜⇩i⇩n› for x2c x2a
using that by auto
have le_length_arena: ‹x1g + x2g - 1 < length x1c› (is ?le) and
is_lit: ‹arena_lit_pre x1c (x1g + x2g - 1)› (is ?lit) and
isA: ‹atm_of (arena_lit x1c (x1g + x2g - 1)) ∈# 𝒜⇩i⇩n› (is ?A) and
final: ‹conflict_min_cach_set_failed_l x2e
(atm_of (arena_lit x1c (x1g + x2g - 1)))
≤ SPEC
(λcach.
RETURN (x1e + 1, cach)
≤ SPEC
(λc. (c, x1d + 1, x2d
(atm_of (x1a ∝ x1f ! (x2f - 1)) := SEEN_FAILED))
∈ nat_rel ×⇩f cach_refinement 𝒜⇩i⇩n))› (is ?final) and
ge1: ‹x1g + x2g ≥ 1›
if
‹case y of (x, xa) ⇒ (case x of (N, ana) ⇒ λcach. length ana ≤ 1 + uint32_max div 2) xa› and
xy: ‹(x, y) ∈ {(arena, N). valid_arena arena N vdom} ×⇩f ana_lookups_rel NU
×⇩f cach_refinement 𝒜⇩i⇩n› and
st:
‹x1 = (x1a, x2)›
‹y = (x1, x2a)›
‹x1b = (x1c, x2b)›
‹x = (x1b, x2c)›
‹x' = (x1d, x2d)›
‹xa = (x1e, x2e)›
‹x2f2 = (x2f, x2f3)›
‹x2f0 = (x2f1, x2f2)›
‹x2 ! x1d = (x1f, x2f0)›
‹x2g0 = (x2g, x2g2)›
‹x2b ! x1e = (x1g, x2g0)› and
xax': ‹(xa, x') ∈ nat_rel ×⇩f cach_refinement 𝒜⇩i⇩n› and
cond: ‹case xa of (i, cach) ⇒ i < length x2b› and
cond': ‹case x' of (i, cach) ⇒ i < length x2› and
inv: ‹case x' of (_, x) ⇒ mark_failed_lits_stack_inv x1a x2 x› and
le: ‹x1d < length x2› ‹x1e < length x2b› and
atm: ‹atm_of (x1a ∝ x1f ! (x2f - 1)) ∈# 𝒜⇩i⇩n›
for x y x1 x1a x2 x2a x1b x1c x2b x2c xa x' x1d x2d x1e x2e x1f x2f x1g x2g
x2f0 x2f1 x2f2 x2f3 x2g0 x2g1 x2g2 x2g3
proof -
obtain i cach where x': ‹x' = (i, cach)› by (cases x')
have [simp]:
‹x1 = (x1a, x2)›
‹y = ((x1a, x2), x2a)›
‹x1b = (x1c, x2b)›
‹x = ((x1c, x2b), x2c)›
‹x' = (x1d, x2d)›
‹xa = (x1d, x2e)›
‹x1f = x1g›
‹x1e = x1d›
‹x2f0 = (x2f1, x2f, x2f3)›
‹x2g = x2f›
‹x2g0 = (x2g, x2g2)› and
st': ‹x2 ! x1d = (x1g, x2f0)› and
cach:‹(x2e, x2d) ∈ cach_refinement 𝒜⇩i⇩n› and
‹(x2c, x2a) ∈ cach_refinement 𝒜⇩i⇩n› and
x2f0_x2g0: ‹((x1g, x2g, x2g2), (x1f, x2f1, x2f, x2f3)) ∈ ana_lookup_rel NU›
using xy st xax' param_nth[of x1e x2 x1d x2b ‹ana_lookup_rel NU›] le
by (auto intro: simp: ana_lookup_rel_alt_def)
have arena: ‹valid_arena x1c x1a vdom›
using xy unfolding st by auto
have ‹x2 ! x1e ∈ set x2›
using le
by auto
then have ‹x2 ! x1d ∈ set x2› and
x2f: ‹x2f ≤ length (x1a ∝ x1f)› and
x1f: ‹x1g ∈# dom_m x1a› and
x2g: ‹x2g > 0› and
x2g_u1_le: ‹x2g - 1 < length (x1a ∝ x1f)›
using inv le x2f0_x2g0 nth_mem[of x1d x2]
unfolding mark_failed_lits_stack_inv_def x' prod.case st st'
by (auto simp del: nth_mem simp: st' ana_lookup_rel_alt_def split: if_splits
dest!: bspec[of ‹set x2› _ ‹(_, _, _, _)›])
have ‹is_Lit (x1c ! (x1g + (x2g - 1)))›
by (rule arena_lifting[OF arena x1f]) (use x2f x2g x2g_u1_le in auto)
then show ?le and ?A
using arena_lifting[OF arena x1f] le x2f x1f x2g atm x2g_u1_le
by (auto simp: arena_lit_def)
show ?lit
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by (rule bex_leI[of _ x1f])
(use arena x1f x2f x2g x2g_u1_le in ‹auto intro!: exI[of _ x1a] exI[of _ vdom]›)
show ‹x1g + x2g ≥ 1›
using x2g by auto
have [simp]: ‹arena_lit x1c (x1g + x2g - Suc 0) = x1a ∝ x1g ! (x2g - Suc 0)›
using that x1f x2f x2g x2g_u1_le by (auto simp: arena_lifting[OF arena])
have ‹atm_of (arena_lit x1c (x1g + x2g - Suc 0)) < length (fst x2e)›
using ‹?A› cach by (auto simp: cach_refinement_alt_def dest: multi_member_split)
then show ?final
using ‹?le› ‹?A› cach x1f x2g_u1_le x2g assms
apply -
apply (rule conflict_min_cach_set_failed[of 𝒜⇩i⇩n, THEN fref_to_Down_curry, THEN order_trans])
by (cases x2e)
(auto simp: cach_refinement_alt_def RETURN_def conc_fun_RES
arena_lifting[OF arena] subset_mset_add_new)
qed
show ?thesis
unfolding isa_mark_failed_lits_stack_def mark_failed_lits_stack_def uncurry_def
apply (rewrite at ‹let _ = length _ in _› Let_def)
apply (intro frefI nres_relI)
apply refine_vcg
subgoal by (auto simp: list_rel_imp_same_length)
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c xa x' x1d x2d x1e x2e
by (auto simp: list_rel_imp_same_length)
subgoal by auto
subgoal by (rule ge1)
subgoal by (rule le_length_arena)
subgoal
by (rule is_lit)
subgoal
by (rule final)
subgoal by auto
done
qed
definition isa_get_literal_and_remove_of_analyse_wl
:: ‹arena ⇒ (nat × nat × bool) list ⇒ nat literal × (nat × nat × bool) list› where
‹isa_get_literal_and_remove_of_analyse_wl C analyse =
(let (i, j, b) = (last analyse) in
(arena_lit C (i + j), analyse[length analyse - 1 := (i, j + 1, b)]))›
definition isa_get_literal_and_remove_of_analyse_wl_pre
:: ‹arena ⇒ (nat × nat × bool) list ⇒ bool› where
‹isa_get_literal_and_remove_of_analyse_wl_pre arena analyse ⟷
(let (i, j, b) = last analyse in
analyse ≠ [] ∧ arena_lit_pre arena (i+j) ∧ j < uint32_max)›
lemma arena_lit_pre_le: ‹length a ≤ uint64_max ⟹
arena_lit_pre a i ⟹ i ≤ uint64_max›
using arena_lifting(7)[of a _ _] unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by fastforce
lemma arena_lit_pre_le2: ‹length a ≤ uint64_max ⟹
arena_lit_pre a i ⟹ i < uint64_max›
using arena_lifting(7)[of a _ _] unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by fastforce
definition lit_redundant_reason_stack_wl_lookup_pre :: ‹nat literal ⇒ arena_el list ⇒ nat ⇒ bool› where
‹lit_redundant_reason_stack_wl_lookup_pre L NU C ⟷
arena_lit_pre NU C ∧
arena_is_valid_clause_idx NU C›
definition lit_redundant_reason_stack_wl_lookup
:: ‹nat literal ⇒ arena_el list ⇒ nat ⇒ nat × nat × bool›
where
‹lit_redundant_reason_stack_wl_lookup L NU C =
(if arena_length NU C > 2 then (C, 1, False)
else if arena_lit NU C = L
then (C, 1, False)
else (C, 0, True))›
definition ana_lookup_conv_lookup :: ‹arena ⇒ (nat × nat × bool) ⇒ (nat × nat × nat × nat)› where
‹ana_lookup_conv_lookup NU = (λ(C, i, b).
(C, (if b then 1 else 0), i, (if b then 1 else arena_length NU C)))›
definition ana_lookup_conv_lookup_pre :: ‹arena ⇒ (nat × nat × bool) ⇒ bool› where
‹ana_lookup_conv_lookup_pre NU = (λ(C, i, b). arena_is_valid_clause_idx NU C)›
definition isa_lit_redundant_rec_wl_lookup
:: ‹trail_pol ⇒ arena ⇒ lookup_clause_rel ⇒
_ ⇒ _ ⇒ _ ⇒ (_ × _ × bool) nres›
where
‹isa_lit_redundant_rec_wl_lookup M NU D cach analysis lbd =
WHILE⇩T⇗λ_. True⇖
(λ(cach, analyse, b). analyse ≠ [])
(λ(cach, analyse, b). do {
ASSERT(analyse ≠ []);
ASSERT(length analyse ≤ 1 + uint32_max div 2);
ASSERT(arena_is_valid_clause_idx NU (fst (last analyse)));
ASSERT(ana_lookup_conv_lookup_pre NU ((last analyse)));
let (C, k, i, len) = ana_lookup_conv_lookup NU ((last analyse));
ASSERT(C < length NU);
ASSERT(arena_is_valid_clause_idx NU C);
ASSERT(arena_lit_pre NU (C + k));
if i ≥ len
then do {
cach ← conflict_min_cach_set_removable_l cach (atm_of (arena_lit NU (C + k)));
RETURN(cach, butlast analyse, True)
}
else do {
ASSERT (isa_get_literal_and_remove_of_analyse_wl_pre NU analyse);
let (L, analyse) = isa_get_literal_and_remove_of_analyse_wl NU analyse;
ASSERT(length analyse ≤ 1 + uint32_max div 2);
ASSERT(get_level_pol_pre (M, L));
let b = ¬level_in_lbd (get_level_pol M L) lbd;
ASSERT(atm_in_conflict_lookup_pre (atm_of L) D);
ASSERT(conflict_min_cach_l_pre (cach, atm_of L));
if (get_level_pol M L = 0 ∨
conflict_min_cach_l cach (atm_of L) = SEEN_REMOVABLE ∨
atm_in_conflict_lookup (atm_of L) D)
then RETURN (cach, analyse, False)
else if b ∨ conflict_min_cach_l cach (atm_of L) = SEEN_FAILED
then do {
cach ← isa_mark_failed_lits_stack NU analyse cach;
RETURN (cach, take 0 analyse, False)
}
else do {
C ← get_propagation_reason_pol M (-L);
case C of
Some C ⇒ do {
ASSERT(lit_redundant_reason_stack_wl_lookup_pre (-L) NU C);
RETURN (cach, analyse @ [lit_redundant_reason_stack_wl_lookup (-L) NU C], False)
}
| None ⇒ do {
cach ← isa_mark_failed_lits_stack NU analyse cach;
RETURN (cach, take 0 analyse, False)
}
}
}
})
(cach, analysis, False)›
lemma isa_lit_redundant_rec_wl_lookup_alt_def:
‹isa_lit_redundant_rec_wl_lookup M NU D cach analysis lbd =
WHILE⇩T⇗λ_. True⇖
(λ(cach, analyse, b). analyse ≠ [])
(λ(cach, analyse, b). do {
ASSERT(analyse ≠ []);
ASSERT(length analyse ≤ 1 + uint32_max div 2);
let (C, i, b) = last analyse;
ASSERT(arena_is_valid_clause_idx NU (fst (last analyse)));
ASSERT(ana_lookup_conv_lookup_pre NU (last analyse));
let (C, k, i, len) = ana_lookup_conv_lookup NU ((C, i, b));
ASSERT(C < length NU);
let _ = map xarena_lit
((Misc.slice
C
(C + arena_length NU C))
NU);
ASSERT(arena_is_valid_clause_idx NU C);
ASSERT(arena_lit_pre NU (C + k));
if i ≥ len
then do {
cach ← conflict_min_cach_set_removable_l cach (atm_of (arena_lit NU (C + k)));
RETURN(cach, butlast analyse, True)
}
else do {
ASSERT (isa_get_literal_and_remove_of_analyse_wl_pre NU analyse);
let (L, analyse) = isa_get_literal_and_remove_of_analyse_wl NU analyse;
ASSERT(length analyse ≤ 1+ uint32_max div 2);
ASSERT(get_level_pol_pre (M, L));
let b = ¬level_in_lbd (get_level_pol M L) lbd;
ASSERT(atm_in_conflict_lookup_pre (atm_of L) D);
ASSERT(conflict_min_cach_l_pre (cach, atm_of L));
if (get_level_pol M L = 0 ∨
conflict_min_cach_l cach (atm_of L) = SEEN_REMOVABLE ∨
atm_in_conflict_lookup (atm_of L) D)
then RETURN (cach, analyse, False)
else if b ∨ conflict_min_cach_l cach (atm_of L) = SEEN_FAILED
then do {
cach ← isa_mark_failed_lits_stack NU analyse cach;
RETURN (cach, [], False)
}
else do {
C ← get_propagation_reason_pol M (-L);
case C of
Some C ⇒ do {
ASSERT(lit_redundant_reason_stack_wl_lookup_pre (-L) NU C);
RETURN (cach, analyse @ [lit_redundant_reason_stack_wl_lookup (-L) NU C], False)
}
| None ⇒ do {
cach ← isa_mark_failed_lits_stack NU analyse cach;
RETURN (cach, [], False)
}
}
}
})
(cach, analysis, False)›
unfolding isa_lit_redundant_rec_wl_lookup_def Let_def take_0
by (auto simp: Let_def)
lemma lit_redundant_rec_wl_lookup_alt_def:
‹lit_redundant_rec_wl_lookup 𝒜 M NU D cach analysis lbd =
WHILE⇩T⇗lit_redundant_rec_wl_inv2 M NU D⇖
(λ(cach, analyse, b). analyse ≠ [])
(λ(cach, analyse, b). do {
ASSERT(analyse ≠ []);
ASSERT(length analyse ≤ length M);
let (C, k, i, len) = ana_lookup_conv NU (last analyse);
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) > k); ― ‹ >= 2 would work too ›
ASSERT (NU ∝ C ! k ∈ lits_of_l M);
ASSERT(NU ∝ C ! k ∈# ℒ⇩a⇩l⇩l 𝒜);
ASSERT(literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ C)));
ASSERT(length (NU ∝ C) ≤ Suc (uint32_max div 2));
ASSERT(len ≤ length (NU ∝ C)); ― ‹makes the refinement easier›
let (C,k, i, len) = (C,k,i,len);
let C = NU ∝ C;
if i ≥ len
then
RETURN(cach (atm_of (C ! k) := SEEN_REMOVABLE), butlast analyse, True)
else do {
let (L, analyse) = get_literal_and_remove_of_analyse_wl2 C analyse;
ASSERT(L ∈# ℒ⇩a⇩l⇩l 𝒜);
let b = ¬level_in_lbd (get_level M L) lbd;
if (get_level M L = 0 ∨
conflict_min_cach cach (atm_of L) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of L) D)
then RETURN (cach, analyse, False)
else if b ∨ conflict_min_cach cach (atm_of L) = SEEN_FAILED
then do {
ASSERT(mark_failed_lits_stack_inv2 NU analyse cach);
cach ← mark_failed_lits_wl NU analyse cach;
RETURN (cach, [], False)
}
else do {
ASSERT(- L ∈ lits_of_l M);
C ← get_propagation_reason M (-L);
case C of
Some C ⇒ do {
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) ≥ 2);
ASSERT(literals_are_in_ℒ⇩i⇩n 𝒜 (mset (NU ∝ C)));
ASSERT(length (NU ∝ C) ≤ Suc (uint32_max div 2));
RETURN (cach, analyse @ [lit_redundant_reason_stack2 (-L) NU C], False)
}
| None ⇒ do {
ASSERT(mark_failed_lits_stack_inv2 NU analyse cach);
cach ← mark_failed_lits_wl NU analyse cach;
RETURN (cach, [], False)
}
}
}
})
(cach, analysis, False)›
unfolding lit_redundant_rec_wl_lookup_def Let_def by auto
lemma valid_arena_nempty:
‹valid_arena arena N vdom ⟹ i ∈# dom_m N ⟹ N ∝ i ≠ []›
using arena_lifting(19)[of arena N vdom i]
arena_lifting(4)[of arena N vdom i]
by auto
lemma isa_lit_redundant_rec_wl_lookup_lit_redundant_rec_wl_lookup:
assumes ‹isasat_input_bounded 𝒜›
shows ‹(uncurry5 isa_lit_redundant_rec_wl_lookup, uncurry5 (lit_redundant_rec_wl_lookup 𝒜)) ∈
[λ(((((_, N), _), _), _), _). literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m N)]⇩f
trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f lookup_clause_rel 𝒜 ×⇩f
cach_refinement 𝒜 ×⇩f Id ×⇩f Id →
⟨cach_refinement 𝒜 ×⇩r Id ×⇩r bool_rel⟩nres_rel›
proof -
have isa_mark_failed_lits_stack: ‹isa_mark_failed_lits_stack x2e x2z x1l
≤ ⇓ (cach_refinement 𝒜)
(mark_failed_lits_wl x2 x2y x1j)›
if
‹case y of
(x, xa) ⇒
(case x of
(x, xa) ⇒
(case x of
(x, xa) ⇒
(case x of
(x, xa) ⇒
(case x of
(uu_, N) ⇒
λ_ _ _ _.
literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m N)) xa)
xa)
xa)
xa› and
‹(x, y)
∈ trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f
lookup_clause_rel 𝒜 ×⇩f cach_refinement 𝒜 ×⇩f Id ×⇩f Id› and
‹x1c = (x1d, x2)› and
‹x1b = (x1c, x2a)› and
‹x1a = (x1b, x2b)› and
‹x1 = (x1a, x2c)› and
‹y = (x1, x2d)› and
‹x1h = (x1i, x2e)› and
‹x1g = (x1h, x2f)› and
‹x1f = (x1g, x2g)› and
‹x1e = (x1f, x2h)› and
‹x = (x1e, x2i)› and
‹(xa, x') ∈ cach_refinement 𝒜 ×⇩f (Id ×⇩f bool_rel)› and
‹case xa of (cach, analyse, b) ⇒ analyse ≠ []› and
‹case x' of (cach, analyse, b) ⇒ analyse ≠ []› and
‹lit_redundant_rec_wl_inv2 x1d x2 x2a x'› and
‹x2j = (x1k, x2k)› and
‹x' = (x1j, x2j)› and
‹x2l = (x1m, x2m)› and
‹xa = (x1l, x2l)› and
‹x1k ≠ []› and
‹x1m ≠ []› and
‹x2o = (x1p, x2p)› and
‹x2n = (x1o, x2o)› and
‹ana_lookup_conv x2 (last x1k) = (x1n, x2n)› and
‹x2q = (x1r, x2r)› and
‹last x1m = (x1q, x2q)› and
‹x1n ∈# dom_m x2› and
‹x1o < length (x2 ∝ x1n)› and
‹x2 ∝ x1n ! x1o ∈ lits_of_l x1d› and
‹x2 ∝ x1n ! x1o ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (x2 ∝ x1n))› and
‹length (x2 ∝ x1n) ≤ Suc (uint32_max div 2)› and
‹x2p ≤ length (x2 ∝ x1n)› and
‹arena_is_valid_clause_idx x2e (fst (last x1m))› and
‹x2t = (x1u, x2u)› and
‹x2s = (x1t, x2t)› and
‹(x1n, x1o, x1p, x2p) = (x1s, x2s)› and
‹x2w = (x1x, x2x)› and
‹x2v = (x1w, x2w)› and
‹ana_lookup_conv_lookup x2e (x1q, x1r, x2r) = (x1v, x2v)› and
‹x1v < length x2e› and
‹arena_is_valid_clause_idx x2e x1v› and
‹arena_lit_pre x2e (x1v + x1w)› and
‹¬ x2x ≤ x1x› and
‹¬ x2u ≤ x1u› and
‹isa_get_literal_and_remove_of_analyse_wl_pre x2e x1m› and
‹get_literal_and_remove_of_analyse_wl2 (x2 ∝ x1s) x1k = (x1y, x2y)› and
‹isa_get_literal_and_remove_of_analyse_wl x2e x1m = (x1z, x2z)› and
‹x1y ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹get_level_pol_pre (x1i, x1z)› and
‹atm_in_conflict_lookup_pre (atm_of x1z) x2f› and
‹conflict_min_cach_l_pre (x1l, atm_of x1z)› and
‹¬ (get_level_pol x1i x1z = 0 ∨
conflict_min_cach_l x1l (atm_of x1z) = SEEN_REMOVABLE ∨
atm_in_conflict_lookup (atm_of x1z) x2f)› and
‹¬ (get_level x1d x1y = 0 ∨
conflict_min_cach x1j (atm_of x1y) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of x1y) x2a)› and
‹¬ level_in_lbd (get_level_pol x1i x1z) x2i ∨
conflict_min_cach_l x1l (atm_of x1z) = SEEN_FAILED› and
‹¬ level_in_lbd (get_level x1d x1y) x2d ∨
conflict_min_cach x1j (atm_of x1y) = SEEN_FAILED› and
inv2: ‹mark_failed_lits_stack_inv2 x2 x2y x1j› and
‹length x1m ≤ 1+ uint32_max div 2›
for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q
x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w x1x x2x x1y x2y x1z
x2z
proof -
have [simp]: ‹x2z = x2y›
using that
by (auto simp: isa_get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
obtain x2y0 where
x2z: ‹(x2y, x2y0) ∈ ana_lookups_rel x2› and
inv: ‹mark_failed_lits_stack_inv x2 x2y0 x1j›
using inv2 unfolding mark_failed_lits_stack_inv2_def
by blast
have 1: ‹mark_failed_lits_wl x2 x2y x1j = mark_failed_lits_wl x2 x2y0 x1j›
unfolding mark_failed_lits_wl_def by auto
show ?thesis
unfolding 1
apply (rule isa_mark_failed_lits_stack_isa_mark_failed_lits_stack[THEN
fref_to_Down_curry2, of 𝒜 x2 x2y0 x1j x2e x2z x1l vdom x2, THEN order_trans])
subgoal using assms by fast
subgoal using that x2z by (auto simp: list_rel_imp_same_length[symmetric]
isa_get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
subgoal using that x2z inv by auto
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule mark_failed_lits_stack_mark_failed_lits_wl[THEN
fref_to_Down_curry2, of 𝒜 x2 x2y0 x1j])
subgoal using inv x2z that by auto
subgoal using that by auto
subgoal by auto
done
qed
have isa_mark_failed_lits_stack2: ‹isa_mark_failed_lits_stack x2e x2z x1l
≤ ⇓ (cach_refinement 𝒜) (mark_failed_lits_wl x2 x2y x1j)›
if
‹case y of
(x, xa) ⇒
(case x of
(x, xa) ⇒
(case x of
(x, xa) ⇒
(case x of
(x, xa) ⇒
(case x of
(uu_, N) ⇒
λ_ _ _ _.
literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m N)) xa)
xa)
xa)
xa› and
‹(x, y)
∈ trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f lookup_clause_rel 𝒜 ×⇩f cach_refinement 𝒜 ×⇩f Id ×⇩f
Id› and
‹ana_lookup_conv_lookup x2e (x1q, x1r, x2r) = (x1v, x2v)› and
‹x1v < length x2e› and
‹arena_is_valid_clause_idx x2e x1v› and
‹arena_lit_pre x2e (x1v + x1w)› and
‹¬ x2x ≤ x1x› and
‹¬ x2u ≤ x1u› and
‹isa_get_literal_and_remove_of_analyse_wl_pre x2e x1m› and
‹get_literal_and_remove_of_analyse_wl2 (x2 ∝ x1s) x1k = (x1y, x2y)› and
‹isa_get_literal_and_remove_of_analyse_wl x2e x1m = (x1z, x2z)› and
‹x1y ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹get_level_pol_pre (x1i, x1z)› and
‹atm_in_conflict_lookup_pre (atm_of x1z) x2f› and
‹conflict_min_cach_l_pre (x1l, atm_of x1z)› and
‹¬ (get_level_pol x1i x1z = 0 ∨
conflict_min_cach_l x1l (atm_of x1z) = SEEN_REMOVABLE ∨
atm_in_conflict_lookup (atm_of x1z) x2f)› and
‹¬ (get_level x1d x1y = 0 ∨
conflict_min_cach x1j (atm_of x1y) = SEEN_REMOVABLE ∨
atm_in_conflict (atm_of x1y) x2a)› and
‹¬ (¬ level_in_lbd (get_level_pol x1i x1z) x2i ∨
conflict_min_cach_l x1l (atm_of x1z) = SEEN_FAILED)› and
‹¬ (¬ level_in_lbd (get_level x1d x1y) x2d ∨
conflict_min_cach x1j (atm_of x1y) = SEEN_FAILED)› and
‹- x1y ∈ lits_of_l x1d› and
‹(xb, x'a) ∈ ⟨nat_rel⟩option_rel› and
‹xb = None› and
‹x'a = None› and
inv2: ‹mark_failed_lits_stack_inv2 x2 x2y x1j› and
‹(xa, x') ∈ cach_refinement 𝒜 ×⇩f (Id ×⇩f bool_rel)› and ‹case xa of (cach, analyse, b) ⇒ analyse ≠ []› and
‹case x' of (cach, analyse, b) ⇒ analyse ≠ []› and
‹lit_redundant_rec_wl_inv2 x1d x2 x2a x'› and
‹x2j = (x1k, x2k)› and
‹x' = (x1j, x2j)› and
‹x2l = (x1m, x2m)› and
‹xa = (x1l, x2l)› and
‹x1k ≠ []› and
‹x1m ≠ []› and
‹x2o = (x1p, x2p)› and
‹x2n = (x1o, x2o)› and
‹ana_lookup_conv x2 (last x1k) = (x1n, x2n)› and
‹x2q = (x1r, x2r)› and
‹last x1m = (x1q, x2q)› and
‹x1n ∈# dom_m x2› and
‹x1o < length (x2 ∝ x1n)› and
‹x2 ∝ x1n ! x1o ∈ lits_of_l x1d› and
‹x2 ∝ x1n ! x1o ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (x2 ∝ x1n))› and
‹length (x2 ∝ x1n) ≤ Suc (uint32_max div 2)› and
‹x2p ≤ length (x2 ∝ x1n)› and
‹arena_is_valid_clause_idx x2e (fst (last x1m))› and
‹x2t = (x1u, x2u)› and
‹x2s = (x1t, x2t)› and
‹(x1n, x1o, x1p, x2p) = (x1s, x2s)› and
‹x2w = (x1x, x2x)› and
‹x2v = (x1w, x2w)› and
‹x1c = (x1d, x2)› and
‹x1b = (x1c, x2a)› and
‹x1a = (x1b, x2b)› and
‹x1 = (x1a, x2c)› and
‹y = (x1, x2d)› and
‹x1h = (x1i, x2e)› and
‹x1g = (x1h, x2f)› and
‹x1f = (x1g, x2g)› and
‹x1e = (x1f, x2h)› and
‹x = (x1e, x2i)› and
‹length x1m ≤ 1 + uint32_max div 2›
for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q
x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w x1x x2x x1y x2y x1z
x2z xb x'a
proof -
have [simp]: ‹x2z = x2y›
using that
by (auto simp: isa_get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
obtain x2y0 where
x2z: ‹(x2y, x2y0) ∈ ana_lookups_rel x2› and
inv: ‹mark_failed_lits_stack_inv x2 x2y0 x1j›
using inv2 unfolding mark_failed_lits_stack_inv2_def
by blast
have 1: ‹mark_failed_lits_wl x2 x2y x1j = mark_failed_lits_wl x2 x2y0 x1j›
unfolding mark_failed_lits_wl_def by auto
show ?thesis
unfolding 1
apply (rule isa_mark_failed_lits_stack_isa_mark_failed_lits_stack[THEN
fref_to_Down_curry2, of 𝒜 x2 x2y0 x1j x2e x2z x1l vdom x2, THEN order_trans])
subgoal using assms by fast
subgoal using that x2z by (auto simp: list_rel_imp_same_length[symmetric]
isa_get_literal_and_remove_of_analyse_wl_def
get_literal_and_remove_of_analyse_wl2_def)
subgoal using that x2z inv by auto
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule mark_failed_lits_stack_mark_failed_lits_wl[THEN
fref_to_Down_curry2, of 𝒜 x2 x2y0 x1j])
subgoal using inv x2z that by auto
subgoal using that by auto
subgoal by auto
done
qed
have [refine0]: ‹get_propagation_reason_pol M' L'
≤ ⇓ (⟨Id⟩option_rel)
(get_propagation_reason M L)›
if ‹(M', M) ∈ trail_pol 𝒜› and ‹(L', L) ∈ Id› and ‹L ∈ lits_of_l M›
for M M' L L'
using get_propagation_reason_pol[of 𝒜, THEN fref_to_Down_curry, of M L M' L'] that by auto
note [simp]=get_literal_and_remove_of_analyse_wl_def isa_get_literal_and_remove_of_analyse_wl_def
arena_lifting and [split] = prod.splits
show ?thesis
supply [[goals_limit=1]] ana_lookup_conv_def[simp] ana_lookup_conv_lookup_def[simp]
supply RETURN_as_SPEC_refine[refine2 add]
unfolding isa_lit_redundant_rec_wl_lookup_alt_def lit_redundant_rec_wl_lookup_alt_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m
by (auto simp: arena_lifting)
subgoal by (auto simp: trail_pol_alt_def)
subgoal by (auto simp: arena_is_valid_clause_idx_def
lit_redundant_rec_wl_inv2_def)
subgoal by (auto simp: ana_lookup_conv_lookup_pre_def)
subgoal by (auto simp: arena_is_valid_clause_idx_def)
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m
by (auto simp: arena_lifting arena_is_valid_clause_idx_def)
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q
x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w x1x x2x
apply (auto simp: arena_is_valid_clause_idx_def lit_redundant_rec_wl_inv_def
isa_get_literal_and_remove_of_analyse_wl_pre_def arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def lit_redundant_rec_wl_ref_def)
by (rule_tac x = ‹x1s› in exI; auto simp: valid_arena_nempty)+
subgoal by (auto simp: arena_lifting arena_is_valid_clause_idx_def
lit_redundant_rec_wl_inv_def split: if_splits)
subgoal using assms
by (auto simp: arena_lifting arena_is_valid_clause_idx_def bind_rule_complete_RES conc_fun_RETURN
in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def
intro!: conflict_min_cach_set_removable[of 𝒜,THEN fref_to_Down_curry, THEN order_trans]
dest: List.last_in_set)
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q
x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w x1x x2x
by (auto simp: arena_is_valid_clause_idx_def lit_redundant_rec_wl_inv_def
isa_get_literal_and_remove_of_analyse_wl_pre_def arena_lit_pre_def
uint32_max_def
arena_is_valid_clause_idx_and_access_def lit_redundant_rec_wl_ref_def)
(rule_tac x = x1s in exI; auto simp: uint32_max_def; fail)+
subgoal by (auto simp: list_rel_imp_same_length)
subgoal by (auto intro!: get_level_pol_pre
simp: get_literal_and_remove_of_analyse_wl2_def)
subgoal by (auto intro!: atm_in_conflict_lookup_pre
simp: get_literal_and_remove_of_analyse_wl2_def)
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o
by (auto intro!: conflict_min_cach_l_pre
simp: get_literal_and_remove_of_analyse_wl2_def)
subgoal
by (auto simp: atm_in_conflict_lookup_atm_in_conflict[THEN fref_to_Down_unRET_uncurry_Id]
nth_conflict_min_cach[THEN fref_to_Down_unRET_uncurry_Id] in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
get_level_get_level_pol atms_of_def
get_literal_and_remove_of_analyse_wl2_def
split: prod.splits)
(subst (asm) atm_in_conflict_lookup_atm_in_conflict[THEN fref_to_Down_unRET_uncurry_Id];
auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n atms_of_def; fail)+
subgoal by (auto simp: get_literal_and_remove_of_analyse_wl2_def
split: prod.splits)
subgoal by (auto simp: atm_in_conflict_lookup_atm_in_conflict[THEN fref_to_Down_unRET_uncurry_Id]
nth_conflict_min_cach[THEN fref_to_Down_unRET_uncurry_Id] in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
get_level_get_level_pol atms_of_def
simp: get_literal_and_remove_of_analyse_wl2_def
split: prod.splits)
apply (rule isa_mark_failed_lits_stack; assumption)
subgoal by (auto simp: split: prod.splits)
subgoal by (auto simp: split: prod.splits)
subgoal by (auto simp: get_literal_and_remove_of_analyse_wl2_def
split: prod.splits)
apply assumption
apply (rule isa_mark_failed_lits_stack2; assumption)
subgoal by auto
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q
x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w x1x x2x x1y x2y x1z
x2z xb x'a xc x'b
unfolding lit_redundant_reason_stack_wl_lookup_pre_def
by (auto simp: lit_redundant_reason_stack_wl_lookup_pre_def arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def arena_is_valid_clause_idx_def
simp: valid_arena_nempty get_literal_and_remove_of_analyse_wl2_def
lit_redundant_reason_stack_wl_lookup_def
lit_redundant_reason_stack2_def
intro!: exI[of _ x'b] bex_leI[of _ x'b])
subgoal premises p for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q
x2q x1r x2r x1s x2s x1t x2t x1u x2u xb x'a xc x'b
using p
by (auto simp add: lit_redundant_reason_stack_wl_lookup_def
lit_redundant_reason_stack_def lit_redundant_reason_stack_wl_lookup_pre_def
lit_redundant_reason_stack2_def get_literal_and_remove_of_analyse_wl2_def
arena_lifting[of x2e x2 vdom])
done
qed
lemma iterate_over_conflict_spec:
fixes D :: ‹'v clause›
assumes ‹NU + NUE ⊨pm add_mset K D› and dist: ‹distinct_mset D›
shows
‹iterate_over_conflict K M NU NUE D ≤ ⇓ Id (SPEC(λD'. D' ⊆# D ∧
NU + NUE ⊨pm add_mset K D'))›
proof -
define I' where
‹I' = (λ(E:: 'v clause, f :: 'v clause).
E ⊆# D ∧ NU + NUE ⊨pm add_mset K E ∧ distinct_mset E ∧ distinct_mset f)›
have init_I': ‹I' (D, D)›
using ‹NU + NUE ⊨pm add_mset K D› dist unfolding I'_def highest_lit_def by auto
have red: ‹is_literal_redundant_spec K NU NUE a x
≤ SPEC (λred. (if ¬ red then RETURN (a, remove1_mset x aa)
else RETURN (remove1_mset x a, remove1_mset x aa))
≤ SPEC (λs'. iterate_over_conflict_inv M D s' ∧ I' s' ∧
(s', s) ∈ measure (λ(D, D'). size D')))›
if
‹iterate_over_conflict_inv M D s› and
‹I' s› and
‹case s of (D, D') ⇒ D' ≠ {#}› and
‹s = (a, aa)› and
‹x ∈# aa›
for s a b aa x
proof -
have ‹x ∈# a› ‹distinct_mset aa›
using that
by (auto simp: I'_def highest_lit_def
eq_commute[of ‹get_level _ _›] iterate_over_conflict_inv_def
get_maximum_level_add_mset add_mset_eq_add_mset
dest!: split: option.splits if_splits)
then show ?thesis
using that
by (auto simp: is_literal_redundant_spec_def iterate_over_conflict_inv_def
I'_def size_mset_remove1_mset_le_iff remove1_mset_add_mset_If
intro: mset_le_subtract)
qed
show ?thesis
unfolding iterate_over_conflict_def
apply (refine_vcg WHILEIT_rule_stronger_inv[where
R = ‹measure (λ(D :: 'v clause, D':: 'v clause).
size D')› and
I' = I'])
subgoal by auto
subgoal by (auto simp: iterate_over_conflict_inv_def highest_lit_def)
subgoal by (rule init_I')
subgoal by (rule red)
subgoal unfolding I'_def iterate_over_conflict_inv_def by auto
subgoal unfolding I'_def iterate_over_conflict_inv_def by auto
done
qed
end
lemma
fixes D :: ‹nat clause› and s and s' and NU :: ‹nat clauses_l› and
S :: ‹nat twl_st_wl› and S' :: ‹nat twl_st_l› and S'' :: ‹nat twl_st›
defines
‹S''' ≡ state⇩W_of S''›
defines
‹M ≡ get_trail_wl S› and
NU: ‹NU ≡ get_clauses_wl S› and
NU'_def: ‹NU' ≡ mset `# ran_mf NU› and
NUE: ‹NUE ≡ get_unit_learned_clss_wl S + get_unit_init_clss_wl S› and
NUE: ‹NUS ≡ get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S› and
M': ‹M' ≡ trail S'''›
assumes
S_S': ‹(S, S') ∈ state_wl_l None› and
S'_S'': ‹(S', S'') ∈ twl_st_l None› and
D'_D: ‹mset (tl outl) = D› and
M_D: ‹M ⊨as CNot D› and
dist_D: ‹distinct_mset D› and
tauto: ‹¬tautology D› and
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M› and
struct_invs: ‹twl_struct_invs S''› and
add_inv: ‹twl_list_invs S'› and
cach_init: ‹conflict_min_analysis_inv M' s' (NU' + NUE + NUS) D› and
NU_P_D: ‹NU' + NUE + NUS ⊨pm add_mset K D› and
lits_D: ‹literals_are_in_ℒ⇩i⇩n 𝒜 D› and
lits_NU: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf NU)› and
K: ‹K = outl ! 0› and
outl_nempty: ‹outl ≠ []› and
‹isasat_input_bounded 𝒜›
shows
‹minimize_and_extract_highest_lookup_conflict 𝒜 M NU D s' lbd outl ≤
⇓ ({((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧ outl!0 = K ∧
E' ⊆# D})
(SPEC (λD'. D' ⊆# D ∧ NU' + NUE + NUS ⊨pm add_mset K D'))›
proof -
show ?thesis
apply (rule order.trans)
apply (rule minimize_and_extract_highest_lookup_conflict_iterate_over_conflict[OF
assms(8-23)[unfolded assms(1-9)],
unfolded assms(1-9)[symmetric]])
apply (rule order.trans)
apply (rule ref_two_step'[OF iterate_over_conflict_spec[OF NU_P_D[unfolded add.assoc] dist_D]])
by (auto simp: conc_fun_RES ac_simps)
qed
lemma (in -) lookup_conflict_upd_None_RETURN_def:
‹RETURN oo lookup_conflict_upd_None = (λ(n, xs) i. RETURN (n- 1, xs [i := NOTIN]))›
by (auto intro!: ext)
definition isa_literal_redundant_wl_lookup ::
"trail_pol ⇒ arena ⇒ lookup_clause_rel ⇒ conflict_min_cach_l
⇒ nat literal ⇒ lbd ⇒ (conflict_min_cach_l × (nat × nat × bool) list × bool) nres"
where
‹isa_literal_redundant_wl_lookup M NU D cach L lbd = do {
ASSERT(get_level_pol_pre (M, L));
ASSERT(conflict_min_cach_l_pre (cach, atm_of L));
if get_level_pol M L = 0 ∨ conflict_min_cach_l cach (atm_of L) = SEEN_REMOVABLE
then RETURN (cach, [], True)
else if conflict_min_cach_l cach (atm_of L) = SEEN_FAILED
then RETURN (cach, [], False)
else do {
C ← get_propagation_reason_pol M (-L);
case C of
Some C ⇒ do {
ASSERT(lit_redundant_reason_stack_wl_lookup_pre (-L) NU C);
isa_lit_redundant_rec_wl_lookup M NU D cach
[lit_redundant_reason_stack_wl_lookup (-L) NU C] lbd}
| None ⇒ do {
RETURN (cach, [], False)
}
}
}›
lemma in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩nD[intro]: ‹L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ atm_of L ∈# 𝒜›
using in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n by blast
lemma isa_literal_redundant_wl_lookup_literal_redundant_wl_lookup:
assumes ‹isasat_input_bounded 𝒜›
shows ‹(uncurry5 isa_literal_redundant_wl_lookup, uncurry5 (literal_redundant_wl_lookup 𝒜)) ∈
[λ(((((_, N), _), _), _), _). literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m N)]⇩f
trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f lookup_clause_rel 𝒜 ×⇩f cach_refinement 𝒜
×⇩f Id ×⇩f Id →
⟨cach_refinement 𝒜 ×⇩r Id ×⇩r bool_rel⟩nres_rel›
proof -
have [intro!]: ‹(x2g, x') ∈ cach_refinement 𝒜 ⟹
(x2g, x') ∈ cach_refinement (fold_mset (+) 𝒜 {#})› for x2g x'
by auto
have [refine0]: ‹get_propagation_reason_pol M (- L)
≤ ⇓ (⟨Id⟩option_rel)
(get_propagation_reason M' (- L'))›
if ‹(M, M') ∈ trail_pol 𝒜› and ‹(L, L') ∈ Id› and ‹-L ∈ lits_of_l M'›
for M M' L L'
using that get_propagation_reason_pol[of 𝒜, THEN fref_to_Down_curry, of M' ‹-L'› M ‹-L›] by auto
show ?thesis
unfolding isa_literal_redundant_wl_lookup_def literal_redundant_wl_lookup_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg
isa_lit_redundant_rec_wl_lookup_lit_redundant_rec_wl_lookup[of 𝒜 vdom, THEN fref_to_Down_curry5])
subgoal
by (rule get_level_pol_pre) auto
subgoal by (rule conflict_min_cach_l_pre) auto
subgoal
by (auto simp: get_level_get_level_pol in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩nD
nth_conflict_min_cach[THEN fref_to_Down_unRET_uncurry_Id])
(subst (asm) nth_conflict_min_cach[THEN fref_to_Down_unRET_uncurry_Id]; auto)+
subgoal by auto
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i
by (subst nth_conflict_min_cach[THEN fref_to_Down_unRET_uncurry_Id];
auto simp del: conflict_min_cach_def)
(auto simp: get_level_get_level_pol in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩nD)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply assumption
subgoal by auto
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' xb x'a
unfolding lit_redundant_reason_stack_wl_lookup_pre_def
by (auto simp: lit_redundant_reason_stack_wl_lookup_pre_def arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def arena_is_valid_clause_idx_def
simp: valid_arena_nempty
intro!: exI[of _ xb])
subgoal using assms by auto
subgoal by auto
subgoal for x y x1 x1a x1b x1c x1d x2 x2a x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i xa x' xb x'a
by (simp add: lit_redundant_reason_stack_wl_lookup_def
lit_redundant_reason_stack_def lit_redundant_reason_stack_wl_lookup_pre_def
lit_redundant_reason_stack2_def
arena_lifting[of x2e x2 vdom])
done
qed
definition (in -) lookup_conflict_remove1 :: ‹nat literal ⇒ lookup_clause_rel ⇒ lookup_clause_rel› where
‹lookup_conflict_remove1 =
(λL (n,xs). (n-1, xs [atm_of L := NOTIN]))›
lemma lookup_conflict_remove1:
‹(uncurry (RETURN oo lookup_conflict_remove1), uncurry (RETURN oo remove1_mset))
∈ [λ(L,C). L ∈# C ∧ -L ∉# C ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f
Id ×⇩f lookup_clause_rel 𝒜 → ⟨lookup_clause_rel 𝒜⟩nres_rel›
apply (intro frefI nres_relI)
apply (case_tac y; case_tac x)
subgoal for x y a b aa ab c
using mset_as_position_remove[of c b ‹atm_of aa›]
by (cases ‹aa›)
(auto simp: lookup_clause_rel_def lookup_conflict_remove1_def lookup_clause_rel_atm_in_iff
minus_notin_trivial2 size_remove1_mset_If in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff minus_notin_trivial
mset_as_position_in_iff_nth)
done
definition (in -) lookup_conflict_remove1_pre :: ‹nat literal × nat × bool option list ⇒ bool› where
‹lookup_conflict_remove1_pre = (λ(L,(n,xs)). n > 0 ∧ atm_of L < length xs)›
definition isa_minimize_and_extract_highest_lookup_conflict
:: ‹trail_pol ⇒ arena ⇒ lookup_clause_rel ⇒ conflict_min_cach_l ⇒ lbd ⇒
out_learned ⇒ (lookup_clause_rel × conflict_min_cach_l × out_learned) nres›
where
‹isa_minimize_and_extract_highest_lookup_conflict = (λM NU nxs s lbd outl. do {
(D, _, s, outl) ←
WHILE⇩T⇗λ(nxs, i, s, outl). length outl ≤ uint32_max⇖
(λ(nxs, i, s, outl). i < length outl)
(λ(nxs, x, s, outl). do {
ASSERT(x < length outl);
let L = outl ! x;
(s', _, red) ← isa_literal_redundant_wl_lookup M NU nxs s L lbd;
if ¬red
then RETURN (nxs, x+1, s', outl)
else do {
ASSERT(lookup_conflict_remove1_pre (L, nxs));
RETURN (lookup_conflict_remove1 L nxs, x, s', delete_index_and_swap outl x)
}
})
(nxs, 1, s, outl);
RETURN (D, s, outl)
})›
lemma isa_minimize_and_extract_highest_lookup_conflict_minimize_and_extract_highest_lookup_conflict:
assumes ‹isasat_input_bounded 𝒜›
shows ‹(uncurry5 isa_minimize_and_extract_highest_lookup_conflict,
uncurry5 (minimize_and_extract_highest_lookup_conflict 𝒜)) ∈
[λ(((((_, N), D), _), _), _). literals_are_in_ℒ⇩i⇩n_mm 𝒜 ((mset ∘ fst) `# ran_m N) ∧
¬tautology D]⇩f
trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f lookup_clause_rel 𝒜 ×⇩f
cach_refinement 𝒜 ×⇩f Id ×⇩f Id →
⟨lookup_clause_rel 𝒜 ×⇩r cach_refinement 𝒜 ×⇩r Id⟩nres_rel›
proof -
have init: ‹((x2f, 1, x2g, x2i), x2a::nat literal multiset, 1, x2b, x2d)
∈ lookup_clause_rel 𝒜 ×⇩r Id ×⇩r cach_refinement 𝒜 ×⇩r Id ›
if
‹(x, y)
∈ trail_pol 𝒜 ×⇩f {(arena, N). valid_arena arena N vdom} ×⇩f lookup_clause_rel 𝒜 ×⇩f
cach_refinement 𝒜 ×⇩f Id ×⇩f Id› and
‹x1c = (x1d, x2)› and
‹x1b = (x1c, x2a)› and
‹x1a = (x1b, x2b)› and
‹x1 = (x1a, x2c)› and
‹y = (x1, x2d)› and
‹x1h = (x1i, x2e)› and
‹x1g = (x1h, x2f)› and
‹x1f = (x1g, x2g)› and
‹x1e = (x1f, x2h)› and
‹x = (x1e, x2i)›
for x y x1 x1a x1b x1c x1d x2 x2b x2c x2d x1e x1f x1g x1h x1i x2e x2f x2g
x2h x2i and
x2a
proof -
show ?thesis
using that by auto
qed
show ?thesis
unfolding isa_minimize_and_extract_highest_lookup_conflict_def uncurry_def
minimize_and_extract_highest_lookup_conflict_def
apply (intro frefI nres_relI)
apply (refine_vcg
isa_literal_redundant_wl_lookup_literal_redundant_wl_lookup[of 𝒜 vdom, THEN fref_to_Down_curry5])
apply (rule init; assumption)
subgoal by (auto simp: minimize_and_extract_highest_lookup_conflict_inv_def)
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal
by (auto simp: lookup_conflict_remove1_pre_def lookup_clause_rel_def atms_of_def
minimize_and_extract_highest_lookup_conflict_inv_def)
subgoal
by (auto simp: minimize_and_extract_highest_lookup_conflict_inv_def
intro!: lookup_conflict_remove1[THEN fref_to_Down_unRET_uncurry]
simp: nth_in_set_tl delete_from_lookup_conflict_pre_def
dest!: in_set_takeD)
subgoal by auto
done
qed
definition set_empty_conflict_to_none where
‹set_empty_conflict_to_none D = None›
definition set_lookup_empty_conflict_to_none where
‹set_lookup_empty_conflict_to_none = (λ(n, xs). (True, n, xs))›
lemma set_empty_conflict_to_none_hnr:
‹(RETURN o set_lookup_empty_conflict_to_none, RETURN o set_empty_conflict_to_none) ∈
[λD. D = {#}]⇩f lookup_clause_rel 𝒜 → ⟨option_lookup_clause_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: option_lookup_clause_rel_def lookup_clause_rel_def
set_empty_conflict_to_none_def set_lookup_empty_conflict_to_none_def)
definition lookup_merge_eq2
:: ‹nat literal ⇒ (nat,nat) ann_lits ⇒ nat clause_l ⇒ conflict_option_rel ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (conflict_option_rel × nat × lbd × out_learned) nres› where
‹lookup_merge_eq2 L M N = (λ(_, zs) clvls lbd outl. do {
ASSERT(length N = 2);
let L' = (if N ! 0 = L then N ! 1 else N ! 0);
ASSERT(get_level M L' ≤ Suc (uint32_max div 2));
let lbd = lbd_write lbd (get_level M L');
ASSERT(atm_of L' < length (snd zs));
ASSERT(length outl < uint32_max);
let outl = outlearned_add M L' zs outl;
ASSERT(clvls < uint32_max);
ASSERT(fst zs < uint32_max);
let clvls = clvls_add M L' zs clvls;
let zs = add_to_lookup_conflict L' zs;
RETURN((False, zs), clvls, lbd, outl)
})›
definition merge_conflict_m_eq2
:: ‹nat literal ⇒ (nat, nat) ann_lits ⇒ nat clause_l ⇒ nat clause option ⇒
(nat clause option × nat × lbd × out_learned) nres›
where
‹merge_conflict_m_eq2 L M Ni D =
SPEC (λ(C, n, lbd, outl). C = Some (remove1_mset L (mset Ni) ∪# the D) ∧
n = card_max_lvl M (remove1_mset L (mset Ni) ∪# the D) ∧
out_learned M C outl)›
lemma lookup_merge_eq2_spec:
assumes
o: ‹((b, n, xs), Some C) ∈ option_lookup_clause_rel 𝒜› and
dist: ‹distinct D› and
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset D)› and
lits_tr: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M› and
n_d: ‹no_dup M› and
tauto: ‹¬tautology (mset D)› and
lits_C: ‹literals_are_in_ℒ⇩i⇩n 𝒜 C› and
no_tauto: ‹⋀K. K ∈ set (remove1 L D) ⟹ - K ∉# C›
‹clvls = card_max_lvl M C› and
out: ‹out_learned M (Some C) outl› and
bounded: ‹isasat_input_bounded 𝒜› and
le2: ‹length D = 2› and
L_D: ‹L ∈ set D›
shows
‹lookup_merge_eq2 L M D (b, n, xs) clvls lbd outl ≤
⇓(option_lookup_clause_rel 𝒜 ×⇩r Id ×⇩r Id)
(merge_conflict_m_eq2 L M D (Some C))›
(is ‹_ ≤ ⇓ ?Ref ?Spec›)
proof -
define lbd_upd where
‹lbd_upd lbd i ≡ lbd_write lbd (get_level M (D!i))› for lbd i
let ?D = ‹remove1 L D›
have le_D_le_upper[simp]: ‹a < length D ⟹ Suc (Suc a) ≤ uint32_max› for a
using simple_clss_size_upper_div2[of 𝒜 ‹mset D›] assms by (auto simp: uint32_max_def)
have Suc_N_uint32_max: ‹Suc n ≤ uint32_max› and
size_C_uint32_max: ‹size C ≤ 1 + uint32_max div 2› and
clvls: ‹clvls = card_max_lvl M C› and
tauto_C: ‹¬ tautology C› and
dist_C: ‹distinct_mset C› and
atms_le_xs: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length xs› and
map: ‹mset_as_position xs C›
using assms simple_clss_size_upper_div2[of 𝒜 C] mset_as_position_distinct_mset[of xs C]
lookup_clause_rel_not_tautolgy[of n xs C] bounded
unfolding option_lookup_clause_rel_def lookup_clause_rel_def
by (auto simp: uint32_max_def)
then have clvls_uint32_max: ‹clvls ≤ 1 + uint32_max div 2›
using size_filter_mset_lesseq[of ‹λL. get_level M L = count_decided M› C]
unfolding uint32_max_def card_max_lvl_def by linarith
have [intro]: ‹((b, a, ba), Some C) ∈ option_lookup_clause_rel 𝒜 ⟹ literals_are_in_ℒ⇩i⇩n 𝒜 C ⟹
Suc (Suc a) ≤ uint32_max› for b a ba C
using lookup_clause_rel_size[of a ba C, OF _ bounded] by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def uint32_max_def)
have [simp]: ‹remdups_mset C = C›
using o mset_as_position_distinct_mset[of xs C] by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def distinct_mset_remdups_mset_id)
have ‹¬tautology C›
using mset_as_position_tautology o by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def)
have ‹distinct_mset C›
using mset_as_position_distinct_mset[of _ C] o
unfolding option_lookup_clause_rel_def lookup_clause_rel_def by auto
have ‹mset (tl outl) ⊆# C›
using out by (auto simp: out_learned_def)
from size_mset_mono[OF this] have outl_le: ‹length outl < uint32_max›
using simple_clss_size_upper_div2[OF bounded lits_C] dist_C tauto_C by (auto simp: uint32_max_def)
define L' where ‹L' ≡ if D ! 0 = L then D ! 1 else D ! 0›
have L'_all: ‹L' ∈# ℒ⇩a⇩l⇩l 𝒜›
using lits le2 by (cases D; cases ‹tl D›)
(auto simp: L'_def literals_are_in_ℒ⇩i⇩n_add_mset)
then have L': ‹atm_of L' ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
by (auto simp: atms_of_def)
have DLL: ‹mset D = {#L, L'#}› ‹set D = {L, L'}› ‹L ≠ L'› ‹remove1 L D = [L']›
using le2 L_D dist by (cases D; cases ‹tl D›; auto simp: L'_def; fail)+
have ‹- L' ∈# C ⟹ False› and [simp]: ‹- L' ∉# C›
using dist no_tauto by (auto simp: DLL)
then have o': ‹((False, add_to_lookup_conflict L' (n, xs)), Some ({#L'#} ∪# C))
∈ option_lookup_clause_rel 𝒜›
using o L'_all unfolding option_lookup_clause_rel_def
by (auto intro!: add_to_lookup_conflict_lookup_clause_rel)
have [iff]: ‹is_in_lookup_conflict (n, xs) L' ⟷ L' ∈# C›
using o mset_as_position_in_iff_nth[of xs C L'] L' no_tauto
apply (auto simp: is_in_lookup_conflict_def option_lookup_clause_rel_def
lookup_clause_rel_def DLL is_pos_neg_not_is_pos
split: option.splits)
by (smt ‹- L' ∉# C› atm_of_uminus is_pos_neg_not_is_pos mset_as_position_in_iff_nth option.inject)
have clvls_add: ‹clvls_add M L' (n, xs) clvls = card_max_lvl M ({#L'#} ∪# C)›
by (cases ‹L' ∈# C›)
(auto simp: clvls_add_def card_max_lvl_add_mset clvls add_mset_union
dest!: multi_member_split)
have out': ‹out_learned M (Some ({#L'#} ∪# C)) (outlearned_add M L' (n, xs) outl)›
using out
by (cases ‹L' ∈# C›)
(auto simp: out_learned_def outlearned_add_def add_mset_union
dest!: multi_member_split)
show ?thesis
unfolding lookup_merge_eq2_def prod.simps L'_def[symmetric]
apply refine_vcg
subgoal by (rule le2)
subgoal using literals_are_in_ℒ⇩i⇩n_trail_get_level_uint32_max[OF bounded lits_tr n_d] by blast
subgoal using atms_le_xs L' by simp
subgoal using outl_le .
subgoal using clvls_uint32_max by (auto simp: uint32_max_def)
subgoal using Suc_N_uint32_max by auto
subgoal
using o' clvls_add out'
by (auto simp: merge_conflict_m_eq2_def DLL
intro!: RETURN_RES_refine)
done
qed
definition isasat_lookup_merge_eq2
:: ‹nat literal ⇒ trail_pol ⇒ arena ⇒ nat ⇒ conflict_option_rel ⇒ nat ⇒ lbd ⇒
out_learned ⇒ (conflict_option_rel × nat × lbd × out_learned) nres› where
‹isasat_lookup_merge_eq2 L M N C = (λ(_, zs) clvls lbd outl. do {
ASSERT(arena_lit_pre N C);
ASSERT(arena_lit_pre N (C+1));
let L' = (if arena_lit N C = L then arena_lit N (C + 1) else arena_lit N C);
ASSERT(get_level_pol_pre (M, L'));
ASSERT(get_level_pol M L' ≤ Suc (uint32_max div 2));
let lbd = lbd_write lbd (get_level_pol M L');
ASSERT(atm_of L' < length (snd zs));
ASSERT(length outl < uint32_max);
let outl = isa_outlearned_add M L' zs outl;
ASSERT(clvls < uint32_max);
ASSERT(fst zs < uint32_max);
let clvls = isa_clvls_add M L' zs clvls;
let zs = add_to_lookup_conflict L' zs;
RETURN((False, zs), clvls, lbd, outl)
})›
lemma isasat_lookup_merge_eq2_lookup_merge_eq2:
assumes valid: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
bxs: ‹((b, xs), C) ∈ option_lookup_clause_rel 𝒜› and
M'M: ‹(M', M) ∈ trail_pol 𝒜› and
bound: ‹isasat_input_bounded 𝒜›
shows
‹isasat_lookup_merge_eq2 L M' arena i (b, xs) clvls lbd outl ≤ ⇓ Id
(lookup_merge_eq2 L M (N ∝ i) (b, xs) clvls lbd outl)›
proof -
define L' where ‹L' ≡ (if arena_lit arena i = L then arena_lit arena (i + 1)
else arena_lit arena i)›
define L'' where ‹L'' ≡ (if N ∝ i ! 0 = L then N ∝ i ! 1 else N ∝ i ! 0)›
have [simp]: ‹L'' = L'›
if ‹length (N ∝ i) = 2›
using that i valid by (auto simp: L''_def L'_def arena_lifting)
have L'_all: ‹L' ∈# ℒ⇩a⇩l⇩l 𝒜›
if ‹length (N ∝ i) = 2›
by (use lits i valid that
literals_are_in_ℒ⇩i⇩n_mm_add_msetD[of 𝒜
‹mset (N ∝ i)› _ ‹arena_lit arena (Suc i)›]
literals_are_in_ℒ⇩i⇩n_mm_add_msetD[of 𝒜
‹mset (N ∝ i)› _ ‹arena_lit arena i›]
nth_mem[of 0 ‹N ∝ i›] nth_mem[of 1 ‹N ∝ i›]
in ‹auto simp: arena_lifting ran_m_def L'_def
simp del: nth_mem
dest:
dest!: multi_member_split›)
show ?thesis
unfolding isasat_lookup_merge_eq2_def lookup_merge_eq2_def prod.simps
L'_def[symmetric] L''_def[symmetric]
apply refine_vcg
subgoal
using valid i
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by (auto intro!: exI[of _ i] exI[of _ N])
subgoal
using valid i
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by (auto intro!: exI[of _ i] exI[of _ N])
subgoal
by (rule get_level_pol_pre[OF _ M'M])
(use L'_all
in ‹auto simp: arena_lifting ran_m_def
simp del: nth_mem
dest:
dest!: multi_member_split›)
subgoal
by (subst get_level_get_level_pol[OF M'M, symmetric])
(use L'_all in auto)
subgoal by auto
subgoal
using M'M L'_all
by (auto simp: isa_clvls_add_clvls_add get_level_get_level_pol
isa_outlearned_add_outlearned_add)
done
qed
definition merge_conflict_m_eq2_pre where
‹merge_conflict_m_eq2_pre 𝒜 =
(λ(((((((L, M), N), i), xs), clvls), lbd), out). i ∈# dom_m N ∧ xs ≠ None ∧ distinct (N ∝ i) ∧
¬tautology (mset (N ∝ i)) ∧
(∀K ∈ set (remove1 L (N ∝ i)). - K ∉# the xs) ∧
literals_are_in_ℒ⇩i⇩n 𝒜 (the xs) ∧ clvls = card_max_lvl M (the xs) ∧
out_learned M xs out ∧ no_dup M ∧
literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N) ∧
isasat_input_bounded 𝒜 ∧
length (N ∝ i) = 2 ∧
L ∈ set (N ∝ i))›
definition merge_conflict_m_g_eq2 :: ‹_› where
‹merge_conflict_m_g_eq2 L M N i D _ _ _ = merge_conflict_m_eq2 L M (N ∝ i) D›
lemma isasat_lookup_merge_eq2:
‹(uncurry7 isasat_lookup_merge_eq2, uncurry7 merge_conflict_m_g_eq2) ∈
[merge_conflict_m_eq2_pre 𝒜]⇩f
Id ×⇩f 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 →
⟨option_lookup_clause_rel 𝒜 ×⇩r nat_rel ×⇩r Id ×⇩r Id ⟩nres_rel›
proof -
have H1: ‹isasat_lookup_merge_eq2 a (aa, ab, ac, ad, ae, b) ba bb (af, ag, bc) bd be
bf
≤ ⇓ Id (lookup_merge_eq2 a bg (bh ∝ bb) (af, ag, bc) bd be bf)›
if
‹merge_conflict_m_eq2_pre 𝒜 (((((((ah, bg), bh), bi), bj), bk), bl), bm)› and
‹((((((((a, aa, ab, ac, ad, ae, b), ba), bb), af, ag, bc), bd), be), bf),
((((((ah, bg), bh), bi), bj), bk), bl), bm)
∈ Id ×⇩f 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›
for a aa ab ac ad ae b ba bb af ag bc bd be bf ah bg bh bi bj bk bl bm
proof -
have
bi: ‹bi ∈# dom_m bh› and
‹(bf, bm) ∈ Id› and
‹bj ≠ None› and
‹(be, bl) ∈ Id› and
‹distinct (bh ∝ bi)› and
‹(bd, bk) ∈ nat_rel› and
‹¬ tautology (mset (bh ∝ bi))› and
o: ‹((af, ag, bc), bj) ∈ option_lookup_clause_rel 𝒜› and
‹∀K∈set (remove1 ah (bh ∝ bi)). - K ∉# the bj› and
st: ‹bb = bi› and
‹literals_are_in_ℒ⇩i⇩n 𝒜 (the bj)› and
valid: ‹valid_arena ba bh vdom› and
‹bk = card_max_lvl bg (the bj)› and
‹(a, ah) ∈ Id› and
tr: ‹((aa, ab, ac, ad, ae, b), bg) ∈ trail_pol 𝒜› and
‹out_learned bg bj bm› and
‹no_dup bg› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf bh)› and
bounded: ‹isasat_input_bounded 𝒜› and
ah: ‹ah ∈ set (bh ∝ bi)›
using that unfolding merge_conflict_m_eq2_pre_def prod.simps prod_rel_iff
by blast+
show ?thesis
by (rule isasat_lookup_merge_eq2_lookup_merge_eq2[OF valid bi[unfolded st[symmetric]]
lits o tr bounded])
qed
have H2: ‹lookup_merge_eq2 a bg (bh ∝ bb) (af, ag, bc) bd be bf
≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩f (nat_rel ×⇩f (Id ×⇩f Id)))
(merge_conflict_m_g_eq2 ah bg bh bi bj bk bl bm)›
if
‹merge_conflict_m_eq2_pre 𝒜 (((((((ah, bg), bh), bi), bj), bk), bl), bm)› and
‹((((((((a, aa, ab, ac, ad, ae, b), ba), bb), af, ag, bc), bd), be), bf),
((((((ah, bg), bh), bi), bj), bk), bl), bm)
∈ Id ×⇩f 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›
for a aa ab ac ad ae b ba bb af ag bc bd be bf ah bg bh bi bj bk bl bm
proof -
have
bi: ‹bi ∈# dom_m bh› and
bj: ‹bj ≠ None› and
dist: ‹distinct (bh ∝ bi)› and
tauto: ‹¬ tautology (mset (bh ∝ bi))› and
o: ‹((af, ag, bc), bj) ∈ option_lookup_clause_rel 𝒜› and
K: ‹∀K∈set (remove1 ah (bh ∝ bi)). - K ∉# the bj› and
st: ‹bb = bi›
‹bd = bk›
‹bf = bm›
‹be = bl›
‹a = ah› and
lits_confl: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (the bj)› and
valid: ‹valid_arena ba bh vdom› and
bk: ‹bk = card_max_lvl bg (the bj)› and
tr: ‹((aa, ab, ac, ad, ae, b), bg) ∈ trail_pol 𝒜› and
out: ‹out_learned bg bj bm› and
‹no_dup bg› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf bh)› and
bounded: ‹isasat_input_bounded 𝒜› and
le2: ‹length (bh ∝ bi) = 2› and
ah: ‹ah ∈ set (bh ∝ bi)›
using that unfolding merge_conflict_m_eq2_pre_def prod.simps prod_rel_iff
by blast+
obtain bj' where bj': ‹bj = Some bj'›
using bj by (cases bj) auto
have n_d: ‹no_dup bg› and lits_tr: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 bg›
using tr unfolding trail_pol_alt_def
by auto
have lits_bi: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (bh ∝ bi))›
using bi lits by (auto simp: literals_are_in_ℒ⇩i⇩n_mm_add_mset ran_m_def
dest!: multi_member_split)
show ?thesis
unfolding st merge_conflict_m_g_eq2_def
apply (rule lookup_merge_eq2_spec[THEN order_trans, OF o[unfolded bj']
dist lits_bi lits_tr n_d tauto lits_confl[unfolded bj' option.sel]
_ bk[unfolded bj' option.sel] _ bounded le2 ah])
subgoal using K unfolding bj' by auto
subgoal using out unfolding bj' .
subgoal unfolding bj' by auto
done
qed
show ?thesis
unfolding lookup_conflict_merge_def uncurry_def
apply (intro nres_relI frefI)
apply clarify
subgoal for a aa ab ac ad ae b ba bb af ag bc bd be bf ah bg bh bi bj bk bl bm
apply (rule H1[THEN order_trans]; assumption?)
apply (subst Down_id_eq)
apply (rule H2)
apply assumption+
done
done
qed
end