Theory IsaSAT_Initialisation_LLVM
theory IsaSAT_Initialisation_LLVM
imports IsaSAT_VMTF_LLVM Watched_Literals.Watched_Literals_Watch_List_Initialisation
IsaSAT_Initialisation IsaSAT_Setup_LLVM IsaSAT_Mark_LLVM
IsaSAT_Initialisation_State_LLVM
begin
hide_const (open) NEMonad.RETURN NEMonad.ASSERT
definition polarity_st_heur_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹polarity_st_heur_init S L = polarity_pol (Tuple15_a S) L›
definition polarity_st_heur_init_code :: ‹twl_st_wll_trail_init ⇒ _› where
‹polarity_st_heur_init_code N C = IsaSAT_Init.read_all_st_code (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. polarity_pol_fast_code M C) N›
lemma polarity_st_heur_init_alt_def:
‹(λN C'. IsaSAT_Init.read_all_st (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. (RETURN ∘∘ polarity_pol) M C') N) =
RETURN oo polarity_st_heur_init›
by (auto simp: IsaSAT_Init.read_all_st_def polarity_st_heur_init_def intro!: ext
split: tuple15.splits)
lemmas polarity_st_heur_init_code_refine [sepref_fr_rules] =
IsaSAT_Init.read_trail_refine[OF polarity_pol_fast_code.refine,
unfolded polarity_st_heur_init_alt_def polarity_st_heur_init_code_def[symmetric]]
definition get_conflict_wl_is_None_init_code :: ‹twl_st_wll_trail_init ⇒ _› where
‹get_conflict_wl_is_None_init_code = IsaSAT_Init.read_all_st_code (λ_ _ M _ _ _ _ _ _ _ _ _ _ _ _. conflict_is_None_code M)›
lemma get_conflict_wl_is_None_heur_init_alt_def:
‹RETURN o get_conflict_wl_is_None_heur_init = IsaSAT_Init.read_all_st (λ_ _ M _ _ _ _ _ _ _ _ _ _ _ _. conflict_is_None M)›
by (auto simp: IsaSAT_Init.read_all_st_def polarity_st_heur_init_def get_conflict_wl_is_None_heur_init_def
conflict_is_None_def
intro!: ext
split: tuple15.splits)
lemmas get_conflict_wl_is_None_init_code_refine [sepref_fr_rules] =
IsaSAT_Init.read_conflict_refine0[OF conflict_is_None_code_refine,
unfolded get_conflict_wl_is_None_init_code_def[symmetric] get_conflict_wl_is_None_heur_init_alt_def[symmetric]]
definition full_arena_length_st_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹full_arena_length_st_init S = length (get_clauses_wl_heur_init S)›
lemma full_arena_length_st_init_alt_def:
‹RETURN o full_arena_length_st_init = IsaSAT_Init.read_all_st (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _. (RETURN ∘ length) M)›
by (auto simp: full_arena_length_st_init_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition full_arena_length_st_init_code :: ‹twl_st_wll_trail_init ⇒ _› where
‹full_arena_length_st_init_code = IsaSAT_Init.read_all_st_code (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _. arena_full_length_impl M)›
definition clss_size_lcount_st_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹clss_size_lcount_st_init S = clss_size_lcount (get_learned_count_init S)›
lemma clss_size_lcount_st_init_alt_def:
‹RETURN o clss_size_lcount_st_init = IsaSAT_Init.read_all_st (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. (RETURN ∘ clss_size_lcount) M)›
by (auto simp: clss_size_lcount_st_init_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition clss_size_lcount_st_init_impl :: ‹twl_st_wll_trail_init ⇒ _› where
‹clss_size_lcount_st_init_impl = IsaSAT_Init.read_all_st_code (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. clss_size_lcount_fast_code M)›
definition clss_size_lcountUE_st_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹clss_size_lcountUE_st_init S = clss_size_lcountUE (get_learned_count_init S)›
lemma clss_size_lcountUE_st_init_alt_def:
‹RETURN o clss_size_lcountUE_st_init = IsaSAT_Init.read_all_st (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. (RETURN ∘ clss_size_lcountUE) M)›
by (auto simp: clss_size_lcountUE_st_init_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition clss_size_lcountUE_st_init_impl :: ‹twl_st_wll_trail_init ⇒ _› where
‹clss_size_lcountUE_st_init_impl = IsaSAT_Init.read_all_st_code (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. clss_size_lcountUE_fast_code M)›
definition clss_size_lcountUEk_st_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹clss_size_lcountUEk_st_init S = clss_size_lcountUEk (get_learned_count_init S)›
lemma clss_size_lcountUEk_st_init_alt_def:
‹RETURN o clss_size_lcountUEk_st_init = IsaSAT_Init.read_all_st (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. (RETURN ∘ clss_size_lcountUEk) M)›
by (auto simp: clss_size_lcountUEk_st_init_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition clss_size_lcountUEk_st_init_impl :: ‹twl_st_wll_trail_init ⇒ _› where
‹clss_size_lcountUEk_st_init_impl = IsaSAT_Init.read_all_st_code (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. clss_size_lcountUEk_fast_code M)›
definition clss_size_lcountUS_st_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹clss_size_lcountUS_st_init S = clss_size_lcountUS (get_learned_count_init S)›
lemma clss_size_lcountUS_st_init_alt_def:
‹RETURN o clss_size_lcountUS_st_init = IsaSAT_Init.read_all_st (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. (RETURN ∘ clss_size_lcountUS) M)›
by (auto simp: clss_size_lcountUS_st_init_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition clss_size_lcountUS_st_init_impl :: ‹twl_st_wll_trail_init ⇒ _› where
‹clss_size_lcountUS_st_init_impl = IsaSAT_Init.read_all_st_code (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. clss_size_lcountUSt_fast_code M)›
definition clss_size_lcountU0_st_init :: ‹twl_st_wl_heur_init ⇒ _› where
‹clss_size_lcountU0_st_init S = clss_size_lcountU0 (get_learned_count_init S)›
lemma clss_size_lcountU0_st_init_alt_def:
‹RETURN o clss_size_lcountU0_st_init = IsaSAT_Init.read_all_st (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. (RETURN ∘ clss_size_lcountU0) M)›
by (auto simp: clss_size_lcountU0_st_init_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition clss_size_lcountU0_st_init_impl :: ‹twl_st_wll_trail_init ⇒ _› where
‹clss_size_lcountU0_st_init_impl = IsaSAT_Init.read_all_st_code (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _. clss_size_lcountU0_fast_code M)›
definition is_failed_loc :: ‹bool ⇒ bool› where
‹is_failed_loc x = x›
sepref_def is_failed_loc_impl
is ‹RETURN o is_failed_loc›
:: ‹bool1_assn⇧k →⇩a bool1_assn›
unfolding is_failed_loc_def
by sepref
lemma is_failed_heur_init_alt_def:
‹RETURN o is_failed_heur_init = IsaSAT_Init.read_all_st (λ_ _ _ _ _ _ _ _ _ _ _ _ M _ _. (RETURN o is_failed_loc) M)›
by (auto simp: is_failed_loc_def IsaSAT_Init.read_all_st_def
intro!: ext
split: tuple15.splits)
definition is_failed_heur_init_impl :: ‹twl_st_wll_trail_init ⇒ _› where
‹is_failed_heur_init_impl = IsaSAT_Init.read_all_st_code (λ_ _ _ _ _ _ _ _ _ _ _ _ M _ _. is_failed_loc_impl M)›
lemmas [sepref_fr_rules] =
IsaSAT_Init.read_b_refine0[OF arena_full_length_impl.refine,
unfolded full_arena_length_st_init_code_def[symmetric] full_arena_length_st_init_alt_def[symmetric]]
IsaSAT_Init.read_n_refine0[OF get_learned_count_number.not_deleted_code_refine,
unfolded clss_size_lcount_st_init_impl_def[symmetric] clss_size_lcount_st_init_alt_def[symmetric]]
IsaSAT_Init.read_n_refine0[OF clss_size_lcountUE_fast_code.refine,
unfolded clss_size_lcountUE_st_init_impl_def[symmetric] clss_size_lcountUE_st_init_alt_def[symmetric]]
IsaSAT_Init.read_n_refine0[OF clss_size_lcountUEk_fast_code.refine,
unfolded clss_size_lcountUEk_st_init_impl_def[symmetric] clss_size_lcountUEk_st_init_alt_def[symmetric]]
IsaSAT_Init.read_n_refine0[OF clss_size_lcountUSt_fast_code.refine,
unfolded clss_size_lcountUS_st_init_impl_def[symmetric] clss_size_lcountUS_st_init_alt_def[symmetric]]
IsaSAT_Init.read_n_refine0[OF clss_size_lcountU0_fast_code.refine,
unfolded clss_size_lcountU0_st_init_impl_def[symmetric] clss_size_lcountU0_st_init_alt_def[symmetric]]
IsaSAT_Init.read_m_refine0[OF is_failed_loc_impl.refine,
unfolded is_failed_heur_init_impl_def[symmetric] is_failed_heur_init_alt_def[symmetric]]
lemmas [unfolded Tuple15_LLVM.inline_direct_return_node_case, llvm_code] =
polarity_st_heur_init_code_def[unfolded IsaSAT_Init.read_all_st_code_def]
full_arena_length_st_init_code_def[unfolded IsaSAT_Init.read_all_st_code_def]
clss_size_lcount_st_init_impl_def[unfolded IsaSAT_Init.read_all_st_code_def]
clss_size_lcountUE_st_init_impl_def[unfolded IsaSAT_Init.read_all_st_code_def]
clss_size_lcountUEk_st_init_impl_def[unfolded IsaSAT_Init.read_all_st_code_def]
clss_size_lcountUS_st_init_impl_def[unfolded IsaSAT_Init.read_all_st_code_def]
clss_size_lcountU0_st_init_impl_def[unfolded IsaSAT_Init.read_all_st_code_def]
is_failed_heur_init_impl_def[unfolded IsaSAT_Init.read_all_st_code_def]
sepref_register atoms_hash_empty
sepref_def (in -) atoms_hash_empty_code
is ‹atoms_hash_int_empty›
:: ‹sint32_nat_assn⇧k →⇩a atoms_hash_assn›
unfolding atoms_hash_int_empty_def array_fold_custom_replicate
by sepref
sepref_def distinct_atms_empty_code
is ‹distinct_atms_int_empty›
:: ‹sint64_nat_assn⇧k →⇩a distinct_atoms_assn›
unfolding distinct_atms_int_empty_def array_fold_custom_replicate
al_fold_custom_empty[where 'l=64]
by sepref
lemmas [sepref_fr_rules] = distinct_atms_empty_code.refine atoms_hash_empty_code.refine
abbreviation unat_rel32 :: ‹(32 word × nat) set› where ‹unat_rel32 ≡ unat_rel›
abbreviation unat_rel64 :: ‹(64 word × nat) set› where ‹unat_rel64 ≡ unat_rel›
abbreviation snat_rel32 :: ‹(32 word × nat) set› where ‹snat_rel32 ≡ snat_rel›
abbreviation snat_rel64 :: ‹(64 word × nat) set› where ‹snat_rel64 ≡ snat_rel›
sepref_def hp_init_ACIDS0_code
is ‹uncurry hp_init_ACIDS0›
:: ‹(arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k →⇩a hp_assn›
unfolding hp_init_ACIDS0_def
array_fold_custom_replicate op_list_replicate_def[symmetric]
atom.fold_option hp_assn_def
apply (annot_unat_const ‹TYPE(64)›)
by sepref
definition init_ACIDS0' :: ‹_ ⇒ nat ⇒ (nat multiset × nat multiset × (nat ⇒ nat)) nres› where
‹init_ACIDS0' 𝒜 n = init_ACIDS0 (mset 𝒜) n›
lemma hp_acids_empty:
‹(uncurry hp_init_ACIDS0, uncurry init_ACIDS0') ∈
Id ×⇩f Id →⇩f ⟨((⟨⟨nat_rel⟩option_rel, ⟨nat_rel⟩option_rel⟩pairing_heaps_rel)) O
acids_encoded_hmrel⟩nres_rel›
proof -
have 1: ‹((𝒜, (λ_. None, λ_. None, λ_. None, λ_. None, λ_. Some 0), None), (𝒜, {#}, λ_. 0)) ∈ acids_encoded_hmrel› for 𝒜
by (auto simp: acids_encoded_hmrel_def bottom_acids0_def pairing_heaps_rel_def map_fun_rel_def
ACIDS.hmrel_def encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_def empty_acids0_def
intro!: relcompI)
have H: ‹mset_nodes ya ≠ {#}› for ya
by (cases ya) auto
show ?thesis
unfolding uncurry0_def hp_init_ACIDS0_def init_ACIDS0_def
init_ACIDS0'_def uncurry_def case_prod_beta
apply (intro frefI nres_relI)
apply refine_rcg
apply (rule relcompI[of])
defer
apply (rule 1)
by (auto simp add: acids_encoded_hmrel_def encoded_hp_prop_def hp_init_ACIDS0_def
ACIDS.hmrel_def encoded_hp_prop_list_conc_def pairing_heaps_rel_def H map_fun_rel_def
split: option.splits dest!: multi_member_split)
qed
lemmas [sepref_fr_rules] =
hp_init_ACIDS0_code.refine[FCOMP hp_acids_empty, unfolded hr_comp_assoc[symmetric]
acids_assn_def[symmetric]]
definition init_ACIDS' where
‹init_ACIDS' 𝒜 n = do {
ac ← init_ACIDS0' 𝒜 n;
RETURN (ac, 0)
}›
lemma init_ACIDS'_alt: ‹init_ACIDS (mset N) n = init_ACIDS' N n›
by (auto simp: init_ACIDS'_def init_ACIDS0'_def init_ACIDS_def)
sepref_register init_ACIDS0' acids_heur_import_variable
sepref_def hp_init_ACIDS_code
is ‹uncurry init_ACIDS'›
:: ‹(arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k →⇩a acids_assn2›
unfolding init_ACIDS'_def acids_assn2_def
apply (annot_unat_const ‹TYPE(64)›)
by sepref
sepref_def acids_heur_import_variable_code
is ‹uncurry acids_heur_import_variable›
:: ‹atom_assn⇧k *⇩a acids_assn2⇧d →⇩a acids_assn2›
unfolding acids_heur_import_variable_def acids_assn2_def
apply (annot_unat_const ‹TYPE(64)›)
by sepref
sepref_def initialise_ACIDS_code
is ‹uncurry initialise_ACIDS›
:: ‹[λ(N, n). True]⇩a (arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k → acids_assn2›
unfolding initialise_ACIDS_def vmtf_cons_def Suc_eq_plus1 atom.fold_option length_uint32_nat_def
option.case_eq_if vmtf_init_assn_def init_ACIDS'_alt
apply (annot_snat_const ‹TYPE(64)›)
supply [[goals_limit = 1]]
by sepref
lemma initialise_ACIDS_rev_alt_def:
‹initialise_ACIDS_rev N n = do {
A ← init_ACIDS (mset N) n;
ASSERT(length N ≤ unat32_max);
(n, A) ← WHILE⇩T⇗ λ_. True⇖
(λ(i, A). i < length_uint32_nat N)
(λ(i, A). do {
ASSERT(i < length_uint32_nat N);
let L = (N ! (length N - 1 - i));
ASSERT (snd A = i);
ASSERT(i + 1 ≤ unat32_max);
A ← acids_heur_import_variable L A;
RETURN (i + 1, A)
})
(0, A);
RETURN A
}› (is ‹?A = ?B›)
proof -
have [refine0]: ‹init_ACIDS (mset (rev N)) n ≤ ⇓ Id (init_ACIDS (mset N) n)›
‹init_ACIDS (mset (N)) n ≤ ⇓ Id (init_ACIDS (mset (rev N)) n)›
by auto
have [refine0]: ‹(A,Aa)∈Id ⟹ ((0, A), 0, Aa) ∈ Id ×⇩r Id› for A Aa
by auto
have K: ‹⋀A Aa x x' x1 x2 x1a x2a.
(x, x') ∈ nat_rel ×⇩f Id ⟹
case x of (i, A) ⇒ i < length_uint32_nat (rev N) ⟹
case x' of (i, A) ⇒ i < length_uint32_nat N ⟹
x' = (x1, x2) ⟹
x = (x1a, x2a) ⟹
x1 < length_uint32_nat N ⟹
x1a < length_uint32_nat (rev N) ⟹
snd x2 = x1 ⟹
x1 + 1 ≤ unat32_max ⟹
snd x2a = x1a ⟹
x1a + 1 ≤ unat32_max ⟹
acids_heur_import_variable (rev N ! x1a) x2a
≤ ⇓ Id
(acids_heur_import_variable (N ! (length N - 1 - x1)) x2)›
‹⋀A Aa x x' x1 x2 x1a x2a.
(x, x') ∈ nat_rel ×⇩f Id ⟹
case x of (i, A) ⇒ i < length_uint32_nat N ⟹
case x' of (i, A) ⇒ i < length_uint32_nat (rev N) ⟹
x' = (x1, x2) ⟹
x = (x1a, x2a) ⟹
x1 < length_uint32_nat N ⟹
x1a < length_uint32_nat (rev N) ⟹
snd x2 = x1 ⟹
x1 + 1 ≤ unat32_max ⟹
snd x2a = x1a ⟹
x1a + 1 ≤ unat32_max ⟹
acids_heur_import_variable (N ! (length N - 1 - x1a)) x2a
≤ ⇓ Id
(acids_heur_import_variable (rev N ! x1) x2)›
by (auto simp: nth_rev)
have ‹?A ≤ ⇓Id ?B›
unfolding initialise_ACIDS_rev_def initialise_ACIDS_def
apply refine_vcg
apply (auto simp: rev_nth; fail)+
apply (rule K; assumption)
apply (auto simp: rev_nth; fail)+
done
moreover have ‹?B ≤ ⇓Id ?A›
unfolding initialise_ACIDS_rev_def initialise_ACIDS_def
apply refine_vcg
apply (auto simp: rev_nth; fail)+
apply (rule K; assumption?)
apply (auto simp: rev_nth; fail)+
done
ultimately show ?thesis
by auto
qed
sepref_def initialise_ACIDS_rev_code
is ‹uncurry initialise_ACIDS_rev›
:: ‹[λ(N, n). True]⇩a (arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k → acids_assn2›
unfolding vmtf_cons_def Suc_eq_plus1 atom.fold_option length_uint32_nat_def
option.case_eq_if vmtf_init_assn_def init_ACIDS'_alt initialise_ACIDS_rev_alt_def nth_rev
apply (annot_snat_const ‹TYPE(64)›)
supply [[goals_limit = 1]]
by sepref
sepref_def initialise_VMTF_code
is ‹uncurry initialise_VMTF›
:: ‹[λ(N, n). True]⇩a (arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k → vmtf_init_assn›
unfolding initialise_VMTF_def vmtf_cons_def Suc_eq_plus1 atom.fold_option length_uint32_nat_def
option.case_eq_if vmtf_init_assn_def
apply (rewrite in ‹let _ = ⌑ in _ › array_fold_custom_replicate op_list_replicate_def[symmetric])
apply (rewrite at 0 in ‹VMTF_Node ⌑› unat_const_fold[where 'a=64])
apply (rewrite at ‹VMTF_Node (⌑ + 1)› annot_snat_unat_conv)
apply (rewrite at 1 in ‹VMTF_Node ⌑› unat_const_fold[where 'a=64])
apply (annot_snat_const ‹TYPE(64)›)
apply (rewrite in ‹list_update _ _ _› annot_index_of_atm)
apply (rewrite in ‹if _ then _ else list_update _ _ _› annot_index_of_atm)
apply (rewrite at ‹⌑› in ‹_ ! atom.the _› annot_index_of_atm)+
apply (rewrite at ‹RETURN ((_, ⌑, _))› annot_snat_unat_conv)
supply [[goals_limit = 1]]
by sepref
sepref_register initialize_Bump_Init
sepref_def initialize_Bump_Init_code
is ‹uncurry initialize_Bump_Init›
:: ‹[λ(N, n). True]⇩a (arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k → heuristic_bump_init_assn›
unfolding initialize_Bump_Init_def
by sepref
sepref_register cons_trail_Propagated_tr
lemma propagate_unit_cls_heur_b_alt_def:
‹propagate_unit_cls_heur_b L S =
do {
let (M, S) = extract_trail_wl_heur_init S;
M ← cons_trail_Propagated_tr L 0 M;
RETURN (IsaSAT_Init.update_a M S)
}›
by (cases S)
(auto simp:propagate_unit_cls_heur_b_def propagate_unit_cls_heur_def isasat_init_getters_and_setters_def
Let_def intro!: ext)
sepref_def propagate_unit_cls_code
is ‹uncurry (propagate_unit_cls_heur_b)›
:: ‹unat_lit_assn⇧k *⇩a isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]] DECISION_REASON_def[simp]
unfolding propagate_unit_cls_heur_b_alt_def
PR_CONST_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
declare propagate_unit_cls_code.refine[sepref_fr_rules]
definition already_propagated_unit_cls_heur'
:: ‹bool ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹already_propagated_unit_cls_heur' = (λunbdd S. RETURN S)›
lemma already_propagated_unit_cls_heur'_alt:
‹already_propagated_unit_cls_heur unbd L = already_propagated_unit_cls_heur' unbd›
unfolding already_propagated_unit_cls_heur'_def already_propagated_unit_cls_heur_def
by auto
definition already_propagated_unit_cls_heur_b where
‹already_propagated_unit_cls_heur_b = already_propagated_unit_cls_heur' False›
sepref_def already_propagated_unit_cls_code
is ‹already_propagated_unit_cls_heur_b›
:: ‹isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding already_propagated_unit_cls_heur'_def
PR_CONST_def already_propagated_unit_cls_heur_b_def
by sepref
sepref_def set_conflict_unit_code
is ‹uncurry set_conflict_unit_heur›
:: ‹[λ(L, (b, n, xs)). atm_of L < length xs]⇩a
unat_lit_assn⇧k *⇩a conflict_option_rel_assn⇧d → conflict_option_rel_assn›
supply [[goals_limit=1]]
unfolding set_conflict_unit_heur_def ISIN_def[symmetric] conflict_option_rel_assn_def
lookup_clause_rel_assn_def
apply (annot_unat_const ‹TYPE(32)›)
by sepref
declare set_conflict_unit_code.refine[sepref_fr_rules]
lemma conflict_propagated_unit_cls_heur_b_alt_def:
‹conflict_propagated_unit_cls_heur_b L S =
do {
let (D, S) = extract_conflict_wl_heur_init S;
let (M, S) = extract_trail_wl_heur_init S;
Refine_Basic.ASSERT(atm_of L < length (snd (snd D)));
D ← set_conflict_unit_heur L D;
Refine_Basic.ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
RETURN (IsaSAT_Init.update_d j (IsaSAT_Init.update_c D (IsaSAT_Init.update_a M S)))
}›
by (cases S)
(auto simp: isasat_init_getters_and_setters_def conflict_propagated_unit_cls_heur_b_def
conflict_propagated_unit_cls_heur_def)
sepref_def conflict_propagated_unit_cls_code
is ‹uncurry (conflict_propagated_unit_cls_heur_b)›
:: ‹unat_lit_assn⇧k *⇩a isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding conflict_propagated_unit_cls_heur_b_alt_def
PR_CONST_def
by sepref
declare conflict_propagated_unit_cls_code.refine[sepref_fr_rules]
sepref_register fm_add_new
lemma add_init_cls_code_bI:
assumes
‹length at' ≤ Suc (Suc unat32_max)› and
‹2 ≤ length at'› and
‹length a1'j ≤ length a1'a› and
‹length a1'a ≤ snat64_max - length at' - 5›
shows ‹append_and_length_fast_code_pre ((True, at'), a1'a)› ‹5 ≤ snat64_max - length at'›
using assms unfolding append_and_length_fast_code_pre_def
by (auto simp: unat64_max_def unat32_max_def snat64_max_def)
lemma add_init_cls_code_bI2:
assumes
‹length at' ≤ Suc (Suc unat32_max)›
shows ‹5 ≤ snat64_max - length at'›
using assms unfolding append_and_length_fast_code_pre_def
by (auto simp: unat64_max_def unat32_max_def snat64_max_def)
lemma add_init_clss_codebI:
assumes
‹length at' ≤ Suc (Suc unat32_max)› and
‹2 ≤ length at'› and
‹length a1'j ≤ length a1'a› and
‹length a1'a ≤ unat64_max - (length at' + 5)›
shows ‹length a1'j < unat64_max›
using assms by (auto simp: unat64_max_def unat32_max_def)
abbreviation clauses_ll_assn where
‹clauses_ll_assn ≡ aal_assn' TYPE(64) TYPE(64) unat_lit_assn›
lemma op_list_list_llen_alt_def: ‹op_list_list_llen xss i = length (xss ! i)›
unfolding op_list_list_llen_def
by auto
lemma op_list_list_idx_alt_def: ‹op_list_list_idx xs i j = xs ! i ! j›
unfolding op_list_list_idx_def ..
sepref_def append_and_length_fast_code
is ‹uncurry2 fm_add_new_fast›
:: ‹[λ((b, C), N). append_and_length_fast_code_pre ((b, C), N)]⇩a
bool1_assn⇧k *⇩a clause_ll_assn⇧k *⇩a (arena_fast_assn)⇧d →
arena_fast_assn ×⇩a sint64_nat_assn›
supply [[goals_limit=1]]
supply [simp] = fm_add_new_bounds1[simplified] shorten_lbd_le
supply [split] = if_splits
unfolding fm_add_new_fast_def fm_add_new_def append_and_length_fast_code_pre_def
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
is_short_clause_def header_size_def
apply (rewrite at ‹APos ⌑› unat_const_fold[where 'a=32])+
apply (rewrite at ‹length _ - 2› annot_snat_unat_downcast[where 'l=32])
apply (rewrite at ‹AStatus _ ⌑› unat_const_fold[where 'a=2])+
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register fm_add_new_fast
lemma add_init_cls_heur_b_alt_def:
‹add_init_cls_heur_b C S = do {
let C = C;
ASSERT(length C ≤ unat32_max + 2);
ASSERT(length C ≥ 2);
let (N, S) = extract_arena_wl_heur_init S;
let (failed, S) = extract_failed_wl_heur_init S;
if (length N ≤ snat64_max - length C - 5 ∧ ¬failed)
then do {
let (vdom, S) = extract_vdom_wl_heur_init S;
let (ivdom, S) = extract_ivdom_wl_heur_init S;
ASSERT(length vdom ≤ length N ∧ vdom = ivdom);
(N, i) ← fm_add_new True C N;
let vdom = vdom @ [i];
let ivdom = ivdom @ [i];
RETURN (IsaSAT_Init.update_b N (IsaSAT_Init.update_k vdom (IsaSAT_Init.update_l ivdom (IsaSAT_Init.update_m failed S))))
} else RETURN (IsaSAT_Init.update_m True (IsaSAT_Init.update_b N S))}›
by (cases S)
(auto simp: isasat_init_getters_and_setters_def conflict_propagated_unit_cls_heur_b_def add_init_cls_heur_b_def add_init_cls_heur_def
conflict_propagated_unit_cls_heur_def)
sepref_def add_init_cls_code_b
is ‹uncurry add_init_cls_heur_b›
:: ‹[λ(C, S). True]⇩a
(clause_ll_assn)⇧k *⇩a isasat_init_assn⇧d → isasat_init_assn›
supply [[goals_limit=1]] append_ll_def[simp]add_init_clss_codebI[intro]
add_init_cls_code_bI[intro] add_init_cls_code_bI2[intro]
unfolding add_init_cls_heur_b_alt_def
PR_CONST_def
Let_def length_uint64_nat_def add_init_cls_heur_b'_def
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
unfolding
nth_rll_def[symmetric] delete_index_and_swap_update_def[symmetric]
delete_index_and_swap_ll_def[symmetric]
append_ll_def[symmetric] fm_add_new_fast_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma already_propagated_unit_cls_conflict_heur_b_alt_def:
‹already_propagated_unit_cls_conflict_heur_b L S = do {
ASSERT (isa_length_trail_pre (get_trail_init_wl_heur S));
let (M, S) = extract_trail_wl_heur_init S;
let j = isa_length_trail M;
RETURN (IsaSAT_Init.update_d j (IsaSAT_Init.update_a M S))
}›
by (cases S)
(auto simp: isasat_init_getters_and_setters_def conflict_propagated_unit_cls_heur_b_def add_init_cls_heur_b_def add_init_cls_heur_def
already_propagated_unit_cls_conflict_heur_def already_propagated_unit_cls_conflict_heur_b_def)
sepref_def already_propagated_unit_cls_conflict_code
is ‹uncurry already_propagated_unit_cls_conflict_heur_b›
:: ‹unat_lit_assn⇧k *⇩a isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding already_propagated_unit_cls_conflict_heur_b_alt_def PR_CONST_def
by sepref
sepref_def (in -) set_conflict_empty_code
is ‹RETURN o lookup_set_conflict_empty›
:: ‹conflict_option_rel_assn⇧d →⇩a conflict_option_rel_assn›
supply [[goals_limit=1]]
unfolding lookup_set_conflict_empty_def conflict_option_rel_assn_def
by sepref
definition set_conflict_to_empty where
‹set_conflict_to_empty = (λ(_, nxs). (False, nxs))›
sepref_def set_conflict_to_empty_impl
is ‹RETURN o set_conflict_to_empty›
:: ‹conflict_option_rel_assn⇧d →⇩a conflict_option_rel_assn›
unfolding set_conflict_to_empty_def conflict_option_rel_assn_def
by sepref
lemma set_empty_clause_as_conflict_heur_alt_def:
‹set_empty_clause_as_conflict_heur S = (do {
let (M, S) = extract_trail_wl_heur_init S;
let (D, S) = extract_conflict_wl_heur_init S;
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
RETURN (IsaSAT_Init.update_c (set_conflict_to_empty D) (IsaSAT_Init.update_d j (IsaSAT_Init.update_a M S)))
})›
by (cases S)
(auto simp: isasat_init_getters_and_setters_def conflict_propagated_unit_cls_heur_b_def set_conflict_to_empty_def
set_empty_clause_as_conflict_heur_def already_propagated_unit_cls_conflict_heur_b_def)
sepref_def set_empty_clause_as_conflict_code
is ‹set_empty_clause_as_conflict_heur›
:: ‹isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding set_empty_clause_as_conflict_heur_alt_def lookup_clause_rel_assn_def
by sepref
definition (in -) add_clause_to_others_heur'
:: ‹twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_clause_to_others_heur' = (λ S.
RETURN S)›
lemma add_clause_to_others_heur'_alt: ‹add_clause_to_others_heur L = add_clause_to_others_heur'›
unfolding add_clause_to_others_heur'_def add_clause_to_others_heur_def
by auto
sepref_def add_clause_to_others_code
is ‹add_clause_to_others_heur'›
:: ‹isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding add_clause_to_others_heur_def add_clause_to_others_heur'_def
by sepref
declare add_clause_to_others_code.refine[sepref_fr_rules]
sepref_register init_dt_step_wl
get_conflict_wl_is_None_heur_init already_propagated_unit_cls_heur
conflict_propagated_unit_cls_heur add_clause_to_others_heur
add_init_cls_heur set_empty_clause_as_conflict_heur
sepref_register polarity_st_heur_init propagate_unit_cls_heur
lemma is_Nil_length: ‹is_Nil xs ⟷ length xs = 0›
by (cases xs) auto
definition pre_simplify_clause_lookup' where
‹pre_simplify_clause_lookup' i xs = pre_simplify_clause_lookup (xs ! i)›
lemma pre_simplify_clause_lookup'I:
‹a < length bb ⟹
a1' < length (bb ! a) ⟹
rdomp (aal_assn' TYPE(64) TYPE(64) unat_lit_assn) bb ⟹
Suc a1' < max_snat 64›
for aa aaa ad ag::‹64 word› and ac :: ‹32 word› and ae af :: ‹1 word›
by (auto dest!: aal_assn_boundsD' bspec[of _ _ ‹bb ! a›])
sepref_def pre_simplify_clause_lookup_impl
is ‹uncurry3 pre_simplify_clause_lookup'›
:: ‹[λ(((i,xs),_),_). i < length xs]⇩a
sint64_nat_assn⇧k *⇩a clauses_ll_assn⇧k *⇩a clause_ll_assn⇧d *⇩a marked_struct_assn⇧d →
bool1_assn ×⇩a clause_ll_assn ×⇩a marked_struct_assn›
supply [intro] = pre_simplify_clause_lookup'I
unfolding pre_simplify_clause_lookup_def pre_simplify_clause_lookup'_def
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
by (annot_snat_const ‹TYPE(64)›)
sepref
definition pre_simplify_clause_lookup_st' where
‹pre_simplify_clause_lookup_st' i xs = pre_simplify_clause_lookup_st (xs ! i)›
lemma pre_simplify_clause_lookup_st_alt_def:
‹pre_simplify_clause_lookup_st = (λC E S⇩0. do {
let (mark, S) = extract_marked_wl_heur_init S⇩0;
(tauto, C, mark) ← pre_simplify_clause_lookup C E mark;
RETURN (tauto, C, (IsaSAT_Init.update_o mark S))
})›
by (auto simp: isasat_init_getters_and_setters_def pre_simplify_clause_lookup_st_def
intro!: ext split: tuple15.splits)
sepref_register pre_simplify_clause_lookup' pre_simplify_clause_lookup_st'
sepref_def pre_simplify_clause_lookup_st_impl
is ‹uncurry3 pre_simplify_clause_lookup_st'›
:: ‹[λ(((i,xs),_),_). i < length xs]⇩a
sint64_nat_assn⇧k *⇩a clauses_ll_assn⇧k *⇩a clause_ll_assn⇧d *⇩a isasat_init_assn⇧d →
bool1_assn ×⇩a clause_ll_assn ×⇩a isasat_init_assn›
unfolding pre_simplify_clause_lookup_st_alt_def
fold_tuple_optimizations pre_simplify_clause_lookup_st'_def
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
pre_simplify_clause_lookup'_def[symmetric]
by sepref
definition init_dt_step_wl_heur_b'
:: ‹nat clause_l list ⇒ nat ⇒ twl_st_wl_heur_init × _ ⇒ (twl_st_wl_heur_init × _) nres› where
‹init_dt_step_wl_heur_b' C i = init_dt_step_wl_heur_b (C!i)›
definition add_tautology_to_clauses' where
‹add_tautology_to_clauses' = (λS.
RETURN S)›
lemma add_tautology_to_clauses_alt_def:
‹add_tautology_to_clauses C S = add_tautology_to_clauses' S›
by (cases S) (auto simp: add_tautology_to_clauses'_def add_tautology_to_clauses_def)
sepref_def add_tautology_to_clauses'_impl
is add_tautology_to_clauses'
:: ‹isasat_init_assn⇧d →⇩a isasat_init_assn›
unfolding add_tautology_to_clauses'_def
by sepref
sepref_def init_dt_step_wl_code_b
is ‹uncurry2 (init_dt_step_wl_heur_b')›
:: ‹[λ((xs, i), S). i < length xs]⇩a
(clauses_ll_assn)⇧k *⇩a sint64_nat_assn⇧k *⇩a (isasat_init_assn ×⇩a clause_ll_assn)⇧d →
isasat_init_assn ×⇩a clause_ll_assn›
supply [[goals_limit=1]]
supply polarity_None_undefined_lit[simp] polarity_st_init_def[simp]
option.splits[split] get_conflict_wl_is_None_heur_init_alt_def[simp]
tri_bool_eq_def[simp]
unfolding init_dt_step_wl_heur_def PR_CONST_def
init_dt_step_wl_heur_b_def
list_length_1_def is_Nil_length init_dt_step_wl_heur_b'_def
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
already_propagated_unit_cls_heur'_alt
add_clause_to_others_heur'_def[symmetric]
add_clause_to_others_heur'_alt
already_propagated_unit_cls_heur_b_def[symmetric]
propagate_unit_cls_heur_b_def[symmetric]
conflict_propagated_unit_cls_heur_b_def[symmetric]
pre_simplify_clause_lookup_st'_def[symmetric]
add_tautology_to_clauses_alt_def
add_init_cls_heur_b_def[symmetric]
unfolding watched_app_def[symmetric]
unfolding nth_rll_def[symmetric]
unfolding is_Nil_length get_conflict_wl_is_None_init
polarity_st_heur_init_alt_def[symmetric]
get_conflict_wl_is_None_heur_init_alt_def[symmetric]
SET_TRUE_def[symmetric] SET_FALSE_def[symmetric] UNSET_def[symmetric]
tri_bool_eq_def[symmetric] polarity_st_heur_init_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register init_dt_wl_heur_unb
abbreviation isasat_atms_ext_rel_assn where
‹isasat_atms_ext_rel_assn ≡ larray64_assn uint64_nat_assn ×⇩a uint32_nat_assn ×⇩a
arl64_assn atom_assn›
abbreviation nat_lit_list_hm_assn where
‹nat_lit_list_hm_assn ≡ hr_comp isasat_atms_ext_rel_assn isasat_atms_ext_rel›
sepref_def init_next_size_impl
is ‹RETURN o init_next_size›
:: ‹[λL. L ≤ unat32_max div 2]⇩a sint64_nat_assn⇧k → sint64_nat_assn›
unfolding init_next_size_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def nat_lit_lits_init_assn_assn_in
is ‹uncurry add_to_atms_ext›
:: ‹atom_assn⇧k *⇩a isasat_atms_ext_rel_assn⇧d →⇩a isasat_atms_ext_rel_assn›
supply [[goals_limit=1]]
unfolding add_to_atms_ext_def length_uint32_nat_def
apply (rewrite at ‹max ⌑ _› value_of_atm_def[symmetric])
apply (rewrite at ‹⌑ < _› value_of_atm_def[symmetric])
apply (rewrite at ‹list_grow _ (init_next_size ⌑)› value_of_atm_def[symmetric])
apply (rewrite at ‹list_grow _ (init_next_size ⌑)› index_of_atm_def[symmetric])
apply (rewrite at ‹⌑ < _› annot_unat_unat_upcast[where 'l=64])
unfolding max_def list_grow_alt
op_list_grow_init'_alt
apply (annot_all_atm_idxs)
apply (rewrite at ‹op_list_grow_init ⌑› unat_const_fold[where 'a=64])
apply (rewrite at ‹_ < ⌑› annot_snat_unat_conv)
apply (annot_unat_const ‹TYPE(64)›)
by sepref
lemma [sepref_fr_rules]:
‹(uncurry nat_lit_lits_init_assn_assn_in, uncurry (RETURN ∘∘ op_set_insert))
∈ [λ(a, b). a ≤ unat32_max div 2]⇩a
atom_assn⇧k *⇩a nat_lit_list_hm_assn⇧d → nat_lit_list_hm_assn›
by (rule nat_lit_lits_init_assn_assn_in.refine[FCOMP add_to_atms_ext_op_set_insert
[unfolded op_set_insert_def[symmetric]]])
hide_const (open) NEMonad.ASSERT NEMonad.RETURN
lemma while_nfoldli:
"do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} ≤ nfoldli l c f σ"
apply (induct l arbitrary: σ)
apply (subst WHILET_unfold)
apply (simp add: FOREACH_cond_def)
apply (subst WHILET_unfold)
apply (auto
simp: FOREACH_cond_def FOREACH_body_def
intro: bind_mono Refine_Basic.bind_mono(1))
done
where
‹extract_atms_cls_i' C i = extract_atms_cls_i (C!i)›
sepref_def
is ‹uncurry2 extract_atms_cls_i'›
:: ‹[λ((N, i), _). i < length N]⇩a
(clauses_ll_assn)⇧k *⇩a sint64_nat_assn⇧k *⇩a nat_lit_list_hm_assn⇧d → nat_lit_list_hm_assn›
supply [dest!] = aal_assn_boundsD'
unfolding extract_atms_cls_i_def extract_atms_cls_i'_def
apply (subst nfoldli_by_idx[abs_def])
unfolding nfoldli_upt_by_while
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
sepref
declare extract_atms_cls_imp.refine[sepref_fr_rules]
sepref_def
is ‹uncurry extract_atms_clss_i›
:: ‹(clauses_ll_assn)⇧k *⇩a nat_lit_list_hm_assn⇧d →⇩a nat_lit_list_hm_assn›
supply [dest] = aal_assn_boundsD'
unfolding extract_atms_clss_i_def
apply (subst nfoldli_by_idx)
unfolding nfoldli_upt_by_while Let_def extract_atms_cls_i'_def[symmetric]
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
op_list_list_len_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
sepref
lemma [sepref_fr_rules]:
‹(uncurry extract_atms_clss_imp, uncurry (RETURN ∘∘ extract_atms_clss))
∈ [λ(a, b). ∀C∈set a. ∀L∈set C. nat_of_lit L ≤ unat32_max]⇩a
(clauses_ll_assn)⇧k *⇩a nat_lit_list_hm_assn⇧d → nat_lit_list_hm_assn›
using extract_atms_clss_imp.refine[FCOMP extract_atms_clss_i_extract_atms_clss]
by simp
sepref_def
is ‹uncurry0 extract_atms_clss_imp_empty_rel›
:: ‹unit_assn⇧k →⇩a isasat_atms_ext_rel_assn›
unfolding extract_atms_clss_imp_empty_rel_def
larray_fold_custom_replicate
supply [[goals_limit=1]]
apply (rewrite at ‹(_, _, ⌑)› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹(⌑, _, _)› annotate_assn[where A=‹larray64_assn uint64_nat_assn›])
apply (rewrite in ‹(⌑, _, _)› snat_const_fold[where 'a=64])
apply (rewrite in ‹(_, ⌑, _)› unat_const_fold[where 'a=32])
apply (annot_unat_const ‹TYPE(64)›)
sepref
lemma [sepref_fr_rules]:
‹(uncurry0 extract_atms_clss_imp_empty_assn, uncurry0 (RETURN op_extract_list_empty))
∈ unit_assn⇧k →⇩a nat_lit_list_hm_assn›
using extract_atms_clss_imp_empty_assn.refine[unfolded uncurry0_def, FCOMP extract_atms_clss_imp_empty_rel
]
unfolding uncurry0_def
by simp
lemma :
‹extract_atms_clss_imp_empty_rel = (RETURN (op_larray_custom_replicate 1024 0, 0, []))›
by (auto simp: extract_atms_clss_imp_empty_rel_def)
subsubsection ‹Full Initialisation›
lemma rewatch_heur_st_init_alt_def:
‹rewatch_heur_st_init = (λS⇩0. do {
let (vdom, S) = extract_vdom_wl_heur_init S⇩0;
ASSERT (vdom = get_vdom_heur_init S⇩0);
let (arena, S) = extract_arena_wl_heur_init S;
ASSERT (arena = get_clauses_wl_heur_init S⇩0);
let (W, S) = extract_watchlist_wl_heur_init S;
ASSERT(length (vdom) ≤ length arena);
W ← rewatch_heur vdom arena W;
RETURN (IsaSAT_Init.update_e W (IsaSAT_Init.update_b arena (IsaSAT_Init.update_k vdom S)))
})›
by (auto simp: rewatch_heur_st_init_def isasat_init_getters_and_setters_def split: tuple15.splits
intro!: ext)
sepref_def rewatch_heur_st_fast_code
is ‹(rewatch_heur_st_init)›
:: ‹[rewatch_heur_st_fast_pre]⇩a
isasat_init_assn⇧d → isasat_init_assn›
supply [[goals_limit=1]]
unfolding rewatch_heur_st_init_alt_def PR_CONST_def rewatch_heur_st_fast_pre_def
rewatch_heur_st_fast_def
by sepref
declare
rewatch_heur_st_fast_code.refine[sepref_fr_rules]
sepref_register rewatch_heur_st init_dt_step_wl_heur
sepref_def init_dt_wl_heur_code_b
is ‹uncurry (init_dt_wl_heur_b)›
:: ‹(clauses_ll_assn)⇧k *⇩a isasat_init_assn⇧d →⇩a
isasat_init_assn›
supply [[goals_limit=1]]
unfolding init_dt_wl_heur_def PR_CONST_def init_dt_step_wl_heur_b_def[symmetric] if_True
init_dt_wl_heur_b_def
apply (subst nfoldli_by_idx[abs_def])
unfolding nfoldli_upt_by_while op_list_list_len_def[symmetric] Let_def
init_dt_step_wl_heur_b'_def[symmetric]
apply (rewrite at ‹(_, _, ⌑)› al_fold_custom_empty[where 'l=64])
apply (annot_snat_const ‹TYPE(64)›)
by sepref
where
‹extract_lits_sorted' xs n vars = extract_lits_sorted (xs, n, vars)›
lemma :
‹extract_lits_sorted = (λ(xs, n, vars). do {res ← extract_lits_sorted' xs n vars; mop_free xs; RETURN res})›
by (auto simp: extract_lits_sorted'_def mop_free_def intro!: ext)
sepref_def (in -)
is ‹uncurry2 extract_lits_sorted'›
:: ‹[λ((xs, n), vars). (∀x∈#mset vars. x < length xs)]⇩a
(larray64_assn uint64_nat_assn)⇧k *⇩a uint32_nat_assn⇧k *⇩a
(arl64_assn atom_assn)⇧d →
arl64_assn atom_assn ×⇩a uint32_nat_assn›
unfolding extract_lits_sorted'_def extract_lits_sorted_def nres_monad1
prod.case
sepref
lemmas [sepref_fr_rules] = extract_lits_sorted'_impl.refine
sepref_def (in -)
is ‹extract_lits_sorted›
:: ‹[λ(xs, n, vars). (∀x∈#mset vars. x < length xs)]⇩a
isasat_atms_ext_rel_assn⇧d →
arl64_assn atom_assn ×⇩a uint32_nat_assn›
apply (subst extract_lits_sorted_extract_lits_sorted')
unfolding extract_lits_sorted'_def extract_lits_sorted_def nres_monad1
prod.case
supply [[goals_limit = 1]]
supply mset_eq_setD[dest] mset_eq_length[dest]
sepref
declare extract_lits_sorted_code.refine[sepref_fr_rules]
abbreviation lits_with_max_assn where
‹lits_with_max_assn ≡ hr_comp (arl64_assn atom_assn ×⇩a uint32_nat_assn) lits_with_max_rel›
lemma [sepref_fr_rules]:
‹(extract_lits_sorted_code, RETURN ∘ mset_set) ∈ nat_lit_list_hm_assn⇧d →⇩a lits_with_max_assn›
(is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
have H: ‹hrr_comp isasat_atms_ext_rel
(λ_. al_assn atom_assn ×⇩a unat_assn) (λ_. lits_with_max_rel) =
(λ_. lits_with_max_assn)›
by (auto simp: hrr_comp_def intro!: ext)
have H: ‹?c
∈ [comp_PRE isasat_atms_ext_rel (λ_. True)
(λ_ (xs, n, vars). ∀x∈#mset vars. x < length xs) (λ_. True)]⇩a
hrp_comp (isasat_atms_ext_rel_assn⇧d) isasat_atms_ext_rel → lits_with_max_assn›
(is ‹_ ∈ [?pre']⇩a ?im' → ?f'›)
using hfref_compI_PRE_aux[OF extract_lits_sorted_code.refine
extract_lits_sorted_mset_set]
unfolding H
by auto
have pre: ‹?pre' x› if ‹?pre x› for x
using that by (auto simp: comp_PRE_def isasat_atms_ext_rel_def init_valid_rep_def)
have im: ‹?im' = ?im›
unfolding prod_hrp_comp hrp_comp_dest hrp_comp_keep by simp
show ?thesis
apply (rule hfref_weaken_pre[OF ])
defer
using H unfolding im PR_CONST_def apply assumption
using pre ..
qed
definition INITIAL_OUTL_SIZE :: ‹nat› where
[simp]: ‹INITIAL_OUTL_SIZE = 160›
sepref_def INITIAL_OUTL_SIZE_impl
is ‹uncurry0 (RETURN INITIAL_OUTL_SIZE)›
:: ‹unit_assn⇧k →⇩a sint64_nat_assn›
unfolding INITIAL_OUTL_SIZE_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition atom_of_value :: ‹nat ⇒ nat› where [simp]: ‹atom_of_value x = x›
lemma atom_of_value_simp_hnr:
‹(∃x. (↑(x = unat xi ∧ P x) ∧* ↑(x = unat xi)) s) =
(∃x. (↑(x = unat xi ∧ P x)) s)›
‹(∃x. (↑(x = unat xi ∧ P x)) s) = (↑(P (unat xi))) s›
unfolding import_param_3[symmetric]
by (auto simp: pred_lift_extract_simps)
lemma atom_of_value_hnr[sepref_fr_rules]:
‹(Mreturn o (λx. x), RETURN o atom_of_value) ∈ [λn. n < 2 ^31]⇩a (uint32_nat_assn)⇧d → atom_assn›
apply sepref_to_hoare
apply vcg'
apply (auto simp: unat_rel_def atom_rel_def unat.rel_def br_def ENTAILS_def
atom_of_value_simp_hnr pure_true_conv Defer_Slot.remove_slot)
apply (rule Defer_Slot.remove_slot)
done
sepref_register atom_of_value
lemma [sepref_gen_algo_rules]: ‹GEN_ALGO (Pos 0) (is_init unat_lit_assn)›
by (auto simp: unat_lit_rel_def is_init_def unat_rel_def unat.rel_def
br_def nat_lit_rel_def GEN_ALGO_def)
schematic_goal mk_free_lbd_assn[sepref_frame_free_rules]: ‹MK_FREE marked_struct_assn ?fr›
unfolding marked_struct_assn_def
by synthesize_free
sepref_def reduce_interval_init_impl
is ‹uncurry0 (RETURN reduce_interval_init)›
:: ‹unit_assn⇧k →⇩a word64_assn›
unfolding reduce_interval_init_def
by sepref
sepref_def inprocessing_interval_init_impl
is ‹uncurry0 (RETURN inprocessing_interval_init)›
:: ‹unit_assn⇧k →⇩a word_assn›
unfolding inprocessing_interval_init_def
by sepref
sepref_def rephasing_end_of_initial_phase_impl
is ‹uncurry0 (RETURN rephasing_end_of_initial_phase)›
:: ‹unit_assn⇧k →⇩a word_assn›
unfolding rephasing_end_of_initial_phase_def
by sepref
sepref_def rephasing_initial_phase_impl
is ‹uncurry0 (RETURN rephasing_initial_phase)›
:: ‹unit_assn⇧k →⇩a word_assn›
unfolding rephasing_initial_phase_def
by sepref
sepref_def subsuming_length_initial_phase_impl
is ‹uncurry0 (RETURN subsuming_length_initial_phase)›
:: ‹unit_assn⇧k →⇩a word_assn›
unfolding subsuming_length_initial_phase_def
by sepref
definition empty_heuristics_stats :: ‹_ ⇒ _ ⇒ restart_heuristics› where
‹empty_heuristics_stats opts φ = (
let fema = ema_init (opts_fema opts) in
let sema = ema_init (opts_sema opts) in let ccount = restart_info_init in
let n = (length φ) in
(fema, sema, ccount, 0, (φ, 0, replicate n False, 0, replicate n False, rephasing_end_of_initial_phase, 0, rephasing_initial_phase),
reluctant_init, False, replicate n False, (inprocessing_interval_init, reduce_interval_init, subsuming_length_initial_phase), fema, sema))›
sepref_def empty_heuristics_stats_impl
is ‹uncurry (RETURN oo empty_heuristics_stats)›
:: ‹opts_assn⇧k *⇩a phase_saver_assn⇧d →⇩a heuristic_int_assn›
supply [[goals_limit=1]]
unfolding heuristic_int_assn_def empty_heuristics_stats_def phase_heur_assn_def
apply (rewrite at ‹replicate _ False› annotate_assn[where A=phase_saver'_assn])
apply (rewrite in ‹replicate _ False› array_fold_custom_replicate)
apply (rewrite at ‹replicate _ False› annotate_assn[where A=phase_saver'_assn])
apply (rewrite in ‹replicate _ False› array_fold_custom_replicate)
apply (rewrite at ‹replicate _ False› annotate_assn[where A=phase_saver_assn])
apply (rewrite in ‹replicate _ False› larray_fold_custom_replicate)
by sepref
lemma finalise_init_code_alt_def:
‹finalise_init_code opts =
(λS. case S of Tuple15 M' N' D' Q' W' vm φ clvls cach
lbd vdom ivdom failed lcount mark ⇒ do {
let init_stats = empty_stats_clss (of_nat(length ivdom));
let heur = empty_heuristics_stats opts φ;
mop_free mark; mop_free failed;
let occs = replicate (length W') [];
vm ← finalize_bump_init vm;
RETURN (IsaSAT M' N' D' Q' W' vm
clvls cach lbd (take 1(replicate 160 (Pos 0))) init_stats
(Restart_Heuristics heur) (AIvdom_init vdom [] ivdom) lcount opts [] occs)
})›
unfolding finalise_init_code_def mop_free_def empty_heuristics_stats_def
by (auto simp: Let_def split: prod.splits tuple15.splits intro!: ext)
sepref_def finalize_vmtf_init_code
is ‹finalize_vmtf_init›
:: ‹vmtf_init_assn⇧d →⇩a vmtf_assn›
unfolding finalize_vmtf_init_def vmtf_init_assn_def vmtf_assn_def atom.fold_option
by sepref
sepref_def finalize_bump_init_code
is ‹finalize_bump_init›
:: ‹heuristic_bump_init_assn⇧d →⇩a heuristic_bump_assn›
unfolding finalize_bump_init_def
by sepref
sepref_def finalise_init_code'
is ‹uncurry finalise_init_code›
:: ‹[λ(_, S). length (get_clauses_wl_heur_init S) ≤ snat64_max]⇩a
opts_assn⇧d *⇩a isasat_init_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]] of_nat_snat[sepref_import_param]
unfolding finalise_init_code_alt_def isasat_init_assn_def
INITIAL_OUTL_SIZE_def[symmetric]
phase_heur_assn_def op_list_list_len_def[symmetric]
apply (rewrite at ‹Pos ⌑› unat_const_fold[where 'a=32])
apply (rewrite at ‹Pos ⌑› atom_of_value_def[symmetric])
apply (rewrite at ‹take ⌑› snat_const_fold[where 'a=64])
apply (rewrite at ‹AIvdom_init _ ⌑ _› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹IsaSAT _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⌑ _› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹take _ ⌑› al_fold_custom_replicate)
apply (rewrite in ‹replicate _ []› aal_fold_custom_empty(1)[where 'l=64 and 'll=64])
by sepref
sepref_register initialise_VMTF
sepref_def init_trail_D_fast_code
is ‹uncurry2 init_trail_D_fast›
:: ‹(arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a trail_pol_fast_assn›
unfolding init_trail_D_def PR_CONST_def init_trail_D_fast_def trail_pol_fast_assn_def
apply (rewrite in ‹let _ = ⌑ in _› annotate_assn[where A=‹arl64_assn unat_lit_assn›])
apply (rewrite in ‹let _ = ⌑ in _› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹let _ = _; _ = ⌑ in _› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹let _ = _; _ = ⌑ in _› annotate_assn[where A=‹arl64_assn uint32_nat_assn›])
apply (rewrite in ‹let _ = _;_ = ⌑ in _› annotate_assn[where A=‹larray64_assn (tri_bool_assn)›])
apply (rewrite in ‹let _ = _;_ = _;_ = ⌑ in _› annotate_assn[where A=‹larray64_assn uint32_nat_assn›])
apply (rewrite in ‹let _ = _ in _› larray_fold_custom_replicate)
apply (rewrite in ‹let _ = _ in _› larray_fold_custom_replicate)
apply (rewrite in ‹let _ = _ in _› larray_fold_custom_replicate)
apply (rewrite at ‹(_, ⌑, _)› unat_const_fold[where 'a=32])
apply (rewrite at ‹(op_larray_custom_replicate _ ⌑)› unat_const_fold[where 'a=32])
apply (rewrite at ‹(_, _, _, _, ⌑)› snat_const_fold[where 'a=64])
apply (annot_snat_const ‹TYPE(64)›)
supply [[goals_limit = 1]]
by sepref
declare init_trail_D_fast_code.refine[sepref_fr_rules]
definition empty_mark_struct :: ‹nat ⇒ nat × bool option list› where
‹empty_mark_struct (n::nat) = (0::nat, replicate n NoMark)›
sepref_def empty_mark_struct_impl
is ‹RETURN o empty_mark_struct›
:: ‹sint64_nat_assn⇧k →⇩a marked_struct_assn›
unfolding empty_mark_struct_def marked_struct_assn_def
apply (rewrite at ‹(⌑, replicate _ NoMark)› unat_const_fold[where 'a=32])
unfolding array_fold_custom_replicate
by sepref
definition combine_conflict where
‹combine_conflict x = x›
sepref_def combine_conflict_impl
is ‹RETURN o combine_conflict›
:: ‹(bool1_assn ×⇩a unat32_assn ×⇩a IICF_Array.array_assn option_bool_impl_assn)⇧d →⇩a conflict_option_rel_assn›
unfolding combine_conflict_def conflict_option_rel_assn_def lookup_clause_rel_assn_def
by sepref
definition combine_ccach where
‹combine_ccach x = x›
sepref_def combine_ccach_impl
is ‹RETURN o combine_ccach›
:: ‹(array_assn minimize_status_assn ×⇩a arl64_assn atom_assn)⇧d →⇩a cach_refinement_l_assn›
unfolding combine_ccach_def cach_refinement_l_assn_def
by sepref
definition combine_lcount where
‹combine_lcount x = x›
sepref_def combine_lcount_impl
is ‹RETURN o combine_lcount›
:: ‹(uint64_nat_assn ×⇩a uint64_nat_assn ×⇩a uint64_nat_assn ×⇩a uint64_nat_assn ×⇩a uint64_nat_assn)⇧k →⇩a lcount_assn›
unfolding combine_lcount_def lcount_assn_def
by sepref
sepref_register empty_mark_struct combine_conflict combine_ccach combine_lcount
lemma init_state_wl_D'_alt_def:
‹init_state_wl_D' = (λ(𝒜⇩i⇩n, n). do {
ASSERT(Suc (2 * (n)) ≤ unat32_max);
let n = Suc (n);
let m = 2 * n;
M ← init_trail_D 𝒜⇩i⇩n n m;
let N = [];
let D = combine_conflict (True, 0, replicate n NOTIN);
let mark = (0, replicate n None);
let WS = replicate m [];
vm ← initialize_Bump_Init 𝒜⇩i⇩n n;
let φ = replicate n False;
let cach = combine_ccach (replicate n SEEN_UNKNOWN, []);
let lbd = empty_lbd;
let vdom = [];
let ivdom = [];
let lcount = combine_lcount (0, 0, 0, 0, 0);
RETURN (Tuple15 M N D 0 WS vm φ 0 cach lbd vdom ivdom False lcount mark)
})›
unfolding combine_conflict_def combine_ccach_def init_state_wl_D'_def combine_lcount_def by auto
sepref_definition init_state_wl_D'_code
is ‹init_state_wl_D'›
:: ‹(arl64_assn atom_assn ×⇩a uint32_nat_assn)⇧k →⇩a isasat_init_assn›
supply[[goals_limit=1]]
unfolding init_state_wl_D'_alt_def PR_CONST_def init_trail_D_fast_def[symmetric] Suc_eq_plus1_left
NoMark_def[symmetric] empty_mark_struct_def[symmetric] of_nat_snat[sepref_import_param]
apply (rewrite at ‹let _ = 1 + ⌑ in _› annot_unat_snat_upcast[where 'l=64])
apply (rewrite at ‹let _ = combine_ccach (_, ⌑) in _› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹let _ = combine_ccach (⌑,_) in _› annotate_assn[where A= ‹array_assn minimize_status_assn›])
apply (rewrite at ‹let _ = combine_ccach (_, ⌑) in _› annotate_assn[where A= ‹arl64_assn atom_assn›])
apply (rewrite in ‹replicate _ []› aal_fold_custom_empty(1)[where 'l=64 and 'll=64])
apply (rewrite at ‹let _= _; _= ⌑ in _› annotate_assn[where A=‹watchlist_fast_assn›])
apply (rewrite at ‹let _= ⌑; _=_;_=_;_ = _;_=_; _ = _ in RETURN _› annotate_assn[where A=‹phase_saver_assn›])
apply (rewrite in ‹let _= ⌑; _=_;_=_;_ = _; _= _; _=_ in RETURN _› larray_fold_custom_replicate)
apply (rewrite in ‹let _= combine_conflict(True, _, ⌑) in _› array_fold_custom_replicate)
unfolding array_fold_custom_replicate
apply (rewrite at ‹let _ = ⌑ in let _ = combine_conflict (True, _, _) in _› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹let _= combine_conflict (True, ⌑, _) in _› unat_const_fold[where 'a=32])
apply (rewrite at ‹let _ = ⌑ in _› annotate_assn[where A=‹arena_fast_assn›])
apply (rewrite at ‹let _= ⌑; _ = _ ; _ =_ in RETURN _› annotate_assn[where A = ‹vdom_fast_assn›])
apply (rewrite at ‹let _= ⌑; _ = _ in RETURN _› annotate_assn[where A = ‹vdom_fast_assn›])
apply (rewrite in ‹let _= ⌑; _=_; _ = _ in RETURN _› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹let _= ⌑; _ = _ in RETURN _› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹Tuple15 _ _ _ _ _ _ _ ⌑› unat_const_fold[where 'a=32])
apply (rewrite at ‹let _ = combine_lcount (⌑, _, _) in RETURN _› unat_const_fold[where 'a=64])
apply (rewrite at ‹let _ = combine_lcount (_, ⌑, _) in RETURN _› unat_const_fold[where 'a=64])
apply (rewrite at ‹let _ = combine_lcount ( _, _, ⌑, _) in RETURN _› unat_const_fold[where 'a=64])
apply (rewrite at ‹let _ = combine_lcount ( _, _, _, ⌑, _) in RETURN _› unat_const_fold[where 'a=64])
apply (rewrite at ‹let _ = combine_lcount ( _, _, _, _, ⌑) in RETURN _› unat_const_fold[where 'a=64])
apply (annot_snat_const ‹TYPE(64)›)
apply (rewrite at ‹RETURN ⌑› annotate_assn[where A=‹isasat_init_assn›])
by sepref
declare init_state_wl_D'_code.refine[sepref_fr_rules]
lemma to_init_state_code_hnr:
‹(Mreturn o to_init_state_code, RETURN o id) ∈ isasat_init_assn⇧d →⇩a isasat_init_assn›
unfolding to_init_state_code_def
by sepref_to_hoare vcg'
abbreviation (in -)lits_with_max_assn_clss where
‹lits_with_max_assn_clss ≡ hr_comp lits_with_max_assn (⟨nat_rel⟩mset_rel)›
lemmas [unfolded Tuple15_LLVM.inline_direct_return_node_case, llvm_code] =
get_conflict_wl_is_None_init_code_def[unfolded IsaSAT_Init.read_all_st_code_def]
lemmas [llvm_code] =
init_state_wl_D'_code_def[unfolded comp_def]
lemmas [unfolded Tuple15_LLVM.inline_direct_return_node_case, llvm_code] =
get_conflict_wl_is_None_init_code_def[unfolded IsaSAT_Init.read_all_st_code_def]
schematic_goal mk_free_isasat_init_assn[sepref_frame_free_rules]: ‹MK_FREE isasat_init_assn ?fr›
unfolding isasat_init_assn_def
by synthesize_free+
experiment
begin
export_llvm init_state_wl_D'_code
rewatch_heur_st_fast_code
init_dt_wl_heur_code_b
init_state_wl_D'_code
end
end