Theory IsaSAT_Decide_LLVM

theory IsaSAT_Decide_LLVM
  imports IsaSAT_Decide_Defs IsaSAT_VMTF_State_LLVM IsaSAT_Setup_LLVM IsaSAT_Rephase_State_LLVM
begin
lemma decide_lit_wl_heur_alt_def:
  ‹decide_lit_wl_heur = (λL' S. do {
      let (M, S) = extract_trail_wl_heur S;
      let (stats, S) = extract_stats_wl_heur S;
      ASSERT(isa_length_trail_pre M);
      let j = isa_length_trail M;
      let S = update_literals_to_update_wl_heur j S;
      ASSERT(cons_trail_Decided_tr_pre (L', M));
      let M = cons_trail_Decided_tr L' M;
      let stats = incr_decision stats;
      let S = update_trail_wl_heur M S;
      let S = update_stats_wl_heur stats S;
        RETURN S})›
   by (auto simp: decide_lit_wl_heur_def state_extractors split: isasat_int_splits intro!: ext)

sepref_def decide_lit_wl_fast_code
  is ‹uncurry decide_lit_wl_heur›
  :: ‹unat_lit_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding decide_lit_wl_heur_alt_def
  by sepref


sepref_register find_unassigned_lit_wl_D_heur decide_lit_wl_heur

sepref_register isa_vmtf_find_next_undef

sepref_def isa_vmtf_find_next_undef_code is
  ‹uncurry isa_vmtf_find_next_undef› :: ‹vmtf_assn⇧k *⇩a trail_pol_fast_assn⇧k →⇩a atom.option_assn›
  unfolding isa_vmtf_find_next_undef_def vmtf_assn_def
  unfolding atom.fold_option
  apply (rewrite in ‹WHILEIT _ ⌑› short_circuit_conv)
  supply [[goals_limit = 1]]
  apply annot_all_atm_idxs
  by sepref

sepref_def isa_bump_find_next_undef_code is
  ‹uncurry isa_bump_find_next_undef› :: ‹heuristic_bump_assn⇧d *⇩a trail_pol_fast_assn⇧k →⇩a atom.option_assn ×⇩a heuristic_bump_assn›
  unfolding isa_bump_find_next_undef_def
  unfolding atom.fold_option
  supply [[goals_limit = 1]]
  apply annot_all_atm_idxs
  by sepref

sepref_register update_next_search
sepref_def update_next_search_code is
  ‹uncurry (RETURN oo update_next_search)› :: ‹atom.option_assn⇧k *⇩a vmtf_assn⇧d →⇩a vmtf_assn›
  unfolding update_next_search_def vmtf_assn_def
  by sepref


sepref_register isa_vmtf_find_next_undef_upd  mop_get_saved_phase_heur get_next_phase_st

sepref_def isa_vmtf_find_next_undef_upd_code is
  ‹uncurry isa_vmtf_find_next_undef_upd›
    :: ‹trail_pol_fast_assn⇧d *⇩a heuristic_bump_assn⇧d →⇩a (trail_pol_fast_assn ×⇩a heuristic_bump_assn) ×⇩a atom.option_assn›
  unfolding isa_vmtf_find_next_undef_upd_def
  by sepref

lemma find_unassigned_lit_wl_D_heur2_alt_def:
  ‹find_unassigned_lit_wl_D_heur2 = (λS. do {
    let (M, S) = extract_trail_wl_heur S;
    let (vm, S) = extract_vmtf_wl_heur S;
    let (heur, S) = extract_heur_wl_heur S;
      ((M, vm), L) ← isa_vmtf_find_next_undef_upd M vm;
      RETURN (update_heur_wl_heur (set_fully_propagated_heur heur) (update_trail_wl_heur M (update_vmtf_wl_heur vm S)), L)
    })›
   by (auto simp: find_unassigned_lit_wl_D_heur2_def state_extractors split: isasat_int_splits intro!: ext)
sepref_register find_unassigned_lit_wl_D_heur2
sepref_def find_unassigned_lit_wl_D_heur_impl
  is ‹find_unassigned_lit_wl_D_heur2›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn ×⇩a atom.option_assn›
  unfolding find_unassigned_lit_wl_D_heur2_alt_def
  by sepref

sepref_definition get_next_phase_heur_stats_impl'
  is ‹uncurry2 (λS C' D'. get_next_phase_heur C' D' S)›
  :: ‹[uncurry2 (λS C D. True)]⇩a heuristic_assn⇧k *⇩a bool1_assn⇧k *⇩a atom_assn⇧k → bool1_assn›
  by sepref

definition get_next_phase_st'_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹get_next_phase_st'_impl = (λN C D. read_heur_wl_heur_code (get_next_phase_heur_stats_impl C D) N)›

definition get_next_phase_st' :: ‹_› where
  ‹get_next_phase_st' N C D = (get_next_phase_st C D N)›

global_interpretation get_next_phase: read_heur_param_adder2 where
  R = bool1_rel and
  R' = atom_rel and
  f' = ‹ λC D S. get_next_phase_heur C D S› and
  f = ‹λC D S. get_next_phase_heur_stats_impl C D S› and
  x_assn = ‹bool1_assn› and
  P = ‹(λ_ _ _. True)›
  rewrites
     ‹(λN C D. read_heur_wl_heur_code (get_next_phase_heur_stats_impl C D) N) = get_next_phase_st'_impl› and
     ‹(λN C D. read_heur_wl_heur (get_next_phase_heur C D) N) = get_next_phase_st'›
  apply unfold_locales
  apply (rule get_next_phase_heur_stats_impl'.refine[unfolded get_next_phase_heur_stats_impl'_def])
  subgoal by (auto simp: get_next_phase_st'_impl_def)
  subgoal by (auto simp: read_all_st_def get_next_phase_st_def get_next_phase_st'_def split: isasat_int_splits
    intro!: ext)
  done

lemmas [sepref_fr_rules] = get_next_phase.refine
lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  get_next_phase_st'_impl_def[unfolded read_all_st_code_def]

sepref_def get_next_phase_st_impl
  is ‹uncurry2 get_next_phase_st›
  :: ‹bool1_assn⇧k *⇩a atom_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a bool1_assn›
  unfolding get_next_phase_st'_def[symmetric]
  by sepref

sepref_def decide_wl_or_skip_D_fast_code
  is ‹decide_wl_or_skip_D_heur›
  :: ‹isasat_bounded_assn⇧d →⇩a bool1_assn ×⇩a isasat_bounded_assn›
  supply[[goals_limit=1]]
  apply (rule hfref_refine_with_pre[OF decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur, unfolded Down_id_eq])
  unfolding decide_wl_or_skip_D_heur'_def option.case_eq_if atom.fold_option
  by sepref

experiment begin

export_llvm
  decide_lit_wl_fast_code
  isa_vmtf_find_next_undef_code
  update_next_search_code
  isa_vmtf_find_next_undef_upd_code
  decide_wl_or_skip_D_fast_code

end


end