Theory IsaSAT_Show

theory IsaSAT_Show
  imports
    Show.Show_Instances
    IsaSAT_Setup
begin

chapter ‹Printing information about progress›

text ‹We provide a function to print some information about the state.
  This is mostly meant to ease extracting statistics and printing information
  during the run.
  Remark that this function is basically an FFI (to follow Andreas Lochbihler words) and is
  not unsafe (since printing has not side effects), but we do not need any correctness theorems.

  However, it seems that the PolyML as targeted by ‹export_code checking› does
  not support that print function. Therefore, we cannot provide the code printing equations
  by default.

  For the LLVM version code equations are not supported and hence we replace the function by
  hand.
›
definition println_string :: ‹String.literal ⇒ unit› where
  ‹println_string _ = ()›

definition print_c :: ‹64 word ⇒ unit› where
  ‹print_c _ = ()›


definition print_char :: ‹64 word ⇒ unit› where
  ‹print_char _ = ()›

definition print_uint64 :: ‹64 word ⇒ unit› where
  ‹print_uint64 _ = ()›


subsection ‹Print Information for IsaSAT›

text ‹Printing the information slows down the solver by a huge factor.›
definition isasat_banner_content where
‹isasat_banner_content =
''c  conflicts       decisions     restarts   uset    avg_lbd
'' @
''c        propagations     reductions     GC    Learnt
''  @
''c                                             clauses ''›

definition isasat_information_banner :: ‹_ ⇒ unit nres› where
‹isasat_information_banner _ =
    RETURN (println_string (String.implode (show isasat_banner_content)))›

definition isasat_current_information_stats :: ‹64 word ⇒ isasat_stats ⇒ clss_size ⇒ isasat_stats› where
  ‹isasat_current_information_stats =
   (λcurr_phase stats (lcount, lcountUE, lcountUEk, lcountUS, _).
     if (stats_conflicts stats) AND 8191 = 8191 ― ‹\<^term>‹8191 = 8192 - 1›, i.e., we print when all first bits are 1.›
     then do{
       let _ = print_c (stats_propagations stats);
         _ = if curr_phase = 1 then print_open_colour 33 else ();
         _ = print_char 126;
         _ = print_uint64 (stats_propagations stats);
         _ = print_uint64 (stats_conflicts stats);
         _ = print_uint64 (of_nat lcount);
         _ = print_uint64 (irredundant_clss stats);
         _ = print_uint64 (stats_restarts stats);
         _ = print_uint64 (stats_reductions stats);
         _ = print_uint64 (stats_fixed stats);
         _ = print_uint64 (stats_gcs stats);
         _ = print_uint64 (ema_extract_value (stats_avg_lbd stats));
         _ = print_uint64 (of_nat lcountUE);
         _ = print_uint64 (of_nat lcountUEk);
         _ = print_uint64 (of_nat lcountUS);
         _ = print_close_colour 0
       in
         stats}
      else stats
    )›

definition isasat_current_information :: ‹64 word ⇒ isasat_stats ⇒ clss_size ⇒ isasat_stats› where
‹isasat_current_information =
  (λcurr_phase stats count. (isasat_current_information_stats curr_phase stats count)
    )›



definition isasat_current_status :: ‹isasat ⇒ isasat nres› where
‹isasat_current_status =
   (λS.
     let curr_phase = current_restart_phase (get_heur S);
        stats = (isasat_current_information curr_phase (get_stats_heur S) (get_learned_count S))
     in RETURN (set_stats_wl_heur stats S))›

lemma isasat_current_status_id:
  ‹(isasat_current_status, RETURN o id) ∈
  {(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ r ∧ learned_clss_count S ≤ u}  →⇩f
   ⟨{(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ r ∧ learned_clss_count S ≤ u}⟩nres_rel›
  by (intro frefI nres_relI)
    (auto simp: twl_st_heur_def isasat_current_status_def learned_clss_count_def)

definition isasat_print_progress :: ‹64 word ⇒ 64 word ⇒ isasat_stats ⇒ clss_size ⇒ unit› where
‹isasat_print_progress c curr_phase =
  (λstats (lcount, lcountUE, lcountUEk, lcountUS, _).
     let _ = print_c (stats_propagations stats);
         _ = if curr_phase = 1 then print_open_colour 33 else ();
         _ = print_char c;
         _ = print_uint64 (stats_propagations stats);
         _ = print_uint64 (stats_conflicts stats);
         _ = print_uint64 (of_nat lcount);
         _ = print_uint64 (irredundant_clss stats);
         _ = print_uint64 (stats_restarts stats);
         _ = print_uint64 (stats_reductions stats);
         _ = print_uint64 (stats_fixed stats);
         _ = print_uint64 (stats_gcs stats);
         _ = print_uint64 (ema_extract_value (stats_avg_lbd stats));
         _ = print_uint64 (of_nat lcountUE);
         _ = print_uint64 (of_nat lcountUEk);
         _ = print_uint64 (of_nat lcountUS);
         _ = print_close_colour 0
     in
       ())›

definition isasat_current_progress :: ‹64 word ⇒ isasat ⇒ unit nres› where
‹isasat_current_progress =
   (λc S.
     let
       curr_phase = current_restart_phase (get_heur S);
       _ = isasat_print_progress c curr_phase (get_stats_heur S) (get_learned_count S)
     in RETURN ())›


end