Theory IsaSAT_Setup0_LLVM
theory IsaSAT_Setup0_LLVM
imports IsaSAT_Watch_List_LLVM IsaSAT_Lookup_Conflict_LLVM
More_Sepref.WB_More_Refinement IsaSAT_Clauses_LLVM LBD_LLVM
IsaSAT_Options_LLVM IsaSAT_VMTF_Setup_LLVM
IsaSAT_Arena_Sorting_LLVM
IsaSAT_Rephase_LLVM
IsaSAT_EMA_LLVM
IsaSAT_Stats_LLVM
IsaSAT_VDom_LLVM
IsaSAT_Bump_Heuristics_State_LLVM
Isabelle_LLVM.LLVM_DS_Block_Alloc
Tuple17_LLVM
begin
hide_const (open) NEMonad.ASSERT NEMonad.RETURN
text ‹
This is the setup for accessing and modifying the state. The construction is kept generic
(even if still targetting only our state). There is a lot of copy-paste that would be nice to automate
at some point.
We define 3 sort of operations:
▸ extracting an element, replacing it by an default element. Modifies the state. The name starts
with \<^text>‹exctr›
▸ reinserting an element, freeing the current one. Modifies the state. The name starts with
\<^text>‹update›
▸ in-place reading a value, possibly with pure parameters. Does not modify the state. The name
starts with \<^text>‹read›
›
type_synonym occs_assn = ‹(64,(64 word),64)array_array_list›
abbreviation ‹occs_assn ≡ aal_assn' TYPE(64) TYPE(64) sint64_nat_assn›
type_synonym twl_st_wll_trail_fast2 =
‹(trail_pol_fast_assn, arena_assn, option_lookup_clause_assn,
64 word, watched_wl_uint32, bump_heuristics_assn,
32 word, cach_refinement_l_assn, lbd_assn, out_learned_assn,
isasat_stats_assn, heur_assn,
aivdom_assn, (64 word × 64 word × 64 word × 64 word × 64 word),
opts_assn, arena_assn, occs_assn) tuple17›
definition isasat_bounded_assn :: ‹isasat ⇒ twl_st_wll_trail_fast2 ⇒ assn› where
‹isasat_bounded_assn = tuple17_assn
trail_pol_fast_assn arena_fast_assn
conflict_option_rel_assn
sint64_nat_assn
watchlist_fast_assn
heuristic_bump_assn
uint32_nat_assn
cach_refinement_l_assn
lbd_assn
out_learned_assn
isasat_stats_assn
heuristic_assn
aivdom_assn
lcount_assn
opts_assn
arena_fast_assn
occs_assn›
sepref_register mop_arena_length
type_synonym twl_st_wll_trail_fast =
‹trail_pol_fast_assn × arena_assn × option_lookup_clause_assn ×
64 word × watched_wl_uint32 × bump_heuristics_assn ×
32 word × cach_refinement_l_assn × lbd_assn × out_learned_assn × isasat_stats ×
heur_assn ×
aivdom_assn × (64 word × 64 word × 64 word × 64 word × 64 word) ×
opts_assn × arena_assn × occs_assn›
text ‹The following constants are not useful for the initialisation for the solver, but only as temporary replacement
for values in state.›
definition bottom_trail :: trail_pol where
‹bottom_trail = do {
let M0 = [] in
let cs = [] in
let M = replicate 0 UNSET in
let M' = replicate 0 0 in
let M'' = replicate 0 1 in
((M0, M, M', M'', 0, cs, 0))
}›
where
‹extract_trail_wl_heur = isasat_state_ops.remove_a bottom_trail›
sepref_def bottom_trail_code
is ‹uncurry0 (RETURN bottom_trail)›
:: ‹unit_assn⇧k →⇩a trail_pol_fast_assn›
unfolding bottom_trail_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 ‹(_, _, _, _ , ⌑)› snat_const_fold[where 'a=64])
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
definition bottom_arena :: ‹arena› where
‹bottom_arena = []›
where
‹extract_arena_wl_heur = isasat_state_ops.remove_b bottom_arena›
sepref_def bottom_arena_code
is ‹uncurry0 (RETURN bottom_arena)›
:: ‹unit_assn⇧k →⇩a arena_fast_assn›
unfolding bottom_arena_def al_fold_custom_empty[where 'l=64]
by sepref
definition bottom_conflict :: ‹conflict_option_rel› where
‹bottom_conflict = (True, 0, replicate 0 NOTIN)›
where
‹extract_conflict_wl_heur = isasat_state_ops.remove_c bottom_conflict›
sepref_def bottom_conflict_code
is ‹uncurry0 (RETURN bottom_conflict)›
:: ‹unit_assn⇧k →⇩a conflict_option_rel_assn›
unfolding bottom_conflict_def
conflict_option_rel_assn_def lookup_clause_rel_assn_def array_fold_custom_replicate
apply (rewrite at ‹(_, ⌑, _)› unat_const_fold[where 'a=32])
apply (annot_snat_const ‹TYPE(32)›)
by sepref
definition bottom_decision_level :: nat where
‹bottom_decision_level = 0›
:: ‹_ ⇒ _› where
‹extract_literals_to_update_wl_heur = isasat_state_ops.remove_d bottom_decision_level›
sepref_def bottom_decision_level_code
is ‹uncurry0 (RETURN bottom_decision_level)›
:: ‹unit_assn⇧k →⇩a sint64_nat_assn›
unfolding bottom_decision_level_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition bottom_watchlist :: ‹(nat) watcher list list› where
‹bottom_watchlist = replicate 0 []›
where
‹extract_watchlist_wl_heur = isasat_state_ops.remove_e bottom_watchlist›
sepref_def bottom_watchlist_code
is ‹uncurry0 (RETURN bottom_watchlist)›
:: ‹unit_assn⇧k →⇩a watchlist_fast_assn›
unfolding bottom_watchlist_def aal_fold_custom_empty[where 'l=64 and 'll=64]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition bottom_atom where
‹bottom_atom = 0›
lemma [sepref_fr_rules]: ‹(uncurry0 (Mreturn 0), uncurry0 (RETURN bottom_atom)) ∈ unit_assn⇧k →⇩a atom_assn›
unfolding bottom_atom_def
apply sepref_to_hoare
apply vcg
apply (auto simp: atom_rel_def unat_rel_def unat.rel_def br_def entails_def ENTAILS_def)
by (smt (verit, best) pure_true_conv rel_simps(51) sep.add_0)
definition bottom_bump :: ‹bump_heuristics› where
‹bottom_bump = Tuple4 empty_acids bottom_vmtf False bottom_atms_hash›
where
‹extract_vmtf_wl_heur = isasat_state_ops.remove_f bottom_bump›
sepref_def bottom_bump_code
is ‹uncurry0 (RETURN bottom_bump)›
:: ‹unit_assn⇧k →⇩a heuristic_bump_assn›
unfolding bottom_bump_def
by sepref
definition bottom_clvls :: ‹nat› where
‹bottom_clvls = 0›
where
‹extract_clvls_wl_heur = isasat_state_ops.remove_g bottom_clvls›
sepref_def bottom_clvls_code
is ‹uncurry0 (RETURN bottom_clvls)›
:: ‹unit_assn⇧k →⇩a uint32_nat_assn›
unfolding bottom_clvls_def
apply (annot_unat_const ‹TYPE(32)›)
by sepref
definition bottom_ccach :: ‹minimize_status list × nat list› where
‹bottom_ccach = (replicate 0 SEEN_UNKNOWN, [])›
where
‹extract_ccach_wl_heur = isasat_state_ops.remove_h bottom_ccach›
sepref_def bottom_ccach_code
is ‹uncurry0 (RETURN bottom_ccach)›
:: ‹unit_assn⇧k →⇩a cach_refinement_l_assn›
unfolding bottom_ccach_def cach_refinement_l_assn_def array_fold_custom_replicate
apply (rewrite at ‹(_, ⌑)› al_fold_custom_empty[where 'l=64])
apply (rewrite at ‹(⌑, _)› annotate_assn[where A = ‹IICF_Array.array_assn minimize_status_assn›])
apply (annot_snat_const ‹TYPE(32)›)
by sepref
where
‹extract_lbd_wl_heur = isasat_state_ops.remove_i empty_lbd›
definition bottom_outl :: ‹out_learned› where
‹bottom_outl = []›
where
‹extract_outl_wl_heur = isasat_state_ops.remove_j bottom_outl›
sepref_def bottom_outl_code
is ‹uncurry0 (RETURN bottom_outl)›
:: ‹unit_assn⇧k →⇩a out_learned_assn›
unfolding bottom_outl_def cach_refinement_l_assn_def array_fold_custom_replicate
apply (rewrite at ‹(⌑)› al_fold_custom_empty[where 'l=64])
by sepref
definition bottom_stats :: ‹isasat_stats› where
‹bottom_stats = empty_stats›
where
‹extract_stats_wl_heur = isasat_state_ops.remove_k bottom_stats›
sepref_def bottom_stats_code
is ‹uncurry0 (RETURN bottom_stats)›
:: ‹unit_assn⇧k →⇩a isasat_stats_assn›
unfolding bottom_stats_def
by sepref
definition bottom_heur_int :: ‹restart_heuristics› where
‹bottom_heur_int = (
let φ = replicate 0 False in
let fema = ema_init (0) in
let sema = ema_init (0) in
let other_fema = ema_init (0) in
let other_sema = ema_init (0) in
let ccount = restart_info_init in
let n = 0 in
(fema, sema, ccount, 0, (φ, 0, replicate n False, 0, replicate n False, 10000, 1000, 1), reluctant_init, False, replicate 0 False, (0, 0, 0), other_fema, other_sema))
›
sepref_def bottom_heur_int_code
is ‹uncurry0 (RETURN bottom_heur_int)›
:: ‹unit_assn⇧k →⇩a heuristic_int_assn›
supply [[goals_limit=1]]
unfolding bottom_heur_int_def heuristic_int_assn_def phase_heur_assn_def
apply (rewrite in ‹(replicate _ False, _)› annotate_assn[where A=phase_saver'_assn])
apply (rewrite in ‹(replicate _ False, _)› array_fold_custom_replicate)
apply (rewrite in ‹(_, _, ⌑, _)› array_fold_custom_replicate)
apply (rewrite in ‹let _ =⌑ in _› annotate_assn[where A=phase_saver_assn])
unfolding larray_fold_custom_replicate
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition bottom_heur :: ‹_› where
‹bottom_heur = Restart_Heuristics (bottom_heur_int)›
where
‹extract_heur_wl_heur = isasat_state_ops.remove_l bottom_heur›
sepref_def bottom_heur_code
is ‹uncurry0 (RETURN bottom_heur)›
:: ‹unit_assn⇧k →⇩a heuristic_assn›
supply [[goals_limit=1]]
unfolding bottom_heur_def
by sepref
definition bottom_vdom :: ‹_› where
‹bottom_vdom = AIvdom_init [] [] []›
where
‹extract_vdom_wl_heur = isasat_state_ops.remove_m bottom_vdom›
sepref_def bottom_vdom_code
is ‹uncurry0 (RETURN bottom_vdom)›
:: ‹unit_assn⇧k →⇩a aivdom_assn›
supply [[goals_limit=1]]
unfolding bottom_vdom_def
unfolding al_fold_custom_empty[where 'l=64]
by sepref
definition bottom_lcount :: ‹clss_size› where
‹bottom_lcount = (0, 0, 0, 0, 0)›
where
‹extract_lcount_wl_heur = isasat_state_ops.remove_n bottom_lcount›
sepref_def bottom_lcount_code
is ‹uncurry0 (RETURN bottom_lcount)›
:: ‹unit_assn⇧k →⇩a lcount_assn›
supply [[goals_limit=1]]
unfolding bottom_lcount_def lcount_assn_def
unfolding al_fold_custom_empty[where 'l=64]
apply (annot_unat_const ‹TYPE(64)›)
by sepref
definition bottom_opts :: ‹opts› where
‹bottom_opts = IsaOptions False False False 0 0 0 0 0 0 0 True›
where
‹extract_opts_wl_heur = isasat_state_ops.remove_o bottom_opts›
sepref_def bottom_opts_code
is ‹uncurry0 (RETURN bottom_opts)›
:: ‹unit_assn⇧k →⇩a opts_assn›
supply [[goals_limit=1]]
unfolding bottom_opts_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition bottom_old_arena :: ‹arena› where
‹bottom_old_arena = []›
where
‹extract_old_arena_wl_heur = isasat_state_ops.remove_p bottom_old_arena›
sepref_def bottom_old_arena_code
is ‹uncurry0 (RETURN bottom_old_arena)›
:: ‹unit_assn⇧k →⇩a arena_fast_assn›
supply [[goals_limit=1]]
unfolding bottom_old_arena_def al_fold_custom_empty[where 'l=64]
by sepref
schematic_goal free_trail_pol_fast_assn[sepref_frame_free_rules]: ‹MK_FREE trail_pol_fast_assn ?a›
unfolding trail_pol_fast_assn_def
by synthesize_free
sepref_def free_trail_pol_fast
is ‹mop_free›
:: ‹trail_pol_fast_assn⇧d →⇩a unit_assn›
by sepref
lemma free_trail_pol_fast_assn2: ‹MK_FREE trail_pol_fast_assn free_trail_pol_fast›
unfolding free_trail_pol_fast_def
by (rule back_subst[of ‹MK_FREE trail_pol_fast_assn›, OF free_trail_pol_fast_assn])
(auto intro!: ext)
schematic_goal free_arena_fast_assn[sepref_frame_free_rules]: ‹MK_FREE arena_fast_assn ?a›
by synthesize_free
sepref_def free_arena_fast
is ‹mop_free›
:: ‹arena_fast_assn⇧d →⇩a unit_assn›
by sepref
lemma free_arena_fast_assn2: ‹MK_FREE arena_fast_assn free_arena_fast›
unfolding free_arena_fast_def
by (rule back_subst[of ‹MK_FREE arena_fast_assn›, OF free_arena_fast_assn])
(auto intro!: ext)
schematic_goal free_conflict_option_rel_assn[sepref_frame_free_rules]: ‹MK_FREE conflict_option_rel_assn ?a›
by synthesize_free
sepref_def free_conflict_option_rel
is ‹mop_free›
:: ‹conflict_option_rel_assn⇧d →⇩a unit_assn›
by sepref
lemma free_conflict_option_rel_assn2: ‹MK_FREE conflict_option_rel_assn free_conflict_option_rel›
unfolding free_conflict_option_rel_def
by (rule back_subst[of ‹MK_FREE conflict_option_rel_assn›, OF free_conflict_option_rel_assn])
(auto intro!: ext)
schematic_goal free_sint64_nat_assn[sepref_frame_free_rules]: ‹MK_FREE sint64_nat_assn ?a›
by synthesize_free
sepref_def free_sint64_nat
is ‹mop_free›
:: ‹sint64_nat_assn⇧d →⇩a unit_assn›
by sepref
lemma free_sint64_nat_assn_assn2: ‹MK_FREE sint64_nat_assn free_sint64_nat›
unfolding free_sint64_nat_def
by (rule back_subst[of ‹MK_FREE sint64_nat_assn›, OF free_sint64_nat_assn])
(auto intro!: ext)
schematic_goal free_watchlist_fast_assn[sepref_frame_free_rules]: ‹MK_FREE watchlist_fast_assn ?a›
by synthesize_free
sepref_def free_watchlist_fast
is ‹mop_free›
:: ‹watchlist_fast_assn⇧d →⇩a unit_assn›
by sepref
lemma free_watchlist_fast_assn2: ‹MK_FREE watchlist_fast_assn free_watchlist_fast›
unfolding free_watchlist_fast_def
by (rule back_subst[of ‹MK_FREE watchlist_fast_assn›, OF free_watchlist_fast_assn])
(auto intro!: ext)
schematic_goal free_heuristic_bump_assn[sepref_frame_free_rules]: ‹MK_FREE heuristic_bump_assn ?a›
unfolding heuristic_bump_assn_def
by synthesize_free
sepref_def free_vmtf_remove
is ‹mop_free›
:: ‹heuristic_bump_assn⇧d →⇩a unit_assn›
by sepref
lemma free_heuristic_bump_assn2: ‹MK_FREE heuristic_bump_assn free_vmtf_remove›
unfolding free_vmtf_remove_def
apply (rule back_subst[of ‹MK_FREE heuristic_bump_assn›, OF free_heuristic_bump_assn])
apply (auto intro!: ext simp: M_monad_laws)
by (metis M_monad_laws(1))
schematic_goal free_uint32_nat_assn[sepref_frame_free_rules]: ‹MK_FREE uint32_nat_assn ?a›
by synthesize_free
sepref_def free_uint32_nat
is ‹mop_free›
:: ‹uint32_nat_assn⇧d →⇩a unit_assn›
by sepref
lemma free_uint32_nat_assn2: ‹MK_FREE uint32_nat_assn free_uint32_nat›
unfolding free_uint32_nat_def
by (rule back_subst[of ‹MK_FREE uint32_nat_assn›, OF free_uint32_nat_assn])
(auto intro!: ext)
schematic_goal free_cach_refinement_l_assn[sepref_frame_free_rules]: ‹MK_FREE cach_refinement_l_assn ?a›
by synthesize_free
sepref_def free_cach_refinement_l
is ‹mop_free›
:: ‹cach_refinement_l_assn⇧d →⇩a unit_assn›
by sepref
lemma free_cach_refinement_l_assn2: ‹MK_FREE cach_refinement_l_assn free_cach_refinement_l›
unfolding free_cach_refinement_l_def
by (rule back_subst[of ‹MK_FREE cach_refinement_l_assn›, OF free_cach_refinement_l_assn])
(auto intro!: ext)
schematic_goal free_lbd_assn[sepref_frame_free_rules]: ‹MK_FREE lbd_assn ?a›
by synthesize_free
sepref_def free_lbd
is ‹mop_free›
:: ‹lbd_assn⇧d →⇩a unit_assn›
by sepref
lemma free_lbd_assn2: ‹MK_FREE lbd_assn free_lbd›
unfolding free_lbd_def
by (rule back_subst[of ‹MK_FREE lbd_assn›, OF free_lbd_assn])
(auto intro!: ext)
schematic_goal free_outl_assn[sepref_frame_free_rules]: ‹MK_FREE out_learned_assn ?a›
by synthesize_free
sepref_def free_outl
is ‹mop_free›
:: ‹out_learned_assn⇧d →⇩a unit_assn›
by sepref
lemma free_outl_assn2: ‹MK_FREE out_learned_assn free_outl›
unfolding free_outl_def
by (rule back_subst[of ‹MK_FREE out_learned_assn›, OF free_outl_assn])
(auto intro!: ext)
schematic_goal free_heur_assn[sepref_frame_free_rules]: ‹MK_FREE heuristic_assn ?a›
unfolding heuristic_assn_def code_hider_assn_def
by synthesize_free
sepref_def free_heur
is ‹mop_free›
:: ‹heuristic_assn⇧d →⇩a unit_assn›
by sepref
lemma free_heur_assn2: ‹MK_FREE heuristic_assn free_heur›
unfolding free_heur_def
by (rule back_subst[of ‹MK_FREE heuristic_assn›, OF free_heur_assn])
(auto intro!: ext)
schematic_goal free_isasat_stats_assn[sepref_frame_free_rules]: ‹MK_FREE isasat_stats_assn ?a›
unfolding isasat_stats_assn_def code_hider_assn_def
by synthesize_free
sepref_def free_stats
is ‹mop_free›
:: ‹isasat_stats_assn⇧d →⇩a unit_assn›
by sepref
lemma free_isasat_stats_assn2: ‹MK_FREE isasat_stats_assn free_stats›
unfolding free_stats_def
by (rule back_subst[of ‹MK_FREE isasat_stats_assn›, OF free_isasat_stats_assn])
(auto intro!: ext)
schematic_goal free_vdom_assn[sepref_frame_free_rules]: ‹MK_FREE aivdom_assn ?a›
unfolding aivdom_assn_def code_hider_assn_def
by synthesize_free
sepref_def free_vdom
is ‹mop_free›
:: ‹aivdom_assn⇧d →⇩a unit_assn›
by sepref
lemma free_vdom_assn2: ‹MK_FREE aivdom_assn free_vdom›
unfolding free_vdom_def
by (rule back_subst[of ‹MK_FREE aivdom_assn›, OF free_vdom_assn])
(auto intro!: ext)
schematic_goal free_lcount_assn[sepref_frame_free_rules]: ‹MK_FREE lcount_assn ?a›
unfolding lcount_assn_def code_hider_assn_def
by synthesize_free
sepref_def free_lcount
is ‹mop_free›
:: ‹lcount_assn⇧d →⇩a unit_assn›
by sepref
lemma free_lcount_assn2: ‹MK_FREE lcount_assn free_lcount›
unfolding free_lcount_def
by (rule back_subst[of ‹MK_FREE lcount_assn›, OF free_lcount_assn])
(auto intro!: ext)
schematic_goal free_opts_assn[sepref_frame_free_rules]: ‹MK_FREE opts_assn ?a›
unfolding opts_assn_def code_hider_assn_def opts_rel_assn_def
by synthesize_free
sepref_def free_opts
is ‹mop_free›
:: ‹opts_assn⇧d →⇩a unit_assn›
by sepref
lemma free_opts_assn2: ‹MK_FREE opts_assn free_opts›
unfolding free_opts_def
by (rule back_subst[of ‹MK_FREE opts_assn›, OF free_opts_assn])
(auto intro!: ext)
schematic_goal free_old_arena_fast_assn[sepref_frame_free_rules]: ‹MK_FREE arena_fast_assn ?a›
by synthesize_free
sepref_def free_old_arena_fast
is ‹mop_free›
:: ‹arena_fast_assn⇧d →⇩a unit_assn›
by sepref
lemma free_old_arena_fast_assn2: ‹MK_FREE arena_fast_assn free_old_arena_fast›
unfolding free_old_arena_fast_def free_arena_fast_def
by (rule back_subst[of ‹MK_FREE arena_fast_assn›, OF free_old_arena_fast_assn])
(auto intro!: ext)
sepref_def free_occs_fast
is ‹mop_free›
:: ‹occs_assn⇧d →⇩a unit_assn›
by sepref
definition bottom_occs :: ‹nat list list› where
‹bottom_occs = op_aal_lempty TYPE(64) TYPE(64) 0›
where
‹extract_occs_wl_heur = isasat_state_ops.remove_q bottom_occs›
sepref_def bottom_occs_code
is ‹uncurry0 (RETURN bottom_occs)›
:: ‹unit_assn⇧k →⇩a occs_assn›
supply [[goals_limit=1]]
unfolding bottom_occs_def aal_fold_custom_empty[where 'l=64 and 'll=64]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
schematic_goal free_occs_fast_assn[sepref_frame_free_rules]: ‹MK_FREE occs_assn ?a›
by synthesize_free
lemma free_occs_fast_assn2: ‹MK_FREE occs_assn free_occs_fast›
unfolding free_occs_fast_def
by (rule back_subst[of ‹MK_FREE occs_assn›, OF free_occs_fast_assn])
(auto intro!: ext)