Theory IsaSAT_Arena_LLVM
theory IsaSAT_Arena_LLVM
imports IsaSAT_Arena IsaSAT_Literals_LLVM Watched_Literals.WB_More_IICF_LLVM
begin
section ‹Code Generation›
hide_const (open) NEMonad.RETURN NEMonad.ASSERT
type_synonym arena_assn = ‹(32 word, 64) array_list›
lemma protected_bind_assoc:
‹Refine_Basic.bind$(Refine_Basic.bind$m$(λ⇩2x. f x))$(λ⇩2y. g y) =
Refine_Basic.bind$m$(λ⇩2x. Refine_Basic.bind$(f x)$(λ⇩2y. g y))› by simp
lemma convert_swap: ‹WB_More_Refinement_List.swap = More_List.swap›
unfolding WB_More_Refinement_List.swap_def More_List.swap_def ..
subsubsection ‹Code Generation›
definition ‹arena_el_impl_rel ≡ unat_rel' TYPE(32) O arena_el_rel›
lemmas [fcomp_norm_unfold] = arena_el_impl_rel_def[symmetric]
abbreviation ‹arena_el_impl_assn ≡ pure arena_el_impl_rel›
paragraph ‹Arena Element Operations›
context
notes [simp] = arena_el_rel_def
notes [split] = arena_el.splits
notes [intro!] = frefI
begin
text ‹Literal›
lemma xarena_lit_refine1: ‹(λeli. eli, xarena_lit) ∈ [is_Lit]⇩f arena_el_rel → nat_lit_rel› by auto
sepref_def xarena_lit_impl [llvm_inline]
is [] ‹RETURN o (λeli. eli)› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn› by sepref
lemmas [sepref_fr_rules] = xarena_lit_impl.refine[FCOMP xarena_lit_refine1]
lemma ALit_refine1: ‹(λx. x,ALit) ∈ nat_lit_rel → arena_el_rel› by auto
sepref_def ALit_impl [llvm_inline] is [] ‹RETURN o (λx. x)›
:: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn› by sepref
lemmas [sepref_fr_rules] = ALit_impl.refine[FCOMP ALit_refine1]
text ‹LBD›
lemma xarena_lbd_refine1: ‹(λeli. eli >> 5, xarena_lbd) ∈ [is_Status]⇩f arena_el_rel → nat_rel›
by (auto simp: is_Status_def)
sepref_def xarena_lbd_impl [llvm_inline]
is [] ‹(RETURN o (λeli. eli >> 5))› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn›
apply (annot_unat_const ‹TYPE(32)›)
by sepref
lemmas [sepref_fr_rules] = xarena_lbd_impl.refine[FCOMP xarena_lbd_refine1]
text ‹Size›
lemma xarena_length_refine1: ‹(λeli. eli, xarena_length) ∈ [is_Size]⇩f arena_el_rel → nat_rel› by auto
sepref_def xarena_len_impl [llvm_inline] is [] ‹RETURN o (λeli. eli)› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn› by sepref
lemmas [sepref_fr_rules] = xarena_len_impl.refine[FCOMP xarena_length_refine1]
lemma ASize_refine1: ‹(λx. x,ASize) ∈ nat_rel → arena_el_rel› by auto
sepref_def ASize_impl [llvm_inline] is [] ‹RETURN o (λx. x)› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn› by sepref
lemmas [sepref_fr_rules] = ASize_impl.refine[FCOMP ASize_refine1]
text ‹Position›
lemma xarena_pos_refine1: ‹(λeli. eli, xarena_pos) ∈ [is_Pos]⇩f arena_el_rel → nat_rel› by auto
sepref_def xarena_pos_impl [llvm_inline] is [] ‹RETURN o (λeli. eli)› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn› by sepref
lemmas [sepref_fr_rules] = xarena_pos_impl.refine[FCOMP xarena_pos_refine1]
lemma APos_refine1: ‹(λx. x,APos) ∈ nat_rel → arena_el_rel› by auto
sepref_def APos_impl [llvm_inline] is [] ‹RETURN o (λx. x)› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn› by sepref
lemmas [sepref_fr_rules] = APos_impl.refine[FCOMP APos_refine1]
text ‹Status›
definition ‹status_impl_rel ≡ unat_rel' TYPE(32) O status_rel›
lemmas [fcomp_norm_unfold] = status_impl_rel_def[symmetric]
abbreviation ‹status_impl_assn ≡ pure status_impl_rel›
lemma xarena_status_refine1: ‹(λeli. eli AND 0b11, xarena_status) ∈ [is_Status]⇩f arena_el_rel → status_rel› by (auto simp: is_Status_def)
sepref_def xarena_status_impl [llvm_inline] is [] ‹RETURN o (λeli. eli AND 0b11)› :: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn›
apply (annot_unat_const ‹TYPE(32)›)
by sepref
lemmas [sepref_fr_rules] = xarena_status_impl.refine[FCOMP xarena_status_refine1]
lemma xarena_used_refine1: ‹(λeli. (eli AND 0b1100) >> 2, xarena_used) ∈ [is_Status]⇩f arena_el_rel → nat_rel›
by (auto simp: is_Status_def status_rel_def bitfield_rel_def)
lemma is_down'_32_2[simp]: ‹is_down' UCAST(32 → 2)›
by (auto simp: is_down')
lemma bitAND_mod: ‹L AND (2^n - 1) = L mod (2^n)› for L :: nat
apply transfer
apply (subst int_int_eq[symmetric])
apply (subst and_nat_def)
using AND_mod[of ‹int _›]
apply (auto simp: zmod_int bitval_bin_last[symmetric])
done
lemma nat_ex_numeral: ‹∃m. n=0 ∨ n = numeral m› for n :: nat
apply (induction n)
apply auto
using llvm_num_const_simps(67) apply blast
using pred_numeral_inc by blast
lemma xarena_used_implI: ‹x AND 12 >> 2 < max_unat 2› for x :: nat
using nat_ex_numeral[of x]
by (auto simp: nat_shiftr_div nat_shifl_div numeral_eq_Suc Suc_numeral max_unat_def
less_mult_imp_div_less
simp flip: numeral_eq_Suc)
sepref_def xarena_used_impl [llvm_inline] is [] ‹RETURN o (λeli.(eli AND 0b1100) >> 2)› :: ‹uint32_nat_assn⇧k →⇩a unat_assn' TYPE(2)›
supply [simp] = xarena_used_implI
apply (annot_unat_const ‹TYPE(32)›)
apply (rewrite at ‹RETURN o (λ_. ⌑)› annot_unat_unat_downcast[where 'l=2])
by sepref
sepref_register ‹(=) :: clause_status ⇒ clause_status ⇒ _›
lemmas [sepref_fr_rules] = xarena_used_impl.refine[FCOMP xarena_used_refine1]
lemma status_eq_refine1: ‹((=),(=)) ∈ status_rel → status_rel → bool_rel›
by (auto simp: status_rel_def)
sepref_def status_eq_impl [llvm_inline] is [] ‹uncurry (RETURN oo (=))›
:: ‹(unat_assn' TYPE(32))⇧k *⇩a (unat_assn' TYPE(32))⇧k →⇩a bool1_assn›
by sepref
lemmas [sepref_fr_rules] = status_eq_impl.refine[FCOMP status_eq_refine1]
sepref_register neq : ‹(op_neq :: clause_status ⇒ _ ⇒ _)›
lemma status_neq_refine1: ‹((≠),op_neq) ∈ status_rel → status_rel → bool_rel›
by (auto simp: status_rel_def)
definition ‹AStatus_impl1 cs used lbd ≡
(cs AND unat_const TYPE(32) 0b11) + (used << 2) + (lbd << unat_const TYPE(32) 5)›
lemma bang_eq_int:
fixes x :: "int"
shows "(x = y) = (∀n. x !! n = y !! n)"
using bin_eqI by auto
lemma bang_eq_nat:
fixes x :: "nat"
shows "(x = y) = (∀n. x !! n = y !! n)"
unfolding int_int_eq[symmetric] bang_eq_int
by (simp add: bit_of_nat_iff_bit)
lemma sum_bitAND_shift_pow2:
‹(a + (b << (n + m))) AND (2^n - 1) = a AND (2^n - 1)› for a b n :: nat
unfolding bitAND_mod
apply (auto simp: nat_shiftr_div)
by (metis mod_mult_self2 power_add semiring_normalization_rules(19))
lemma and_bang_nat: ‹(x AND y) !! n = (x !! n ∧ y !! n)› for x y n :: nat
unfolding and_nat_def
by (metis and_nat_def bit_and_iff)
lemma AND_12_AND_15_AND_12: ‹a AND 12 = (a AND 15) AND 12› for a :: nat
proof -
have [simp]: ‹(12::nat) !! n ⟹ (15::nat) !! n› for n :: nat
by (auto simp: nat_set_bit_test_bit bin_nth_numeral_unfold
nat_bin_nth_bl' nth_Cons split: nat.splits)
show ?thesis
by (subst bang_eq_nat, (subst and_bang_nat)+)
(auto simp: and_bang_nat)
qed
lemma AStatus_shift_safe:
‹c ≥ 2 ⟹ x42 + (x43 << c) AND 3 = x42 AND 3›
‹(x53 << 2) AND 3 = 0›
‹x42 + (x43 << 4) AND 12 = x42 AND 12›
‹x42 + (x43 << 5) AND 12 = x42 AND 12›
‹Suc (x42 + (x43 << 5)) AND 12 = (Suc x42) AND 12›
‹Suc ((x42) + (x43 << 5)) AND 3 = Suc x42 AND 3›
‹Suc (x42 << 2) AND 3 = Suc 0›
‹x42 ≤ 3 ⟹ Suc ((x42 << 2) + (x43 << 5)) >> 5 = x43›
for x42 x43 x53 :: nat
proof -
show ‹c ≥ 2 ⟹ x42 + (x43 << c) AND 3 = x42 AND 3›
using sum_bitAND_shift_pow2[of x42 x43 2 ‹c - 2›]
by auto
show ‹(x53 << 2) AND 3 = 0›
using bitAND_mod[of _ 2]
by (auto simp: nat_shiftr_div)
have 15: ‹(15 :: nat) = 2 ^4 -1› by auto
show H: ‹x42 + (x43 << 4) AND 12 = x42 AND 12› for x42 x43 :: nat
apply (subst AND_12_AND_15_AND_12)
apply (subst (2) AND_12_AND_15_AND_12)
unfolding bitAND_mod 15
by (auto simp: nat_shiftr_div)
from H[of x42 ‹x43 << 1›] show ‹x42 + (x43 << 5) AND 12 = x42 AND 12›
by (auto simp: nat_shiftr_div ac_simps)
from H[of ‹Suc x42› ‹x43 << 1›] show ‹Suc (x42 + (x43 << 5)) AND 12 = (Suc x42) AND 12›
by (auto simp: nat_shiftr_div ac_simps)
have [simp]: ‹(a + x53 * 32) mod 4 = (a mod 4)› for a x53 :: nat
by (metis (no_types, lifting) add_eq_self_zero cong_exp_iff_simps(1) cong_exp_iff_simps(2)
mod_add_eq mod_eq_nat1E mod_mult_right_eq mult_0_right order_refl)
note [simp] = this[of ‹Suc a› for a, simplified]
show ‹Suc ((x42) + (x43 << 5)) AND 3 = Suc x42 AND 3›
using bitAND_mod[of _ 2]
by (auto simp: nat_shiftr_div)
show ‹Suc (x42 << 2) AND 3 = Suc 0›
using bitAND_mod[of _ 2]
by (auto simp: nat_shiftr_div mod_Suc)
show ‹x42 ≤ 3 ⟹ Suc ((x42 << 2) + (x43 << 5)) >> 5 = x43›
by (auto simp: nat_shiftr_div nat_shifl_div)
qed
lemma less_unat_AND_shift: ‹x42 < 2^n ⟹ x42 >> n = 0› for x42 :: nat
by (auto simp: nat_shifl_div)
lemma [simp]: ‹(a + (w << n)) >> n = (a >> n) + w› ‹((w << n)) >> n = w›
‹n ≤ m ⟹ ((w << n)) >> m = w >> (m - n)›
‹n ≥ m ⟹ ((w << n)) >> m = w << (n - m)› for w n :: nat
apply (auto simp: nat_shiftr_div nat_shifl_div)
apply (metis div_mult2_eq le_add_diff_inverse nonzero_mult_div_cancel_right power_add power_eq_0_iff
zero_neq_numeral)
by (smt Groups.mult_ac(2) le_add_diff_inverse nonzero_mult_div_cancel_right power_add power_eq_0_iff semiring_normalization_rules(19) zero_neq_numeral)
lemma less_numeral_pred:
‹a ≤ numeral b ⟷ a = numeral b ∨ a ≤ pred_numeral b› for a :: nat
by (auto simp: numeral_eq_Suc)
lemma nat_shiftl_numeral [simp]:
"(numeral w :: nat) << numeral w' = numeral (num.Bit0 w) << pred_numeral w'"
by (metis mult_2 nat_shiftr_div numeral_Bit0 numeral_eq_Suc power.simps(2)
semiring_normalization_rules(18) semiring_normalization_rules(7))
lemma nat_shiftl_numeral' [simp]:
"(numeral w :: nat) << 1 = numeral (num.Bit0 w)"
"(1 :: nat) << n = 2 ^ n"
using nat_shiftl_numeral[of w num.One, unfolded numeral.numeral_One]
by (auto simp: nat_shiftr_div)
lemma shiftr_nat_alt_def: ‹(a :: nat) >> b = nat (int a >> b)›
apply (induction b)
apply (auto simp: nat_shiftr)
by (smt (z3) div_div_p2_eq_div_p2s(2) int_nat_eq nat_2 nat_int.Rep_inverse' nat_shifl_div numeral_2_eq_2 semiring_1_class.of_nat_power shiftr_int_def zdiv_int)
lemma nat_shiftr_numeral [simp]:
"(1 :: nat) >> numeral w' = 0"
"(numeral num.One :: nat) >> numeral w' = 0"
"(numeral (num.Bit0 w) :: nat) >> numeral w' = numeral w >> pred_numeral w'"
"(numeral (num.Bit1 w) :: nat) >> numeral w' = numeral w >> pred_numeral w'"
unfolding shiftr_nat_alt_def
by (auto simp: shiftr_def)
lemma nat_shiftr_numeral_Suc0 [simp]:
"(1 :: nat) >> Suc 0 = 0"
"(numeral num.One :: nat) >> Suc 0 = 0"
"(numeral (num.Bit0 w) :: nat) >> Suc 0 = numeral w"
"(numeral (num.Bit1 w) :: nat) >> Suc 0 = numeral w"
unfolding shiftr_nat_alt_def
by auto
lemma nat_shiftr_numeral1 [simp]:
"(1 :: nat) >> 1 = 0"
"(numeral num.One :: nat) >> 1 = 0"
"(numeral (num.Bit0 w) :: nat) >> 1 = numeral w"
"(numeral (num.Bit1 w) :: nat) >> 1 = numeral w"
unfolding shiftr_nat_alt_def
by auto
lemma nat_numeral_and_one: ‹(1 :: nat) AND 1 = 1›
by simp
lemma AStatus_refine1: ‹(AStatus_impl1, AStatus) ∈ status_rel → br id (λn. n ≤ 3) → nat_rel → arena_el_rel›
apply (auto simp: status_rel_def bitfield_rel_def AStatus_impl1_def AStatus_shift_safe br_def
less_unat_AND_shift
split: if_splits)
apply (auto simp: less_numeral_pred le_Suc_eq nat_and_numerals nat_numeral_and_one;
auto simp flip: One_nat_def)+
done
lemma AStatus_implI:
assumes ‹b << 5 < max_unat 32›
shows ‹b << 5 < max_unat 32 - 7› ‹(a AND 3) + 4 + (b << 5) < max_unat 32›
‹(a AND 3) + (b << 5) < max_unat 32›
proof -
show ‹b << 5 < max_unat 32 - 7›
using assms
by (auto simp: max_unat_def nat_shiftr_div)
have ‹(a AND 3) + 4 + (b << 5) ≤ 7 + (b << 5)›
using AND_upper_nat2[of 3 a]
by auto
also have ‹7 + (b << 5) < max_unat 32›
using ‹b << 5 < max_unat 32 - 7› by auto
finally show ‹(a AND 3) + 4 + (b << 5) < max_unat 32› .
then show ‹(a AND 3) + (b << 5) < max_unat 32›
by auto
qed
lemma nat_shiftr_mono: ‹a < b ⟹ a << n < b << n› for a b :: nat
by (simp add: nat_shiftr_div)
lemma AStatus_implI3:
assumes ‹(ac :: 2 word, ba) ∈ unat_rel›
shows ‹(a AND (3::nat)) + (ba << (2::nat)) < max_unat (32::nat)› and
‹b << 5 < max_unat 32 ⟹ (a AND 3) + (ba << 2) + (b << 5) < max_unat 32›
proof -
have ‹ba < 4›
using assms unat_lt_max_unat[of ac] by (auto simp: unat_rel_def unat.rel_def br_def
max_unat_def)
from nat_shiftr_mono[OF this, of 2] have ‹ba << 2 < 16› by auto
moreover have ‹(a AND (3::nat)) ≤ 3›
using AND_upper_nat2[of a 3] by auto
ultimately have ‹(a AND (3::nat)) + (ba << (2::nat)) < 19›
by linarith
also have ‹19 ≤ max_unat 32›
by (auto simp: max_unat_def)
finally show ‹(a AND (3::nat)) + (ba << (2::nat)) < max_unat (32::nat)› .
show ‹(a AND 3) + (ba << 2) + (b << 5) < max_unat 32› if ‹b << 5 < max_unat 32›
proof -
have ‹b << 5 < max_unat 32 - 19›
using that
by (auto simp: max_unat_def nat_shiftr_div)
then show ?thesis
using ‹(a AND (3::nat)) + (ba << (2::nat)) < 19› by linarith
qed
qed
lemma AStatus_implI2: ‹(ac :: 2 word, ba) ∈ unat_rel ⟹ ba << (2::nat) < max_unat (32::nat)›
using order.strict_trans2[OF unat_lt_max_unat[of ac], of ‹max_unat 28›]
by (auto simp: unat_rel_def unat.rel_def br_def max_unat_def nat_shiftr_div
intro!: )
lemma is_up_2_32[simp]: ‹is_up' UCAST(2 → 32)›
by (simp add: is_up')
sepref_def AStatus_impl [llvm_inline]
is [] ‹uncurry2 (RETURN ooo AStatus_impl1)›
:: ‹[λ((a,b), c). c << 5 < max_unat 32]⇩a
uint32_nat_assn⇧k *⇩a (unat_assn' TYPE(2))⇧k *⇩a uint32_nat_assn⇧k → uint32_nat_assn›
unfolding AStatus_impl1_def
supply [split] = if_splits and [intro] = AStatus_implI AStatus_implI2 AStatus_implI3
apply (rewrite in ‹⌑ << 2› annot_unat_unat_upcast[where 'l=‹32›])
apply (annot_unat_const ‹TYPE(32)›)
by sepref
lemma Collect_eq_simps3: ‹P O {(c, a). a = c ∧ Q c} = {(a, b). (a, b) ∈ P ∧ Q b}›
‹P O {(c, a). c = a ∧ Q c} = {(a, b). (a, b) ∈ P ∧ Q b}›
by auto
lemma unat_rel_2_br: ‹(((unat_rel :: (2 word × _) set) O br id (λn. n ≤ 3))) = ((unat_rel))›
apply (auto simp add: unat_rel_def unat.rel_def br_def Collect_eq_simps3 max_unat_def)
subgoal for a
using unat_lt_max_unat[of ‹a :: 2 word›] by (auto simp: max_unat_def)
done
lemmas [sepref_fr_rules] = AStatus_impl.refine[FCOMP AStatus_refine1, unfolded unat_rel_2_br]
subsubsection ‹Arena Operations›
paragraph ‹Length›
abbreviation ‹arena_fast_assn ≡ al_assn' TYPE(64) arena_el_impl_assn›
lemma arena_lengthI:
assumes ‹arena_is_valid_clause_idx a b›
shows ‹Suc 0 ≤ b›
and ‹b < length a›
and ‹is_Size (a ! (b - Suc 0))›
using SIZE_SHIFT_def assms
by (auto simp: arena_is_valid_clause_idx_def arena_lifting)
lemma arena_length_alt:
‹arena_length arena i = (
let l = xarena_length (arena!(i - snat_const TYPE(64) 1))
in snat_const TYPE(64) 2 + op_unat_snat_upcast TYPE(64) l)›
by (simp add: arena_length_def SIZE_SHIFT_def)
sepref_register arena_length
sepref_def arena_length_impl
is ‹uncurry (RETURN oo arena_length)›
:: ‹[uncurry arena_is_valid_clause_idx]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → snat_assn' TYPE(64)›
unfolding arena_length_alt
supply [dest] = arena_lengthI
by sepref
paragraph ‹Literal at given position›
lemma arena_lit_implI:
assumes ‹arena_lit_pre a b›
shows ‹b < length a› ‹is_Lit (a ! b)›
using assms unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by (fastforce dest: arena_lifting)+
sepref_register arena_lit xarena_lit
sepref_def arena_lit_impl
is ‹uncurry (RETURN oo arena_lit)›
:: ‹[uncurry arena_lit_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → unat_lit_assn›
supply [intro] = arena_lit_implI
unfolding arena_lit_def
by sepref
sepref_register mop_arena_lit mop_arena_lit2
sepref_def mop_arena_lit_impl
is ‹uncurry (mop_arena_lit)›
:: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a unat_lit_assn›
supply [intro] = arena_lit_implI
unfolding mop_arena_lit_def
by sepref
sepref_def mop_arena_lit2_impl
is ‹uncurry2 (mop_arena_lit2)›
:: ‹[λ((N, _), _). length N ≤ snat64_max]⇩a
arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k → unat_lit_assn›
supply [intro] = arena_lit_implI
supply [dest] = arena_lit_pre_le_lengthD
unfolding mop_arena_lit2_def
by sepref
paragraph ‹Status of the clause›
lemma arena_status_implI:
assumes ‹arena_is_valid_clause_vdom a b›
shows ‹2 ≤ b› ‹b - 2 < length a› ‹is_Status (a ! (b-2))›
using assms STATUS_SHIFT_def arena_dom_status_iff
unfolding arena_is_valid_clause_vdom_def
by (auto dest: valid_arena_in_vdom_le_arena arena_lifting)
sepref_register arena_status xarena_status
sepref_def arena_status_impl
is ‹uncurry (RETURN oo arena_status)›
:: ‹[uncurry arena_is_valid_clause_vdom]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → status_impl_assn›
supply [intro] = arena_status_implI
unfolding arena_status_def STATUS_SHIFT_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
paragraph ‹Swap literals›
sepref_register swap_lits
sepref_def swap_lits_impl is ‹uncurry3 (RETURN oooo swap_lits)›
:: ‹[λ(((C,i),j),arena). C + i < length arena ∧ C + j < length arena]⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn›
unfolding swap_lits_def convert_swap
unfolding gen_swap
by sepref
paragraph ‹Get LBD›
lemma get_clause_LBD_pre_implI:
assumes ‹get_clause_LBD_pre a b›
shows ‹2 ≤ b› ‹b - 2 < length a› ‹is_Status (a ! (b-2))›
using assms arena_dom_status_iff
unfolding arena_is_valid_clause_vdom_def get_clause_LBD_pre_def
apply (auto dest: valid_arena_in_vdom_le_arena simp: arena_lifting arena_is_valid_clause_idx_def)
using STATUS_SHIFT_def arena_lifting apply auto
by (meson less_imp_diff_less)
sepref_register arena_lbd mop_arena_lbd
sepref_def arena_lbd_impl
is ‹uncurry (RETURN oo arena_lbd)›
:: ‹[uncurry get_clause_LBD_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →uint32_nat_assn›
unfolding arena_lbd_def LBD_SHIFT_def
supply [dest] = get_clause_LBD_pre_implI
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def mop_arena_lbd_impl
is ‹uncurry mop_arena_lbd›
:: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a uint32_nat_assn›
unfolding mop_arena_lbd_def
by sepref
paragraph ‹used flag›
sepref_register arena_used
sepref_def arena_used_impl
is ‹uncurry (RETURN oo arena_used)›
:: ‹[uncurry get_clause_LBD_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → unat_assn' TYPE(2)›
unfolding arena_used_def LBD_SHIFT_def
supply [dest] = get_clause_LBD_pre_implI
apply (annot_snat_const ‹TYPE(64)›)
by sepref
paragraph ‹Get Saved Position›
lemma arena_posI:
assumes ‹get_saved_pos_pre a b›
shows ‹3 ≤ b›
and ‹b < length a›
and ‹is_Pos (a ! (b - 3))›
using POS_SHIFT_def assms is_short_clause_def[of ‹_ ∝ b›]
apply (auto simp: get_saved_pos_pre_def arena_is_valid_clause_idx_def arena_lifting
MAX_LENGTH_SHORT_CLAUSE_def[symmetric] arena_lifting(11) arena_lifting(4)
simp del: MAX_LENGTH_SHORT_CLAUSE_def)
using arena_lifting(1) arena_lifting(4) header_size_def by fastforce
lemma arena_pos_alt:
‹arena_pos arena i = (
let l = xarena_pos (arena!(i - snat_const TYPE(64) 3))
in snat_const TYPE(64) 2 + op_unat_snat_upcast TYPE(64) l)›
by (simp add: arena_pos_def POS_SHIFT_def)
sepref_register arena_pos
sepref_def arena_pos_impl
is ‹uncurry (RETURN oo arena_pos)›
:: ‹[uncurry get_saved_pos_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → snat_assn' TYPE(64)›
unfolding arena_pos_alt
supply [dest] = arena_posI
by sepref
paragraph ‹Update LBD›
lemma update_lbdI:
assumes ‹update_lbd_pre ((b, lbd), a)›
shows ‹2 ≤ b›
and ‹b -2 < length a›
and ‹arena_is_valid_clause_vdom a b›
and ‹get_clause_LBD_pre a b›
using LBD_SHIFT_def assms
apply (auto simp: arena_is_valid_clause_idx_def arena_lifting update_lbd_pre_def
arena_is_valid_clause_vdom_def get_clause_LBD_pre_def
dest: arena_lifting(10))
by (simp add: less_imp_diff_less valid_arena_def)
lemma shorten_lbd_le: ‹shorten_lbd baa << 5 < max_unat 32›
proof -
have ‹shorten_lbd baa << 5 ≤ 67108863 << 5›
using AND_upper_nat2[of baa 67108863]
by (auto simp: nat_shiftr_div shorten_lbd_def)
also have ‹67108863 << 5 < max_unat 32›
by (auto simp: max_unat_def nat_shiftr_div)
finally show ?thesis .
qed
sepref_register update_lbd AStatus shorten_lbd
sepref_def shorten_lbd_impl
is ‹RETURN o shorten_lbd›
:: ‹uint32_nat_assn⇧k →⇩a uint32_nat_assn›
unfolding shorten_lbd_def
apply (annot_unat_const ‹TYPE(32)›)
by sepref
sepref_def update_lbd_impl
is ‹uncurry2 (RETURN ooo update_lbd)›
:: ‹[update_lbd_pre]⇩a sint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn›
unfolding update_lbd_def LBD_SHIFT_def
supply [simp] = update_lbdI shorten_lbd_le
and [dest] = arena_posI
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def mop_arena_update_lbd_impl
is ‹uncurry2 mop_arena_update_lbd›
:: ‹sint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k *⇩a arena_fast_assn⇧d →⇩a arena_fast_assn›
unfolding mop_arena_update_lbd_def
by sepref
paragraph ‹Update Saved Position›
lemma update_posI:
assumes ‹isa_update_pos_pre ((b, pos), a)›
shows ‹3 ≤ b› ‹2 ≤ pos› ‹b-3 < length a›
using assms POS_SHIFT_def
unfolding isa_update_pos_pre_def
apply (auto simp: arena_is_valid_clause_idx_def arena_lifting)
apply (metis (full_types) MAX_LENGTH_SHORT_CLAUSE_def arena_is_valid_clause_idx_def arena_posI(1) get_saved_pos_pre_def)
by (simp add: less_imp_diff_less valid_arena_def)
lemma update_posI2:
assumes ‹isa_update_pos_pre ((b, pos), a)›
assumes ‹rdomp (al_assn arena_el_impl_assn :: _ ⇒ arena_assn ⇒ assn) a›
shows ‹pos - 2 < max_unat 32›
proof -
obtain N vdom where
‹valid_arena a N vdom› and
‹b ∈# dom_m N›
using assms(1) unfolding isa_update_pos_pre_def arena_is_valid_clause_idx_def
by auto
then have eq: ‹length (N ∝ b) = arena_length a b› and
le: ‹b < length a› and
size: ‹is_Size (a ! (b - SIZE_SHIFT))›
by (auto simp: arena_lifting)
have ‹i<length a ⟹ rdomp arena_el_impl_assn (a ! i)› for i
using rdomp_al_dest'[OF assms(2)]
by auto
from this[of ‹b - SIZE_SHIFT›] have ‹rdomp arena_el_impl_assn (a ! (b - SIZE_SHIFT))›
using le by auto
then have ‹length (N ∝ b) ≤ unat32_max + 2›
using size eq unfolding rdomp_pure
apply (auto simp: rdomp_def arena_el_impl_rel_def is_Size_def
comp_def pure_def unat_rel_def unat.rel_def br_def
arena_length_def unat32_max_def)
subgoal for x
using unat_lt_max_unat[of x]
apply (auto simp: max_unat_def)
done
done
then show ?thesis
using assms POS_SHIFT_def
unfolding isa_update_pos_pre_def
by (auto simp: arena_is_valid_clause_idx_def arena_lifting eq
unat32_max_def max_unat_def)
qed
sepref_register arena_update_pos
sepref_def update_pos_impl
is ‹uncurry2 (RETURN ooo arena_update_pos)›
:: ‹[isa_update_pos_pre]⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn›
unfolding arena_update_pos_def POS_SHIFT_def
apply (annot_snat_const ‹TYPE(64)›)
apply (rewrite at ‹APos ⌑› annot_snat_unat_downcast[where 'l=32])
supply [simp] = update_posI and [dest] = update_posI2
by sepref
sepref_register IRRED LEARNED DELETED
lemma IRRED_impl[sepref_import_param]: ‹(0,IRRED) ∈ status_impl_rel›
unfolding status_impl_rel_def status_rel_def unat_rel_def unat.rel_def
by (auto simp: in_br_conv)
lemma LEARNED_impl[sepref_import_param]: ‹(1,LEARNED) ∈ status_impl_rel›
unfolding status_impl_rel_def status_rel_def unat_rel_def unat.rel_def
by (auto simp: in_br_conv)
lemma DELETED_impl[sepref_import_param]: ‹(3,DELETED) ∈ status_impl_rel›
unfolding status_impl_rel_def status_rel_def unat_rel_def unat.rel_def
by (auto simp: in_br_conv)
lemma mark_garbageI:
assumes ‹mark_garbage_pre (a, b)›
shows ‹2 ≤ b› ‹b-2 < length a›
using assms STATUS_SHIFT_def
unfolding mark_garbage_pre_def
apply (auto simp: arena_is_valid_clause_idx_def arena_lifting)
by (simp add: less_imp_diff_less valid_arena_def)
extra_information_mark_to_delete
sepref_def mark_garbage_impl is ‹uncurry (RETURN oo extra_information_mark_to_delete)›
:: ‹[mark_garbage_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn›
unfolding extra_information_mark_to_delete_def STATUS_SHIFT_def
apply (rewrite at ‹AStatus _ _ ⌑› annot_snat_unat_downcast[where 'l=32])
apply (rewrite at ‹AStatus _ ⌑› unat_const_fold[where 'a=2])
apply (annot_snat_const ‹TYPE(64)›)
supply [simp] = mark_garbageI
by sepref
lemma bit_shiftr_shiftl_same_le:
‹a << b >> b ≤ a› for a b c :: nat
unfolding nat_int_comparison
by (auto simp: nat_shiftr_div nat_shifl_div)
lemma bit_shiftl_shiftr_same_le:
‹a >> b << b ≤ a› for a b c :: nat
by (auto simp: nat_shiftr_div nat_shifl_div)
lemma valid_arena_arena_lbd_shift_le:
assumes
‹rdomp (al_assn arena_el_impl_assn) a› and
‹b ∈# dom_m N› and
‹valid_arena a N vdom›
shows ‹arena_lbd a b << 5 < max_unat 32›
proof -
have ‹2 ≤ b› ‹b - 2 < length a› and st: ‹is_Status (a ! (b-2))›
using assms LBD_SHIFT_def by (auto simp: arena_is_valid_clause_idx_def
less_imp_diff_less arena_lifting)
then have H: ‹rdomp arena_el_impl_assn (a ! (b - 2))›
using rdomp_al_dest'[of arena_el_impl_assn a] assms
by auto
then obtain x :: ‹32 word› and x51 :: ‹clause_status› and x52 where
H: ‹a ! (b - 2) = AStatus x51 x52 (unat x >> 5)›
‹(unat x AND 3, x51) ∈ status_rel›
using st bit_shiftr_shiftl_same_le[of ‹arena_lbd a b› 4]
by (auto simp: arena_el_impl_rel_def unat_rel_def unat.rel_def
br_def arena_lbd_def LBD_SHIFT_def)
show ?thesis
apply (rule order.strict_trans1[of _ ‹unat x›])
using bit_shiftl_shiftr_same_le[of ‹unat x› 5] unat_lt_max_unat[of ‹x›] H
by (auto simp: arena_el_impl_rel_def unat_rel_def unat.rel_def
br_def arena_lbd_def LBD_SHIFT_def)
qed
lemma arena_mark_used_implI:
assumes ‹arena_act_pre a b›
shows ‹2 ≤ b› ‹b - 2 < length a› ‹is_Status (a ! (b-2))›
‹arena_is_valid_clause_vdom a b›
‹get_clause_LBD_pre a b›
‹rdomp (al_assn arena_el_impl_assn) a ⟹ arena_lbd a b << 5 < max_unat 32›
using assms STATUS_SHIFT_def valid_arena_arena_lbd_shift_le[of a b]
apply (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def arena_lifting)
subgoal by (simp add: less_imp_diff_less valid_arena_def)
subgoal for N vdom by (auto simp: arena_is_valid_clause_vdom_def arena_lifting)
subgoal for N vdom by (auto simp: arena_is_valid_clause_vdom_def arena_lifting
get_clause_LBD_pre_def arena_is_valid_clause_idx_def)
done
lemma mark_used_alt_def:
‹RETURN oo mark_used =
(λarena i. do {
lbd ← RETURN (arena_lbd arena i); let status = arena_status arena i;
RETURN (arena[i - STATUS_SHIFT := AStatus status (arena_used arena i OR 1) lbd])})›
by (auto simp: mark_used_def Let_def intro!: ext)
sepref_register mark_used mark_used2
sepref_def mark_used_impl is ‹uncurry (RETURN oo mark_used)›
:: ‹[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn›
unfolding mark_used_def STATUS_SHIFT_def mark_used_alt_def
supply [intro] = arena_mark_used_implI
apply (rewrite at ‹_ OR ⌑› unat_const_fold[where 'a=2])
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def mark_used2_impl is ‹uncurry (RETURN oo mark_used2)›
:: ‹[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn›
unfolding mark_used2_def STATUS_SHIFT_def mark_used_alt_def
supply [intro] = arena_mark_used_implI
apply (rewrite at ‹_ OR ⌑› unat_const_fold[where 'a=2])
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register mark_unused
sepref_def mark_unused_impl is ‹uncurry (RETURN oo mark_unused)›
:: ‹[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn›
unfolding mark_unused_def STATUS_SHIFT_def
supply [intro] = arena_mark_used_implI
apply (rewrite at ‹_ - ⌑› snat_const_fold[where 'a=64])
apply (rewrite at ‹_ - ⌑› snat_const_fold[where 'a=64])
apply (annot_unat_const ‹TYPE(2)›)
by sepref
sepref_def mop_arena_mark_used_impl
is ‹uncurry mop_arena_mark_used›
:: ‹arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k →⇩a arena_fast_assn›
unfolding mop_arena_mark_used_def
by sepref
sepref_def mop_arena_mark_used2_impl
is ‹uncurry mop_arena_mark_used2›
:: ‹arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k →⇩a arena_fast_assn›
unfolding mop_arena_mark_used2_def
by sepref
paragraph ‹Marked as used?›
lemma arena_marked_as_used_implI:
assumes ‹marked_as_used_pre a b›
shows ‹2 ≤ b› ‹b - 2 < length a› ‹is_Status (a ! (b-2))›
using assms STATUS_SHIFT_def
apply (auto simp: marked_as_used_pre_def arena_is_valid_clause_idx_def arena_lifting)
subgoal using arena_lifting(2) less_imp_diff_less by blast
done
sepref_register marked_as_used
sepref_def marked_as_used_impl
is ‹uncurry (RETURN oo marked_as_used)›
:: ‹[uncurry marked_as_used_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → unat_assn' TYPE(2)›
supply [intro] = arena_marked_as_used_implI
unfolding marked_as_used_def STATUS_SHIFT_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register MAX_LENGTH_SHORT_CLAUSE mop_arena_status
sepref_def MAX_LENGTH_SHORT_CLAUSE_impl is ‹uncurry0 (RETURN MAX_LENGTH_SHORT_CLAUSE)› :: ‹unit_assn⇧k →⇩a sint64_nat_assn›
unfolding MAX_LENGTH_SHORT_CLAUSE_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition arena_other_watched_as_swap :: ‹nat list ⇒ nat ⇒ nat ⇒ nat ⇒ nat nres› where
‹arena_other_watched_as_swap S L C i = do {
ASSERT(i < 2 ∧
C + i < length S ∧
C < length S ∧
(C + 1) < length S);
K ← RETURN (S ! C);
K' ← RETURN (S ! (1 + C));
RETURN (L XOR K XOR K')
}›
lemma arena_other_watched_as_swap_arena_other_watched:
assumes
N: ‹(N, N') ∈ ⟨arena_el_rel⟩list_rel› and
L: ‹(L, L') ∈ nat_lit_rel› and
C: ‹(C, C') ∈ nat_rel› and
i: ‹(i, i') ∈ nat_rel›
shows
‹arena_other_watched_as_swap N L C i ≤ ⇓nat_lit_rel
(arena_other_watched N' L' C' i')›
proof -
have eq: ‹i =i'› ‹C=C'›
using assms by auto
have A: ‹Pos (L div 2) = A ⟹ even L ⟹ L = 2 * atm_of A› for A :: ‹nat literal›
by (cases A)
auto
have Ci: ‹(C' + i', C' + i') ∈ nat_rel›
unfolding eq by auto
have [simp]: ‹L = N ! (C+i)› if ‹L' = arena_lit N' (C' + i')› ‹C' + i' < length N'›
‹arena_lit_pre2 N' C i›
using that param_nth[OF that(2) Ci N] C i L
unfolding arena_lit_pre2_def
apply - apply normalize_goal+
subgoal for N'' vdom
using arena_lifting(6)[of N' N'' vdom C i] A[of ‹arena_lit N' (C' + i')›]
apply (simp only: list_rel_imp_same_length[of N] eq)
apply (cases ‹N' ! (C' + i')›; cases ‹arena_lit N' (C' + i')›)
apply (simp_all add: eq nat_lit_rel_def br_def)
apply (auto split: if_splits simp: eq_commute[of _ ‹Pos (L div 2)›]
eq_commute[of _ ‹ALit (Pos (_ div 2))›] arena_lit_def)
using div2_even_ext_nat by blast
done
have [simp]: ‹N ! (C' + i') XOR N ! C' XOR N ! Suc C' = N ! (C' + (Suc 0 - i))› if ‹i < 2›
using that i
by (cases i; cases ‹i-1›)
(auto simp: bin_pos_same_XOR3_nat)
have Ci': ‹(C' + (1 - i'), C' + (1 - i')) ∈ nat_rel›
unfolding eq by auto
have [intro!]: ‹(N ! (Suc C' - i'), arena_lit N' (Suc C' - i')) ∈ nat_lit_rel›
if ‹arena_lit_pre2 N' C i› ‹i < 2›
using that param_nth[OF _ Ci' N]
unfolding arena_lit_pre2_def
apply - apply normalize_goal+
apply (subgoal_tac ‹C' + (Suc 0 - i') < length N'›)
defer
subgoal for N'' vdom
using
arena_lifting(7)[of N' N'' vdom C i]
arena_lifting(7)[of N' N'' vdom C ‹Suc 0 - i›]
arena_lifting(21,4)[of N' N'' vdom C]
by (cases i')
(auto simp: arena_lit_pre2_def list_rel_imp_same_length[of N] eq
simp del: arena_el_rel_def)
apply (subgoal_tac ‹(Suc 0 - i') < length (x ∝ C)›)
defer
subgoal for N'' vdom
using
arena_lifting(7)[of N' N'' vdom C i]
arena_lifting(7)[of N' N'' vdom C ‹Suc 0 - i›]
arena_lifting(21,4)[of N' N'' vdom C]
by (cases i')
(auto simp: arena_lit_pre2_def list_rel_imp_same_length[of N] eq
simp del: arena_el_rel_def)
subgoal for N'' vdom
using
arena_lifting(6)[of N' N'' vdom C ‹Suc 0 - i›]
by (cases ‹N' ! (C' + (Suc 0 - i'))›)
(auto simp: arena_lit_pre2_def list_rel_imp_same_length[of N] eq
arena_lit_def arena_lifting)
done
show ?thesis
using assms
unfolding arena_other_watched_as_swap_def arena_other_watched_def
le_ASSERT_iff mop_arena_lit2_def
apply (refine_vcg)
apply (auto simp: le_ASSERT_iff list_rel_imp_same_length arena_lit_pre2_def
arena_lifting
bin_pos_same_XOR3_nat)
apply (metis (no_types, lifting) add.comm_neutral add_Suc_right arena_lifting(21,4,7))
using arena_lifting(4) by auto
qed
sepref_def arena_other_watched_as_swap_impl
is ‹uncurry3 arena_other_watched_as_swap›
:: ‹(al_assn' (TYPE(64)) uint32_nat_assn)⇧k *⇩a uint32_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a
sint64_nat_assn⇧k →⇩a uint32_nat_assn›
supply[[goals_limit=1]]
unfolding arena_other_watched_as_swap_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma arena_other_watched_as_swap_arena_other_watched':
‹(arena_other_watched_as_swap, arena_other_watched) ∈
⟨arena_el_rel⟩list_rel → nat_lit_rel → nat_rel → nat_rel →
⟨nat_lit_rel⟩nres_rel›
apply (intro fun_relI nres_relI)
using arena_other_watched_as_swap_arena_other_watched
by blast
lemma arena_fast_al_unat_assn:
‹hr_comp (al_assn unat_assn) (⟨arena_el_rel⟩list_rel) = arena_fast_assn›
unfolding al_assn_def hr_comp_assoc
by (auto simp: arena_el_impl_rel_def list_rel_compp)
lemmas [sepref_fr_rules] =
arena_other_watched_as_swap_impl.refine[FCOMP arena_other_watched_as_swap_arena_other_watched',
unfolded arena_fast_al_unat_assn]
lemma arena_lit_pre2_le_lengthD: ‹arena_lit_pre2 arena i j ⟹ i + j < length arena›
apply (auto simp: arena_lit_pre2_def)
using arena_lifting(7) nat_le_iff_add by auto
sepref_def mop_arena_update_lit_code
is ‹uncurry3 mop_arena_update_lit›
:: ‹[λ(((_, _), _), N). length N ≤ snat64_max]⇩a
sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a unat_lit_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn›
supply [intro] = arena_lit_implI
supply [dest] = arena_lit_pre2_le_lengthD
unfolding mop_arena_update_lit_def arenap_update_lit_def
by sepref
lemma arena_shorten_preI:
assumes ‹arena_shorten_pre C j arena›
shows
‹j ≥ 2› and
‹C - Suc 0 < length arena› and
‹C ≥ Suc 0› and
‹j > MAX_LENGTH_SHORT_CLAUSE ⟹ C ≥ 3›
using assms arena_lifting[of arena _ _ C]
unfolding arena_shorten_pre_def by (auto simp: arena_is_valid_clause_idx_def SHIFTS_def
header_size_def
intro: less_imp_diff_less)
sepref_def mop_arena_shorten_code
is ‹uncurry2 mop_arena_shorten›
:: ‹sint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k *⇩a arena_fast_assn⇧d →⇩a arena_fast_assn›
supply [dest] = arena_shorten_preI
supply [dest] = arena_lit_pre2_le_lengthD
unfolding mop_arena_shorten_def arena_shorten_def SIZE_SHIFT_def POS_SHIFT_def
apply (rewrite at ‹_[_ := ASize (_ - ⌑), _ := _]› unat_const_fold[where 'a=32])
apply (rewrite at ‹_[_ := ASize (_ - ⌑)]› unat_const_fold[where 'a=32])
apply (rewrite at ‹_[_ := _, _ := APos ⌑]› unat_const_fold[where 'a=32])
apply (annot_snat_const ‹TYPE (64)›)
apply (rewrite at ‹( _ < ⌑)› annot_unat_snat_upcast[where 'l=64])
by sepref
end
sepref_def mop_arena_length_impl
is ‹uncurry mop_arena_length›
:: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a sint64_nat_assn›
unfolding mop_arena_length_def
by sepref
sepref_def mop_arena_status_impl
is ‹uncurry mop_arena_status›
:: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a status_impl_assn›
supply [[goals_limit=1]]
unfolding mop_arena_status_def
by sepref
sepref_def status_neq_impl is [] ‹uncurry (RETURN oo (≠))›
:: ‹(unat_assn' TYPE(32))⇧k *⇩a (unat_assn' TYPE(32))⇧k →⇩a bool1_assn›
by sepref
lemmas [sepref_fr_rules] = status_neq_impl.refine[FCOMP status_neq_refine1]
sepref_register mop_arena_set_status
lemma arena_is_valid_clause_idxI:
‹arena_is_valid_clause_idx arena C ⟹ get_clause_LBD_pre arena C›
‹arena_is_valid_clause_idx arena C ⟹ C ≥ 2›
‹arena_is_valid_clause_idx arena C ⟹ rdomp (al_assn arena_el_impl_assn) arena ⟹ arena_lbd arena C << 5 < max_unat 32›
‹arena_is_valid_clause_idx arena C ⟹ C - 2 < length arena›
using valid_arena_arena_lbd_shift_le[of arena C]
unfolding arena_is_valid_clause_vdom_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def
apply (auto simp: arena_lifting)
using STATUS_SHIFT_def arena_lifting(16) apply auto[1]
defer
using arena_lifting(2) less_imp_diff_less apply blast
done
sepref_def mop_arena_set_status_impl
is ‹uncurry2 mop_arena_set_status›
:: ‹arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k *⇩a status_impl_assn⇧k →⇩a arena_fast_assn›
supply [intro] = arena_is_valid_clause_idxI
unfolding mop_arena_set_status_def arena_set_status_def LBD_SHIFT_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
experiment begin
export_llvm
MAX_LENGTH_SHORT_CLAUSE_impl
mop_arena_status_impl
arena_length_impl
arena_lit_impl
arena_status_impl
swap_lits_impl
arena_lbd_impl
arena_pos_impl
update_lbd_impl
update_pos_impl
mark_garbage_impl
mark_used_impl
mark_unused_impl
marked_as_used_impl
MAX_LENGTH_SHORT_CLAUSE_impl
mop_arena_status_impl
end
end