Theory IsaSAT_Setup_LLVM

theory IsaSAT_Setup_LLVM
  imports IsaSAT_Setup IsaSAT_Watch_List_LLVM IsaSAT_Lookup_Conflict_LLVM
    Watched_Literals.WB_More_Refinement IsaSAT_Clauses_LLVM LBD_LLVM
begin


no_notation WB_More_Refinement.fref ("[_]⇩f _ → _" [0,60,60] 60)
no_notation WB_More_Refinement.freft ("_ →⇩f _" [60,60] 60)


(*TODO Move*)
abbreviation "word32_rel ≡ word_rel :: (32 word × _) set"
abbreviation "word64_rel ≡ word_rel :: (64 word × _) set"
abbreviation "word32_assn ≡ word_assn :: 32 word ⇒ _"
abbreviation "word64_assn ≡ word_assn :: 64 word ⇒ _"

abbreviation stats_rel :: ‹(stats × stats) set› where
  ‹stats_rel ≡ word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel
     ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel›

abbreviation ema_rel :: ‹(ema×ema) set› where
  ‹ema_rel ≡ word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel›

abbreviation ema_assn :: ‹ema ⇒ ema ⇒ assn› where
  ‹ema_assn ≡ word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn›

abbreviation stats_assn :: ‹stats ⇒ stats ⇒ assn› where
  ‹stats_assn ≡ word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a ema_assn›


lemma [sepref_import_param]:
  "(ema_get_value, ema_get_value) ∈ ema_rel → word64_rel"
  "(ema_bitshifting,ema_bitshifting) ∈ word64_rel"
  "(ema_reinit,ema_reinit) ∈ ema_rel → ema_rel"
  "(ema_init,ema_init) ∈ word_rel → ema_rel"
  by auto


lemma ema_bitshifting_inline[llvm_inline]:
  "ema_bitshifting = (0x100000000::_::len word)" by (auto simp: ema_bitshifting_def)

lemma ema_reinit_inline[llvm_inline]:
  "ema_reinit = (λ(value, α, β, wait, period).
    (value, α, 0x100000000::_::len word, 0::_ word, 0:: _ word))"
  by auto

lemmas [llvm_inline] = ema_init_def

sepref_def ema_update_impl is "uncurry (RETURN oo ema_update)"
  :: "uint32_nat_assn⇧k *⇩a ema_assn⇧k →⇩a ema_assn"
  unfolding ema_update_def
  apply (rewrite at ‹let _ = of_nat ⌑ * _ in _› annot_unat_unat_upcast[where 'l = 64])
  apply (rewrite at ‹let _=_ + _; _=⌑ in _› fold_COPY)
  (* TODO: The let x=y seems to be inlined, making necessary this COPY! Is this behaviour correct? *)
  apply (annot_unat_const "TYPE(64)")
  supply [[goals_limit = 1]]
  by sepref

lemma [sepref_import_param]:
  "(incr_propagation,incr_propagation) ∈ stats_rel → stats_rel"
  "(incr_conflict,incr_conflict) ∈ stats_rel → stats_rel"
  "(incr_decision,incr_decision) ∈ stats_rel → stats_rel"
  "(incr_restart,incr_restart) ∈ stats_rel → stats_rel"
  "(incr_lrestart,incr_lrestart) ∈ stats_rel → stats_rel"
  "(incr_uset,incr_uset) ∈ stats_rel → stats_rel"
  "(incr_GC,incr_GC) ∈ stats_rel → stats_rel"
  "(add_lbd,add_lbd) ∈ word64_rel → stats_rel → stats_rel"
  by auto

lemmas [llvm_inline] =
  incr_propagation_def
  incr_conflict_def
  incr_decision_def
  incr_restart_def
  incr_lrestart_def
  incr_uset_def
  incr_GC_def


abbreviation (input) "restart_info_rel ≡ word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel"

abbreviation (input) restart_info_assn where
  ‹restart_info_assn ≡ word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn›

lemma restart_info_params[sepref_import_param]:
  "(incr_conflict_count_since_last_restart,incr_conflict_count_since_last_restart) ∈
    restart_info_rel → restart_info_rel"
  "(restart_info_update_lvl_avg,restart_info_update_lvl_avg) ∈
    word32_rel → restart_info_rel → restart_info_rel"
  "(restart_info_init,restart_info_init) ∈ restart_info_rel"
  "(restart_info_restart_done,restart_info_restart_done) ∈ restart_info_rel → restart_info_rel"
  by auto

lemmas [llvm_inline] =
  incr_conflict_count_since_last_restart_def
  restart_info_update_lvl_avg_def
  restart_info_init_def
  restart_info_restart_done_def


(* TODO: Define vmtf_node_rel, such that sepref sees syntactically an assertion of form "pure ..."*)
type_synonym vmtf_node_assn = "(64 word × 32 word × 32 word)"

definition "vmtf_node1_rel ≡ { ((a,b,c),(VMTF_Node a b c)) | a b c. True}"
definition "vmtf_node2_assn ≡ uint64_nat_assn ×⇩a atom.option_assn ×⇩a atom.option_assn"

definition "vmtf_node_assn ≡ hr_comp vmtf_node2_assn vmtf_node1_rel"
lemmas [fcomp_norm_unfold] = vmtf_node_assn_def[symmetric]


lemma vmtf_node_assn_pure[safe_constraint_rules]: ‹CONSTRAINT is_pure vmtf_node_assn›
  unfolding vmtf_node_assn_def vmtf_node2_assn_def
  by solve_constraint


(*

  TODO: Test whether this setup is safe in general?
    E.g., synthesize destructors when side-tac can prove is_pure.

lemmas [sepref_frame_free_rules] = mk_free_is_pure
lemmas [simp] = vmtf_node_assn_pure[unfolded CONSTRAINT_def]
*)

lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF vmtf_node_assn_pure[unfolded CONSTRAINT_def]]


lemma
    vmtf_Node_refine1: "(λa b c. (a,b,c), VMTF_Node) ∈ Id → Id → Id → vmtf_node1_rel"
and vmtf_stamp_refine1: "(λ(a,b,c). a, stamp) ∈ vmtf_node1_rel → Id"
and vmtf_get_prev_refine1: "(λ(a,b,c). b, get_prev) ∈ vmtf_node1_rel → ⟨Id⟩option_rel"
and vmtf_get_next_refine1: "(λ(a,b,c). c, get_next) ∈ vmtf_node1_rel → ⟨Id⟩option_rel"
  by (auto simp: vmtf_node1_rel_def)

sepref_def VMTF_Node_impl is []
  "uncurry2 (RETURN ooo (λa b c. (a,b,c)))"
  :: "uint64_nat_assn⇧k *⇩a (atom.option_assn)⇧k *⇩a (atom.option_assn)⇧k →⇩a vmtf_node2_assn"
  unfolding vmtf_node2_assn_def by sepref

sepref_def VMTF_stamp_impl
  is [] "RETURN o (λ(a,b,c). a)"
  :: "vmtf_node2_assn⇧k →⇩a uint64_nat_assn"
  unfolding vmtf_node2_assn_def
  by sepref

sepref_def VMTF_get_prev_impl
  is [] "RETURN o (λ(a,b,c). b)"
  :: "vmtf_node2_assn⇧k →⇩a atom.option_assn"
  unfolding vmtf_node2_assn_def
  by sepref

sepref_def VMTF_get_next_impl
  is [] "RETURN o (λ(a,b,c). c)"
  :: "vmtf_node2_assn⇧k →⇩a atom.option_assn"
  unfolding vmtf_node2_assn_def
  by sepref

(* TODO: This should be done automatically! For all structured ID-relations on hr_comp! *)
lemma workaround_hrcomp_id_norm[fcomp_norm_unfold]: "hr_comp R (⟨nat_rel⟩option_rel) = R" by simp

lemmas [sepref_fr_rules] =
  VMTF_Node_impl.refine[FCOMP vmtf_Node_refine1]
  VMTF_stamp_impl.refine[FCOMP vmtf_stamp_refine1]
  VMTF_get_prev_impl.refine[FCOMP vmtf_get_prev_refine1]
  VMTF_get_next_impl.refine[FCOMP vmtf_get_next_refine1]




type_synonym vmtf_assn = ‹vmtf_node_assn ptr × 64 word × 32 word × 32 word × 32 word›

type_synonym vmtf_remove_assn = ‹vmtf_assn × (32 word array_list64 × 1 word ptr)›


abbreviation vmtf_assn :: "_ ⇒ vmtf_assn ⇒ assn" where
  ‹vmtf_assn ≡ (array_assn vmtf_node_assn ×⇩a uint64_nat_assn ×⇩a atom_assn ×⇩a atom_assn
    ×⇩a atom.option_assn)›

abbreviation atoms_hash_assn :: ‹bool list ⇒ 1 word ptr ⇒ assn› where
  ‹atoms_hash_assn ≡ array_assn bool1_assn›

abbreviation distinct_atoms_assn where
  ‹distinct_atoms_assn ≡ arl64_assn atom_assn ×⇩a atoms_hash_assn›

definition vmtf_remove_assn
  :: ‹isa_vmtf_remove_int ⇒ vmtf_remove_assn ⇒ assn›
where
  ‹vmtf_remove_assn ≡ vmtf_assn ×⇩a distinct_atoms_assn›


paragraph ‹Options›

type_synonym opts_assn = "1 word × 1 word × 1 word"

definition opts_assn
  :: ‹opts ⇒ opts_assn ⇒ assn›
where
  ‹opts_assn ≡ bool1_assn ×⇩a bool1_assn ×⇩a bool1_assn›

lemma workaround_opt_assn: "RETURN o (λ(a,b,c). f a b c) = (λ(a,b,c). RETURN (f a b c))" by auto

sepref_register opts_restart opts_reduce opts_unbounded_mode

sepref_def opts_restart_impl is "RETURN o opts_restart" :: "opts_assn⇧k →⇩a bool1_assn"
  unfolding opts_restart_def workaround_opt_assn opts_assn_def
  by sepref

sepref_def opts_reduce_impl is "RETURN o opts_reduce" :: "opts_assn⇧k →⇩a bool1_assn"
  unfolding opts_reduce_def workaround_opt_assn opts_assn_def
  by sepref

sepref_def opts_unbounded_mode_impl is "RETURN o opts_unbounded_mode" :: "opts_assn⇧k →⇩a bool1_assn"
  unfolding opts_unbounded_mode_def workaround_opt_assn opts_assn_def
  by sepref

abbreviation "watchlist_fast_assn ≡ aal_assn' TYPE(64) TYPE(64) watcher_fast_assn"


type_synonym vdom_fast_assn = ‹64 word array_list64›
abbreviation vdom_fast_assn :: ‹vdom ⇒ vdom_fast_assn ⇒ assn› where
  ‹vdom_fast_assn ≡ arl64_assn sint64_nat_assn›

type_synonym phase_saver_assn = "1 word larray64"
abbreviation phase_saver_assn :: ‹phase_saver ⇒ phase_saver_assn ⇒ assn› where
  ‹phase_saver_assn ≡ larray64_assn bool1_assn›

type_synonym phase_saver'_assn = "1 word ptr"

abbreviation phase_saver'_assn :: ‹phase_saver ⇒ phase_saver'_assn ⇒ assn› where
  ‹phase_saver'_assn ≡ array_assn bool1_assn›

(* TODO: Move *)
type_synonym arena_assn = "(32 word, 64) array_list"
type_synonym heur_assn = ‹(ema × ema × restart_info × 64 word ×
   phase_saver_assn × 64 word × phase_saver'_assn × 64 word × phase_saver'_assn × 64 word × 64 word × 64 word)›

type_synonym twl_st_wll_trail_fast =
  ‹trail_pol_fast_assn × arena_assn × option_lookup_clause_assn ×
    64 word × watched_wl_uint32 × vmtf_remove_assn ×
    32 word × cach_refinement_l_assn × lbd_assn × out_learned_assn × stats ×
    heur_assn ×
    vdom_fast_assn × vdom_fast_assn × 64 word × opts_assn × arena_assn›


abbreviation phase_heur_assn where
  ‹phase_heur_assn ≡ phase_saver_assn ×⇩a sint64_nat_assn ×⇩a phase_saver'_assn ×⇩a sint64_nat_assn ×⇩a
     phase_saver'_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn›

definition heuristic_assn :: ‹restart_heuristics ⇒ heur_assn ⇒ assn› where
  ‹heuristic_assn = ema_assn ×⇩a
  ema_assn ×⇩a
  restart_info_assn ×⇩a
  word64_assn ×⇩a phase_heur_assn›

definition isasat_bounded_assn :: ‹twl_st_wl_heur ⇒ twl_st_wll_trail_fast ⇒ assn› where
‹isasat_bounded_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_assn ×⇩a
  uint32_nat_assn ×⇩a
  cach_refinement_l_assn ×⇩a
  lbd_assn ×⇩a
  out_learned_assn ×⇩a
  stats_assn ×⇩a
  heuristic_assn ×⇩a
  vdom_fast_assn ×⇩a
  vdom_fast_assn ×⇩a
  uint64_nat_assn ×⇩a
  opts_assn ×⇩a arena_fast_assn›


sepref_register NORMAL_PHASE QUIET_PHASE DEFAULT_INIT_PHASE

sepref_def NORMAL_PHASE_impl
  is ‹uncurry0 (RETURN NORMAL_PHASE)›
  :: ‹unit_assn⇧k →⇩a word_assn›
  unfolding NORMAL_PHASE_def
  by sepref

sepref_def QUIET_PHASE_impl
  is ‹uncurry0 (RETURN QUIET_PHASE)›
  :: ‹unit_assn⇧k →⇩a word_assn›
  unfolding QUIET_PHASE_def
  by sepref



subsubsection ‹Lift Operations to State›

(*TODO proper setup to test if the conflict is none*)
sepref_def get_conflict_wl_is_None_fast_code
  is ‹RETURN o get_conflict_wl_is_None_heur›
  :: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
  unfolding get_conflict_wl_is_None_heur_alt_def isasat_bounded_assn_def length_ll_def[symmetric]
    conflict_option_rel_assn_def
  supply [[goals_limit=1]]
  by sepref


sepref_def isa_count_decided_st_fast_code
  is ‹RETURN o isa_count_decided_st›
  :: ‹isasat_bounded_assn⇧k →⇩a uint32_nat_assn›
  supply [[goals_limit=2]]
  unfolding isa_count_decided_st_def isasat_bounded_assn_def
  by sepref

sepref_def polarity_pol_fast
  is ‹uncurry (mop_polarity_pol)›
  :: ‹trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k →⇩a tri_bool_assn›
  unfolding mop_polarity_pol_def trail_pol_fast_assn_def
    polarity_pol_def polarity_pol_pre_def
  by sepref

sepref_def polarity_st_heur_pol_fast
  is ‹uncurry (mop_polarity_st_heur)›
  :: ‹isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k →⇩a tri_bool_assn›
  unfolding mop_polarity_st_heur_alt_def isasat_bounded_assn_def polarity_st_pre_def
    mop_polarity_st_heur_alt_def
  supply [[goals_limit = 1]]
  by sepref


subsection ‹More theorems›

lemma count_decided_st_heur_alt_def:
   ‹count_decided_st_heur = (λ(M, _). count_decided_pol M)›
  by (auto simp: count_decided_st_heur_def count_decided_pol_def)

sepref_def count_decided_st_heur_pol_fast
  is ‹RETURN o count_decided_st_heur›
  :: ‹isasat_bounded_assn⇧k →⇩a uint32_nat_assn›
  unfolding isasat_bounded_assn_def count_decided_st_heur_alt_def
  supply [[goals_limit = 1]]
  by sepref

sepref_def access_lit_in_clauses_heur_fast_code
  is ‹uncurry2 (RETURN ooo access_lit_in_clauses_heur)›
  :: ‹[λ((S, i), j). access_lit_in_clauses_heur_pre ((S, i), j) ∧
           length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
      isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k  *⇩a sint64_nat_assn⇧k → unat_lit_assn›
  supply [[goals_limit=1]] arena_lit_pre_le[dest]
  unfolding isasat_bounded_assn_def access_lit_in_clauses_heur_alt_def
    access_lit_in_clauses_heur_pre_def
  unfolding fold_tuple_optimizations
  by sepref


sepref_register ‹(=) :: clause_status ⇒ clause_status ⇒ _›


lemma [def_pat_rules]: "append_ll ≡ op_list_list_push_back"
  by (rule eq_reflection) (auto simp: append_ll_def fun_eq_iff)

sepref_register rewatch_heur mop_append_ll mop_arena_length

sepref_def mop_append_ll_impl
  is ‹uncurry2 mop_append_ll›
  :: ‹[λ((W, i), _). length (W ! (nat_of_lit i)) < sint64_max]⇩a
    watchlist_fast_assn⇧d *⇩a unat_lit_assn⇧k *⇩a watcher_fast_assn⇧k → watchlist_fast_assn›
  unfolding mop_append_ll_def
  by sepref


sepref_def rewatch_heur_fast_code
  is ‹uncurry2 (rewatch_heur)›
  :: ‹[λ((vdom, arena), W). (∀x ∈ set vdom. x ≤ sint64_max) ∧ length arena ≤ sint64_max ∧
        length vdom ≤ sint64_max]⇩a
        vdom_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a watchlist_fast_assn⇧d → watchlist_fast_assn›
  supply [[goals_limit=1]]
     arena_lit_pre_le_sint64_max[dest] arena_is_valid_clause_idx_le_uint64_max[dest]
  supply [simp] = append_ll_def
  supply [dest] = arena_lit_implI(1)
  unfolding rewatch_heur_alt_def Let_def PR_CONST_def
  unfolding while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  unfolding if_not_swap
    FOREACH_cond_def FOREACH_body_def
  apply (annot_snat_const "TYPE(64)")
  by sepref


sepref_def rewatch_heur_st_fast_code
  is ‹(rewatch_heur_st_fast)›
  :: ‹[rewatch_heur_st_fast_pre]⇩a
       isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding rewatch_heur_st_def PR_CONST_def rewatch_heur_st_fast_pre_def
    isasat_bounded_assn_def rewatch_heur_st_fast_def
  unfolding fold_tuple_optimizations
  by sepref


sepref_register length_avdom

sepref_def length_avdom_fast_code
  is ‹RETURN o length_avdom›
  :: ‹isasat_bounded_assn⇧k →⇩a sint64_nat_assn›
  unfolding length_avdom_alt_def isasat_bounded_assn_def
  supply [[goals_limit = 1]]
  by sepref

sepref_register get_the_propagation_reason_heur

sepref_def get_the_propagation_reason_heur_fast_code
  is ‹uncurry get_the_propagation_reason_heur›
  :: ‹isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k →⇩a snat_option_assn' TYPE(64)›
  unfolding get_the_propagation_reason_heur_alt_def
     isasat_bounded_assn_def
  supply [[goals_limit = 1]]
  by sepref


sepref_def clause_is_learned_heur_code2
  is ‹uncurry (RETURN oo clause_is_learned_heur)›
  :: ‹[λ(S, C). arena_is_valid_clause_vdom (get_clauses_wl_heur S) C]⇩a
      isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k → bool1_assn›
  supply [[goals_limit = 1]]
  unfolding clause_is_learned_heur_alt_def isasat_bounded_assn_def
  by sepref

sepref_register clause_lbd_heur


lemma clause_lbd_heur_alt_def:
  ‹clause_lbd_heur = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom,
     lcount) C.
     arena_lbd N' C)›
  by (intro ext) (auto simp: clause_lbd_heur_def)

sepref_def clause_lbd_heur_code2
  is ‹uncurry (RETURN oo clause_lbd_heur)›
  :: ‹[λ(S, C). get_clause_LBD_pre (get_clauses_wl_heur S) C]⇩a
       isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k → uint32_nat_assn›
  unfolding isasat_bounded_assn_def clause_lbd_heur_alt_def
  supply [[goals_limit = 1]]
  by sepref



sepref_register mark_garbage_heur


sepref_def mark_garbage_heur_code2
  is ‹uncurry2 (RETURN ooo mark_garbage_heur)›
  :: ‹[λ((C, i), S). mark_garbage_pre (get_clauses_wl_heur S, C) ∧ i < length_avdom S ∧
         get_learned_count S ≥ 1]⇩a
       sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit = 1]]
  unfolding mark_garbage_heur_def isasat_bounded_assn_def delete_index_and_swap_alt_def
    length_avdom_def fold_tuple_optimizations
  apply (annot_unat_const "TYPE(64)")
  by sepref

sepref_register delete_index_vdom_heur


sepref_def delete_index_vdom_heur_fast_code2
  is ‹uncurry (RETURN oo delete_index_vdom_heur)›
  :: ‹[λ(i, S). i < length_avdom S]⇩a
        sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit = 1]]
  unfolding delete_index_vdom_heur_def isasat_bounded_assn_def delete_index_and_swap_alt_def
    length_avdom_def fold_tuple_optimizations
  by sepref

sepref_register access_length_heur

sepref_def access_length_heur_fast_code2
  is ‹uncurry (RETURN oo access_length_heur)›
  :: ‹[λ(S, C). arena_is_valid_clause_idx (get_clauses_wl_heur S) C]⇩a
       isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k → sint64_nat_assn›
  supply [[goals_limit = 1]]
  unfolding access_length_heur_alt_def isasat_bounded_assn_def fold_tuple_optimizations
  by sepref

sepref_register marked_as_used_st

sepref_def marked_as_used_st_fast_code
  is ‹uncurry (RETURN oo marked_as_used_st)›
  :: ‹[λ(S, C). marked_as_used_pre (get_clauses_wl_heur S) C]⇩a
       isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k → bool1_assn›
  supply [[goals_limit = 1]]
  unfolding marked_as_used_st_alt_def isasat_bounded_assn_def fold_tuple_optimizations
  by sepref


sepref_register mark_unused_st_heur
sepref_def mark_unused_st_fast_code
  is ‹uncurry (RETURN oo mark_unused_st_heur)›
  :: ‹[λ(C, S). arena_act_pre (get_clauses_wl_heur S) C]⇩a
        sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  unfolding mark_unused_st_heur_def isasat_bounded_assn_def
    arena_act_pre_mark_used[intro!]
  supply [[goals_limit = 1]]
  by sepref


sepref_def get_slow_ema_heur_fast_code
  is ‹RETURN o get_slow_ema_heur›
  :: ‹isasat_bounded_assn⇧k →⇩a ema_assn›
  unfolding get_slow_ema_heur_alt_def isasat_bounded_assn_def heuristic_assn_def
  by sepref

sepref_def get_fast_ema_heur_fast_code
  is ‹RETURN o get_fast_ema_heur›
  :: ‹isasat_bounded_assn⇧k →⇩a ema_assn›
  unfolding get_fast_ema_heur_alt_def isasat_bounded_assn_def heuristic_assn_def
  by sepref

sepref_def get_conflict_count_since_last_restart_heur_fast_code
  is ‹RETURN o get_conflict_count_since_last_restart_heur›
  :: ‹isasat_bounded_assn⇧k →⇩a word64_assn›
  unfolding get_counflict_count_heur_alt_def isasat_bounded_assn_def heuristic_assn_def
  by sepref

sepref_def get_learned_count_fast_code
  is ‹RETURN o get_learned_count›
  :: ‹isasat_bounded_assn⇧k →⇩a uint64_nat_assn›
  unfolding get_learned_count_alt_def isasat_bounded_assn_def
  by sepref

sepref_register incr_restart_stat

sepref_def incr_restart_stat_fast_code
  is ‹incr_restart_stat›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding incr_restart_stat_def isasat_bounded_assn_def PR_CONST_def
    heuristic_assn_def fold_tuple_optimizations
  by sepref

sepref_register incr_lrestart_stat

sepref_def incr_lrestart_stat_fast_code
  is ‹incr_lrestart_stat›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding incr_lrestart_stat_def isasat_bounded_assn_def PR_CONST_def
    heuristic_assn_def fold_tuple_optimizations
  by sepref


sepref_def opts_restart_st_fast_code
  is ‹RETURN o opts_restart_st›
  :: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
  unfolding opts_restart_st_def isasat_bounded_assn_def
  by sepref


sepref_def opts_reduction_st_fast_code
  is ‹RETURN o opts_reduction_st›
  :: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
  unfolding opts_reduction_st_def isasat_bounded_assn_def
  by sepref

sepref_register opts_reduction_st opts_restart_st


lemma emag_get_value_alt_def:
  ‹ema_get_value = (λ(a, b, c, d). a)›
  by auto
sepref_def ema_get_value_impl
  is ‹RETURN o ema_get_value›
  :: ‹ema_assn⇧k →⇩a word_assn›
  unfolding emag_get_value_alt_def
  by sepref


sepref_register isasat_length_trail_st

sepref_def isasat_length_trail_st_code
  is ‹RETURN o isasat_length_trail_st›
  :: ‹[isa_length_trail_pre o get_trail_wl_heur]⇩a isasat_bounded_assn⇧k  → sint64_nat_assn›
  supply [[goals_limit=1]]
  unfolding isasat_length_trail_st_alt_def isasat_bounded_assn_def
  by sepref

sepref_register get_pos_of_level_in_trail_imp_st

sepref_def get_pos_of_level_in_trail_imp_st_code
  is ‹uncurry get_pos_of_level_in_trail_imp_st›
  :: ‹isasat_bounded_assn⇧k *⇩a uint32_nat_assn⇧k  →⇩a sint64_nat_assn›
  supply [[goals_limit=1]]
  unfolding get_pos_of_level_in_trail_imp_alt_def isasat_bounded_assn_def
  apply (rewrite in "_" eta_expand[where f = RETURN])
  apply (rewrite in "RETURN ⌑" annot_unat_snat_upcast[where 'l=64])
  by sepref



sepref_register neq : "(op_neq :: clause_status ⇒ _ ⇒ _)"
lemma status_neq_refine1: "((≠),op_neq) ∈ status_rel → status_rel → bool_rel"
  by (auto simp: status_rel_def)

sepref_def status_neq_impl is [] "uncurry (RETURN oo (≠))"
  :: "(unat_assn' TYPE(32))⇧k *⇩a (unat_assn' TYPE(32))⇧k →⇩a bool1_assn"
  by sepref

lemmas [sepref_fr_rules] = status_neq_impl.refine[FCOMP status_neq_refine1]

lemma clause_not_marked_to_delete_heur_alt_def:
  ‹RETURN oo clause_not_marked_to_delete_heur = (λ(M, arena, D, oth) C.
      RETURN (arena_status arena C ≠ DELETED))›
  unfolding clause_not_marked_to_delete_heur_def by (auto intro!: ext)

sepref_def clause_not_marked_to_delete_heur_fast_code
  is ‹uncurry (RETURN oo clause_not_marked_to_delete_heur)›
  :: ‹[clause_not_marked_to_delete_heur_pre]⇩a isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k → bool1_assn›
  supply [[goals_limit=1]]
  unfolding clause_not_marked_to_delete_heur_alt_def isasat_bounded_assn_def
     clause_not_marked_to_delete_heur_pre_def
  by sepref

lemma mop_clause_not_marked_to_delete_heur_alt_def:
  ‹mop_clause_not_marked_to_delete_heur = (λ(M, arena, D, oth) C. do {
    ASSERT(clause_not_marked_to_delete_heur_pre ((M, arena, D, oth), C));
     RETURN (arena_status arena C ≠ DELETED)
   })›
  unfolding clause_not_marked_to_delete_heur_def mop_clause_not_marked_to_delete_heur_def
  by (auto intro!: ext)

sepref_def mop_clause_not_marked_to_delete_heur_impl
  is ‹uncurry mop_clause_not_marked_to_delete_heur›
  :: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a bool1_assn›
  unfolding mop_clause_not_marked_to_delete_heur_alt_def
    clause_not_marked_to_delete_heur_pre_def  prod.case isasat_bounded_assn_def
  by sepref

sepref_def delete_index_and_swap_code2
  is ‹uncurry (RETURN oo delete_index_and_swap)›
  :: ‹[λ(xs, i). i < length xs]⇩a
      vdom_fast_assn⇧d *⇩a sint64_nat_assn⇧k → vdom_fast_assn›
  unfolding delete_index_and_swap.simps
  by sepref

sepref_def mop_mark_garbage_heur_impl
  is ‹uncurry2 mop_mark_garbage_heur›
  :: ‹[λ((C, i), S). length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
      sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding mop_mark_garbage_heur_alt_def
    clause_not_marked_to_delete_heur_pre_def prod.case isasat_bounded_assn_def
  apply (annot_unat_const "TYPE(64)")
  by sepref

sepref_def mop_mark_unused_st_heur_impl
  is ‹uncurry mop_mark_unused_st_heur›
  :: ‹ sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  unfolding mop_mark_unused_st_heur_def
  by sepref


sepref_def mop_arena_lbd_st_impl
  is ‹uncurry mop_arena_lbd_st›
  :: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a uint32_nat_assn›
  supply [[goals_limit=1]]
  unfolding mop_arena_lbd_st_alt_def isasat_bounded_assn_def
  by sepref

sepref_def mop_arena_status_st_impl
  is ‹uncurry mop_arena_status_st›
  :: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a status_impl_assn›
  supply [[goals_limit=1]]
  unfolding mop_arena_status_st_alt_def isasat_bounded_assn_def
  by sepref

sepref_def mop_marked_as_used_st_impl
  is ‹uncurry mop_marked_as_used_st›
  :: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a bool1_assn›
  supply [[goals_limit=1]]
  unfolding mop_marked_as_used_st_alt_def isasat_bounded_assn_def
  by sepref

sepref_def mop_arena_length_st_impl
  is ‹uncurry mop_arena_length_st›
  :: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a sint64_nat_assn›
  supply [[goals_limit=1]]
  unfolding mop_arena_length_st_alt_def isasat_bounded_assn_def
  by sepref

sepref_register incr_wasted_st full_arena_length_st wasted_bytes_st
sepref_def incr_wasted_st_impl
  is ‹uncurry (RETURN oo incr_wasted_st)›
  :: ‹word64_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply[[goals_limit=1]]
  unfolding incr_wasted_st_def incr_wasted.simps
    isasat_bounded_assn_def heuristic_assn_def
  by sepref

sepref_def full_arena_length_st_impl
  is ‹RETURN o full_arena_length_st›
  :: ‹isasat_bounded_assn⇧k →⇩a sint64_nat_assn›
  unfolding full_arena_length_st_def isasat_bounded_assn_def
  by sepref


sepref_def wasted_bytes_st_impl
  is ‹RETURN o wasted_bytes_st›
  :: ‹isasat_bounded_assn⇧k →⇩a word64_assn›
  supply [[goals_limit=1]]
  unfolding isasat_bounded_assn_def
    heuristic_assn_def wasted_bytes_st_def
  by sepref

lemma set_zero_wasted_def:
  ‹set_zero_wasted = (λ(fast_ema, slow_ema, res_info, wasted, φ, target, best).
    (fast_ema, slow_ema, res_info, 0, φ, target, best))›
  by (auto intro!: ext)

sepref_def set_zero_wasted_impl
  is ‹RETURN o set_zero_wasted›
  :: ‹heuristic_assn⇧d →⇩a heuristic_assn›
  unfolding heuristic_assn_def set_zero_wasted_def
  by sepref

lemma mop_save_phase_heur_alt_def:
  ‹mop_save_phase_heur = (λ L b (fast_ema, slow_ema, res_info, wasted, φ, target, best). do {
    ASSERT(L < length φ);
    RETURN (fast_ema, slow_ema, res_info, wasted, φ[L := b], target,
                 best)})›
  unfolding mop_save_phase_heur_def save_phase_heur_def save_phase_heur_pre_def
    heuristic_assn_def
  by (auto intro!: ext)

sepref_def mop_save_phase_heur_impl
  is ‹uncurry2 (mop_save_phase_heur)›
  :: ‹atom_assn⇧k *⇩a bool1_assn⇧k *⇩a heuristic_assn⇧d →⇩a heuristic_assn›
  supply [[goals_limit=1]]
  unfolding mop_save_phase_heur_alt_def save_phase_heur_def save_phase_heur_pre_def
    heuristic_assn_def
  apply annot_all_atm_idxs
  by sepref

sepref_register set_zero_wasted mop_save_phase_heur

experiment begin

export_llvm
  ema_update_impl
  VMTF_Node_impl
  VMTF_stamp_impl
  VMTF_get_prev_impl
  VMTF_get_next_impl
  opts_restart_impl
  opts_reduce_impl
  opts_unbounded_mode_impl
  get_conflict_wl_is_None_fast_code
  isa_count_decided_st_fast_code
  polarity_st_heur_pol_fast
  count_decided_st_heur_pol_fast
  access_lit_in_clauses_heur_fast_code
  rewatch_heur_fast_code
  rewatch_heur_st_fast_code
  set_zero_wasted_impl

end

end