Theory IsaSAT_Restart_Simp_LLVM

theory IsaSAT_Restart_Simp_LLVM
imports  IsaSAT_Restart_Heuristics_LLVM IsaSAT_Garbage_Collect_LLVM
  IsaSAT_Other_LLVM IsaSAT_Propagate_Conflict_LLVM IsaSAT_Inprocessing_LLVM IsaSAT_Restart_LLVM
begin

sepref_register cdcl_twl_mark_clauses_to_delete mark_to_delete_clauses_GC_wl_D_heur

sepref_def cdcl_twl_restart_wl_heur_fast_code
  is ‹cdcl_twl_restart_wl_heur›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  unfolding cdcl_twl_restart_wl_heur_def
  supply [[goals_limit = 1]]
  by sepref

sepref_def cdcl_twl_mark_clauses_to_delete_fast_code
  is ‹cdcl_twl_mark_clauses_to_delete›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  unfolding cdcl_twl_mark_clauses_to_delete_def
  supply [[goals_limit = 1]]
  by sepref


sepref_def cdcl_twl_full_restart_wl_D_GC_heur_prog_fast_code
  is ‹cdcl_twl_full_restart_wl_D_GC_heur_prog›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]⇩a
     isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit = 1]]
  unfolding cdcl_twl_full_restart_wl_D_GC_heur_prog_def
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_def cdcl_twl_full_restart_wl_D_inprocess_heur_prog_fast_code
  is ‹cdcl_twl_full_restart_wl_D_inprocess_heur_prog›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]⇩a
     isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit = 1]]
  supply [simp] = isasat_fast_relaxed_def
  unfolding cdcl_twl_full_restart_wl_D_inprocess_heur_prog_def
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_register restart_required_heur cdcl_twl_restart_wl_heur
  cdcl_twl_full_restart_wl_D_inprocess_heur_prog

sepref_def restart_prog_wl_D_heur_fast_code
  is ‹uncurry4 restart_prog_wl_D_heur›
  :: ‹[λ((((S, _), _), n), _). isasat_fast_relaxed2 S n]⇩a
      isasat_bounded_assn⇧d *⇩a uint64_nat_assn⇧k  *⇩a uint64_nat_assn⇧k  *⇩a uint64_nat_assn⇧k *⇩a
        bool1_assn⇧k → isasat_bounded_assn ×⇩a uint64_nat_assn ×⇩a uint64_nat_assn ×⇩a uint64_nat_assn›
  unfolding restart_prog_wl_D_heur_def isasat_fast_relaxed_def isasat_fast_relaxed2_def
  supply [[goals_limit = 1]]
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

lemma cdcl_twl_stgy_restart_prog_bounded_wl_heurI1:
  assumes
    ‹isasat_fast a1'b›
    ‹learned_clss_count a2'e ≤ Suc (learned_clss_count a1'b)›
  shows ‹learned_clss_count a2'e ≤ unat64_max›
  using assms
  by (auto simp: isasat_fast_def)

lemma cdcl_twl_stgy_restart_prog_bounded_wl_heurI2:
  ‹isasat_fast x ⟹ learned_clss_count x ≤ unat64_max›
  by (auto simp: isasat_fast_def)


lemma cdcl_twl_stgy_restart_prog_bounded_wl_heurI3:
  assumes
    ‹isasat_fast S›
    ‹length (get_clauses_wl_heur T) ≤ length (get_clauses_wl_heur S)›
    ‹learned_clss_count T ≤ (learned_clss_count S)›
  shows ‹isasat_fast T›
  using assms
  by (auto simp: isasat_fast_def)

sepref_register cdcl_twl_stgy_restart_prog_bounded_wl_heur
sepref_def cdcl_twl_stgy_restart_prog_wl_heur_fast_code
  is ‹cdcl_twl_stgy_restart_prog_bounded_wl_heur›
  :: ‹[λS. isasat_fast S]⇩a isasat_bounded_assn⇧d → bool1_assn ×⇩a isasat_bounded_assn›
  unfolding cdcl_twl_stgy_restart_prog_bounded_wl_heur_def
  supply [[goals_limit = 1]] isasat_fast_countD[dest]
  supply [intro] = cdcl_twl_stgy_restart_prog_bounded_wl_heurI2
  supply [sepref_bounds_simps del] = unat32_max_def snat32_max_def unat64_max_def snat64_max_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

experiment
begin
   export_llvm opts_reduction_st_fast_code
    opts_restart_st_fast_code
    get_conflict_count_since_last_restart_heur_fast_code
    get_fast_ema_heur_fast_code
    get_slow_ema_heur_fast_code
    get_learned_count_fast_code
    upper_restart_bound_reached_fast_impl
    minimum_number_between_restarts_impl
    restart_required_heur_fast_code
    cdcl_twl_full_restart_wl_D_GC_heur_prog_fast_code
    cdcl_twl_restart_wl_heur_fast_code
    cdcl_twl_mark_clauses_to_delete_fast_code
    cdcl_twl_local_restart_wl_D_heur_fast_code
   get_conflict_wl_is_None_fast_code
end

end