Theory IsaSAT_Rephase_LLVM (Isabelle2019: June 2019)

theory IsaSAT_Rephase_LLVM
  imports IsaSAT_Rephase IsaSAT_Show_LLVM
begin

sepref_def rephase_random_impl
  is ‹uncurry rephase_random›
  :: ‹word_assn⇧^k *⇩_a phase_saver_assn⇧^d →⇩_a phase_saver_assn›
  supply [[goals_limit=1]]
  unfolding rephase_random_def
    while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  apply (annot_snat_const "TYPE(64)")
  by sepref

sepref_def rephase_init_impl
  is ‹uncurry rephase_init›
  :: ‹bool1_assn⇧^k *⇩_a phase_saver_assn⇧^d →⇩_a phase_saver_assn›
  unfolding rephase_init_def
    while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  apply (annot_snat_const "TYPE(64)")
  by sepref

sepref_def copy_phase_impl
  is ‹uncurry copy_phase›
  :: ‹phase_saver_assn⇧^k *⇩_a phase_saver'_assn⇧^d →⇩_a phase_saver'_assn›
  unfolding copy_phase_alt_def
    while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  unfolding simp_thms(21) ― ‹remove \<^term>‹a ∧ True› from condition›
  apply (annot_snat_const "TYPE(64)")
  by sepref

definition copy_phase2 where
  ‹copy_phase2 = copy_phase›

sepref_def copy_phase_impl2
  is ‹uncurry copy_phase2›
  :: ‹phase_saver'_assn⇧^k *⇩_a phase_saver_assn⇧^d →⇩_a phase_saver_assn›
  unfolding copy_phase_def copy_phase2_def
    while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  unfolding simp_thms(21) ― ‹remove \<^term>‹a ∧ True› from condition›
  apply (annot_snat_const "TYPE(64)")
  by sepref



sepref_register rephase_init rephase_random copy_phase

sepref_def phase_save_phase_impl
  is ‹uncurry phase_save_phase›
  :: ‹sint64_nat_assn⇧^k *⇩_a phase_heur_assn⇧^d →⇩_a phase_heur_assn›
  supply [[goals_limit=1]]
  unfolding phase_save_phase_def
  by sepref


sepref_def save_phase_heur_impl
  is ‹uncurry save_rephase_heur›
  ::  ‹sint64_nat_assn⇧^k *⇩_a heuristic_assn⇧^d →⇩_a heuristic_assn›
  supply [[goals_limit=1]]
  unfolding save_rephase_heur_def heuristic_assn_def
  by sepref


sepref_def save_phase_heur_st
  is save_phase_st
  ::  ‹isasat_bounded_assn⇧^d →⇩_a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding save_phase_st_def isasat_bounded_assn_def
  by sepref

sepref_def phase_save_rephase_impl
  is ‹uncurry phase_rephase›
  :: ‹word_assn⇧^k *⇩_a phase_heur_assn⇧^d →⇩_a phase_heur_assn›
  unfolding phase_rephase_def copy_phase2_def[symmetric]
  by sepref


sepref_def rephase_heur_impl
  is ‹uncurry rephase_heur›
  :: ‹word_assn⇧^k *⇩_a heuristic_assn⇧^d →⇩_a heuristic_assn›
  unfolding rephase_heur_def heuristic_assn_def
  by sepref

lemma current_rephasing_phase_alt_def:
  ‹RETURN o current_rephasing_phase =
    (λ(fast_ema, slow_ema, res_info, wasted,
      (φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase, length_phase)).
      RETURN curr_phase)›
  unfolding current_rephasing_phase_def
    phase_current_rephasing_phase_def
  by (auto intro!: ext)

sepref_def current_rephasing_phase
  is ‹RETURN o current_rephasing_phase›
  :: ‹heuristic_assn⇧^k →⇩_a word64_assn›
  unfolding current_rephasing_phase_alt_def heuristic_assn_def
  by sepref

sepref_register rephase_heur
sepref_def rephase_heur_st_impl
  is rephase_heur_st
  ::  ‹isasat_bounded_assn⇧^d →⇩_a isasat_bounded_assn›
  unfolding rephase_heur_st_def isasat_bounded_assn_def
  by sepref


experiment
begin
export_llvm rephase_heur_st_impl
  save_phase_heur_st
end

end