theory IsaSAT_Lookup_Conflict_LLVM
imports
IsaSAT_Lookup_Conflict
IsaSAT_Trail_LLVM
IsaSAT_Clauses_LLVM
LBD_LLVM
begin
sepref_decl_op nat_lit_eq: ‹(=) :: nat literal ⇒ _ ⇒ _› ::
‹(Id :: (nat literal × _) set) → (Id :: (nat literal × _) set) → bool_rel› .
sepref_def nat_lit_eq_impl
is [] ‹uncurry (RETURN oo (λx y. x = y))›
:: ‹uint32_nat_assn⇧k *⇩a uint32_nat_assn⇧k →⇩a bool1_assn›
by sepref
lemma nat_lit_rel: ‹((=), op_nat_lit_eq) ∈ nat_lit_rel → nat_lit_rel → bool_rel›
by (auto simp: nat_lit_rel_def br_def split: if_splits; presburger)
sepref_register "(=) :: nat literal ⇒ _ ⇒ _"
declare nat_lit_eq_impl.refine[FCOMP nat_lit_rel, sepref_fr_rules]
sepref_register set_lookup_conflict_aa
type_synonym lookup_clause_assn = ‹32 word × (1 word) ptr›
type_synonym (in -) option_lookup_clause_assn = ‹1 word × lookup_clause_assn›
type_synonym (in -) out_learned_assn = ‹32 word array_list64›
abbreviation (in -) out_learned_assn :: ‹out_learned ⇒ out_learned_assn ⇒ assn› where
‹out_learned_assn ≡ arl64_assn unat_lit_assn›
definition minimize_status_int_rel :: ‹(nat × minimize_status) set› where
‹minimize_status_int_rel = {(0, SEEN_UNKNOWN), (1, SEEN_FAILED), (2, SEEN_REMOVABLE)}›
abbreviation minimize_status_ref_rel where
‹minimize_status_ref_rel ≡ snat_rel' TYPE(8)›
abbreviation minimize_status_ref_assn where
‹minimize_status_ref_assn ≡ pure minimize_status_ref_rel›
definition minimize_status_rel :: ‹_› where
‹minimize_status_rel = minimize_status_ref_rel O minimize_status_int_rel›
abbreviation minimize_status_assn :: ‹_› where
‹minimize_status_assn ≡ pure minimize_status_rel›
lemma minimize_status_assn_alt_def:
‹minimize_status_assn = pure (snat_rel O minimize_status_int_rel)›
unfolding minimize_status_rel_def ..
lemmas [fcomp_norm_unfold] = minimize_status_assn_alt_def[symmetric]
definition minimize_status_rel_eq :: ‹minimize_status ⇒ minimize_status ⇒ bool› where
[simp]: ‹minimize_status_rel_eq = (=)›
lemma minimize_status_rel_eq:
‹((=), minimize_status_rel_eq) ∈ minimize_status_int_rel → minimize_status_int_rel → bool_rel›
by (auto simp: minimize_status_int_rel_def)
sepref_def minimize_status_rel_eq_impl
is [] ‹uncurry (RETURN oo (=))›
:: ‹minimize_status_ref_assn⇧k *⇩a minimize_status_ref_assn⇧k →⇩a bool1_assn›
supply [[goals_limit=1]]
by sepref
sepref_register minimize_status_rel_eq
lemmas [sepref_fr_rules] = minimize_status_rel_eq_impl.refine[unfolded convert_fref, FCOMP minimize_status_rel_eq]
lemma
SEEN_FAILED_rel: ‹(1, SEEN_FAILED) ∈ minimize_status_int_rel› and
SEEN_UNKNOWN_rel: ‹(0, SEEN_UNKNOWN) ∈ minimize_status_int_rel› and
SEEN_REMOVABLE_rel: ‹(2, SEEN_REMOVABLE) ∈ minimize_status_int_rel›
by (auto simp: minimize_status_int_rel_def)
sepref_def SEEN_FAILED_impl
is [] ‹uncurry0 (RETURN 1)›
:: ‹unit_assn⇧k →⇩a minimize_status_ref_assn›
supply [[goals_limit=1]]
apply (annot_snat_const "TYPE(8)")
by sepref
sepref_def SEEN_UNKNOWN_impl
is [] ‹uncurry0 (RETURN 0)›
:: ‹unit_assn⇧k →⇩a minimize_status_ref_assn›
supply [[goals_limit=1]]
apply (annot_snat_const "TYPE(8)")
by sepref
sepref_def SEEN_REMOVABLE_impl
is [] ‹uncurry0 (RETURN 2)›
:: ‹unit_assn⇧k →⇩a minimize_status_ref_assn›
supply [[goals_limit=1]]
apply (annot_snat_const "TYPE(8)")
by sepref
lemmas [sepref_fr_rules] = SEEN_FAILED_impl.refine[FCOMP SEEN_FAILED_rel]
SEEN_UNKNOWN_impl.refine[FCOMP SEEN_UNKNOWN_rel]
SEEN_REMOVABLE_impl.refine[FCOMP SEEN_REMOVABLE_rel]
definition option_bool_impl_rel where
‹option_bool_impl_rel = bool1_rel O option_bool_rel›
abbreviation option_bool_impl_assn :: ‹_› where
‹option_bool_impl_assn ≡ pure (option_bool_impl_rel)›
lemma option_bool_impl_assn_alt_def:
‹option_bool_impl_assn = hr_comp bool1_assn option_bool_rel›
unfolding option_bool_impl_rel_def by (simp add: hr_comp_pure)
lemmas [fcomp_norm_unfold] = option_bool_impl_assn_alt_def[symmetric]
option_bool_impl_rel_def[symmetric]
lemma Some_rel: ‹(λ_. True, ISIN) ∈ bool_rel → option_bool_rel›
by (auto simp: option_bool_rel_def)
sepref_def Some_impl
is [] ‹RETURN o (λ_. True)›
:: ‹bool1_assn⇧k →⇩a bool1_assn›
by sepref
lemmas [sepref_fr_rules] = Some_impl.refine[FCOMP Some_rel]
lemma is_Notin_rel: ‹(λx. ¬x, is_NOTIN) ∈ option_bool_rel → bool_rel›
by (auto simp: option_bool_rel_def)
sepref_def is_Notin_impl
is [] ‹RETURN o (λx. ¬x)›
:: ‹bool1_assn⇧k →⇩a bool1_assn›
by sepref
lemmas [sepref_fr_rules] = is_Notin_impl.refine[FCOMP is_Notin_rel]
lemma NOTIN_rel: ‹(False, NOTIN) ∈ option_bool_rel›
by (auto simp: option_bool_rel_def)
sepref_def NOTIN_impl
is [] ‹uncurry0 (RETURN False)›
:: ‹unit_assn⇧k →⇩a bool1_assn›
by sepref
lemmas [sepref_fr_rules] = NOTIN_impl.refine[FCOMP NOTIN_rel]
definition (in -) lookup_clause_rel_assn
:: ‹lookup_clause_rel ⇒ lookup_clause_assn ⇒ assn›
where
‹lookup_clause_rel_assn ≡ (uint32_nat_assn ×⇩a array_assn option_bool_impl_assn)›
definition (in -)conflict_option_rel_assn
:: ‹conflict_option_rel ⇒ option_lookup_clause_assn ⇒ assn›
where
‹conflict_option_rel_assn ≡ (bool1_assn ×⇩a lookup_clause_rel_assn)›
lemmas [fcomp_norm_unfold] = conflict_option_rel_assn_def[symmetric]
lookup_clause_rel_assn_def[symmetric]
definition (in -)ana_refinement_fast_rel where
‹ana_refinement_fast_rel ≡ snat_rel' TYPE(64) ×⇩r unat_rel' TYPE(32) ×⇩r bool1_rel›
abbreviation (in -)ana_refinement_fast_assn where
‹ana_refinement_fast_assn ≡ sint64_nat_assn ×⇩a uint32_nat_assn ×⇩a bool1_assn›
lemma ana_refinement_fast_assn_def:
‹ana_refinement_fast_assn = pure ana_refinement_fast_rel›
by (auto simp: ana_refinement_fast_rel_def)
abbreviation (in -)analyse_refinement_fast_assn where
‹analyse_refinement_fast_assn ≡
arl64_assn ana_refinement_fast_assn›
lemma lookup_clause_assn_is_None_alt_def:
‹RETURN o lookup_clause_assn_is_None = (λ(b, _, _). RETURN b)›
unfolding lookup_clause_assn_is_None_def by auto
sepref_def lookup_clause_assn_is_None_impl
is ‹RETURN o lookup_clause_assn_is_None›
:: ‹conflict_option_rel_assn⇧k →⇩a bool1_assn›
unfolding lookup_clause_assn_is_None_alt_def conflict_option_rel_assn_def
lookup_clause_rel_assn_def
by sepref
lemma size_lookup_conflict_alt_def:
‹RETURN o size_lookup_conflict = (λ(_, b, _). RETURN b)›
unfolding size_lookup_conflict_def by auto
sepref_def size_lookup_conflict_impl
is ‹RETURN o size_lookup_conflict›
:: ‹conflict_option_rel_assn⇧k →⇩a uint32_nat_assn›
unfolding size_lookup_conflict_alt_def conflict_option_rel_assn_def
lookup_clause_rel_assn_def
by sepref
sepref_def is_in_conflict_code
is ‹uncurry (RETURN oo is_in_lookup_conflict)›
:: ‹[λ((n, xs), L). atm_of L < length xs]⇩a
lookup_clause_rel_assn⇧k *⇩a unat_lit_assn⇧k → bool1_assn›
supply [[goals_limit=1]]
unfolding is_in_lookup_conflict_def is_NOTIN_alt_def[symmetric]
lookup_clause_rel_assn_def
by sepref
lemma lookup_clause_assn_is_empty_alt_def:
‹lookup_clause_assn_is_empty = (λS. size_lookup_conflict S = 0)›
by (auto simp: size_lookup_conflict_def lookup_clause_assn_is_empty_def fun_eq_iff)
sepref_def lookup_clause_assn_is_empty_impl
is ‹RETURN o lookup_clause_assn_is_empty›
:: ‹conflict_option_rel_assn⇧k →⇩a bool1_assn›
unfolding lookup_clause_assn_is_empty_alt_def
apply (annot_unat_const "TYPE(32)")
by sepref
definition the_lookup_conflict :: ‹conflict_option_rel ⇒ _› where
‹the_lookup_conflict = snd›
lemma the_lookup_conflict_alt_def:
‹RETURN o the_lookup_conflict = (λ(_, (n, xs)). RETURN (n, xs))›
by (auto simp: the_lookup_conflict_def)
sepref_def the_lookup_conflict_impl
is ‹RETURN o the_lookup_conflict›
:: ‹conflict_option_rel_assn⇧d →⇩a lookup_clause_rel_assn›
unfolding the_lookup_conflict_alt_def conflict_option_rel_assn_def
lookup_clause_rel_assn_def
by sepref
definition Some_lookup_conflict :: ‹_ ⇒ conflict_option_rel› where
‹Some_lookup_conflict xs = (False, xs)›
lemma Some_lookup_conflict_alt_def:
‹RETURN o Some_lookup_conflict = (λxs. RETURN (False, xs))›
by (auto simp: Some_lookup_conflict_def)
sepref_def Some_lookup_conflict_impl
is ‹RETURN o Some_lookup_conflict›
:: ‹lookup_clause_rel_assn⇧d →⇩a conflict_option_rel_assn›
unfolding Some_lookup_conflict_alt_def conflict_option_rel_assn_def
lookup_clause_rel_assn_def
by sepref
sepref_register Some_lookup_conflict
type_synonym cach_refinement_l_assn = ‹8 word ptr × 32 word array_list64›
definition (in -) cach_refinement_l_assn :: "_ ⇒ cach_refinement_l_assn ⇒ _" where
‹cach_refinement_l_assn ≡ array_assn minimize_status_assn ×⇩a arl64_assn atom_assn›
sepref_register conflict_min_cach_l
sepref_def delete_from_lookup_conflict_code
is ‹uncurry delete_from_lookup_conflict›
:: ‹unat_lit_assn⇧k *⇩a lookup_clause_rel_assn⇧d →⇩a lookup_clause_rel_assn›
unfolding delete_from_lookup_conflict_def NOTIN_def[symmetric]
conflict_option_rel_assn_def
lookup_clause_rel_assn_def
apply (annot_unat_const "TYPE(32)")
by sepref
lemma arena_is_valid_clause_idx_le_uint64_max:
‹arena_is_valid_clause_idx be bd ⟹
length be ≤ sint64_max ⟹
bd + arena_length be bd ≤ sint64_max›
‹arena_is_valid_clause_idx be bd ⟹ length be ≤ sint64_max ⟹
bd ≤ sint64_max›
using arena_lifting(10)[of be _ _ bd]
by (fastforce simp: arena_lifting arena_is_valid_clause_idx_def)+
lemma add_to_lookup_conflict_alt_def:
‹RETURN oo add_to_lookup_conflict = (λL (n, xs). RETURN (if xs ! atm_of L = NOTIN then n + 1 else n,
xs[atm_of L := ISIN (is_pos L)]))›
unfolding add_to_lookup_conflict_def by (auto simp: fun_eq_iff)
sepref_register ISIN NOTIN atm_of add_to_lookup_conflict
sepref_def add_to_lookup_conflict_impl
is ‹uncurry (RETURN oo add_to_lookup_conflict)›
:: ‹[λ(L, (n, xs)). atm_of L < length xs ∧ n + 1 ≤ uint32_max]⇩a
unat_lit_assn⇧k *⇩a (lookup_clause_rel_assn)⇧d → lookup_clause_rel_assn›
unfolding add_to_lookup_conflict_alt_def lookup_clause_rel_assn_def
is_NOTIN_alt_def[symmetric] fold_is_None NOTIN_def
apply (rewrite at ‹_ + ⌑› unat_const_fold[where 'a = ‹32›])
by sepref
lemma isa_lookup_conflict_merge_alt_def:
‹isa_lookup_conflict_merge i0 = (λM N i zs clvls lbd outl.
do {
let xs = the_lookup_conflict zs;
ASSERT( arena_is_valid_clause_idx N i);
(_, clvls, zs, lbd, outl) ← WHILE⇩T⇗λ(i::nat, clvls :: nat, zs, lbd, outl).
length (snd zs) = length (snd xs) ∧
Suc (fst zs) ≤ uint32_max ∧ Suc clvls ≤ uint32_max⇖
(λ(j :: nat, clvls, zs, lbd, outl). j < i + arena_length N i)
(λ(j :: nat, clvls, zs, lbd, outl). do {
ASSERT(j < length N);
ASSERT(arena_lit_pre N j);
ASSERT(get_level_pol_pre (M, arena_lit N j));
ASSERT(get_level_pol M (arena_lit N j) ≤ Suc (uint32_max div 2));
let lbd = lbd_write lbd (get_level_pol M (arena_lit N j));
ASSERT(atm_of (arena_lit N j) < length (snd zs));
ASSERT(¬is_in_lookup_conflict zs (arena_lit N j) ⟶ length outl < uint32_max);
let outl = isa_outlearned_add M (arena_lit N j) zs outl;
let clvls = isa_clvls_add M (arena_lit N j) zs clvls;
let zs = add_to_lookup_conflict (arena_lit N j) zs;
RETURN(Suc j, clvls, zs, lbd, outl)
})
(i + i0, clvls, xs, lbd, outl);
RETURN (Some_lookup_conflict zs, clvls, lbd, outl)
})›
unfolding isa_lookup_conflict_merge_def Some_lookup_conflict_def
the_lookup_conflict_def
by (auto simp: fun_eq_iff)
sepref_def resolve_lookup_conflict_merge_fast_code
is ‹uncurry6 isa_set_lookup_conflict_aa›
:: ‹[λ((((((M, N), i), (_, xs)), _), _), out).
length N ≤ sint64_max]⇩a
trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a conflict_option_rel_assn⇧d *⇩a
uint32_nat_assn⇧k *⇩a lbd_assn⇧d *⇩a out_learned_assn⇧d →
conflict_option_rel_assn ×⇩a uint32_nat_assn ×⇩a lbd_assn ×⇩a out_learned_assn›
supply
literals_are_in_ℒ⇩i⇩n_trail_get_level_uint32_max[dest]
arena_is_valid_clause_idx_le_uint64_max[dest]
unfolding isa_set_lookup_conflict_aa_def lookup_conflict_merge_def
PR_CONST_def nth_rll_def[symmetric]
isa_outlearned_add_def isa_clvls_add_def
isa_lookup_conflict_merge_alt_def
fmap_rll_u_def[symmetric]
fmap_rll_def[symmetric]
is_NOTIN_def[symmetric] add_0_right
apply (rewrite at ‹RETURN (⌑, _ ,_, _)› Suc_eq_plus1)
apply (rewrite at ‹RETURN (_ + ⌑, _ ,_, _)› snat_const_fold[where 'a = ‹64›])
apply (rewrite in ‹If _ ⌑› unat_const_fold[where 'a = ‹32›])
supply [[goals_limit = 1]]
unfolding fold_tuple_optimizations
by sepref
sepref_register isa_resolve_merge_conflict_gt2
lemma arena_is_valid_clause_idx_le_uint64_max2:
‹arena_is_valid_clause_idx be bd ⟹
length be ≤ sint64_max ⟹
bd + arena_length be bd ≤ sint64_max›
‹arena_is_valid_clause_idx be bd ⟹ length be ≤ sint64_max ⟹
bd < sint64_max›
using arena_lifting(10)[of be _ _ bd]
apply (fastforce simp: arena_lifting arena_is_valid_clause_idx_def)
using arena_lengthI(2) less_le_trans by blast
sepref_def resolve_merge_conflict_fast_code
is ‹uncurry6 isa_resolve_merge_conflict_gt2›
:: ‹[uncurry6 (λM N i (b, xs) clvls lbd outl. length N ≤ sint64_max)]⇩a
trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a conflict_option_rel_assn⇧d *⇩a
uint32_nat_assn⇧k *⇩a lbd_assn⇧d *⇩a out_learned_assn⇧d →
conflict_option_rel_assn ×⇩a uint32_nat_assn ×⇩a lbd_assn ×⇩a out_learned_assn›
supply
literals_are_in_ℒ⇩i⇩n_trail_get_level_uint32_max[dest]
fmap_length_rll_u_def[simp]
arena_is_valid_clause_idx_le_uint64_max[intro]
arena_is_valid_clause_idx_le_uint64_max2[dest]
unfolding isa_resolve_merge_conflict_gt2_def lookup_conflict_merge_def
PR_CONST_def nth_rll_def[symmetric]
isa_outlearned_add_def isa_clvls_add_def
isa_lookup_conflict_merge_alt_def
fmap_rll_u_def[symmetric]
fmap_rll_def[symmetric]
is_NOTIN_def[symmetric] add_0_right
apply (rewrite at ‹RETURN (⌑, _ ,_, _)› Suc_eq_plus1)
apply (rewrite at ‹WHILEIT _ _ _ (_ + ⌑, _ ,_, _)› snat_const_fold[where 'a = ‹64›])
apply (rewrite at ‹RETURN (_ + ⌑, _ ,_, _, _)› snat_const_fold[where 'a = ‹64›])
apply (rewrite in ‹If _ ⌑› unat_const_fold[where 'a = ‹32›])
supply [[goals_limit = 1]]
unfolding fold_tuple_optimizations
by sepref
sepref_def atm_in_conflict_code
is ‹uncurry (RETURN oo atm_in_conflict_lookup)›
:: ‹[uncurry atm_in_conflict_lookup_pre]⇩a
atom_assn⇧k *⇩a lookup_clause_rel_assn⇧k → bool1_assn›
unfolding atm_in_conflict_lookup_def atm_in_conflict_lookup_pre_def
is_NOTIN_alt_def[symmetric] fold_is_None NOTIN_def lookup_clause_rel_assn_def
apply (rewrite at ‹ _ ! _› annot_index_of_atm)
by sepref
sepref_def conflict_min_cach_l_code
is ‹uncurry (RETURN oo conflict_min_cach_l)›
:: ‹[conflict_min_cach_l_pre]⇩a cach_refinement_l_assn⇧k *⇩a atom_assn⇧k → minimize_status_assn›
unfolding conflict_min_cach_l_def conflict_min_cach_l_pre_def cach_refinement_l_assn_def
apply (rewrite at "nth _" eta_expand)
apply (rewrite at ‹ _ ! _› annot_index_of_atm)
by sepref
lemma conflict_min_cach_set_failed_l_alt_def:
‹conflict_min_cach_set_failed_l = (λ(cach, sup) L. do {
ASSERT(L < length cach);
ASSERT(length sup ≤ 1 + uint32_max div 2);
let b = (cach ! L = SEEN_UNKNOWN);
RETURN (cach[L := SEEN_FAILED], if b then sup @ [L] else sup)
})›
unfolding conflict_min_cach_set_failed_l_def Let_def by auto
lemma le_uint32_max_div2_le_uint32_max: ‹a2' ≤ Suc (uint32_max div 2) ⟹ a2' < uint32_max›
by (auto simp: uint32_max_def)
sepref_def conflict_min_cach_set_failed_l_code
is ‹uncurry conflict_min_cach_set_failed_l›
:: ‹cach_refinement_l_assn⇧d *⇩a atom_assn⇧k →⇩a cach_refinement_l_assn›
supply [[goals_limit=1]] le_uint32_max_div2_le_uint32_max[dest]
unfolding conflict_min_cach_set_failed_l_alt_def
minimize_status_rel_eq_def[symmetric] cach_refinement_l_assn_def
apply (rewrite at ‹ _ ! _› annot_index_of_atm)
apply (rewrite at ‹list_update _ _ _› annot_index_of_atm)
by sepref
lemma conflict_min_cach_set_removable_l_alt_def:
‹conflict_min_cach_set_removable_l = (λ(cach, sup) L. do {
ASSERT(L < length cach);
ASSERT(length sup ≤ 1 + uint32_max div 2);
let b = (cach ! L = SEEN_UNKNOWN);
RETURN (cach[L := SEEN_REMOVABLE], if b then sup @ [L] else sup)
})›
unfolding conflict_min_cach_set_removable_l_def by auto
sepref_def conflict_min_cach_set_removable_l_code
is ‹uncurry conflict_min_cach_set_removable_l›
:: ‹cach_refinement_l_assn⇧d *⇩a atom_assn⇧k →⇩a cach_refinement_l_assn›
unfolding conflict_min_cach_set_removable_l_alt_def
minimize_status_rel_eq_def[symmetric] cach_refinement_l_assn_def
apply (rewrite at ‹ _ ! _› annot_index_of_atm)
apply (rewrite at ‹list_update _ _ _› annot_index_of_atm)
by sepref
lemma lookup_conflict_size_impl_alt_def:
‹RETURN o (λ(n, xs). n) = (λ(n, xs). RETURN n)›
by auto
sepref_def lookup_conflict_size_impl
is [] ‹RETURN o (λ(n, xs). n)›
:: ‹lookup_clause_rel_assn⇧k →⇩a uint32_nat_assn›
unfolding lookup_clause_rel_assn_def lookup_conflict_size_impl_alt_def
by sepref
lemma single_replicate: ‹[C] = op_list_append [] C›
by auto
sepref_register lookup_conflict_remove1
sepref_register isa_lit_redundant_rec_wl_lookup
sepref_register isa_mark_failed_lits_stack
sepref_register lit_redundant_rec_wl_lookup conflict_min_cach_set_removable_l
get_propagation_reason_pol lit_redundant_reason_stack_wl_lookup
sepref_register isa_minimize_and_extract_highest_lookup_conflict isa_literal_redundant_wl_lookup
lemma set_lookup_empty_conflict_to_none_alt_def:
‹RETURN o set_lookup_empty_conflict_to_none = (λ(n, xs). RETURN (True, n, xs))›
by (auto simp: set_lookup_empty_conflict_to_none_def)
sepref_def set_lookup_empty_conflict_to_none_imple
is ‹RETURN o set_lookup_empty_conflict_to_none›
:: ‹lookup_clause_rel_assn⇧d →⇩a conflict_option_rel_assn›
unfolding set_lookup_empty_conflict_to_none_alt_def
lookup_clause_rel_assn_def conflict_option_rel_assn_def
by sepref
lemma isa_mark_failed_lits_stackI:
assumes
‹length ba ≤ Suc (uint32_max div 2)› and
‹a1' < length ba›
shows ‹Suc a1' ≤ uint32_max›
using assms by (auto simp: uint32_max_def)
sepref_register conflict_min_cach_set_failed_l
sepref_def isa_mark_failed_lits_stack_fast_code
is ‹uncurry2 (isa_mark_failed_lits_stack)›
:: ‹[λ((N, _), _). length N ≤ sint64_max]⇩a
arena_fast_assn⇧k *⇩a analyse_refinement_fast_assn⇧k *⇩a cach_refinement_l_assn⇧d →
cach_refinement_l_assn›
supply [[goals_limit = 1]] neq_Nil_revE[elim!] image_image[simp]
mark_failed_lits_stack_inv_helper1[dest] mark_failed_lits_stack_inv_helper2[dest]
fmap_length_rll_u_def[simp] isa_mark_failed_lits_stackI[intro]
arena_is_valid_clause_idx_le_uint64_max[intro] le_uint32_max_div2_le_uint32_max[intro]
unfolding isa_mark_failed_lits_stack_def PR_CONST_def
conflict_min_cach_set_failed_def[symmetric]
conflict_min_cach_def[symmetric]
get_literal_and_remove_of_analyse_wl_def
nth_rll_def[symmetric]
fmap_rll_def[symmetric]
arena_lit_def[symmetric]
minimize_status_rel_eq_def[symmetric]
apply (rewrite at 1 in ‹conflict_min_cach_set_failed_l _ ⌑› snat_const_fold[where 'a = ‹64›])
apply (rewrite in ‹RETURN (_ + ⌑, _)› snat_const_fold[where 'a = ‹64›])
apply (rewrite at 0 in ‹(⌑, _)› snat_const_fold[where 'a = ‹64›])
apply (rewrite at ‹arena_lit _ (_ + ⌑ - _)› annot_unat_snat_upcast[where 'l = 64])
by sepref
sepref_def isa_get_literal_and_remove_of_analyse_wl_fast_code
is ‹uncurry (RETURN oo isa_get_literal_and_remove_of_analyse_wl)›
:: ‹[λ(arena, analyse). isa_get_literal_and_remove_of_analyse_wl_pre arena analyse ∧
length arena ≤ sint64_max]⇩a
arena_fast_assn⇧k *⇩a analyse_refinement_fast_assn⇧d →
unat_lit_assn ×⇩a analyse_refinement_fast_assn›
supply [[goals_limit=1]] arena_lit_pre_le2[dest]
and [dest] = arena_lit_implI
unfolding isa_get_literal_and_remove_of_analyse_wl_pre_def
isa_get_literal_and_remove_of_analyse_wl_def
apply (rewrite at ‹length _ - ⌑› snat_const_fold[where 'a=64])
apply (rewrite at ‹arena_lit _ (_ + ⌑)› annot_unat_snat_upcast[where 'l = 64])
apply (annot_unat_const "TYPE(32)")
by sepref
sepref_def ana_lookup_conv_lookup_fast_code
is ‹uncurry (RETURN oo ana_lookup_conv_lookup)›
:: ‹[uncurry ana_lookup_conv_lookup_pre]⇩a arena_fast_assn⇧k *⇩a
(ana_refinement_fast_assn)⇧k
→ sint64_nat_assn ×⇩a sint64_nat_assn ×⇩a sint64_nat_assn ×⇩a sint64_nat_assn›
unfolding ana_lookup_conv_lookup_pre_def ana_lookup_conv_lookup_def
apply (rewrite at ‹(_, _, ⌑, _)› annot_unat_snat_upcast[where 'l = 64])
apply (annot_snat_const "TYPE(64)")
by sepref
sepref_def lit_redundant_reason_stack_wl_lookup_fast_code
is ‹uncurry2 (RETURN ooo lit_redundant_reason_stack_wl_lookup)›
:: ‹[uncurry2 lit_redundant_reason_stack_wl_lookup_pre]⇩a
unat_lit_assn⇧k *⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →
ana_refinement_fast_assn›
unfolding lit_redundant_reason_stack_wl_lookup_def lit_redundant_reason_stack_wl_lookup_pre_def
apply (rewrite at ‹⌑ < _› snat_const_fold[where 'a=64])
apply (annot_unat_const "TYPE(32)")
by sepref
lemma isa_lit_redundant_rec_wl_lookupI:
assumes
‹length ba ≤ Suc (uint32_max div 2)›
shows ‹length ba < uint32_max›
using assms by (auto simp: uint32_max_def)
lemma arena_lit_pre_le: ‹
arena_lit_pre a i ⟹ length a ≤ sint64_max ⟹ i ≤ sint64_max›
using arena_lifting(7)[of a _ _] unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by fastforce
lemma get_propagation_reason_pol_get_propagation_reason_pol_raw: ‹do {
C ← get_propagation_reason_pol M (-L);
case C of
Some C ⇒ f C
| None ⇒ g
} = do {
C ← get_propagation_reason_raw_pol M (-L);
if C ≠ DECISION_REASON then f C else g
}›
by (cases M) (auto simp: get_propagation_reason_pol_def get_propagation_reason_raw_pol_def)
sepref_register atm_in_conflict_lookup
sepref_def lit_redundant_rec_wl_lookup_fast_code
is ‹uncurry5 (isa_lit_redundant_rec_wl_lookup)›
:: ‹[λ(((((M, NU), D), cach), analysis), lbd). length NU ≤ sint64_max]⇩a
trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a (lookup_clause_rel_assn)⇧k *⇩a
cach_refinement_l_assn⇧d *⇩a analyse_refinement_fast_assn⇧d *⇩a lbd_assn⇧k →
cach_refinement_l_assn ×⇩a analyse_refinement_fast_assn ×⇩a bool1_assn›
supply [[goals_limit = 1]] neq_Nil_revE[elim] image_image[simp]
literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l[intro]
literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms[intro]
literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l_atms[intro] nth_rll_def[simp]
fmap_length_rll_u_def[simp]
isa_lit_redundant_rec_wl_lookupI[intro]
arena_lit_pre_le[dest] isa_mark_failed_lits_stackI[intro]
unfolding isa_lit_redundant_rec_wl_lookup_def
conflict_min_cach_set_removable_def[symmetric]
conflict_min_cach_def[symmetric]
get_literal_and_remove_of_analyse_wl_def
nth_rll_def[symmetric] PR_CONST_def
fmap_rll_u_def[symmetric] minimize_status_rel_eq_def[symmetric]
fmap_rll_def[symmetric] length_0_conv[symmetric]
apply (subst get_propagation_reason_pol_get_propagation_reason_pol_raw)
apply (rewrite at ‹get_level_pol _ _ = ⌑› unat_const_fold[where 'a=32])
apply (rewrite at ‹(_, ⌑, _)› annotate_assn[where A=analyse_refinement_fast_assn])
apply (annot_snat_const "TYPE(64)")
unfolding nth_rll_def[symmetric]
fmap_rll_def[symmetric]
fmap_length_rll_def[symmetric]
unfolding nth_rll_def[symmetric]
fmap_rll_def[symmetric]
fmap_length_rll_def[symmetric]
fmap_rll_u_def[symmetric]
by sepref
sepref_def delete_index_and_swap_code
is ‹uncurry (RETURN oo delete_index_and_swap)›
:: ‹[λ(xs, i). i < length xs]⇩a
(arl64_assn unat_lit_assn)⇧d *⇩a sint64_nat_assn⇧k → arl64_assn unat_lit_assn›
unfolding delete_index_and_swap.simps
by sepref
sepref_def lookup_conflict_upd_None_code
is ‹uncurry (RETURN oo lookup_conflict_upd_None)›
:: ‹[λ((n, xs), i). i < length xs ∧ n > 0]⇩a
lookup_clause_rel_assn⇧d *⇩a sint32_nat_assn⇧k → lookup_clause_rel_assn›
unfolding lookup_conflict_upd_None_RETURN_def lookup_clause_rel_assn_def
apply (annot_unat_const "TYPE(32)")
by sepref
lemma uint32_max_ge0: ‹0 < uint32_max› by (auto simp: uint32_max_def)
sepref_def literal_redundant_wl_lookup_fast_code
is ‹uncurry5 isa_literal_redundant_wl_lookup›
:: ‹[λ(((((M, NU), D), cach), L), lbd). length NU ≤ sint64_max]⇩a
trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a lookup_clause_rel_assn⇧k *⇩a
cach_refinement_l_assn⇧d *⇩a unat_lit_assn⇧k *⇩a lbd_assn⇧k →
cach_refinement_l_assn ×⇩a analyse_refinement_fast_assn ×⇩a bool1_assn›
supply [[goals_limit=1]]
literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l[intro] uint32_max_ge0[intro!]
literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l_atms[intro]
unfolding isa_literal_redundant_wl_lookup_def PR_CONST_def
minimize_status_rel_eq_def[symmetric]
apply (rewrite at ‹(_, ⌑, _)› al_fold_custom_empty[where 'l=64])+
unfolding single_replicate
apply (rewrite at ‹get_level_pol _ _ = ⌑› unat_const_fold[where 'a=32])
unfolding al_fold_custom_empty[where 'l=64]
apply (subst get_propagation_reason_pol_get_propagation_reason_pol_raw)
by sepref
sepref_def conflict_remove1_code
is ‹uncurry (RETURN oo lookup_conflict_remove1)›
:: ‹[lookup_conflict_remove1_pre]⇩a unat_lit_assn⇧k *⇩a lookup_clause_rel_assn⇧d →
lookup_clause_rel_assn›
supply [[goals_limit=2]]
unfolding lookup_conflict_remove1_def lookup_conflict_remove1_pre_def lookup_clause_rel_assn_def
apply (annot_unat_const "TYPE(32)")
by sepref
sepref_def minimize_and_extract_highest_lookup_conflict_fast_code
is ‹uncurry5 isa_minimize_and_extract_highest_lookup_conflict›
:: ‹[λ(((((M, NU), D), cach), lbd), outl). length NU ≤ sint64_max]⇩a
trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a lookup_clause_rel_assn⇧d *⇩a
cach_refinement_l_assn⇧d *⇩a lbd_assn⇧k *⇩a out_learned_assn⇧d →
lookup_clause_rel_assn ×⇩a cach_refinement_l_assn ×⇩a out_learned_assn›
supply [[goals_limit=1]]
literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l[intro]
minimize_and_extract_highest_lookup_conflict_inv_def[simp]
in_ℒ⇩a⇩l⇩l_less_uint32_max'[intro]
unfolding isa_minimize_and_extract_highest_lookup_conflict_def
PR_CONST_def
minimize_and_extract_highest_lookup_conflict_inv_def
apply (rewrite at ‹(_, ⌑, _, _)› snat_const_fold[where 'a = 64])
apply (annot_snat_const "TYPE(64)")
by sepref
lemma isasat_lookup_merge_eq2_alt_def:
‹isasat_lookup_merge_eq2 L M N C = (λzs clvls lbd outl. do {
let zs = the_lookup_conflict zs;
ASSERT(arena_lit_pre N C);
ASSERT(arena_lit_pre N (C+1));
let L0 = arena_lit N C;
let L' = (if L0 = L then arena_lit N (C + 1) else L0);
ASSERT(get_level_pol_pre (M, L'));
ASSERT(get_level_pol M L' ≤ Suc (uint32_max div 2));
let lbd = lbd_write lbd (get_level_pol M L');
ASSERT(atm_of L' < length (snd zs));
ASSERT(length outl < uint32_max);
let outl = isa_outlearned_add M L' zs outl;
ASSERT(clvls < uint32_max);
ASSERT(fst zs < uint32_max);
let clvls = isa_clvls_add M L' zs clvls;
let zs = add_to_lookup_conflict L' zs;
RETURN(Some_lookup_conflict zs, clvls, lbd, outl)
})›
by (auto simp: the_lookup_conflict_def Some_lookup_conflict_def Let_def
isasat_lookup_merge_eq2_def fun_eq_iff)
sepref_def isasat_lookup_merge_eq2_fast_code
is ‹uncurry7 isasat_lookup_merge_eq2›
:: ‹[λ(((((((L, M), NU), _), _), _), _), _). length NU ≤ sint64_max]⇩a
unat_lit_assn⇧k *⇩a trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a
conflict_option_rel_assn⇧d *⇩a uint32_nat_assn⇧k *⇩a lbd_assn⇧d *⇩a out_learned_assn⇧d →
conflict_option_rel_assn ×⇩a uint32_nat_assn ×⇩a lbd_assn ×⇩a out_learned_assn›
supply [[goals_limit = 1]]
unfolding isasat_lookup_merge_eq2_alt_def
isa_outlearned_add_def isa_clvls_add_def
is_NOTIN_def[symmetric]
supply
image_image[simp] literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[simp]
literals_are_in_ℒ⇩i⇩n_trail_get_level_uint32_max[dest]
fmap_length_rll_u_def[simp] the_lookup_conflict_def[simp]
arena_is_valid_clause_idx_le_uint64_max[dest]
arena_lit_pre_le2[dest] arena_lit_pre_le[dest]
apply (rewrite in ‹if _ then _ + ⌑ else _› unat_const_fold[where 'a=32])
apply (rewrite in ‹if _ then arena_lit _ (_ + ⌑) else _› snat_const_fold[where 'a=64])
by sepref
experiment begin
export_llvm
nat_lit_eq_impl
minimize_status_rel_eq_impl
SEEN_FAILED_impl
SEEN_UNKNOWN_impl
SEEN_REMOVABLE_impl
Some_impl
is_Notin_impl
NOTIN_impl
lookup_clause_assn_is_None_impl
size_lookup_conflict_impl
is_in_conflict_code
lookup_clause_assn_is_empty_impl
the_lookup_conflict_impl
Some_lookup_conflict_impl
delete_from_lookup_conflict_code
add_to_lookup_conflict_impl
resolve_lookup_conflict_merge_fast_code
resolve_merge_conflict_fast_code
atm_in_conflict_code
conflict_min_cach_l_code
conflict_min_cach_set_failed_l_code
conflict_min_cach_set_removable_l_code
lookup_conflict_size_impl
set_lookup_empty_conflict_to_none_imple
isa_mark_failed_lits_stack_fast_code
isa_get_literal_and_remove_of_analyse_wl_fast_code
ana_lookup_conv_lookup_fast_code
lit_redundant_reason_stack_wl_lookup_fast_code
lit_redundant_rec_wl_lookup_fast_code
delete_index_and_swap_code
lookup_conflict_upd_None_code
literal_redundant_wl_lookup_fast_code
conflict_remove1_code
minimize_and_extract_highest_lookup_conflict_fast_code
isasat_lookup_merge_eq2_fast_code
end
end