theory IsaSAT_Initialisation_LLVM
imports IsaSAT_Setup_LLVM IsaSAT_VMTF_LLVM Watched_Literals.Watched_Literals_Watch_List_Initialisation
Watched_Literals.Watched_Literals_Watch_List_Initialisation
IsaSAT_Initialisation
begin
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"
type_synonym (in -)vmtf_assn_option_fst_As =
‹vmtf_node_assn ptr × 64 word × 32 word × 32 word × 32 word›
type_synonym (in -)vmtf_remove_assn_option_fst_As =
‹vmtf_assn_option_fst_As × (32 word array_list64) × 1 word ptr›
abbreviation (in -) vmtf_conc_option_fst_As :: ‹_ ⇒ _ ⇒ llvm_amemory ⇒ bool› where
‹vmtf_conc_option_fst_As ≡ (array_assn vmtf_node_assn ×⇩a uint64_nat_assn ×⇩a
atom.option_assn ×⇩a atom.option_assn ×⇩a atom.option_assn)›
abbreviation vmtf_remove_conc_option_fst_As
:: ‹isa_vmtf_remove_int_option_fst_As ⇒ vmtf_remove_assn_option_fst_As ⇒ assn›
where
‹vmtf_remove_conc_option_fst_As ≡ vmtf_conc_option_fst_As ×⇩a distinct_atoms_assn›
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
type_synonym (in -)twl_st_wll_trail_init =
‹trail_pol_fast_assn × arena_assn × option_lookup_clause_assn ×
64 word × watched_wl_uint32 × vmtf_remove_assn_option_fst_As × phase_saver_assn ×
32 word × cach_refinement_l_assn × lbd_assn × vdom_fast_assn × 1 word›
definition isasat_init_assn
:: ‹twl_st_wl_heur_init ⇒ trail_pol_fast_assn × arena_assn × option_lookup_clause_assn ×
64 word × watched_wl_uint32 × _ × phase_saver_assn ×
32 word × cach_refinement_l_assn × lbd_assn × vdom_fast_assn × 1 word ⇒ assn›
where
‹isasat_init_assn =
trail_pol_fast_assn ×⇩a arena_fast_assn ×⇩a
conflict_option_rel_assn ×⇩a
sint64_nat_assn ×⇩a
watchlist_fast_assn ×⇩a
vmtf_remove_conc_option_fst_As ×⇩a phase_saver_assn ×⇩a
uint32_nat_assn ×⇩a
cach_refinement_l_assn ×⇩a
lbd_assn ×⇩a
vdom_fast_assn ×⇩a
bool1_assn›
sepref_def initialise_VMTF_code
is ‹uncurry initialise_VMTF›
:: ‹[λ(N, n). True]⇩a (arl64_assn atom_assn)⇧k *⇩a sint64_nat_assn⇧k → vmtf_remove_conc_option_fst_As›
unfolding initialise_VMTF_def vmtf_cons_def Suc_eq_plus1 atom.fold_option length_uint32_nat_def
option.case_eq_if
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
declare initialise_VMTF_code.refine[sepref_fr_rules]
sepref_register cons_trail_Propagated_tr
sepref_def propagate_unit_cls_code
is ‹uncurry (propagate_unit_cls_heur)›
:: ‹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_def isasat_init_assn_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' where
‹already_propagated_unit_cls_heur' = (λ(M, N, D, Q, oth).
RETURN (M, N, D, Q, oth))›
lemma already_propagated_unit_cls_heur'_alt:
‹already_propagated_unit_cls_heur L = already_propagated_unit_cls_heur'›
unfolding already_propagated_unit_cls_heur_def already_propagated_unit_cls_heur'_def
by auto
sepref_def already_propagated_unit_cls_code
is ‹already_propagated_unit_cls_heur'›
:: ‹isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding already_propagated_unit_cls_heur'_def isasat_init_assn_def
PR_CONST_def
by sepref
declare already_propagated_unit_cls_code.refine[sepref_fr_rules]
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]
sepref_def conflict_propagated_unit_cls_code
is ‹uncurry (conflict_propagated_unit_cls_heur)›
:: ‹unat_lit_assn⇧k *⇩a isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding conflict_propagated_unit_cls_heur_def isasat_init_assn_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 uint32_max)› and
‹2 ≤ length at'› and
‹length a1'j ≤ length a1'a› and
‹length a1'a ≤ sint64_max - length at' - 5›
shows ‹append_and_length_fast_code_pre ((True, at'), a1'a)› ‹5 ≤ sint64_max - length at'›
using assms unfolding append_and_length_fast_code_pre_def
by (auto simp: uint64_max_def uint32_max_def sint64_max_def)
lemma add_init_cls_code_bI2:
assumes
‹length at' ≤ Suc (Suc uint32_max)›
shows ‹5 ≤ sint64_max - length at'›
using assms unfolding append_and_length_fast_code_pre_def
by (auto simp: uint64_max_def uint32_max_def sint64_max_def)
lemma add_init_clss_codebI:
assumes
‹length at' ≤ Suc (Suc uint32_max)› and
‹2 ≤ length at'› and
‹length a1'j ≤ length a1'a› and
‹length a1'a ≤ uint64_max - (length at' + 5)›
shows ‹length a1'j < uint64_max›
using assms by (auto simp: uint64_max_def uint32_max_def)
abbreviation clauses_ll_assn where
‹clauses_ll_assn ≡ aal_assn' TYPE(64) TYPE(64) unat_lit_assn›
definition fm_add_new_fast' where
‹fm_add_new_fast' b C i = fm_add_new_fast b (C!i)›
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 ‹uncurry3 fm_add_new_fast'›
:: ‹[λ(((b, C), i), N). i < length C ∧ append_and_length_fast_code_pre ((b, C!i), N)]⇩a
bool1_assn⇧k *⇩a clauses_ll_assn⇧k *⇩a sint64_nat_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]
supply [split] = if_splits
unfolding fm_add_new_fast_def fm_add_new_def append_and_length_fast_code_pre_def
fm_add_new_fast'_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 "AActivity ⌑" unat_const_fold[where 'a=32])+
apply (rewrite at "APos ⌑" unat_const_fold[where 'a=32])+
apply (rewrite at "op_list_list_llen _ _ - 2" annot_snat_unat_downcast[where 'l=32])
apply (annot_snat_const "TYPE(64)")
by sepref
sepref_register fm_add_new_fast'
sepref_def add_init_cls_code_b
is ‹uncurry2 add_init_cls_heur_b'›
:: ‹[λ((xs, i), S). i < length xs]⇩a
(clauses_ll_assn)⇧k *⇩a sint64_nat_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_def add_init_cls_heur_b_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 isasat_init_assn_def
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]
fm_add_new_fast'_def[symmetric]
apply (annot_snat_const "TYPE(64)")
by sepref
declare
add_init_cls_code_b.refine[sepref_fr_rules]
sepref_def already_propagated_unit_cls_conflict_code
is ‹uncurry already_propagated_unit_cls_conflict_heur›
:: ‹unat_lit_assn⇧k *⇩a isasat_init_assn⇧d →⇩a isasat_init_assn›
supply [[goals_limit=1]]
unfolding already_propagated_unit_cls_conflict_heur_def isasat_init_assn_def
PR_CONST_def
by sepref
declare already_propagated_unit_cls_conflict_code.refine[sepref_fr_rules]
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
declare set_conflict_empty_code.refine[sepref_fr_rules]
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_def isasat_init_assn_def
conflict_option_rel_assn_def lookup_clause_rel_assn_def
by sepref
declare set_empty_clause_as_conflict_code.refine[sepref_fr_rules]
definition (in -) add_clause_to_others_heur'
:: ‹twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_clause_to_others_heur' = (λ (M, N, D, Q, NS, US, WS).
RETURN (M, N, D, Q, NS, US, WS))›
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
..
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 isasat_init_assn_def add_clause_to_others_heur'_def
by sepref
declare add_clause_to_others_code.refine[sepref_fr_rules]
sepref_def get_conflict_wl_is_None_init_code
is ‹RETURN o get_conflict_wl_is_None_heur_init›
:: ‹isasat_init_assn⇧k →⇩a bool1_assn›
unfolding get_conflict_wl_is_None_heur_init_alt_def isasat_init_assn_def length_ll_def[symmetric]
conflict_option_rel_assn_def
supply [[goals_limit=1]]
by sepref
declare get_conflict_wl_is_None_init_code.refine[sepref_fr_rules]
sepref_def polarity_st_heur_init_code
is ‹uncurry (RETURN oo polarity_st_heur_init)›
:: ‹[λ(S, L). polarity_pol_pre (get_trail_wl_heur_init S) L]⇩a isasat_init_assn⇧k *⇩a unat_lit_assn⇧k → tri_bool_assn›
unfolding polarity_st_heur_init_def isasat_init_assn_def
supply [[goals_limit = 1]]
by sepref
declare polarity_st_heur_init_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 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)›
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⇧d →
isasat_init_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
init_dt_step_wl_heur_b'_def list_length_1_def is_Nil_length
op_list_list_llen_alt_def[symmetric] op_list_list_idx_alt_def[symmetric]
already_propagated_unit_cls_heur'_alt
add_init_cls_heur_b'_def[symmetric] add_clause_to_others_heur'_def[symmetric]
add_clause_to_others_heur'_alt
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]
apply (annot_snat_const "TYPE(64)")
by sepref
declare
init_dt_step_wl_code_b.refine[sepref_fr_rules]
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 ≤ uint32_max div 2]⇩a sint64_nat_assn⇧k → sint64_nat_assn›
unfolding init_next_size_def
apply (annot_snat_const "TYPE(64)")
by sepref
find_in_thms op_list_grow_init in sepref_fr_rules
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
find_theorems nfoldli WHILET
lemma [sepref_fr_rules]:
‹(uncurry nat_lit_lits_init_assn_assn_in, uncurry (RETURN ∘∘ op_set_insert))
∈ [λ(a, b). a ≤ uint32_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 convert_fref op_set_insert_def[symmetric]]])
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
definition extract_atms_cls_i' where
‹extract_atms_cls_i' C i = extract_atms_cls_i (C!i)›
lemma aal_assn_boundsD':
assumes A: "rdomp (aal_assn' TYPE('l::len2) TYPE('ll::len2) A) xss" and ‹i < length xss›
shows "length (xss ! i) < max_snat LENGTH('ll)"
using aal_assn_boundsD_aux1[OF A] assms
by auto
sepref_def extract_atms_cls_imp
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)")
by sepref
declare extract_atms_cls_imp.refine[sepref_fr_rules]
sepref_def extract_atms_clss_imp
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)")
by sepref
lemma extract_atms_clss_hnr[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 ≤ uint32_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[unfolded convert_fref]]
by simp
sepref_def extract_atms_clss_imp_empty_assn
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)")
by sepref
lemma extract_atms_clss_imp_empty_assn[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
[unfolded convert_fref]]
unfolding uncurry0_def
by simp
lemma extract_atms_clss_imp_empty_rel_alt_def:
‹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›
sepref_def rewatch_heur_st_fast_code
is ‹(rewatch_heur_st_fast)›
:: ‹[rewatch_heur_st_fast_pre]⇩a
isasat_init_assn⇧d → isasat_init_assn›
supply [[goals_limit=1]]
unfolding rewatch_heur_st_def PR_CONST_def rewatch_heur_st_fast_pre_def
isasat_init_assn_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 (annot_snat_const "TYPE(64)")
by sepref
declare
init_dt_wl_heur_code_b.refine[sepref_fr_rules]
definition extract_lits_sorted' where
‹extract_lits_sorted' xs n vars = extract_lits_sorted (xs, n, vars)›
lemma extract_lits_sorted_extract_lits_sorted':
‹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 -) extract_lits_sorted'_impl
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
by sepref
lemmas [sepref_fr_rules] = extract_lits_sorted'_impl.refine
sepref_def (in -) extract_lits_sorted_code
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]
by 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 extract_lits_sorted_hnr[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[unfolded convert_fref]]
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]:
‹(return 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)
sepref_def finalise_init_code'
is ‹uncurry finalise_init_code›
:: ‹[λ(_, S). length (get_clauses_wl_heur_init S) ≤ sint64_max]⇩a
opts_assn⇧d *⇩a isasat_init_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]]
unfolding finalise_init_code_def isasat_init_assn_def isasat_bounded_assn_def
INITIAL_OUTL_SIZE_def[symmetric] atom.fold_the vmtf_remove_assn_def
heuristic_assn_def
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 ‹(_, _,_,⌑, _,_,_,_,_)› snat_const_fold[where 'a=64])
apply (rewrite at ‹(_, _,_,⌑, _,_,_)› snat_const_fold[where 'a=64])
apply (annot_unat_const "TYPE(64)")
apply (rewrite at ‹(_, ⌑, _)› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹(_, ⌑)› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹take _ ⌑› al_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› array_fold_custom_replicate)
by sepref
declare finalise_init_code'.refine[sepref_fr_rules]
sepref_register initialise_VMTF
abbreviation snat64_assn :: ‹nat ⇒ 64 word ⇒ _› where ‹snat64_assn ≡ snat_assn›
abbreviation snat32_assn :: ‹nat ⇒ 32 word ⇒ _› where ‹snat32_assn ≡ snat_assn›
abbreviation unat64_assn :: ‹nat ⇒ 64 word ⇒ _› where ‹unat64_assn ≡ unat_assn›
abbreviation unat32_assn :: ‹nat ⇒ 32 word ⇒ _› where ‹unat32_assn ≡ unat_assn›
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 (annot_snat_const "TYPE(64)")
supply [[goals_limit = 1]]
by sepref
declare init_trail_D_fast_code.refine[sepref_fr_rules]
sepref_def 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'_def PR_CONST_def init_trail_D_fast_def[symmetric] isasat_init_assn_def
cach_refinement_l_assn_def Suc_eq_plus1_left conflict_option_rel_assn_def lookup_clause_rel_assn_def
apply (rewrite at ‹let _ = 1 + ⌑ in _› annot_unat_snat_upcast[where 'l=64])
apply (rewrite at ‹let _ = (_, ⌑) in _› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹let _ = (⌑,_) in _› annotate_assn[where A= ‹array_assn minimize_status_assn›])
apply (rewrite at ‹let _ = (_, ⌑) 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 _= (True, _, ⌑) in _› array_fold_custom_replicate)
unfolding array_fold_custom_replicate
apply (rewrite at ‹let _ = ⌑ in let _ = (True, _, _) in _› al_fold_custom_empty[where 'l=64])
apply (rewrite in ‹let _= (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 in ‹let _= ⌑ in RETURN _› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹(_,⌑, _ ,_, _, False)› unat_const_fold[where 'a=32])
apply (annot_snat_const "TYPE(64)")
apply (rewrite at ‹RETURN ⌑› annotate_assn[where A=‹isasat_init_assn›, unfolded isasat_init_assn_def
conflict_option_rel_assn_def cach_refinement_l_assn_def lookup_clause_rel_assn_def])
by sepref
declare init_state_wl_D'_code.refine[sepref_fr_rules]
lemma to_init_state_code_hnr:
‹(return 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)›
experiment
begin
export_llvm init_state_wl_D'_code
rewatch_heur_st_fast_code
init_dt_wl_heur_code_b
end
end