Theory IsaSAT_Clauses
theory IsaSAT_Clauses
imports IsaSAT_Arena
begin
chapter ‹The memory representation: Manipulation of all clauses›
subsubsection ‹Representation of Clauses›
named_theorems isasat_codegen ‹lemmas that should be unfolded to generate (efficient) code›
type_synonym clause_annot = ‹clause_status × nat × nat›
type_synonym clause_annots = ‹clause_annot list›
definition list_fmap_rel :: ‹_ ⇒ (arena × nat clauses_l) set› where
‹list_fmap_rel vdom = {(arena, N). valid_arena arena N vdom}›
lemma nth_clauses_l:
‹(uncurry2 (RETURN ooo (λN i j. arena_lit N (i+j))),
uncurry2 (RETURN ooo (λN i j. N ∝ i ! j)))
∈ [λ((N, i), j). i ∈# dom_m N ∧ j < length (N ∝ i)]⇩f
list_fmap_rel vdom ×⇩f nat_rel ×⇩f nat_rel → ⟨Id⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: list_fmap_rel_def arena_lifting)
abbreviation clauses_l_fmat where
‹clauses_l_fmat ≡ list_fmap_rel›
type_synonym vdom = ‹nat set›
definition fmap_rll :: ‹(nat, 'a literal list × bool) fmap ⇒ nat ⇒ nat ⇒ 'a literal› where
[simp]: ‹fmap_rll l i j = l ∝ i ! j›
definition fmap_rll_u :: ‹(nat, 'a literal list × bool) fmap ⇒ nat ⇒ nat ⇒ 'a literal› where
[simp]: ‹fmap_rll_u = fmap_rll›
definition fmap_rll_u64 :: ‹(nat, 'a literal list × bool) fmap ⇒ nat ⇒ nat ⇒ 'a literal› where
[simp]: ‹fmap_rll_u64 = fmap_rll›
definition fmap_length_rll_u :: ‹(nat, 'a literal list × bool) fmap ⇒ nat ⇒ nat› where
‹fmap_length_rll_u l i = length_uint32_nat (l ∝ i)›
declare fmap_length_rll_u_def[symmetric, isasat_codegen]
definition fmap_length_rll_u64 :: ‹(nat, 'a literal list × bool) fmap ⇒ nat ⇒ nat› where
‹fmap_length_rll_u64 l i = length_uint32_nat (l ∝ i)›
declare fmap_length_rll_u_def[symmetric, isasat_codegen]
definition fmap_length_rll :: ‹(nat, 'a literal list × bool) fmap ⇒ nat ⇒ nat› where
[simp]: ‹fmap_length_rll l i = length (l ∝ i)›
definition fmap_swap_ll where
[simp]: ‹fmap_swap_ll N i j f = (N(i ↪ swap (N ∝ i) j f))›
text ‹From a performance point of view, appending several time a single element is less efficient
than reserving a space that is large enough directly. However, in this case the list of clauses \<^term>‹N›
is so large that there should not be any difference›
definition fm_add_new where
‹fm_add_new b C N0 = do {
let s = length C - 2;
let lbd = shorten_lbd s;
let st = (if b then AStatus IRRED 0 lbd else AStatus LEARNED 0 lbd);
let l = length N0;
let N = (if is_short_clause C then
(((N0 @ [st]))) @ [ASize s]
else ((((N0 @ [APos 0]) @ [st]))) @ [ASize (s)]);
(i, N) ← WHILE⇩T⇗ λ(i, N). i < length C ⟶ length N < header_size C + length N0 + length C⇖
(λ(i, N). i < length C)
(λ(i, N). do {
ASSERT(i < length C);
RETURN (i+1, N @ [ALit (C ! i)])
})
(0, N);
RETURN (N, l + header_size C)
}›
lemma nth_append_clause:
‹a < length C ⟹ append_clause b C N ! (length N + header_size C + a) = ALit (C ! a)›
unfolding append_clause_def header_size_Suc_def append_clause_skeleton_def
by (auto simp: nth_Cons nth_append)
lemma fm_add_new_append_clause:
‹fm_add_new b C N ≤ RETURN (append_clause b C N, length N + header_size C)›
unfolding fm_add_new_def
apply (rewrite at ‹let _ = length _ in _› Let_def)
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(i, _). Suc (length C) - i)› and
I' = ‹λ(i, N'). N' = take (length N + header_size C + i) (append_clause b C N) ∧
i ≤ length C›])
subgoal by auto
subgoal by (auto simp: append_clause_def header_size_def
append_clause_skeleton_def split: if_splits)
subgoal by (auto simp: append_clause_def header_size_def
append_clause_skeleton_def split: if_splits)
subgoal by simp
subgoal by simp
subgoal by auto
subgoal by (auto simp: take_Suc_conv_app_nth nth_append_clause)
subgoal by auto
subgoal by auto
subgoal by auto
done
definition fm_add_new_at_position
:: ‹bool ⇒ nat ⇒ 'v clause_l ⇒ 'v clauses_l ⇒ 'v clauses_l›
where
‹fm_add_new_at_position b i C N = fmupd i (C, b) N›
definition AStatus_IRRED where
‹AStatus_IRRED = AStatus IRRED 0›
definition AStatus_IRRED2 where
‹AStatus_IRRED2 = AStatus IRRED 1›
definition AStatus_LEARNED where
‹AStatus_LEARNED = AStatus LEARNED 1›
definition AStatus_LEARNED2 where
‹AStatus_LEARNED2 = AStatus LEARNED 0›
definition (in -)fm_add_new_fast where
[simp]: ‹fm_add_new_fast = fm_add_new›
lemma (in -)append_and_length_code_fast:
‹length ba ≤ Suc (Suc unat32_max) ⟹
2 ≤ length ba ⟹
length b ≤ unat64_max - (unat32_max + 5) ⟹
(aa, header_size ba) ∈ uint64_nat_rel ⟹
(ab, length b) ∈ uint64_nat_rel ⟹
length b + header_size ba ≤ unat64_max›
by (auto simp: unat64_max_def unat32_max_def header_size_def)
definition (in -)four_uint64_nat where
[simp]: ‹four_uint64_nat = (4 :: nat)›
definition (in -)five_uint64_nat where
[simp]: ‹five_uint64_nat = (5 :: nat)›
definition append_and_length_fast_code_pre where
‹append_and_length_fast_code_pre ≡ λ((b, C), N). length C ≤ unat32_max+2 ∧ length C ≥ 2 ∧
length N + length C + MAX_HEADER_SIZE ≤ snat64_max›
lemma fm_add_new_alt_def:
‹fm_add_new b C N0 = do {
let s = length C - 2;
let lbd = shorten_lbd s;
let st = (if b then AStatus_IRRED lbd else AStatus_LEARNED2 lbd);
let l = length N0;
let N =
(if is_short_clause C
then ((N0 @ [st])) @
[ASize s]
else (((N0 @ [APos 0]) @ [st])) @
[ASize s]);
(i, N) ←
WHILE⇩T⇗ λ(i, N). i < length C ⟶ length N < header_size C + length N0 + length C⇖
(λ(i, N). i < length C)
(λ(i, N). do {
_ ← ASSERT (i < length C);
RETURN (i + 1, N @ [ALit (C ! i)])
})
(0, N);
RETURN (N, l + header_size C)
}›
unfolding fm_add_new_def Let_def AStatus_LEARNED2_def AStatus_IRRED2_def
AStatus_LEARNED_def AStatus_IRRED_def
by auto
definition fmap_swap_ll_u64 where
[simp]: ‹fmap_swap_ll_u64 = fmap_swap_ll›
definition fm_mv_clause_to_new_arena where
‹fm_mv_clause_to_new_arena C old_arena new_arena0 = do {
ASSERT(arena_is_valid_clause_idx old_arena C);
ASSERT(C ≥ (if (arena_length old_arena C) ≤ 4 then MIN_HEADER_SIZE else MAX_HEADER_SIZE));
let st = C - (if (arena_length old_arena C) ≤ 4 then MIN_HEADER_SIZE else MAX_HEADER_SIZE);
ASSERT(C + (arena_length old_arena C) ≤ length old_arena);
let en = C + (arena_length old_arena C);
(i, new_arena) ←
WHILE⇩T⇗ λ(i, new_arena). i < en ⟶ length new_arena < length new_arena0 + (arena_length old_arena C) + (if (arena_length old_arena C) ≤ 4 then MIN_HEADER_SIZE else MAX_HEADER_SIZE) ⇖
(λ(i, new_arena). i < en)
(λ(i, new_arena). do {
ASSERT (i < length old_arena ∧ i < en);
RETURN (i + 1, new_arena @ [old_arena ! i])
})
(st, new_arena0);
RETURN (new_arena)
}›
lemma valid_arena_append_clause_slice:
assumes
‹valid_arena old_arena N vd› and
‹valid_arena new_arena N' vd'› and
‹C ∈# dom_m N›
shows ‹valid_arena (new_arena @ clause_slice old_arena N C)
(fmupd (length new_arena + header_size (N ∝ C)) (N ∝ C, irred N C) N')
(insert (length new_arena + header_size (N ∝ C)) vd')›
proof -
define pos st lbd used where
‹pos = (if is_long_clause (N ∝ C) then arena_pos old_arena C - 2 else 0)› and
‹st = arena_status old_arena C› and
‹lbd = arena_lbd old_arena C› and
‹used = arena_used old_arena C›
have ‹2 ≤ length (N ∝ C)›
unfolding st_def used_def lbd_def
append_clause_skeleton_def arena_status_def
xarena_status_def arena_used_def
xarena_used_def
arena_lbd_def xarena_lbd_def
using arena_lifting[OF assms(1,3)]
by (auto simp: is_Status_def is_Pos_def is_Size_def)
have
45: ‹4 = (Suc (Suc (Suc (Suc 0))))›
‹5 = Suc (Suc (Suc (Suc (Suc 0))))›
‹3 = (Suc (Suc (Suc 0)))›
‹2 = (Suc (Suc 0))›
by auto
have sl: ‹clause_slice old_arena N C =
(if is_long_clause (N ∝ C) then [APos pos]
else []) @
[AStatus st used lbd, ASize (length (N ∝ C) - 2)] @
map ALit (N ∝ C)›
unfolding st_def used_def lbd_def
append_clause_skeleton_def arena_status_def
xarena_status_def arena_used_def
xarena_used_def
pos_def arena_pos_def
xarena_pos_def
arena_lbd_def xarena_lbd_def
arena_length_def xarena_length_def
using arena_lifting[OF assms(1,3)]
by (auto simp: is_Status_def is_Pos_def is_Size_def
header_size_def 45
slice_Suc_nth[of ‹C - Suc (Suc (Suc (Suc 0)))›]
slice_Suc_nth[of ‹C - Suc (Suc (Suc 0))›]
slice_Suc_nth[of ‹C - Suc (Suc 0)›]
slice_Suc_nth[of ‹C - Suc 0›]
SHIFTS_alt_def arena_length_def
arena_pos_def xarena_pos_def
arena_status_def xarena_status_def)
have ‹2 ≤ length (N ∝ C)› and
‹pos ≤ length (N ∝ C) - 2› and
‹st = IRRED ⟷ irred N C› and
‹st ≠ DELETED›
unfolding st_def used_def lbd_def pos_def
append_clause_skeleton_def st_def
using arena_lifting[OF assms(1,3)]
by (cases ‹is_short_clause (N ∝ C)›;
auto split: arena_el.splits if_splits
simp: header_size_def arena_pos_def; fail)+
then have ‹valid_arena (append_clause_skeleton pos st used lbd (N ∝ C) new_arena)
(fmupd (length new_arena + header_size (N ∝ C)) (N ∝ C, irred N C) N')
(insert (length new_arena + header_size (N ∝ C)) vd')›
apply -
by (rule valid_arena_append_clause_skeleton[OF assms(2), of ‹N ∝ C› _ st
pos used lbd]) auto
moreover have
‹append_clause_skeleton pos st used lbd (N ∝ C) new_arena =
new_arena @ clause_slice old_arena N C›
by (auto simp: append_clause_skeleton_def sl)
ultimately show ?thesis
by auto
qed
lemma fm_mv_clause_to_new_arena:
assumes ‹valid_arena old_arena N vd› and
‹valid_arena new_arena N' vd'› and
‹C ∈# dom_m N›
shows ‹fm_mv_clause_to_new_arena C old_arena new_arena ≤
SPEC(λnew_arena'.
new_arena' = new_arena @ clause_slice old_arena N C ∧
valid_arena (new_arena @ clause_slice old_arena N C)
(fmupd (length new_arena + header_size (N ∝ C)) (N ∝ C, irred N C) N')
(insert (length new_arena + header_size (N ∝ C)) vd'))›
proof -
define st and en where
‹st = C - (if arena_length old_arena C ≤ 4 then MIN_HEADER_SIZE else MAX_HEADER_SIZE)› and
‹en = C + arena_length old_arena C›
have st:
‹st = C - header_size (N ∝ C)›
using assms
unfolding st_def
by (auto simp: st_def header_size_def
arena_lifting)
show ?thesis
using assms
unfolding fm_mv_clause_to_new_arena_def st_def[symmetric]
en_def[symmetric] Let_def
apply (refine_vcg
WHILEIT_rule_stronger_inv[where R = ‹measure (λ(i, N). en - i)› and
I' = ‹λ(i, new_arena'). i ≤ C + length (N∝C) ∧ i ≥ st ∧
new_arena' = new_arena @
Misc.slice (C - header_size (N∝C)) i old_arena›])
subgoal
unfolding arena_is_valid_clause_idx_def
by auto
subgoal using arena_lifting(4)[OF assms(1)] by (auto
dest!: arena_lifting(1)[of _ N _ C] simp: header_size_def split: if_splits)
subgoal using arena_lifting(10, 4) en_def by auto
subgoal
by auto
subgoal by auto
subgoal
using arena_lifting[OF assms(1,3)]
by (auto simp: st)
subgoal
by (auto simp: st arena_lifting)
subgoal
using arena_lifting[OF assms(1,3)]
by (auto simp: st en_def)
subgoal
using arena_lifting[OF assms(1,3)]
by (auto simp: st en_def)
subgoal by auto
subgoal using arena_lifting[OF assms(1,3)]
by (auto simp: slice_len_min_If en_def st_def header_size_def)
subgoal
using arena_lifting[OF assms(1,3)]
by (auto simp: st en_def)
subgoal
using arena_lifting[OF assms(1,3)]
by (auto simp: st)
subgoal
by (auto simp: st en_def arena_lifting[OF assms(1,3)]
slice_append_nth)
subgoal by auto
subgoal by (auto simp: en_def arena_lifting)
subgoal
using valid_arena_append_clause_slice[OF assms]
by auto
done
qed
lemma size_learned_clss_dom_m: ‹size (learned_clss_l N) ≤ size (dom_m N)›
unfolding ran_m_def
apply (rule order_trans[OF size_filter_mset_lesseq])
by (auto simp: ran_m_def)
lemma valid_arena_ge_length_clauses:
assumes ‹valid_arena arena N vdom›
shows ‹length arena ≥ (∑C ∈# dom_m N. length (N ∝ C) + header_size (N ∝ C))›
proof -
obtain xs where
mset_xs: ‹mset xs = dom_m N› and sorted: ‹sorted xs› and dist[simp]: ‹distinct xs› and set_xs: ‹set xs = set_mset (dom_m N)›
using distinct_mset_dom distinct_mset_mset_distinct mset_sorted_list_of_multiset by fastforce
then have 1: ‹set_mset (mset xs) = set xs› by (meson set_mset_mset)
have diff: ‹xs ≠ [] ⟹ a ∈ set xs ⟹ a < last xs ⟹ a + length (N ∝ a) ≤ last xs› for a
using valid_minimal_difference_between_valid_index[OF assms, of a ‹last xs›]
mset_xs[symmetric] sorted by (cases xs rule: rev_cases; auto simp: sorted_append)
have ‹set xs ⊆ set_mset (dom_m N)›
using mset_xs[symmetric] by auto
then have ‹(∑A∈set xs. length (N ∝ A) + header_size (N ∝ A)) ≤ Max (insert 0 ((λA. A + length (N ∝ A)) ` (set xs)))›
(is ‹?P xs ≤ ?Q xs›)
using sorted dist
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
then have IH: ‹(∑A∈set xs. length (N ∝ A) + header_size (N ∝ A))
≤ Max (insert 0 ((λA. A + length (N ∝ A)) ` set xs))› and
x_dom: ‹x ∈# dom_m N› and
x_max: ‹⋀a. a ∈ set xs ⟹ x > a› and
xs_N: ‹set xs ⊆ set_mset (dom_m N)›
apply (clarsimp_all simp: sorted_append order.order_iff_strict sorted_wrt_append)
apply (metis (full_types) insert_subset order_less_le subsetI)
apply (metis (full_types) insert_subset order_less_le subsetI)
apply (meson distinct_sorted_append snoc.prems(2) snoc.prems(3))
apply blast
done
have x_ge: ‹header_size (N ∝ x) ≤ x›
using assms ‹x ∈# dom_m N› arena_lifting(1) by blast
have diff: ‹a ∈ set xs ⟹ a + length (N ∝ a) + header_size (N ∝ x) ≤ x›
‹a ∈ set xs ⟹ a + length (N ∝ a) ≤ x› for a
using valid_minimal_difference_between_valid_index[OF assms, of a x]
x_max[of a] xs_N x_dom by auto
have ‹?P (xs @ [x]) ≤ ?P xs + length (N ∝ x) + header_size (N ∝ x)›
using snoc by auto
also have ‹... ≤ ?Q xs + (length (N ∝ x) + header_size (N ∝ x))›
using IH by auto
also have ‹... ≤ (length (N ∝ x) + x)›
by (subst linordered_ab_semigroup_add_class.Max_add_commute2[symmetric]; auto intro: diff x_ge)
also have ‹... = Max (insert (x + length (N ∝ x)) ((λx. x + length (N ∝ x)) ` set xs))›
by (subst eq_commute)
(auto intro!: linorder_class.Max_eqI intro: order_trans[OF diff(2)])
finally show ?case by auto
qed
also have ‹... ≤ (if xs = [] then 0 else last xs + length (N ∝ last xs))›
using sorted distinct_sorted_append[of ‹butlast xs› ‹last xs›] dist
by (cases ‹xs› rule: rev_cases)
(auto intro: order_trans[OF diff])
also have ‹... ≤ length arena›
using arena_lifting(7)[OF assms, of ‹last xs› ‹length (N ∝ last xs) - 1›] mset_xs[symmetric] assms
by (cases ‹xs› rule: rev_cases) (auto simp: arena_lifting)
finally show ?thesis
unfolding mset_xs[symmetric]
by (subst distinct_sum_mset_sum) auto
qed
lemma valid_arena_size_dom_m_le_arena: ‹valid_arena arena N vdom ⟹ size (dom_m N) ≤ length arena›
using valid_arena_ge_length_clauses[of arena N vdom]
ordered_comm_monoid_add_class.sum_mset_mono[of ‹dom_m N› ‹λ_. 1›
‹λC. length (N ∝ C) + header_size (N ∝ C)›]
by (fastforce simp: header_size_def split: if_splits)
end