Theory IsaSAT_Rephase_LLVM

theory IsaSAT_Rephase_LLVM
  imports IsaSAT_Rephase IsaSAT_Literals_LLVM
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN
 
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›


definition phase_heur_assn :: ‹phase_save_heur ⇒ _› where
  ‹phase_heur_assn ≡ phase_saver_assn ×⇩a word64_assn ×⇩a phase_saver'_assn ×⇩a word64_assn ×⇩a
     phase_saver'_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn›

schematic_goal mk_free_lookup_clause_rel_assn[sepref_frame_free_rules]: ‹MK_FREE phase_heur_assn ?fr›
  unfolding phase_heur_assn_def
  by synthesize_free+

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_def rephase_flipped_impl
  is ‹rephase_flipped›
  :: ‹phase_saver_assn⇧d →⇩a phase_saver_assn›
  supply [[goals_limit=1]]
  unfolding rephase_flipped_def
    while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref


sepref_register rephase_init rephase_random copy_phase reset_best_phase reset_target_phase
    rephase_flipped

sepref_def reset_best_phase_impl
  is ‹reset_best_phase›
  :: ‹phase_heur_assn⇧d →⇩a phase_heur_assn›
  supply [[goals_limit=1]]
  unfolding reset_best_phase_def phase_heur_assn_def
  by sepref

sepref_def reset_target_phase_impl
  is ‹reset_target_phase›
  :: ‹phase_heur_assn⇧d →⇩a phase_heur_assn›
  supply [[goals_limit=1]]
  unfolding reset_target_phase_def phase_heur_assn_def
  by sepref

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

sepref_def get_next_phase_imp
  is ‹uncurry2 get_next_phase_stats›
  :: ‹bool1_assn⇧k *⇩a atom_assn⇧k *⇩a phase_heur_assn⇧k →⇩a bool1_assn›
  unfolding get_next_phase_stats_def phase_heur_assn_def
  apply annot_all_atm_idxs
  by  sepref

sepref_register current_phase_letter
sepref_def current_phase_letter_impl
  is ‹RETURN o current_phase_letter›
  :: ‹word64_assn⇧k →⇩a word64_assn›
  unfolding current_phase_letter_def
  by sepref

end