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 zero_some_stats :: ‹stats ⇒ stats› where
‹zero_some_stats = (λ(propa, confl, decs, frestarts, lrestarts, uset, gcs, lbds).
     (propa, confl, decs, frestarts, lrestarts, uset, gcs, 0))›

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

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

definition isasat_current_information :: ‹64 word ⇒ stats ⇒ _ ⇒ stats› where
‹isasat_current_information =
   (λcurr_phase (propa, confl, decs, frestarts, lrestarts, uset, gcs, lbds) lcount.
     if confl AND 8191 = 8191 ― ‹\<^term>‹8191 = 8192 - 1›, i.e., we print when all first bits are 1.›
     then do{
       let _ = print_c propa;
         _ = if curr_phase = 1 then print_open_colour 33 else ();
         _ = print_uint64 propa;
         _ = print_uint64 confl;
         _ = print_uint64 frestarts;
         _ = print_uint64 lrestarts;
         _ = print_uint64 uset;
         _ = print_uint64 gcs;
         _ = print_uint64 lbds;
         _ = print_close_colour 0
       in
       zero_some_stats (propa, confl, decs, frestarts, lrestarts, uset, gcs, lbds)}
      else (propa, confl, decs, frestarts, lrestarts, uset, gcs, lbds)
    )›


definition isasat_current_status :: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹isasat_current_status =
   (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats,
       heur, avdom,
       vdom, lcount, opts, old_arena).
     let curr_phase = current_restart_phase heur;
        stats = (isasat_current_information curr_phase stats lcount)
     in RETURN (M', N', D', j, W', vm, clvls, cach, lbd, outl, stats,
       heur, avdom,
       vdom, lcount, opts, old_arena))›

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}  →⇩f
   ⟨{(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ r}⟩nres_rel›
  by (intro frefI nres_relI)
    (auto simp: twl_st_heur_def isasat_current_status_def)

definition isasat_print_progress :: ‹64 word ⇒ 64 word ⇒ stats ⇒ _ ⇒ unit› where
‹isasat_print_progress c curr_phase =
   (λ(propa, confl, decs, frestarts, lrestarts, uset, gcs, lbds) lcount.
     let
         _ = print_c propa;
         _ = if curr_phase = 1 then print_open_colour 33 else ();
         _ = print_char c;
         _ = print_uint64 propa;
         _ = print_uint64 confl;
         _ = print_uint64 frestarts;
         _ = print_uint64 lrestarts;
         _ = print_uint64 uset;
         _ = print_uint64 gcs;
         _ = print_close_colour 0
     in
       ())›


definition isasat_current_progress :: ‹64 word ⇒ twl_st_wl_heur ⇒ unit nres› where
‹isasat_current_progress =
   (λc (M', N', D', j, W', vm, clvls, cach, lbd, outl, stats,
       heur, avdom,
       vdom, lcount, opts, old_arena).
     let
       curr_phase = current_restart_phase heur;
       _ = isasat_print_progress c curr_phase stats lcount
     in RETURN ())›


end