Theory IsaSAT_Show_LLVM

theory IsaSAT_Show_LLVM
  imports
    IsaSAT_Show
    IsaSAT_Setup0_LLVM
begin


sepref_register isasat_current_information print_c print_uint64

sepref_def print_c_impl
  is ‹RETURN o print_c›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding print_c_def
  by sepref

sepref_def print_uint64_impl
  is ‹RETURN o print_uint64›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding print_uint64_def
  by sepref

sepref_def print_open_colour_impl
  is ‹RETURN o print_open_colour›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding print_open_colour_def
  by sepref


sepref_def print_close_colour_impl
  is ‹RETURN o print_close_colour›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding print_close_colour_def
  by sepref

sepref_def print_char_impl
  is ‹RETURN o print_char›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding print_char_def
  by sepref


sepref_def isasat_current_information_impl [llvm_code]
  is ‹uncurry2 (RETURN ooo isasat_current_information_stats)›
  :: ‹word_assn⇧^k *⇩_a isasat_stats_assn⇧^d *⇩_a lcount_assn⇧^k →⇩_a isasat_stats_assn›
  unfolding isasat_current_information_stats_def
    isasat_current_information_def lcount_assn_def
  by sepref

lemma isasat_current_status_alt_def:
‹isasat_current_status =
   (λS.
  let
      (heur, S) = extract_heur_wl_heur S;
      (stats, S) = extract_stats_wl_heur S;
      (lcount, S) = extract_lcount_wl_heur S;
       curr_phase = current_restart_phase (heur);
        stats = (isasat_current_information curr_phase stats lcount)
     in RETURN (update_stats_wl_heur stats (update_heur_wl_heur heur (update_lcount_wl_heur lcount S))))›
  by (auto simp: isasat_current_status_def state_extractors split: isasat_int_splits intro!: ext)

sepref_def isasat_current_status_fast_code
  is ‹isasat_current_status›
  :: ‹isasat_bounded_assn⇧^d →⇩_a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding isasat_current_status_alt_def isasat_current_information_def
  by sepref

lemma isasat_current_progress_alt_def:
‹isasat_current_progress =
   (λc S. case S of Tuple17 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena occs ⇒
     let
       curr_phase = current_restart_phase heur;
       _ = isasat_print_progress c curr_phase stats clss
     in RETURN ())›
   unfolding isasat_current_progress_def
  apply (intro ext, rename_tac c S, case_tac S)
  apply (auto simp: Let_def intro!: ext)
  done


sepref_def isasat_print_progress_impl
  is ‹uncurry3 (RETURN oooo isasat_print_progress)›
  :: ‹word_assn⇧^k *⇩_a word_assn⇧^k *⇩_a isasat_stats_assn⇧^k *⇩_a lcount_assn⇧^k →⇩_a unit_assn›
  unfolding isasat_current_progress_alt_def isasat_print_progress_def lcount_assn_def
 by sepref

sepref_register isasat_current_progress
sepref_def isasat_current_progress_impl
  is ‹uncurry isasat_current_progress›
  :: ‹word_assn⇧^k *⇩_a isasat_assn⇧^k →⇩_a unit_assn›
  supply [[goals_limit=1]]
  unfolding isasat_current_progress_alt_def isasat_bounded_assn_def
  by sepref
end