theory IsaSAT_Arena
imports
Watched_Literals.WB_More_Refinement_List
IsaSAT_Literals
begin
chapter ‹The memory representation: Arenas›
text ‹
We implement an ``arena'' memory representation: This is a flat representation of clauses, where
all clauses and their headers are put one after the other. A lot of the work done here could be done
automatically by a C compiler (see paragraph on Cadical below).
While this has some advantages from a performance point of view compared to an array of arrays, it
allows to emulate pointers to the middle of array with extra information put before the pointer.
This is an optimisation that is considered as important (at least according to Armin Biere).
In Cadical, the representation is done that way although it is implicit by putting an array into a
structure (and rely on UB behaviour to make sure that the array is ``inlined'' into the structure).
Cadical also uses another trick: the array is but inside a union. This union contains either the
clause or a pointer to the new position if it has been moved (during GC-ing). There is no
way for us to do so in a type-safe manner that works both for ‹uint64› and \<^typ>‹nat› (unless we
know some details of the implementation). For ‹uint64›, we could use the space used by the
headers. However, it is not clear if we want to do do, since the behaviour would change between the
two types, making a comparison impossible. This means that half of the blocking literals will be
lost (if we iterate over the watch lists) or all (if we iterate over the clauses directly).
The order in memory is in the following order:
▸ the saved position (was optional in cadical too; since sr-19, not optional);
▸ the status;
▸ the activity;
▸ the LBD;
▸ the size;
▸ the clause.
Remark that the information can be compressed to reduce the size in memory:
▸ the saved position can be skipped for short clauses;
▸ the LBD will most of the time be much shorter than a 32-bit integer, so only an
approximation can be kept and the remaining bits be reused;
▸ the activity is not kept by cadical (to use instead a MTF-like scheme).
As we are already wasteful with memory, we implement the first optimisation. Point two can be
implemented automatically by a (non-standard-compliant) C compiler.
In our case, the refinement is done in two steps:
▸ First, we refine our clause-mapping to a big list. This list contains the original elements.
For type safety, we introduce a datatype that enumerates all possible kind of elements.
▸ Then, we refine all these elements to uint32 elements.
In our formalisation, we distinguish active clauses (clauses that are not marked to be deleted) from
dead clauses (that have been marked to be deleted but can still be accessed). Any dead clause can be
removed from the addressable clauses (\<^term>‹vdom› for virtual domain). Remark that we actually do not
need the full virtual domain, just the list of all active position (TODO?).
Remark that in our formalisation, we don't (at least not yet) plan to reuse freed spaces
(the predicate about dead clauses must be strengthened to do so). Due to the fact that an arena
is very different from an array of clauses, we refine our data structure by hand to the long list
instead of introducing refinement rules. This is mostly done because iteration is very different
(and it does not change what we had before anyway).
Some technical details: due to the fact that we plan to refine the arena to uint32 and that our
clauses can be tautologies, the size does not fit into uint32 (technically, we have the bound
\<^term>‹uint32_max +1›). Therefore, we restrict the clauses to have at least length 2 and we keep
\<^term>‹length C - 2› instead of \<^term>‹length C› (same for position saving). If we ever add a
preprocessing path that removes tautologies, we could get rid of these two limitations.
To our own surprise, using an arena (without position saving) was exactly as fast as the our former
resizable array of arrays. We did not expect this result since:
▸ First, we cannot use ‹uint32› to iterate over clauses anymore (at least no without an
additional trick like considering a slice).
▸ Second, there is no reason why MLton would not already use the trick for array.
(We assume that there is no gain due the order in which we iterate over clauses, which seems a
reasonnable assumption, even when considering than some clauses will subsume the previous one, and
therefore, have a high chance to be in the same watch lists).
We can mark clause as used. This trick is used to implement a MTF-like scheme to keep clauses.
›
section ‹Status of a clause›
datatype clause_status = IRRED | LEARNED | DELETED
instantiation clause_status :: default
begin
definition default_clause_status where ‹default_clause_status = DELETED›
instance by standard
end
section ‹Definition›
text ‹The following definitions are the offset between the beginning of the clause and the
specific headers before the beginning of the clause. Remark that the first offset is not always
valid. Also remark that the fields are ∗‹before› the actual content of the clause.
›
definition POS_SHIFT :: nat where
‹POS_SHIFT = 5›
definition STATUS_SHIFT :: nat where
‹STATUS_SHIFT = 4›
definition ACTIVITY_SHIFT :: nat where
‹ACTIVITY_SHIFT = 3›
definition LBD_SHIFT :: nat where
‹LBD_SHIFT = 2›
definition SIZE_SHIFT :: nat where
‹SIZE_SHIFT = 1›
definition MAX_LENGTH_SHORT_CLAUSE :: nat where
[simp]: ‹MAX_LENGTH_SHORT_CLAUSE = 4›
definition is_short_clause where
[simp]: ‹is_short_clause C ⟷ length C ≤ MAX_LENGTH_SHORT_CLAUSE›
abbreviation is_long_clause where
‹is_long_clause C ≡ ¬is_short_clause C›
definition header_size :: ‹nat clause_l ⇒ nat› where
‹header_size C = (if is_short_clause C then 4 else 5)›
lemmas SHIFTS_def = POS_SHIFT_def STATUS_SHIFT_def ACTIVITY_SHIFT_def LBD_SHIFT_def SIZE_SHIFT_def
text ‹
In an attempt to avoid unfolding definitions and to not rely on the actual value
of the positions of the headers before the clauses.
›
lemma arena_shift_distinct:
‹i > 3 ⟹ i - SIZE_SHIFT ≠ i - LBD_SHIFT›
‹i > 3 ⟹ i - SIZE_SHIFT ≠ i - ACTIVITY_SHIFT›
‹i > 3 ⟹ i - SIZE_SHIFT ≠ i - STATUS_SHIFT›
‹i > 3 ⟹ i - LBD_SHIFT ≠ i - ACTIVITY_SHIFT›
‹i > 3 ⟹ i - LBD_SHIFT ≠ i - STATUS_SHIFT›
‹i > 3 ⟹ i - ACTIVITY_SHIFT ≠ i - STATUS_SHIFT›
‹i > 4 ⟹ i - SIZE_SHIFT ≠ i - POS_SHIFT›
‹i > 4 ⟹ i - LBD_SHIFT ≠ i - POS_SHIFT›
‹i > 4 ⟹ i - ACTIVITY_SHIFT ≠ i - POS_SHIFT›
‹i > 4 ⟹ i - STATUS_SHIFT ≠ i - POS_SHIFT›
‹i > 3 ⟹ j > 3 ⟹ i - SIZE_SHIFT = j - SIZE_SHIFT ⟷ i = j›
‹i > 3 ⟹ j > 3 ⟹ i - LBD_SHIFT = j - LBD_SHIFT ⟷ i = j›
‹i > 4 ⟹ j > 4 ⟹ i - ACTIVITY_SHIFT = j - ACTIVITY_SHIFT ⟷ i = j›
‹i > 3 ⟹ j > 3 ⟹ i - STATUS_SHIFT = j - STATUS_SHIFT ⟷ i = j›
‹i > 4 ⟹ j > 4 ⟹ i - POS_SHIFT = j - POS_SHIFT ⟷ i = j›
‹i ≥ header_size C ⟹ i - SIZE_SHIFT ≠ i - LBD_SHIFT›
‹i ≥ header_size C ⟹ i - SIZE_SHIFT ≠ i - ACTIVITY_SHIFT›
‹i ≥ header_size C ⟹ i - SIZE_SHIFT ≠ i - STATUS_SHIFT›
‹i ≥ header_size C ⟹ i - LBD_SHIFT ≠ i - ACTIVITY_SHIFT›
‹i ≥ header_size C ⟹ i - LBD_SHIFT ≠ i - STATUS_SHIFT›
‹i ≥ header_size C ⟹ i - ACTIVITY_SHIFT ≠ i - STATUS_SHIFT›
‹i ≥ header_size C ⟹ is_long_clause C ⟹ i - SIZE_SHIFT ≠ i - POS_SHIFT›
‹i ≥ header_size C ⟹ is_long_clause C ⟹ i - LBD_SHIFT ≠ i - POS_SHIFT›
‹i ≥ header_size C ⟹ is_long_clause C ⟹ i - ACTIVITY_SHIFT ≠ i - POS_SHIFT›
‹i ≥ header_size C ⟹ is_long_clause C ⟹ i - STATUS_SHIFT ≠ i - POS_SHIFT›
‹i ≥ header_size C ⟹ j ≥ header_size C' ⟹ i - SIZE_SHIFT = j - SIZE_SHIFT ⟷ i = j›
‹i ≥ header_size C ⟹ j ≥ header_size C' ⟹ i - LBD_SHIFT = j - LBD_SHIFT ⟷ i = j›
‹i ≥ header_size C ⟹ j ≥ header_size C' ⟹ i - ACTIVITY_SHIFT = j - ACTIVITY_SHIFT ⟷ i = j›
‹i ≥ header_size C ⟹ j ≥ header_size C' ⟹ i - STATUS_SHIFT = j - STATUS_SHIFT ⟷ i = j›
‹i ≥ header_size C ⟹ j ≥ header_size C' ⟹ is_long_clause C ⟹ is_long_clause C' ⟹
i - POS_SHIFT = j - POS_SHIFT ⟷ i = j›
unfolding POS_SHIFT_def STATUS_SHIFT_def ACTIVITY_SHIFT_def LBD_SHIFT_def SIZE_SHIFT_def
header_size_def
by (auto split: if_splits simp: is_short_clause_def)
lemma header_size_ge0[simp]: ‹0 < header_size x1›
by (auto simp: header_size_def)
datatype arena_el =
is_Lit: ALit (xarena_lit: ‹nat literal›) |
is_LBD: ALBD (xarena_lbd: nat) |
is_Act: AActivity (xarena_act: nat) |
is_Size: ASize (xarena_length: nat) |
is_Pos: APos (xarena_pos: nat) |
is_Status: AStatus (xarena_status: clause_status) (xarena_used: bool)
type_synonym arena = ‹arena_el list›
definition xarena_active_clause :: ‹arena ⇒ nat clause_l × bool ⇒ bool› where
‹xarena_active_clause arena = (λ(C, red).
(length C ≥ 2 ∧
header_size C + length C = length arena ∧
(is_long_clause C ⟶ (is_Pos (arena!(header_size C - POS_SHIFT)) ∧
xarena_pos(arena!(header_size C - POS_SHIFT)) ≤ length C - 2))) ∧
is_Status(arena!(header_size C - STATUS_SHIFT)) ∧
(xarena_status(arena!(header_size C - STATUS_SHIFT)) = IRRED ⟷ red) ∧
(xarena_status(arena!(header_size C - STATUS_SHIFT)) = LEARNED ⟷ ¬red) ∧
is_LBD(arena!(header_size C - LBD_SHIFT)) ∧
is_Act(arena!(header_size C - ACTIVITY_SHIFT)) ∧
is_Size(arena!(header_size C - SIZE_SHIFT)) ∧
xarena_length(arena!(header_size C - SIZE_SHIFT)) + 2 = length C ∧
drop (header_size C) arena = map ALit C
)›
text ‹As \<^term>‹(N∝i, irred N i)› is automatically simplified to \<^term>‹the (fmlookup N i)›, we provide an
alternative definition that uses the result after the simplification.›
lemma xarena_active_clause_alt_def:
‹xarena_active_clause arena (the (fmlookup N i)) ⟷ (
(length (N∝i) ≥ 2 ∧
header_size (N∝i) + length (N∝i) = length arena ∧
(is_long_clause (N∝i) ⟶ (is_Pos (arena!(header_size (N∝i) - POS_SHIFT)) ∧
xarena_pos(arena!(header_size (N∝i) - POS_SHIFT)) ≤ length (N∝i) - 2)) ∧
is_Status(arena!(header_size (N∝i) - STATUS_SHIFT)) ∧
(xarena_status(arena!(header_size (N∝i) - STATUS_SHIFT)) = IRRED ⟷ irred N i) ∧
(xarena_status(arena!(header_size (N∝i) - STATUS_SHIFT)) = LEARNED ⟷ ¬irred N i) ∧
is_LBD(arena!(header_size (N∝i) - LBD_SHIFT)) ∧
is_Act(arena!(header_size (N∝i) - ACTIVITY_SHIFT)) ∧
is_Size(arena!(header_size (N∝i) - SIZE_SHIFT)) ∧
xarena_length(arena!(header_size (N∝i) - SIZE_SHIFT)) + 2 = length (N∝i) ∧
drop (header_size (N∝i)) arena = map ALit (N∝i)
))›
proof -
have C: ‹the (fmlookup N i) = (N ∝ i, irred N i)›
by simp
show ?thesis
apply (subst C)
unfolding xarena_active_clause_def prod.case
by meson
qed
text ‹The extra information is required to prove ``separation'' between active and dead clauses. And
it is true anyway and does not require any extra work to prove.
TODO generalise LBD to extract from every clause?›
definition arena_dead_clause :: ‹arena ⇒ bool› where
‹arena_dead_clause arena ⟷
is_Status(arena!(4 - STATUS_SHIFT)) ∧ xarena_status(arena!(4 - STATUS_SHIFT)) = DELETED ∧
is_LBD(arena!(4 - LBD_SHIFT)) ∧
is_Act(arena!(4 - ACTIVITY_SHIFT)) ∧
is_Size(arena!(4 - SIZE_SHIFT))
›
text ‹When marking a clause as garbage, we do not care whether it was used or not.›
definition extra_information_mark_to_delete where
‹extra_information_mark_to_delete arena i = arena[i - STATUS_SHIFT := AStatus DELETED False]›
text ‹This extracts a single clause from the complete arena.›
abbreviation clause_slice where
‹clause_slice arena N i ≡ Misc.slice (i - header_size (N∝i)) (i + length(N∝i)) arena›
abbreviation dead_clause_slice where
‹dead_clause_slice arena N i ≡ Misc.slice (i - 4) i arena›
text ‹We now can lift the validity of the active and dead clauses to the whole memory and link it
the mapping to clauses and the addressable space.
In our first try, the predicated \<^term>‹xarena_active_clause› took the whole
arena as parameter. This however turned out to make the proof about updates less modular, since the
slicing already takes care to ignore all irrelevant changes.
›
definition valid_arena :: ‹arena ⇒ nat clauses_l ⇒ nat set ⇒ bool› where
‹valid_arena arena N vdom ⟷
(∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))) ∧
(∀i ∈ vdom. i ∉# dom_m N ⟶ (i < length arena ∧ i ≥ 4 ∧
arena_dead_clause (dead_clause_slice arena N i)))
›
lemma valid_arena_empty: ‹valid_arena [] fmempty {}›
unfolding valid_arena_def
by auto
definition arena_status where
‹arena_status arena i = xarena_status (arena!(i - STATUS_SHIFT))›
definition arena_used where
‹arena_used arena i = xarena_used (arena!(i - STATUS_SHIFT))›
definition arena_length where
‹arena_length arena i = 2 + xarena_length (arena!(i - SIZE_SHIFT))›
definition arena_lbd where
‹arena_lbd arena i = xarena_lbd (arena!(i - LBD_SHIFT))›
definition arena_act where
‹arena_act arena i = xarena_act (arena!(i - ACTIVITY_SHIFT))›
definition arena_pos where
‹arena_pos arena i = 2 + xarena_pos (arena!(i - POS_SHIFT))›
definition arena_lit where
‹arena_lit arena i = xarena_lit (arena!i)›
definition "op_incr_mod32 n ≡ (n+1 :: nat) mod 2^32"
definition arena_incr_act where
‹arena_incr_act arena i = arena[i - ACTIVITY_SHIFT := AActivity (op_incr_mod32 (xarena_act (arena!(i - ACTIVITY_SHIFT))))]›
section ‹Separation properties›
text ‹The following two lemmas talk about the minimal distance between two clauses in memory. They
are important for the proof of correctness of all update function.
›
lemma minimal_difference_between_valid_index:
assumes ‹∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
‹i ∈# dom_m N› and ‹j ∈# dom_m N› and ‹j > i›
shows ‹j - i ≥ length (N∝i) + header_size (N∝j)›
proof (rule ccontr)
assume False: ‹¬ ?thesis›
let ?Ci = ‹the (fmlookup N i)›
let ?Cj = ‹the (fmlookup N j)›
have
1: ‹xarena_active_clause (clause_slice arena N i) (N ∝ i, irred N i)› and
2: ‹xarena_active_clause (clause_slice arena N j) (N ∝ j, irred N j)› and
i_le: ‹i < length arena› and
i_ge: ‹i ≥ header_size(N∝i)›and
j_le: ‹j < length arena› and
j_ge: ‹j ≥ header_size(N∝j)›
using assms
by auto
have Ci: ‹?Ci = (N ∝ i, irred N i)› and Cj: ‹?Cj = (N ∝ j, irred N j)›
by auto
have
eq: ‹Misc.slice i (i + length (N ∝ i)) arena = map ALit (N ∝ i)› and
‹length (N ∝ i) - Suc 0 < length (N ∝ i)› and
length_Ni: ‹length (N∝i) ≥ 2›
using 1 i_ge
unfolding xarena_active_clause_def extra_information_mark_to_delete_def prod.case
apply simp_all
apply force
done
from arg_cong[OF this(1), of ‹λn. n ! (length (N∝i) - 1)›] this(2-)
have lit: ‹is_Lit (arena ! (i + length(N∝i) - 1))›
using i_le i_ge by (auto simp: map_nth slice_nth)
have
Cj2: ‹2 ≤ length (N ∝ j)›
using 2 j_le j_ge
unfolding xarena_active_clause_def extra_information_mark_to_delete_def prod.case
header_size_def
by simp
have headerj: ‹header_size (N ∝ j) ≥ 4›
unfolding header_size_def by (auto split: if_splits)
then have [simp]: ‹header_size (N ∝ j) - POS_SHIFT < length (N ∝ j) + header_size (N ∝ j)›
using Cj2
by linarith
have [simp]:
‹is_long_clause (N ∝ j) ⟶ j + (header_size (N ∝ j) - POS_SHIFT) - header_size (N ∝ j) = j - POS_SHIFT›
‹j + (header_size (N ∝ j) - STATUS_SHIFT) - header_size (N ∝ j) = j - STATUS_SHIFT›
‹j + (header_size (N ∝ j) - SIZE_SHIFT) - header_size (N ∝ j) = j - SIZE_SHIFT›
‹j + (header_size (N ∝ j) - LBD_SHIFT) - header_size (N ∝ j) = j - LBD_SHIFT›
‹j + (header_size (N ∝ j) - ACTIVITY_SHIFT) - header_size (N ∝ j) = j - ACTIVITY_SHIFT›
using Cj2 headerj unfolding POS_SHIFT_def STATUS_SHIFT_def LBD_SHIFT_def SIZE_SHIFT_def
ACTIVITY_SHIFT_def
by (auto simp: header_size_def)
have
pos: ‹is_long_clause (N ∝ j) ⟶ is_Pos (arena ! (j - POS_SHIFT))› and
st: ‹is_Status (arena ! (j - STATUS_SHIFT))› and
size: ‹is_Size (arena ! (j - SIZE_SHIFT))› and
lbd: ‹is_LBD (arena ! (j - LBD_SHIFT))› and
act: ‹is_Act (arena ! (j - ACTIVITY_SHIFT))›
using 2 j_le j_ge Cj2 headerj
unfolding xarena_active_clause_def extra_information_mark_to_delete_def prod.case
by (simp_all add: slice_nth)
have False if ji: ‹j - i ≥ length (N∝i)›
proof -
have Suc3: ‹3 = Suc (Suc (Suc 0))›
by auto
have Suc4: ‹4 = Suc (Suc (Suc (Suc 0)))›
by auto
have Suc5: ‹5 = Suc (Suc (Suc (Suc (Suc 0))))›
by auto
have j_i_1[iff]:
‹j - 1 = i + length (N ∝ i) - 1 ⟷ j = i + length (N ∝ i)›
‹j - 2 = i + length (N ∝ i) - 1 ⟷ j = i + length (N ∝ i) + 1›
‹j - 3 = i + length (N ∝ i) - 1 ⟷ j = i + length (N ∝ i) + 2›
‹j - 4 = i + length (N ∝ i) - 1 ⟷ j = i + length (N ∝ i) + 3›
‹j - 5 = i + length (N ∝ i) - 1 ⟷ j = i + length (N ∝ i) + 4›
using False that j_ge i_ge length_Ni unfolding Suc4 Suc5 header_size_def numeral_2_eq_2
by (auto split: if_splits)
have H4: ‹Suc (j - i) ≤ length (N ∝ i) + 4 ⟹ j - i = length (N ∝ i) ∨
j - i = length (N ∝ i) + 1 ∨ j - i = length (N ∝ i) + 2 ∨ j - i = length (N ∝ i) + 3›
using False ji j_ge i_ge length_Ni unfolding Suc3 Suc4
by (auto simp: le_Suc_eq header_size_def split: if_splits)
have H5: ‹Suc (j - i) ≤ length (N ∝ i) + 5 ⟹ j - i = length (N ∝ i) ∨
j - i = length (N ∝ i) + 1 ∨ j - i = length (N ∝ i) + 2 ∨ j - i = length (N ∝ i) + 3 ∨
(is_long_clause (N ∝ j) ∧ j = i+length (N ∝ i) + 4)›
using False ji j_ge i_ge length_Ni unfolding Suc3 Suc4
by (auto simp: le_Suc_eq header_size_def split: if_splits)
consider
‹is_long_clause (N ∝ j)› ‹j - POS_SHIFT = i + length(N∝i) - 1› |
‹j - STATUS_SHIFT = i + length(N∝i) - 1› |
‹j - LBD_SHIFT = i + length(N∝i) - 1› |
‹j - ACTIVITY_SHIFT = i + length(N∝i) - 1› |
‹j - SIZE_SHIFT = i + length(N∝i) - 1›
using False ji j_ge i_ge length_Ni
unfolding header_size_def not_less_eq_eq STATUS_SHIFT_def SIZE_SHIFT_def
LBD_SHIFT_def ACTIVITY_SHIFT_def le_Suc_eq POS_SHIFT_def j_i_1
apply (cases ‹is_short_clause (N ∝ j)›)
subgoal
using H4 by auto
subgoal
using H5 by auto
done
then show False
using lit pos st size lbd act
by cases auto
qed
moreover have False if ji: ‹j - i < length (N∝i)›
proof -
from arg_cong[OF eq, of ‹λxs. xs ! (j-i-1)›]
have ‹is_Lit (arena ! (j-1))›
using that j_le i_le ‹j > i›
by (auto simp: slice_nth)
then show False
using size unfolding SIZE_SHIFT_def by auto
qed
ultimately show False
by linarith
qed
lemma minimal_difference_between_invalid_index:
assumes ‹valid_arena arena N vdom› and
‹i ∈# dom_m N› and ‹j ∉# dom_m N› and ‹j ≥ i› and ‹j ∈ vdom›
shows ‹j - i ≥ length (N∝i) + 4›
proof (rule ccontr)
assume False: ‹¬ ?thesis›
let ?Ci = ‹the (fmlookup N i)›
let ?Cj = ‹the (fmlookup N j)›
have
1: ‹xarena_active_clause (clause_slice arena N i) (N ∝ i, irred N i)› and
2: ‹arena_dead_clause (dead_clause_slice arena N j)› and
i_le: ‹i < length arena› and
i_ge: ‹i ≥ header_size(N∝i)›and
j_le: ‹j < length arena› and
j_ge: ‹j ≥ 4›
using assms unfolding valid_arena_def
by auto
have Ci: ‹?Ci = (N ∝ i, irred N i)› and Cj: ‹?Cj = (N ∝ j, irred N j)›
by auto
have
eq: ‹Misc.slice i (i + length (N ∝ i)) arena = map ALit (N ∝ i)› and
‹length (N ∝ i) - Suc 0 < length (N ∝ i)› and
length_Ni: ‹length (N∝i) ≥ 2› and
pos: ‹is_long_clause (N ∝ i) ⟶
is_Pos (arena ! (i - POS_SHIFT))› and
status: ‹is_Status (arena ! (i - STATUS_SHIFT))› and
lbd: ‹is_LBD (arena ! (i - LBD_SHIFT))› and
act: ‹is_Act (arena ! (i - ACTIVITY_SHIFT))› and
size: ‹is_Size (arena ! (i - SIZE_SHIFT))› and
st_init: ‹(xarena_status (arena ! (i - STATUS_SHIFT)) = IRRED) = (irred N i)› and
st_learned: ‹(xarena_status (arena ! (i - STATUS_SHIFT)) = LEARNED) = (¬ irred N i)›
using 1 i_ge i_le
unfolding xarena_active_clause_def extra_information_mark_to_delete_def prod.case
unfolding STATUS_SHIFT_def LBD_SHIFT_def ACTIVITY_SHIFT_def SIZE_SHIFT_def POS_SHIFT_def
apply (simp_all add: header_size_def slice_nth split: if_splits)
apply force+
done
have
st: ‹is_Status (arena ! (j - STATUS_SHIFT))› and
del: ‹xarena_status (arena ! (j - STATUS_SHIFT)) = DELETED›
using 2 j_le j_ge unfolding arena_dead_clause_def STATUS_SHIFT_def
by (simp_all add: header_size_def slice_nth)
consider
‹j - STATUS_SHIFT ≥ i› |
‹j - STATUS_SHIFT < i›
using False ‹j ≥ i› unfolding STATUS_SHIFT_def
by linarith
then show False
proof cases
case 1
then have ‹j - STATUS_SHIFT < i + length (N∝i)›
using ‹j ≥ i› False j_ge
unfolding not_less_eq_eq STATUS_SHIFT_def
by simp
with arg_cong[OF eq, of ‹λn. n ! (j - STATUS_SHIFT - i)›]
have lit: ‹is_Lit (arena ! (j - STATUS_SHIFT))›
using 1 ‹j ≥ i› i_le i_ge j_ge by (auto simp: map_nth slice_nth STATUS_SHIFT_def)
with st
show False by auto
next
case 2
then consider
‹j - STATUS_SHIFT = i - STATUS_SHIFT› |
‹j - STATUS_SHIFT = i - LBD_SHIFT› |
‹j - STATUS_SHIFT = i - ACTIVITY_SHIFT› |
‹j - STATUS_SHIFT = i - SIZE_SHIFT› |
‹is_long_clause (N ∝ i)› and ‹j - STATUS_SHIFT = i - POS_SHIFT›
using ‹j ≥ i›
unfolding STATUS_SHIFT_def LBD_SHIFT_def ACTIVITY_SHIFT_def SIZE_SHIFT_def POS_SHIFT_def
by force
then show False
apply cases
subgoal using st status st_init st_learned del by auto
subgoal using st lbd by auto
subgoal using st act by auto
subgoal using st size by auto
subgoal using st pos by auto
done
qed
qed
text ‹At first we had the weaker \<^term>‹i - j ≥ 1› which we replaced by \<^term>‹i - j ≥ 4›.
The former however was able to solve many more goals due to different handling between \<^term>‹1›
(which is simplified to \<^term>‹Suc 0›) and \<^term>‹4› (whi::natch is not). Therefore, we replaced \<^term>‹4›
by \<^term>‹Suc (Suc (Suc (Suc 0)))›
›
lemma minimal_difference_between_invalid_index2:
assumes ‹valid_arena arena N vdom› and
‹i ∈# dom_m N› and ‹j ∉# dom_m N› and ‹j < i› and ‹j ∈ vdom›
shows ‹i - j ≥ Suc (Suc (Suc (Suc 0)))› and
‹is_long_clause (N ∝ i) ⟹ i - j ≥ Suc (Suc (Suc (Suc (Suc 0))))›
proof -
let ?Ci = ‹the (fmlookup N i)›
let ?Cj = ‹the (fmlookup N j)›
have
1: ‹xarena_active_clause (clause_slice arena N i) (N ∝ i, irred N i)› and
2: ‹arena_dead_clause (dead_clause_slice arena N j)› and
i_le: ‹i < length arena› and
i_ge: ‹i ≥ header_size(N∝i)›and
j_le: ‹j < length arena› and
j_ge: ‹j ≥ 4›
using assms unfolding valid_arena_def
by auto
have Ci: ‹?Ci = (N ∝ i, irred N i)› and Cj: ‹?Cj = (N ∝ j, irred N j)›
by auto
have
eq: ‹Misc.slice i (i + length (N ∝ i)) arena = map ALit (N ∝ i)› and
‹length (N ∝ i) - Suc 0 < length (N ∝ i)› and
length_Ni: ‹length (N∝i) ≥ 2› and
pos: ‹is_long_clause (N ∝ i) ⟶
is_Pos (arena ! (i - POS_SHIFT))› and
status: ‹is_Status (arena ! (i - STATUS_SHIFT))› and
lbd: ‹is_LBD (arena ! (i - LBD_SHIFT))› and
act: ‹is_Act (arena ! (i - ACTIVITY_SHIFT))› and
size: ‹is_Size (arena ! (i - SIZE_SHIFT))› and
st_init: ‹(xarena_status (arena ! (i - STATUS_SHIFT)) = IRRED) ⟷ (irred N i)› and
st_learned: ‹ (xarena_status (arena ! (i - STATUS_SHIFT)) = LEARNED) ⟷ ¬irred N i›
using 1 i_ge i_le
unfolding xarena_active_clause_def extra_information_mark_to_delete_def prod.case
unfolding STATUS_SHIFT_def LBD_SHIFT_def ACTIVITY_SHIFT_def SIZE_SHIFT_def POS_SHIFT_def
apply (simp_all add: header_size_def slice_nth split: if_splits)
apply force+
done
have
st: ‹is_Status (arena ! (j - STATUS_SHIFT))› and
del: ‹xarena_status (arena ! (j - STATUS_SHIFT)) = DELETED› and
lbd': ‹is_LBD (arena ! (j - LBD_SHIFT))› and
act': ‹is_Act (arena ! (j - ACTIVITY_SHIFT))› and
size': ‹is_Size (arena ! (j - SIZE_SHIFT))›
using 2 j_le j_ge unfolding arena_dead_clause_def SHIFTS_def
by (simp_all add: header_size_def slice_nth)
have 4: ‹4 = Suc (Suc (Suc (Suc 0)))› and 5: ‹5 = Suc (Suc (Suc (Suc (Suc 0))))›
by auto
have [simp]: ‹a < 4 ⟹ j - Suc a = i - Suc 0 ⟷ i = j - a› for a
using ‹i > j› j_ge i_ge
by (auto split: if_splits simp: not_less_eq_eq le_Suc_eq )
have [simp]: ‹Suc i - j = Suc a ⟷ i - j = a› for a
using ‹i > j› j_ge i_ge
by (auto split: if_splits simp: not_less_eq_eq le_Suc_eq)
show 1: ‹i - j ≥ Suc (Suc (Suc (Suc 0)))› (is ?A)
proof (rule ccontr)
assume False: ‹¬?A›
consider
‹i - STATUS_SHIFT = j - STATUS_SHIFT› |
‹i - STATUS_SHIFT = j - LBD_SHIFT› |
‹i - STATUS_SHIFT = j - ACTIVITY_SHIFT› |
‹i - STATUS_SHIFT = j - SIZE_SHIFT›
using False ‹i > j› j_ge i_ge unfolding SHIFTS_def header_size_def 4
by (auto split: if_splits simp: not_less_eq_eq le_Suc_eq )
then show False
apply cases
subgoal using st status st_init st_learned del by auto
subgoal using status lbd' by auto
subgoal using status act' by auto
subgoal using status size' by auto
done
qed
show ‹i - j ≥ Suc (Suc (Suc (Suc (Suc 0))))› (is ?A)
if long: ‹is_long_clause (N ∝ i)›
proof (rule ccontr)
assume False: ‹¬?A›
have [simp]: ‹a < 5 ⟹ a' < 4 ⟹ i - Suc a = j - Suc a' ⟷ i - a = j - a'› for a a'
using ‹i > j› j_ge i_ge long
by (auto split: if_splits simp: not_less_eq_eq le_Suc_eq )
have ‹i - j = Suc (Suc (Suc (Suc 0)))›
using 1 ‹i > j› False j_ge i_ge long unfolding SHIFTS_def header_size_def 4
by (auto split: if_splits simp: not_less_eq_eq le_Suc_eq)
then have ‹i - POS_SHIFT = j - SIZE_SHIFT›
using 1 ‹i > j› j_ge i_ge long unfolding SHIFTS_def header_size_def 4 5
by (auto split: if_splits simp: not_less_eq_eq le_Suc_eq)
then show False
using pos long size'
by auto
qed
qed
lemma valid_arena_in_vdom_le_arena:
assumes ‹valid_arena arena N vdom› and ‹j ∈ vdom›
shows ‹j < length arena› and ‹j ≥ 4›
using assms unfolding valid_arena_def
by (cases ‹j ∈# dom_m N›; auto simp: header_size_def
dest!: multi_member_split split: if_splits; fail)+
lemma valid_minimal_difference_between_valid_index:
assumes ‹valid_arena arena N vdom› and
‹i ∈# dom_m N› and ‹j ∈# dom_m N› and ‹j > i›
shows ‹j - i ≥ length (N∝i) + header_size (N∝j)›
by (rule minimal_difference_between_valid_index[OF _ assms(2-4)])
(use assms(1) in ‹auto simp: valid_arena_def›)
subsubsection ‹Updates›
paragraph ‹Mark to delete›
lemma clause_slice_extra_information_mark_to_delete:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∈# dom_m N› and
dom: ‹∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))›
shows
‹clause_slice (extra_information_mark_to_delete arena i) N ia =
(if ia = i then extra_information_mark_to_delete (clause_slice arena N ia) (header_size (N∝i))
else clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ header_size(N ∝ ia)› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding xarena_active_clause_def
by auto
show ?thesis
using minimal_difference_between_valid_index[OF dom i ia] i_ge
minimal_difference_between_valid_index[OF dom ia i] ia_ge
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def STATUS_SHIFT_def drop_update_swap
Misc.slice_def header_size_def split: if_splits)
qed
lemma clause_slice_extra_information_mark_to_delete_dead:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∉# dom_m N› ‹ia ∈ vdom› and
dom: ‹valid_arena arena N vdom›
shows
‹arena_dead_clause (dead_clause_slice (extra_information_mark_to_delete arena i) N ia) =
arena_dead_clause (dead_clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ 4› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding valid_arena_def
by auto
show ?thesis
using minimal_difference_between_invalid_index[OF dom i ia(1) _ ia(2)] i_ge ia_ge
using minimal_difference_between_invalid_index2[OF dom i ia(1) _ ia(2)] ia_ge
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def STATUS_SHIFT_def drop_update_swap
arena_dead_clause_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma length_extra_information_mark_to_delete[simp]:
‹length (extra_information_mark_to_delete arena i) = length arena›
unfolding extra_information_mark_to_delete_def by auto
lemma valid_arena_mono: ‹valid_arena ab ar vdom1 ⟹ vdom2 ⊆ vdom1 ⟹ valid_arena ab ar vdom2›
unfolding valid_arena_def
by fast
lemma valid_arena_extra_information_mark_to_delete:
assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N›
shows ‹valid_arena (extra_information_mark_to_delete arena i) (fmdrop i N) (insert i vdom)›
proof -
let ?arena = ‹extra_information_mark_to_delete arena i›
have [simp]: ‹i ∉# remove1_mset i (dom_m N)›
‹⋀ia. ia ∉# remove1_mset i (dom_m N) ⟷ ia =i ∨ (i ≠ ia ∧ ia ∉# dom_m N)›
using assms distinct_mset_dom[of N]
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset)
have
dom: ‹∀i∈#dom_m N.
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
dom': ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
vdom: ‹⋀i. i∈vdom ⟶ i ∉# dom_m N ⟶ 4 ≤ i ∧ arena_dead_clause (dead_clause_slice arena N i)›
using assms unfolding valid_arena_def by auto
have ‹ia∈#dom_m (fmdrop i N) ⟹
ia < length ?arena ∧
header_size (fmdrop i N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena (fmdrop i N) ia) (the (fmlookup (fmdrop i N) ia))› for ia
using dom'[of ia] clause_slice_extra_information_mark_to_delete[OF i _ dom, of ia]
by auto
moreover have ‹ia ≠ i ⟶ ia∈insert i vdom ⟶
ia ∉# dom_m (fmdrop i N) ⟶
4 ≤ ia ∧ arena_dead_clause
(dead_clause_slice (extra_information_mark_to_delete arena i) (fmdrop i N) ia)› for ia
using vdom[of ia] clause_slice_extra_information_mark_to_delete_dead[OF i _ _ arena, of ia]
by auto
moreover have ‹4 ≤ i ∧ arena_dead_clause
(dead_clause_slice (extra_information_mark_to_delete arena i) (fmdrop i N) i)›
using dom'[of i, OF i]
unfolding arena_dead_clause_def xarena_active_clause_alt_def
extra_information_mark_to_delete_def apply -
by (simp_all add: SHIFTS_def header_size_def Misc.slice_def drop_update_swap min_def
split: if_splits)
force+
ultimately show ?thesis
using assms unfolding valid_arena_def
by auto
qed
lemma valid_arena_extra_information_mark_to_delete':
assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N›
shows ‹valid_arena (extra_information_mark_to_delete arena i) (fmdrop i N) vdom›
using valid_arena_extra_information_mark_to_delete[OF assms]
by (auto intro: valid_arena_mono)
paragraph ‹Removable from addressable space›
lemma valid_arena_remove_from_vdom:
assumes ‹valid_arena arena N (insert i vdom)›
shows ‹valid_arena arena N vdom›
using assms valid_arena_def
by (auto dest!: in_diffD)
paragraph ‹Update activity›
definition update_act where
‹update_act C act arena = arena[C - ACTIVITY_SHIFT := AActivity act]›
lemma clause_slice_update_act:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∈# dom_m N› and
dom: ‹∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))›
shows
‹clause_slice (update_act i act arena) N ia =
(if ia = i then update_act (header_size (N∝i)) act (clause_slice arena N ia)
else clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ header_size(N ∝ ia)› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding xarena_active_clause_def
by auto
show ?thesis
using minimal_difference_between_valid_index[OF dom i ia] i_ge
minimal_difference_between_valid_index[OF dom ia i] ia_ge
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def STATUS_SHIFT_def drop_update_swap
ACTIVITY_SHIFT_def update_act_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma length_update_act[simp]:
‹length (update_act i act arena) = length arena›
by (auto simp: update_act_def)
lemma clause_slice_update_act_dead:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∉# dom_m N› ‹ia ∈ vdom› and
dom: ‹valid_arena arena N vdom›
shows
‹arena_dead_clause (dead_clause_slice (update_act i act arena) N ia) =
arena_dead_clause (dead_clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ 4› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding valid_arena_def
by auto
show ?thesis
using minimal_difference_between_invalid_index[OF dom i ia(1) _ ia(2)] i_ge ia_ge
using minimal_difference_between_invalid_index2[OF dom i ia(1) _ ia(2)] ia_ge
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def STATUS_SHIFT_def drop_update_swap
arena_dead_clause_def update_act_def ACTIVITY_SHIFT_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma xarena_active_clause_update_act_same:
assumes
‹i ≥ header_size (N ∝ i)› and
‹i < length arena› and
‹xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))›
shows ‹xarena_active_clause (update_act (header_size (N∝i)) act (clause_slice arena N i))
(the (fmlookup N i))›
using assms
by (cases ‹is_short_clause (N ∝ i)›)
(simp_all add: xarena_active_clause_alt_def update_act_def SHIFTS_def Misc.slice_def
header_size_def)
lemma valid_arena_update_act:
assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N›
shows ‹valid_arena (update_act i act arena) N vdom›
proof -
let ?arena = ‹update_act i act arena›
have [simp]: ‹i ∉# remove1_mset i (dom_m N)›
‹⋀ia. ia ∉# remove1_mset i (dom_m N) ⟷ ia =i ∨ (i ≠ ia ∧ ia ∉# dom_m N)›
using assms distinct_mset_dom[of N]
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset)
have
dom: ‹∀i∈#dom_m N.
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
dom': ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
vdom: ‹⋀i. i∈vdom ⟶ i ∉# dom_m N ⟶ 4 ≤ i ∧ arena_dead_clause (dead_clause_slice arena N i)›
using assms unfolding valid_arena_def by auto
have ‹ia∈#dom_m N ⟹ ia ≠ i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_update_act[OF i _ dom, of ia act]
by auto
moreover have ‹ia = i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_update_act[OF i _ dom, of ia act] i
by (simp add: xarena_active_clause_update_act_same)
moreover have ‹ia∈vdom ⟶
ia ∉# dom_m N ⟶
4 ≤ ia ∧ arena_dead_clause
(dead_clause_slice (update_act i act arena) (fmdrop i N) ia)› for ia
using vdom[of ia] clause_slice_update_act_dead[OF i _ _ arena, of ia] i
by auto
ultimately show ?thesis
using assms unfolding valid_arena_def
by auto
qed
paragraph ‹Update LBD›
definition update_lbd where
‹update_lbd C lbd arena = arena[C - LBD_SHIFT := ALBD lbd]›
lemma clause_slice_update_lbd:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∈# dom_m N› and
dom: ‹∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))›
shows
‹clause_slice (update_lbd i lbd arena) N ia =
(if ia = i then update_lbd (header_size (N∝i)) lbd (clause_slice arena N ia)
else clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ header_size(N ∝ ia)› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding xarena_active_clause_def
by auto
show ?thesis
using minimal_difference_between_valid_index[OF dom i ia] i_ge
minimal_difference_between_valid_index[OF dom ia i] ia_ge
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def drop_update_swap
update_lbd_def SHIFTS_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma length_update_lbd[simp]:
‹length (update_lbd i lbd arena) = length arena›
by (auto simp: update_lbd_def)
lemma clause_slice_update_lbd_dead:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∉# dom_m N› ‹ia ∈ vdom› and
dom: ‹valid_arena arena N vdom›
shows
‹arena_dead_clause (dead_clause_slice (update_lbd i lbd arena) N ia) =
arena_dead_clause (dead_clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ 4› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding valid_arena_def
by auto
show ?thesis
using minimal_difference_between_invalid_index[OF dom i ia(1) _ ia(2)] i_ge ia_ge
using minimal_difference_between_invalid_index2[OF dom i ia(1) _ ia(2)] ia_ge
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def drop_update_swap
arena_dead_clause_def update_lbd_def SHIFTS_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma xarena_active_clause_update_lbd_same:
assumes
‹i ≥ header_size (N ∝ i)› and
‹i < length arena› and
‹xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))›
shows ‹xarena_active_clause (update_lbd (header_size (N∝i)) lbd (clause_slice arena N i))
(the (fmlookup N i))›
using assms
by (cases ‹is_short_clause (N ∝ i)›)
(simp_all add: xarena_active_clause_alt_def update_lbd_def SHIFTS_def Misc.slice_def
header_size_def)
lemma valid_arena_update_lbd:
assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N›
shows ‹valid_arena (update_lbd i lbd arena) N vdom›
proof -
let ?arena = ‹update_lbd i lbd arena›
have [simp]: ‹i ∉# remove1_mset i (dom_m N)›
‹⋀ia. ia ∉# remove1_mset i (dom_m N) ⟷ ia = i ∨ (i ≠ ia ∧ ia ∉# dom_m N)›
using assms distinct_mset_dom[of N]
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset)
have
dom: ‹∀i∈#dom_m N.
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
dom': ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
vdom: ‹⋀i. i∈vdom ⟶ i ∉# dom_m N ⟶ 4 ≤ i ∧ arena_dead_clause (dead_clause_slice arena N i)›
using assms unfolding valid_arena_def by auto
have ‹ia∈#dom_m N ⟹ ia ≠ i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_update_lbd[OF i _ dom, of ia lbd]
by auto
moreover have ‹ia = i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_update_lbd[OF i _ dom, of ia lbd] i
by (simp add: xarena_active_clause_update_lbd_same)
moreover have ‹ia∈vdom ⟶
ia ∉# dom_m N ⟶
4 ≤ ia ∧ arena_dead_clause
(dead_clause_slice (update_lbd i lbd arena) (fmdrop i N) ia)› for ia
using vdom[of ia] clause_slice_update_lbd_dead[OF i _ _ arena, of ia] i
by auto
ultimately show ?thesis
using assms unfolding valid_arena_def
by auto
qed
paragraph ‹Update saved position›
definition update_pos_direct where
‹update_pos_direct C pos arena = arena[C - POS_SHIFT := APos pos]›
definition arena_update_pos where
‹arena_update_pos C pos arena = arena[C - POS_SHIFT := APos (pos - 2)]›
lemma arena_update_pos_alt_def:
‹arena_update_pos C i N = update_pos_direct C (i - 2) N›
by (auto simp: arena_update_pos_def update_pos_direct_def)
lemma clause_slice_update_pos:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∈# dom_m N› and
dom: ‹∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
long: ‹is_long_clause (N ∝ i)›
shows
‹clause_slice (update_pos_direct i pos arena) N ia =
(if ia = i then update_pos_direct (header_size (N∝i)) pos (clause_slice arena N ia)
else clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ header_size(N ∝ ia)› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding xarena_active_clause_def
by auto
show ?thesis
using minimal_difference_between_valid_index[OF dom i ia] i_ge
minimal_difference_between_valid_index[OF dom ia i] ia_ge long
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def drop_update_swap
update_pos_direct_def SHIFTS_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma clause_slice_update_pos_dead:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∉# dom_m N› ‹ia ∈ vdom› and
dom: ‹valid_arena arena N vdom› and
long: ‹is_long_clause (N ∝ i)›
shows
‹arena_dead_clause (dead_clause_slice (update_pos_direct i pos arena) N ia) =
arena_dead_clause (dead_clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ 4› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i long unfolding valid_arena_def
by auto
show ?thesis
using minimal_difference_between_invalid_index[OF dom i ia(1) _ ia(2)] i_ge ia_ge
using minimal_difference_between_invalid_index2[OF dom i ia(1) _ ia(2)] ia_ge long
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def drop_update_swap
arena_dead_clause_def update_pos_direct_def SHIFTS_def
Misc.slice_def header_size_def split: if_splits)
qed
lemma xarena_active_clause_update_pos_same:
assumes
‹i ≥ header_size (N ∝ i)› and
‹i < length arena› and
‹xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))› and
long: ‹is_long_clause (N ∝ i)› and
‹pos ≤ length (N ∝ i) - 2›
shows ‹xarena_active_clause (update_pos_direct (header_size (N∝i)) pos (clause_slice arena N i))
(the (fmlookup N i))›
using assms
by (simp_all add: update_pos_direct_def SHIFTS_def Misc.slice_def
header_size_def xarena_active_clause_alt_def)
lemma length_update_pos[simp]:
‹length (update_pos_direct i pos arena) = length arena›
by (auto simp: update_pos_direct_def)
lemma valid_arena_update_pos:
assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N› and
long: ‹is_long_clause (N ∝ i)›and
pos: ‹pos ≤ length (N ∝ i) - 2›
shows ‹valid_arena (update_pos_direct i pos arena) N vdom›
proof -
let ?arena = ‹update_pos_direct i pos arena›
have [simp]: ‹i ∉# remove1_mset i (dom_m N)›
‹⋀ia. ia ∉# remove1_mset i (dom_m N) ⟷ ia =i ∨ (i ≠ ia ∧ ia ∉# dom_m N)›
using assms distinct_mset_dom[of N]
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset)
have
dom: ‹∀i∈#dom_m N.
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
dom': ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
vdom: ‹⋀i. i∈vdom ⟶ i ∉# dom_m N ⟶ 4 ≤ i ∧ arena_dead_clause (dead_clause_slice arena N i)›
using assms unfolding valid_arena_def by auto
have ‹ia∈#dom_m N ⟹ ia ≠ i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_update_pos[OF i _ dom, of ia pos] long
by auto
moreover have ‹ia = i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_update_pos[OF i _ dom, of ia pos] i long pos
by (simp add: xarena_active_clause_update_pos_same)
moreover have ‹ia∈vdom ⟶
ia ∉# dom_m N ⟶
4 ≤ ia ∧ arena_dead_clause
(dead_clause_slice (update_pos_direct i pos arena) N ia)› for ia
using vdom[of ia] clause_slice_update_pos_dead[OF i _ _ arena, of ia] i long
by auto
ultimately show ?thesis
using assms unfolding valid_arena_def
by auto
qed
paragraph ‹Swap literals›
definition swap_lits where
‹swap_lits C i j arena = swap arena (C +i) (C + j)›
lemma clause_slice_swap_lits:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∈# dom_m N› and
dom: ‹∀i ∈# dom_m N. i < length arena ∧ i ≥ header_size (N∝i) ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
k: ‹k < length (N ∝ i)› and
l: ‹l < length (N ∝ i)›
shows
‹clause_slice (swap_lits i k l arena) N ia =
(if ia = i then swap_lits (header_size (N∝i)) k l (clause_slice arena N ia)
else clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ header_size(N ∝ ia)› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding xarena_active_clause_def
by auto
show ?thesis
using minimal_difference_between_valid_index[OF dom i ia] i_ge
minimal_difference_between_valid_index[OF dom ia i] ia_ge k l
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def drop_update_swap
swap_lits_def SHIFTS_def swap_def ac_simps
Misc.slice_def header_size_def split: if_splits)
qed
lemma length_swap_lits[simp]:
‹length (swap_lits i k l arena) = length arena›
by (auto simp: swap_lits_def)
lemma clause_slice_swap_lits_dead:
assumes
i: ‹i ∈# dom_m N› and
ia: ‹ia ∉# dom_m N› ‹ia ∈ vdom› and
dom: ‹valid_arena arena N vdom›and
k: ‹k < length (N ∝ i)› and
l: ‹l < length (N ∝ i)›
shows
‹arena_dead_clause (dead_clause_slice (swap_lits i k l arena) N ia) =
arena_dead_clause (dead_clause_slice arena N ia)›
proof -
have ia_ge: ‹ia ≥ 4› ‹ia < length arena› and
i_ge: ‹i ≥ header_size(N ∝ i)› ‹i < length arena›
using dom ia i unfolding valid_arena_def
by auto
show ?thesis
using minimal_difference_between_invalid_index[OF dom i ia(1) _ ia(2)] i_ge ia_ge
using minimal_difference_between_invalid_index2[OF dom i ia(1) _ ia(2)] ia_ge k l
by (cases ‹ia < i›)
(auto simp: extra_information_mark_to_delete_def drop_update_swap
arena_dead_clause_def swap_lits_def SHIFTS_def swap_def ac_simps
Misc.slice_def header_size_def split: if_splits)
qed
lemma xarena_active_clause_swap_lits_same:
assumes
‹i ≥ header_size (N ∝ i)› and
‹i < length arena› and
‹xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))›and
k: ‹k < length (N ∝ i)› and
l: ‹l < length (N ∝ i)›
shows ‹xarena_active_clause (clause_slice (swap_lits i k l arena) N i)
(the (fmlookup (N(i ↪ swap (N ∝ i) k l)) i))›
using assms
unfolding xarena_active_clause_alt_def
by (cases ‹is_short_clause (N ∝ i)›)
(simp_all add: swap_lits_def SHIFTS_def min_def swap_nth_if map_swap swap_swap
header_size_def ac_simps is_short_clause_def split: if_splits)
lemma is_short_clause_swap[simp]: ‹is_short_clause (swap (N ∝ i) k l) = is_short_clause (N ∝ i)›
by (auto simp: header_size_def is_short_clause_def split: if_splits)
lemma header_size_swap[simp]: ‹header_size (swap (N ∝ i) k l) = header_size (N ∝ i)›
by (auto simp: header_size_def split: if_splits)
lemma valid_arena_swap_lits:
assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N› and
k: ‹k < length (N ∝ i)› and
l: ‹l < length (N ∝ i)›
shows ‹valid_arena (swap_lits i k l arena) (N(i ↪ swap (N ∝ i) k l)) vdom›
proof -
let ?arena = ‹swap_lits i k l arena›
have [simp]: ‹i ∉# remove1_mset i (dom_m N)›
‹⋀ia. ia ∉# remove1_mset i (dom_m N) ⟷ ia =i ∨ (i ≠ ia ∧ ia ∉# dom_m N)›
using assms distinct_mset_dom[of N]
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset)
have
dom: ‹∀i∈#dom_m N.
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
dom': ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
vdom: ‹⋀i. i∈vdom ⟶ i ∉# dom_m N ⟶ 4 ≤ i ∧ arena_dead_clause (dead_clause_slice arena N i)›
using assms unfolding valid_arena_def by auto
have ‹ia∈#dom_m N ⟹ ia ≠ i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] clause_slice_swap_lits[OF i _ dom, of ia k l] k l
by auto
moreover have ‹ia = i ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia)
(the (fmlookup (N(i ↪ swap (N ∝ i) k l)) ia))›
for ia
using dom'[of ia] clause_slice_swap_lits[OF i _ dom, of ia k l] i k l
xarena_active_clause_swap_lits_same[OF _ _ _ k l, of arena]
by auto
moreover have ‹ia∈vdom ⟶
ia ∉# dom_m N ⟶
4 ≤ ia ∧ arena_dead_clause (dead_clause_slice (swap_lits i k l arena) (fmdrop i N) ia)›
for ia
using vdom[of ia] clause_slice_swap_lits_dead[OF i _ _ arena, of ia] i k l
by auto
ultimately show ?thesis
using i k l arena unfolding valid_arena_def
by auto
qed
paragraph ‹Learning a clause›
definition append_clause_skeleton where
‹append_clause_skeleton pos st used act lbd C arena =
(if is_short_clause C then
arena @ (AStatus st used) # AActivity act # ALBD lbd #
ASize (length C - 2) # map ALit C
else arena @ APos pos # (AStatus st used) # AActivity act #
ALBD lbd # ASize (length C - 2) # map ALit C)›
definition append_clause where
‹append_clause b C arena =
append_clause_skeleton 0 (if b then IRRED else LEARNED) False 0 (length C - 2) C arena›
lemma arena_active_clause_append_clause:
assumes
‹i ≥ header_size (N ∝ i)› and
‹i < length arena› and
‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))›
shows ‹xarena_active_clause (clause_slice (append_clause_skeleton pos st used act lbd C arena) N i)
(the (fmlookup N i))›
proof -
have ‹drop (header_size (N ∝ i)) (clause_slice arena N i) = map ALit (N ∝ i)› and
‹header_size (N ∝ i) ≤ i› and
‹i < length arena›
using assms
unfolding xarena_active_clause_alt_def
by auto
from arg_cong[OF this(1), of length] this(2-)
have ‹i + length (N ∝ i) ≤ length arena›
unfolding xarena_active_clause_alt_def
by (auto simp add: slice_len_min_If header_size_def is_short_clause_def split: if_splits)
then have ‹clause_slice (append_clause_skeleton pos st used act lbd C arena) N i =
clause_slice arena N i›
by (auto simp add: append_clause_skeleton_def)
then show ?thesis
using assms by simp
qed
lemma length_append_clause[simp]:
‹length (append_clause_skeleton pos st used act lbd C arena) =
length arena + length C + header_size C›
‹length (append_clause b C arena) = length arena + length C + header_size C›
by (auto simp: append_clause_skeleton_def header_size_def
append_clause_def)
lemma arena_active_clause_append_clause_same: ‹2 ≤ length C ⟹ st ≠ DELETED ⟹
pos ≤ length C - 2 ⟹
b ⟷ (st = IRRED) ⟹
xarena_active_clause
(Misc.slice (length arena) (length arena + header_size C + length C)
(append_clause_skeleton pos st used act lbd C arena))
(the (fmlookup (fmupd (length arena + header_size C) (C, b) N)
(length arena + header_size C)))›
unfolding xarena_active_clause_alt_def append_clause_skeleton_def
by (cases st)
(auto simp: header_size_def slice_start0 SHIFTS_def slice_Cons split: if_splits)
lemma clause_slice_append_clause:
assumes
ia: ‹ia ∉# dom_m N› ‹ia ∈ vdom› and
dom: ‹valid_arena arena N vdom› and
‹arena_dead_clause (dead_clause_slice (arena) N ia)›
shows
‹arena_dead_clause (dead_clause_slice (append_clause_skeleton pos st used act lbd C arena) N ia)›
proof -
have ia_ge: ‹ia ≥ 4› ‹ia < length arena›
using dom ia unfolding valid_arena_def
by auto
then have ‹dead_clause_slice (arena) N ia =
dead_clause_slice (append_clause_skeleton pos st used act lbd C arena) N ia›
by (auto simp add: extra_information_mark_to_delete_def drop_update_swap
append_clause_skeleton_def
arena_dead_clause_def swap_lits_def SHIFTS_def swap_def ac_simps
Misc.slice_def header_size_def split: if_splits)
then show ?thesis
using assms by simp
qed
lemma valid_arena_append_clause_skeleton:
assumes arena: ‹valid_arena arena N vdom› and le_C: ‹length C ≥ 2› and
b: ‹b ⟷ (st = IRRED)› and st: ‹st ≠ DELETED› and
pos: ‹pos ≤ length C - 2›
shows ‹valid_arena (append_clause_skeleton pos st used act lbd C arena)
(fmupd (length arena + header_size C) (C, b) N)
(insert (length arena + header_size C) vdom)›
proof -
let ?arena = ‹append_clause_skeleton pos st used act lbd C arena›
let ?i= ‹length arena + header_size C›
let ?N = ‹(fmupd (length arena + header_size C) (C, b) N)›
let ?vdom = ‹insert (length arena + header_size C) vdom›
have
dom: ‹∀i∈#dom_m N.
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
dom': ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
vdom: ‹⋀i. i∈vdom ⟶ i ∉# dom_m N ⟶ i ≤ length arena ∧ 4 ≤ i ∧
arena_dead_clause (dead_clause_slice arena N i)›
using assms unfolding valid_arena_def by auto
have [simp]: ‹?i ∉# dom_m N›
using dom'[of ?i]
by auto
have ‹ia∈#dom_m N ⟹
ia < length ?arena ∧
header_size (N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena N ia) (the (fmlookup N ia))› for ia
using dom'[of ia] arena_active_clause_append_clause[of N ia arena]
by auto
moreover have ‹ia = ?i ⟹
ia < length ?arena ∧
header_size (?N ∝ ia) ≤ ia ∧
xarena_active_clause (clause_slice ?arena ?N ia) (the (fmlookup ?N ia))› for ia
using dom'[of ia] le_C arena_active_clause_append_clause_same[of C st pos b arena used]
b st pos
by auto
moreover have ‹ia∈vdom ⟶
ia ∉# dom_m N ⟶ ia < length (?arena) ∧
4 ≤ ia ∧ arena_dead_clause (Misc.slice (ia - 4) ia (?arena))› for ia
using vdom[of ia] clause_slice_append_clause[of ia N vdom arena pos st used act lbd C, OF _ _ arena]
le_C b st
by auto
ultimately show ?thesis
unfolding valid_arena_def
by auto
qed
lemma valid_arena_append_clause:
assumes arena: ‹valid_arena arena N vdom› and le_C: ‹length C ≥ 2›
shows ‹valid_arena (append_clause b C arena)
(fmupd (length arena + header_size C) (C, b) N)
(insert (length arena + header_size C) vdom)›
using valid_arena_append_clause_skeleton[OF assms(1,2),
of b ‹if b then IRRED else LEARNED›]
by (auto simp: append_clause_def)
subsubsection ‹Refinement Relation›
definition status_rel:: "(nat × clause_status) set" where
‹status_rel = {(0, IRRED), (1, LEARNED), (3, DELETED)}›
definition bitfield_rel where
‹bitfield_rel n = {(a, b). b ⟷ a AND (2 ^ n) > 0}›
definition arena_el_relation where
‹arena_el_relation x el = (case el of
AStatus n b ⇒ (x AND 0b11, n) ∈ status_rel ∧ (x, b) ∈ bitfield_rel 2
| APos n ⇒ (x, n) ∈ nat_rel
| ASize n ⇒ (x, n) ∈ nat_rel
| ALBD n ⇒ (x, n) ∈ nat_rel
| AActivity n ⇒ (x, n) ∈ nat_rel
| ALit n ⇒ (x, n) ∈ nat_lit_rel
)›
definition arena_el_rel where
arena_el_rel_interal_def: ‹arena_el_rel = {(x, el). arena_el_relation x el}›
lemmas arena_el_rel_def = arena_el_rel_interal_def[unfolded arena_el_relation_def]
subsubsection ‹Preconditions and Assertions for the refinement›
text ‹The following lemma expresses the relation between the arena and the clauses and especially
shows the preconditions to be able to generate code.
The conditions on \<^term>‹arena_status› are in the direction to simplify proofs: If we would try to go
in the opposite direction, we could rewrite \<^term>‹¬irred N i› into \<^term>‹arena_status arena i ≠ LEARNED›,
which is a weaker property.
The inequality on the length are here to enable simp to prove inequalities \<^term>‹arena_length arena C > Suc 0›
automatically. Normally the arithmetic part can prove it from \<^term>‹arena_length arena C ≥ 2›,
but as this inequality is simplified away, it does not work.
›
lemma arena_lifting:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹i ∈# dom_m N›
shows
‹i ≥ header_size (N ∝ i)› and
‹i < length arena›
‹is_Size (arena ! (i - SIZE_SHIFT))›
‹length (N ∝ i) = arena_length arena i›
‹j < length (N ∝ i) ⟹ N ∝ i ! j = arena_lit arena (i + j)› and
‹j < length (N ∝ i) ⟹ is_Lit (arena ! (i+j))› and
‹j < length (N ∝ i) ⟹ i + j < length arena› and
‹N ∝ i ! 0 = arena_lit arena i› and
‹is_Lit (arena ! i)› and
‹i + length (N ∝ i) ≤ length arena› and
‹is_long_clause (N ∝ i) ⟹ is_Pos (arena ! ( i - POS_SHIFT))› and
‹is_long_clause (N ∝ i) ⟹ arena_pos arena i ≤ arena_length arena i› and
‹is_LBD (arena ! (i - LBD_SHIFT))› and
‹is_Act (arena ! (i - ACTIVITY_SHIFT))› and
‹is_Status (arena ! (i - STATUS_SHIFT))› and
‹SIZE_SHIFT ≤ i› and
‹LBD_SHIFT ≤ i›
‹ACTIVITY_SHIFT ≤ i› and
‹arena_length arena i ≥ 2› and
‹arena_length arena i ≥ Suc 0› and
‹arena_length arena i ≥ 0› and
‹arena_length arena i > Suc 0› and
‹arena_length arena i > 0› and
‹arena_status arena i = LEARNED ⟷ ¬irred N i› and
‹arena_status arena i = IRRED ⟷ irred N i› and
‹arena_status arena i ≠ DELETED› and
‹Misc.slice i (i + arena_length arena i) arena = map ALit (N ∝ i)›
proof -
have
dom: ‹⋀i. i∈#dom_m N ⟹
i < length arena ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))›
using valid unfolding valid_arena_def
by blast+
have
i_le: ‹i < length arena› and
i_ge: ‹header_size (N ∝ i) ≤ i› and
xi: ‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))›
using dom[OF i] by fast+
have
ge2: ‹2 ≤ length (N ∝ i)› and
‹header_size (N ∝ i) + length (N ∝ i) = length (clause_slice arena N i)› and
pos: ‹is_long_clause (N ∝ i) ⟶
is_Pos (clause_slice arena N i ! (header_size (N ∝ i) - POS_SHIFT)) ∧
xarena_pos (clause_slice arena N i ! (header_size (N ∝ i) - POS_SHIFT))
≤ length (N ∝ i) - 2› and
status: ‹is_Status
(clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT))› and
init: ‹(xarena_status
(clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT)) =
IRRED) =
irred N i› and
learned: ‹(xarena_status
(clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT)) =
LEARNED) =
(¬ irred N i)› and
lbd: ‹is_LBD (clause_slice arena N i ! (header_size (N ∝ i) - LBD_SHIFT))› and
act: ‹is_Act (clause_slice arena N i ! (header_size (N ∝ i) - ACTIVITY_SHIFT))› and
size: ‹is_Size (clause_slice arena N i ! (header_size (N ∝ i) - SIZE_SHIFT))› and
size': ‹Suc (Suc (xarena_length
(clause_slice arena N i !
(header_size (N ∝ i) - SIZE_SHIFT)))) =
length (N ∝ i)› and
clause: ‹Misc.slice i (i + length (N ∝ i)) arena = map ALit (N ∝ i)›
using xi i_le i_ge unfolding xarena_active_clause_alt_def arena_length_def
by simp_all
have [simp]:
‹clause_slice arena N i ! (header_size (N ∝ i) - LBD_SHIFT) = ALBD (arena_lbd arena i)›
‹clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT) =
AStatus (arena_status arena i) (arena_used arena i)›
using size size' i_le i_ge ge2 lbd status size'
unfolding header_size_def arena_length_def arena_lbd_def arena_status_def arena_used_def
by (auto simp: SHIFTS_def slice_nth)
have HH:
‹arena_length arena i = length (N ∝ i)› and ‹is_Size (arena ! (i - SIZE_SHIFT))›
using size size' i_le i_ge ge2 lbd status size' ge2
unfolding header_size_def arena_length_def arena_lbd_def arena_status_def
by (cases ‹arena ! (i - Suc 0)›; auto simp: SHIFTS_def slice_nth; fail)+
then show ‹length (N ∝ i) = arena_length arena i› and ‹is_Size (arena ! (i - SIZE_SHIFT))›
using i_le i_ge size' size ge2 HH unfolding numeral_2_eq_2
by (simp_all split:)
show ‹arena_length arena i ≥ 2›
‹arena_length arena i ≥ Suc 0› and
‹arena_length arena i ≥ 0› and
‹arena_length arena i > Suc 0› and
‹arena_length arena i > 0›
using ge2 unfolding HH by auto
show
‹i ≥ header_size (N ∝ i)› and
‹i < length arena›
using i_le i_ge by auto
show is_lit: ‹is_Lit (arena ! (i+j))› ‹N ∝ i ! j = arena_lit arena (i + j)›
if ‹j < length (N ∝ i)›
for j
using arg_cong[OF clause, of ‹λxs. xs ! j›] i_le i_ge that
by (auto simp: slice_nth arena_lit_def)
show i_le_arena: ‹i + length (N ∝ i) ≤ length arena›
using arg_cong[OF clause, of length] i_le i_ge
by (auto simp: arena_lit_def slice_len_min_If)
show ‹is_Pos (arena ! (i - POS_SHIFT))› and
‹arena_pos arena i ≤ arena_length arena i›
if ‹is_long_clause (N ∝ i)›
using pos ge2 i_le i_ge that unfolding arena_pos_def HH
by (auto simp: SHIFTS_def slice_nth header_size_def)
show ‹is_LBD (arena ! (i - LBD_SHIFT))› and
‹is_Act (arena ! (i - ACTIVITY_SHIFT))› and
‹is_Status (arena ! (i - STATUS_SHIFT))›
using lbd act ge2 i_le i_ge status unfolding arena_pos_def
by (auto simp: SHIFTS_def slice_nth header_size_def)
show ‹SIZE_SHIFT ≤ i› and ‹LBD_SHIFT ≤ i› and
‹ACTIVITY_SHIFT ≤ i›
using i_ge unfolding header_size_def SHIFTS_def by (auto split: if_splits)
show ‹j < length (N ∝ i) ⟹ i + j < length arena›
using i_le_arena by linarith
show
‹N ∝ i ! 0 = arena_lit arena i› and
‹is_Lit (arena ! i)›
using is_lit[of 0] ge2 by fastforce+
show
‹arena_status arena i = LEARNED ⟷ ¬irred N i ›and
‹arena_status arena i = IRRED ⟷ irred N i› and
‹arena_status arena i ≠ DELETED›
using learned init unfolding arena_status_def
by (auto simp: arena_status_def)
show
‹Misc.slice i (i + arena_length arena i) arena = map ALit (N ∝ i)›
apply (subst list_eq_iff_nth_eq, intro conjI allI)
subgoal
using HH i_le_arena i_le
by (auto simp: slice_nth slice_len_min_If)
subgoal for j
using HH i_le_arena i_le is_lit[of j]
by (cases ‹arena ! (i + j)›)
(auto simp: slice_nth slice_len_min_If
arena_lit_def)
done
qed
lemma arena_dom_status_iff:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹i ∈ vdom›
shows
‹i ∈# dom_m N ⟷ arena_status arena i ≠ DELETED› (is ‹?eq› is ‹?A ⟷ ?B›) and
‹is_LBD (arena ! (i - LBD_SHIFT))› (is ?lbd) and
‹is_Act (arena ! (i - ACTIVITY_SHIFT))› (is ?act) and
‹is_Status (arena ! (i - STATUS_SHIFT))› (is ?stat) and
‹4 ≤ i› (is ?ge)
proof -
have H1: ?eq ?lbd ?act ?stat ?ge
if ‹?A›
proof -
have
‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i))› and
i_ge: ‹header_size (N ∝ i) ≤ i› and
i_le: ‹i < length arena›
using assms that unfolding valid_arena_def by blast+
then have ‹is_Status (clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT))› and
‹(xarena_status (clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT)) = IRRED) =
irred N i› and
‹(xarena_status (clause_slice arena N i ! (header_size (N ∝ i) - STATUS_SHIFT)) = LEARNED) =
(¬ irred N i)› and
‹is_LBD (clause_slice arena N i ! (header_size (N ∝ i) - LBD_SHIFT))› and
‹is_Act (clause_slice arena N i ! (header_size (N ∝ i) - ACTIVITY_SHIFT)) ›
unfolding xarena_active_clause_alt_def arena_status_def
by blast+
then show ?eq and ?lbd and ?act and ?stat and ?ge
using i_ge i_le that
unfolding xarena_active_clause_alt_def arena_status_def
by (auto simp: SHIFTS_def header_size_def slice_nth split: if_splits)
qed
moreover have H2: ?eq
if ‹?B›
proof -
have ?A
proof (rule ccontr)
assume ‹i ∉# dom_m N›
then have
‹arena_dead_clause (Misc.slice (i - 4) i arena)› and
i_ge: ‹4 ≤ i› and
i_le: ‹i < length arena›
using assms unfolding valid_arena_def by blast+
then show False
using ‹?B›
unfolding arena_dead_clause_def
by (auto simp: arena_status_def slice_nth SHIFTS_def)
qed
then show ?eq
using arena_lifting[OF valid, of i] that
by auto
qed
moreover have ?lbd ?act ?stat ?ge if ‹¬?A›
proof -
have
‹arena_dead_clause (Misc.slice (i - 4) i arena)› and
i_ge: ‹4 ≤ i› and
i_le: ‹i < length arena›
using assms that unfolding valid_arena_def by blast+
then show ?lbd ?act ?stat ?ge
unfolding arena_dead_clause_def
by (auto simp: SHIFTS_def slice_nth)
qed
ultimately show ?eq and ?lbd and ?act and ?stat and ?ge
by blast+
qed
lemma valid_arena_one_notin_vdomD:
‹valid_arena M N vdom ⟹ Suc 0 ∉ vdom›
using arena_dom_status_iff[of M N vdom 1]
by auto
text ‹This is supposed to be used as for assertions. There might be a more ``local'' way to define
it, without the need for an existentially quantified clause set. However, I did not find a definition
which was really much more useful and more practical.
›
definition arena_is_valid_clause_idx :: ‹arena ⇒ nat ⇒ bool› where
‹arena_is_valid_clause_idx arena i ⟷
(∃N vdom. valid_arena arena N vdom ∧ i ∈# dom_m N)›
text ‹This precondition has weaker preconditions is restricted to extracting the status (the other
headers can be extracted but only garbage is returned).
›
definition arena_is_valid_clause_vdom :: ‹arena ⇒ nat ⇒ bool› where
‹arena_is_valid_clause_vdom arena i ⟷
(∃N vdom. valid_arena arena N vdom ∧ i ∈ vdom)›
lemma SHIFTS_alt_def:
‹POS_SHIFT = Suc (Suc (Suc (Suc (Suc 0))))›
‹STATUS_SHIFT = Suc (Suc (Suc (Suc 0)))›
‹ACTIVITY_SHIFT = Suc (Suc (Suc 0))›
‹LBD_SHIFT = Suc (Suc 0)›
‹SIZE_SHIFT = Suc 0›
by (auto simp: SHIFTS_def)
definition arena_is_valid_clause_idx_and_access :: ‹arena ⇒ nat ⇒ nat ⇒ bool› where
‹arena_is_valid_clause_idx_and_access arena i j ⟷
(∃N vdom. valid_arena arena N vdom ∧ i ∈# dom_m N ∧ j < length (N ∝ i))›
text ‹This is the precondition for direct memory access: \<^term>‹N ! (i::nat)› where
\<^term>‹(i::nat) = j + (j - i)› instead of \<^term>‹N ∝ j ! (i - j)›.›
definition arena_lit_pre where
‹arena_lit_pre arena i ⟷
(∃j. i ≥ j ∧ arena_is_valid_clause_idx_and_access arena j (i - j))›
definition arena_lit_pre2 where
‹arena_lit_pre2 arena i j ⟷
(∃N vdom. valid_arena arena N vdom ∧ i ∈# dom_m N ∧ j < length (N ∝ i))›
definition swap_lits_pre where
‹swap_lits_pre C i j arena ⟷ C + i < length arena ∧ C + j < length arena›
definition update_lbd_pre where
‹update_lbd_pre = (λ((C, lbd), arena). arena_is_valid_clause_idx arena C)›
definition get_clause_LBD_pre where
‹get_clause_LBD_pre = arena_is_valid_clause_idx›
paragraph ‹Saved position›
definition get_saved_pos_pre where
‹get_saved_pos_pre arena C ⟷ arena_is_valid_clause_idx arena C ∧
arena_length arena C > MAX_LENGTH_SHORT_CLAUSE›
definition isa_update_pos_pre where
‹isa_update_pos_pre = (λ((C, pos), arena). arena_is_valid_clause_idx arena C ∧ pos ≥ 2 ∧
pos ≤ arena_length arena C ∧ arena_length arena C > MAX_LENGTH_SHORT_CLAUSE)›
definition mark_garbage_pre where
‹mark_garbage_pre = (λ(arena, C). arena_is_valid_clause_idx arena C)›
definition arena_act_pre where
‹arena_act_pre = arena_is_valid_clause_idx›
lemma length_clause_slice_list_update[simp]:
‹length (clause_slice (arena[i := x]) a b) = length (clause_slice arena a b)›
by (auto simp: Misc.slice_def)
definition arena_decr_act where
‹arena_decr_act arena i = arena[i - ACTIVITY_SHIFT :=
AActivity (xarena_act (arena!(i - ACTIVITY_SHIFT)) div 2)]›
lemma length_arena_decr_act[simp]:
‹length (arena_decr_act arena C) = length arena›
by (auto simp: arena_decr_act_def)
definition mark_used where
‹mark_used arena i =
arena[i - STATUS_SHIFT := AStatus (xarena_status (arena!(i - STATUS_SHIFT))) True]›
lemma length_mark_used[simp]: ‹length (mark_used arena C) = length arena›
by (auto simp: mark_used_def)
lemma valid_arena_mark_used:
assumes C: ‹C ∈# dom_m N› and valid: ‹valid_arena arena N vdom›
shows
‹valid_arena (mark_used arena C) N vdom›
proof -
let ?arena = ‹mark_used arena C›
have act: ‹∀i∈#dom_m N.
i < length (arena) ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))› and
dead: ‹⋀i. i ∈ vdom ⟹ i ∉# dom_m N ⟹ i < length arena ∧
4 ≤ i ∧ arena_dead_clause (Misc.slice (i - 4) i arena)› and
C_ge: ‹header_size (N ∝ C) ≤ C› and
C_le: ‹C < length arena› and
C_act: ‹xarena_active_clause (clause_slice arena N C)
(the (fmlookup N C))›
using assms
by (auto simp: valid_arena_def)
have
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - LBD_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - LBD_SHIFT)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - STATUS_SHIFT) =
AStatus (xarena_status (clause_slice arena N C ! (header_size (N ∝ C) - STATUS_SHIFT)))
True› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - SIZE_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - SIZE_SHIFT)› and
[simp]: ‹is_long_clause (N ∝ C) ⟹ clause_slice ?arena N C ! (header_size (N ∝ C) - POS_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - POS_SHIFT)› and
[simp]: ‹length (clause_slice ?arena N C) = length (clause_slice arena N C)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - ACTIVITY_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - ACTIVITY_SHIFT)› and
[simp]: ‹Misc.slice C (C + length (N ∝ C)) ?arena =
Misc.slice C (C + length (N ∝ C)) arena›
using C_le C_ge unfolding SHIFTS_def mark_used_def header_size_def
by (auto simp: Misc.slice_def drop_update_swap split: if_splits)
have ‹xarena_active_clause (clause_slice ?arena N C) (the (fmlookup N C))›
using C_act C_le C_ge unfolding xarena_active_clause_alt_def
by simp
then have 1: ‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i)) ⟹
xarena_active_clause (clause_slice (mark_used arena C) N i) (the (fmlookup N i))›
if ‹i ∈# dom_m N›
for i
using minimal_difference_between_valid_index[of N arena C i, OF act]
minimal_difference_between_valid_index[of N arena i C, OF act] assms
that C_ge
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: mark_used_def header_size_def STATUS_SHIFT_def
split: if_splits)
have 2:
‹arena_dead_clause (Misc.slice (i - 4) i ?arena)›
if ‹i ∈ vdom›‹i ∉# dom_m N›‹arena_dead_clause (Misc.slice (i - 4) i arena)›
for i
proof -
have i_ge: ‹i ≥ 4› ‹i < length arena›
using that valid unfolding valid_arena_def
by auto
show ?thesis
using dead[of i] that C_le C_ge
minimal_difference_between_invalid_index[OF valid, of C i]
minimal_difference_between_invalid_index2[OF valid, of C i]
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: mark_used_def header_size_def STATUS_SHIFT_def C
split: if_splits)
qed
show ?thesis
using 1 2 valid
by (auto simp: valid_arena_def)
qed
definition mark_unused where
‹mark_unused arena i =
arena[i - STATUS_SHIFT := AStatus (xarena_status (arena!(i - STATUS_SHIFT))) False]›
lemma length_mark_unused[simp]: ‹length (mark_unused arena C) = length arena›
by (auto simp: mark_unused_def)
lemma valid_arena_mark_unused:
assumes C: ‹C ∈# dom_m N› and valid: ‹valid_arena arena N vdom›
shows
‹valid_arena (mark_unused arena C) N vdom›
proof -
let ?arena = ‹mark_unused arena C›
have act: ‹∀i∈#dom_m N.
i < length (arena) ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))› and
dead: ‹⋀i. i ∈ vdom ⟹ i ∉# dom_m N ⟹ i < length arena ∧
4 ≤ i ∧ arena_dead_clause (Misc.slice (i - 4) i arena)› and
C_ge: ‹header_size (N ∝ C) ≤ C› and
C_le: ‹C < length arena› and
C_act: ‹xarena_active_clause (clause_slice arena N C)
(the (fmlookup N C))›
using assms
by (auto simp: valid_arena_def)
have
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - LBD_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - LBD_SHIFT)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - STATUS_SHIFT) =
AStatus (xarena_status (clause_slice arena N C ! (header_size (N ∝ C) - STATUS_SHIFT)))
False› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - SIZE_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - SIZE_SHIFT)› and
[simp]: ‹is_long_clause (N ∝ C) ⟹ clause_slice ?arena N C ! (header_size (N ∝ C) - POS_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - POS_SHIFT)› and
[simp]: ‹length (clause_slice ?arena N C) = length (clause_slice arena N C)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - ACTIVITY_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - ACTIVITY_SHIFT)› and
[simp]: ‹Misc.slice C (C + length (N ∝ C)) ?arena =
Misc.slice C (C + length (N ∝ C)) arena›
using C_le C_ge unfolding SHIFTS_def mark_unused_def header_size_def
by (auto simp: Misc.slice_def drop_update_swap split: if_splits)
have ‹xarena_active_clause (clause_slice ?arena N C) (the (fmlookup N C))›
using C_act C_le C_ge unfolding xarena_active_clause_alt_def
by simp
then have 1: ‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i)) ⟹
xarena_active_clause (clause_slice (mark_unused arena C) N i) (the (fmlookup N i))›
if ‹i ∈# dom_m N›
for i
using minimal_difference_between_valid_index[of N arena C i, OF act]
minimal_difference_between_valid_index[of N arena i C, OF act] assms
that C_ge
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: mark_unused_def header_size_def STATUS_SHIFT_def
split: if_splits)
have 2:
‹arena_dead_clause (Misc.slice (i - 4) i ?arena)›
if ‹i ∈ vdom›‹i ∉# dom_m N›‹arena_dead_clause (Misc.slice (i - 4) i arena)›
for i
proof -
have i_ge: ‹i ≥ 4› ‹i < length arena›
using that valid unfolding valid_arena_def
by auto
show ?thesis
using dead[of i] that C_le C_ge
minimal_difference_between_invalid_index[OF valid, of C i]
minimal_difference_between_invalid_index2[OF valid, of C i]
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: mark_unused_def header_size_def STATUS_SHIFT_def C
split: if_splits)
qed
show ?thesis
using 1 2 valid
by (auto simp: valid_arena_def)
qed
definition marked_as_used :: ‹arena ⇒ nat ⇒ bool› where
‹marked_as_used arena C = xarena_used (arena ! (C - STATUS_SHIFT))›
definition marked_as_used_pre where
‹marked_as_used_pre = arena_is_valid_clause_idx›
lemma valid_arena_vdom_le:
assumes ‹valid_arena arena N ovdm›
shows ‹finite ovdm› and ‹card ovdm ≤ length arena›
proof -
have incl: ‹ovdm ⊆ {4..< length arena}›
apply auto
using assms valid_arena_in_vdom_le_arena by blast+
from card_mono[OF _ this] show ‹card ovdm ≤ length arena› by auto
have ‹length arena ≥ 4 ∨ ovdm = {}›
using incl by auto
with card_mono[OF _ incl] have ‹ovdm ≠ {} ⟹ card ovdm < length arena›
by auto
from finite_subset[OF incl] show ‹finite ovdm› by auto
qed
lemma valid_arena_vdom_subset:
assumes ‹valid_arena arena N (set vdom)› and ‹distinct vdom›
shows ‹length vdom ≤ length arena›
proof -
have ‹set vdom ⊆ {0 ..< length arena}›
using assms by (auto simp: valid_arena_def)
from card_mono[OF _ this] show ?thesis using assms by (auto simp: distinct_card)
qed
lemma valid_arena_arena_incr_act:
assumes C: ‹C ∈# dom_m N› and valid: ‹valid_arena arena N vdom›
shows
‹valid_arena (arena_incr_act arena C) N vdom›
proof -
let ?arena = ‹arena_incr_act arena C›
have act: ‹∀i∈#dom_m N.
i < length (arena) ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))› and
dead: ‹⋀i. i ∈ vdom ⟹ i ∉# dom_m N ⟹ i < length arena ∧
4 ≤ i ∧ arena_dead_clause (Misc.slice (i - 4) i arena)› and
C_ge: ‹header_size (N ∝ C) ≤ C› and
C_le: ‹C < length arena› and
C_act: ‹xarena_active_clause (clause_slice arena N C)
(the (fmlookup N C))›
using assms
by (auto simp: valid_arena_def)
have
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - LBD_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - LBD_SHIFT)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - STATUS_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - STATUS_SHIFT)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - SIZE_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - SIZE_SHIFT)› and
[simp]: ‹is_long_clause (N ∝ C) ⟹ clause_slice ?arena N C ! (header_size (N ∝ C) - POS_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - POS_SHIFT)› and
[simp]: ‹length (clause_slice ?arena N C) = length (clause_slice arena N C)› and
[simp]: ‹is_Act (clause_slice ?arena N C ! (header_size (N ∝ C) - ACTIVITY_SHIFT))› and
[simp]: ‹Misc.slice C (C + length (N ∝ C)) ?arena =
Misc.slice C (C + length (N ∝ C)) arena›
using C_le C_ge unfolding SHIFTS_def arena_incr_act_def header_size_def
by (auto simp: Misc.slice_def drop_update_swap split: if_splits)
have ‹xarena_active_clause (clause_slice ?arena N C) (the (fmlookup N C))›
using C_act C_le C_ge unfolding xarena_active_clause_alt_def
by simp
then have 1: ‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i)) ⟹
xarena_active_clause (clause_slice (arena_incr_act arena C) N i) (the (fmlookup N i))›
if ‹i ∈# dom_m N›
for i
using minimal_difference_between_valid_index[of N arena C i, OF act]
minimal_difference_between_valid_index[of N arena i C, OF act] assms
that C_ge
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: arena_incr_act_def header_size_def ACTIVITY_SHIFT_def
split: if_splits)
have 2:
‹arena_dead_clause (Misc.slice (i - 4) i ?arena)›
if ‹i ∈ vdom›‹i ∉# dom_m N›‹arena_dead_clause (Misc.slice (i - 4) i arena)›
for i
proof -
have i_ge: ‹i ≥ 4› ‹i < length arena›
using that valid unfolding valid_arena_def
by auto
show ?thesis
using dead[of i] that C_le C_ge
minimal_difference_between_invalid_index[OF valid, of C i]
minimal_difference_between_invalid_index2[OF valid, of C i]
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: arena_incr_act_def header_size_def ACTIVITY_SHIFT_def C
split: if_splits)
qed
show ?thesis
using 1 2 valid
by (auto simp: valid_arena_def arena_incr_act_def)
qed
lemma valid_arena_arena_decr_act:
assumes C: ‹C ∈# dom_m N› and valid: ‹valid_arena arena N vdom›
shows
‹valid_arena (arena_decr_act arena C) N vdom›
proof -
let ?arena = ‹arena_decr_act arena C›
have act: ‹∀i∈#dom_m N.
i < length (arena) ∧
header_size (N ∝ i) ≤ i ∧
xarena_active_clause (clause_slice arena N i)
(the (fmlookup N i))› and
dead: ‹⋀i. i ∈ vdom ⟹ i ∉# dom_m N ⟹ i < length arena ∧
4 ≤ i ∧ arena_dead_clause (Misc.slice (i - 4) i arena)› and
C_ge: ‹header_size (N ∝ C) ≤ C› and
C_le: ‹C < length arena› and
C_act: ‹xarena_active_clause (clause_slice arena N C)
(the (fmlookup N C))›
using assms
by (auto simp: valid_arena_def)
have
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - LBD_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - LBD_SHIFT)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - STATUS_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - STATUS_SHIFT)› and
[simp]: ‹clause_slice ?arena N C ! (header_size (N ∝ C) - SIZE_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - SIZE_SHIFT)› and
[simp]: ‹is_long_clause (N ∝ C) ⟹ clause_slice ?arena N C ! (header_size (N ∝ C) - POS_SHIFT) =
clause_slice arena N C ! (header_size (N ∝ C) - POS_SHIFT)› and
[simp]: ‹length (clause_slice ?arena N C) = length (clause_slice arena N C)› and
[simp]: ‹is_Act (clause_slice ?arena N C ! (header_size (N ∝ C) - ACTIVITY_SHIFT))› and
[simp]: ‹Misc.slice C (C + length (N ∝ C)) ?arena =
Misc.slice C (C + length (N ∝ C)) arena›
using C_le C_ge unfolding SHIFTS_def arena_decr_act_def header_size_def
by (auto simp: Misc.slice_def drop_update_swap split: if_splits)
have ‹xarena_active_clause (clause_slice ?arena N C) (the (fmlookup N C))›
using C_act C_le C_ge unfolding xarena_active_clause_alt_def
by simp
then have 1: ‹xarena_active_clause (clause_slice arena N i) (the (fmlookup N i)) ⟹
xarena_active_clause (clause_slice (arena_decr_act arena C) N i) (the (fmlookup N i))›
if ‹i ∈# dom_m N›
for i
using minimal_difference_between_valid_index[of N arena C i, OF act]
minimal_difference_between_valid_index[of N arena i C, OF act] assms
that C_ge
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: arena_decr_act_def header_size_def ACTIVITY_SHIFT_def
split: if_splits)
have 2:
‹arena_dead_clause (Misc.slice (i - 4) i ?arena)›
if ‹i ∈ vdom›‹i ∉# dom_m N›‹arena_dead_clause (Misc.slice (i - 4) i arena)›
for i
proof -
have i_ge: ‹i ≥ 4› ‹i < length arena›
using that valid unfolding valid_arena_def
by auto
show ?thesis
using dead[of i] that C_le C_ge
minimal_difference_between_invalid_index[OF valid, of C i]
minimal_difference_between_invalid_index2[OF valid, of C i]
by (cases ‹C < i›; cases ‹C > i›)
(auto simp: arena_decr_act_def header_size_def ACTIVITY_SHIFT_def C
split: if_splits)
qed
show ?thesis
using 1 2 valid
by (auto simp: valid_arena_def)
qed
lemma length_arena_incr_act[simp]:
‹length (arena_incr_act arena C) = length arena›
by (auto simp: arena_incr_act_def)
section ‹MOP versions of operations›
subsection ‹Access to literals›
definition mop_arena_lit where
‹mop_arena_lit arena s = do {
ASSERT(arena_lit_pre arena s);
RETURN (arena_lit arena s)
}›
lemma arena_lit_pre_le_lengthD: ‹arena_lit_pre arena C ⟹ C < length arena›
apply (auto simp: arena_lit_pre_def arena_is_valid_clause_idx_and_access_def)
using arena_lifting(7) nat_le_iff_add by auto
definition mop_arena_lit2 :: ‹arena ⇒ nat ⇒ nat ⇒ nat literal nres› where
‹mop_arena_lit2 arena i j = do {
ASSERT(arena_lit_pre arena (i+j));
let s = i+j;
RETURN (arena_lit arena s)
}›
named_theorems mop_arena_lit ‹Theorems on mop-forms of arena constants›
lemma mop_arena_lit_itself:
‹mop_arena_lit arena k' ≤ SPEC( λc. (c, N ∝ i!j) ∈ Id) ⟹ mop_arena_lit arena k' ≤ SPEC( λc. (c, N ∝ i!j) ∈ Id)›
‹mop_arena_lit2 arena i' k' ≤ SPEC( λc. (c, N ∝ i!j) ∈ Id) ⟹ mop_arena_lit2 arena i' k' ≤ SPEC( λc. (c, N ∝ i!j) ∈ Id)›
.
lemma [mop_arena_lit]:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹i ∈# dom_m N›
shows
‹k = i+j ⟹ j < length (N ∝ i) ⟹ mop_arena_lit arena k ≤ SPEC( λc. (c, N ∝ i!j) ∈ Id)›
‹i=i' ⟹ j=j' ⟹j < length (N ∝ i) ⟹ mop_arena_lit2 arena i' j' ≤ SPEC( λc. (c, N ∝ i!j) ∈ Id)›
using assms apply (auto simp: arena_lifting mop_arena_lit_def mop_arena_lit2_def Let_def
intro!: ASSERT_leI)
apply (metis arena_is_valid_clause_idx_and_access_def arena_lifting(4) arena_lit_pre_def diff_add_inverse le_add1)+
done
lemma mop_arena_lit2[mop_arena_lit]:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹(C, C') ∈ nat_rel› ‹(i, i') ∈ nat_rel›
shows
‹mop_arena_lit2 arena C i ≤ ⇓Id (mop_clauses_at N C' i')›
using assms unfolding mop_clauses_swap_def mop_arena_lit2_def mop_clauses_at_def
by refine_rcg
(auto simp: arena_lifting valid_arena_swap_lits arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
intro!: exI[of _ C])
definition mop_arena_lit2' :: ‹nat set ⇒ arena ⇒ nat ⇒ nat ⇒ nat literal nres› where
‹mop_arena_lit2' vdom = mop_arena_lit2›
lemma mop_arena_lit2'[mop_arena_lit]:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹(C, C') ∈ nat_rel› ‹(i, i') ∈ nat_rel›
shows
‹mop_arena_lit2' vdom arena C i ≤ ⇓Id (mop_clauses_at N C' i')›
using mop_arena_lit2[OF assms]
unfolding mop_arena_lit2'_def
.
lemma arena_lit_pre2_arena_lit[dest]:
‹arena_lit_pre2 N i j ⟹ arena_lit_pre N (i+j)›
by (auto simp: arena_lit_pre_def arena_lit_pre2_def arena_is_valid_clause_idx_and_access_def
intro!: exI[of _ i])
subsection ‹Swapping of literals›
definition mop_arena_swap where
‹mop_arena_swap C i j arena = do {
ASSERT(swap_lits_pre C i j arena);
RETURN (swap_lits C i j arena)
}›
lemma mop_arena_swap[mop_arena_lit]:
assumes valid: ‹valid_arena arena N vdom› and
i: ‹(C, C') ∈ nat_rel› ‹(i, i') ∈ nat_rel› ‹(j, j') ∈ nat_rel›
shows
‹mop_arena_swap C i j arena ≤ ⇓{(N', N). valid_arena N' N vdom} (mop_clauses_swap N C' i' j')›
using assms unfolding mop_clauses_swap_def mop_arena_swap_def swap_lits_pre_def
by refine_rcg
(auto simp: arena_lifting valid_arena_swap_lits)
subsection ‹Position Saving›
definition mop_arena_pos :: ‹arena ⇒ nat ⇒ nat nres› where
‹mop_arena_pos arena C = do {
ASSERT(get_saved_pos_pre arena C);
RETURN (arena_pos arena C)
}›
definition mop_arena_length :: ‹arena_el list ⇒ nat ⇒ nat nres› where
‹mop_arena_length arena C = do {
ASSERT(arena_is_valid_clause_idx arena C);
RETURN (arena_length arena C)
}›
subsection ‹Clause length›
lemma mop_arena_length:
‹(uncurry mop_arena_length, uncurry (RETURN oo (λN c. length (N ∝ c)))) ∈
[λ(N, i). i ∈# dom_m N]⇩f {(N, N'). valid_arena N N' vdom} ×⇩f nat_rel → ⟨nat_rel⟩nres_rel›
unfolding mop_arena_length_def
by (intro frefI nres_relI)
(auto 5 3 intro!: ASSERT_leI simp: append_ll_def arena_is_valid_clause_idx_def
arena_lifting)
definition mop_arena_lbd where
‹mop_arena_lbd arena C = do {
ASSERT(get_clause_LBD_pre arena C);
RETURN(arena_lbd arena C)
}›
definition mop_arena_status where
‹mop_arena_status arena C = do {
ASSERT(arena_is_valid_clause_vdom arena C);
RETURN(arena_status arena C)
}›
definition mop_marked_as_used where
‹mop_marked_as_used arena C = do {
ASSERT(marked_as_used_pre arena C);
RETURN(marked_as_used arena C)
}›
definition arena_other_watched :: ‹arena ⇒ nat literal ⇒ nat ⇒ nat ⇒ nat literal nres› where
‹arena_other_watched S L C i = do {
ASSERT(i < 2 ∧ arena_lit S (C + i) = L ∧ arena_lit_pre2 S C i ∧
arena_lit_pre2 S C (1-i));
mop_arena_lit2 S C (1 - i)
}›
end