Theory IsaSAT_Rephase_State

theory IsaSAT_Rephase_State
  imports IsaSAT_Rephase IsaSAT_Setup IsaSAT_Show
begin

definition rephase_heur_stats :: ‹64 word ⇒ 64 word ⇒ 64 word ⇒ restart_heuristics ⇒ restart_heuristics nres› where
  ‹rephase_heur_stats = (λend_of_phase lrephase b (fast_ema, slow_ema, restart_info, wasted, φ, relu).
    do {
      φ ← phase_rephase end_of_phase lrephase b φ;
      RETURN (fast_ema, slow_ema, restart_info, wasted, φ, relu)
   })›


definition rephase_heur :: ‹64 word ⇒ 64 word ⇒ 64 word ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics nres› where
  ‹rephase_heur = (λend_of_phase lrephase b heur.
  do {
  φ ← rephase_heur_stats end_of_phase lrephase b (get_content heur);
  RETURN (Restart_Heuristics φ)
  })›


lemma rephase_heur_spec:
  ‹heuristic_rel 𝒜 heur ⟹ rephase_heur end_of_phase lrephase b heur ≤  ⇓Id (SPEC(heuristic_rel 𝒜))›
  unfolding rephase_heur_def rephase_heur_stats_def
  apply (refine_vcg phase_rephase_spec[THEN order_trans])
  apply (auto simp: heuristic_rel_def heuristic_rel_stats_def)
  done

definition rephase_heur_st :: ‹isasat ⇒ isasat nres› where
  ‹rephase_heur_st = (λS. do {
      let lcount = get_global_conflict_count S;
      let heur = get_heur S;
      let stats = get_stats_heur S;
      let rephase_count = stats_rephase stats;
      let stats = incr_rephase_total stats;
      let b = current_restart_phase heur;
      heur ← rephase_heur lcount rephase_count b heur;
      let _ = isasat_print_progress (current_phase_letter (current_rephasing_phase heur))
                  b stats (get_learned_count S);
      RETURN (set_stats_wl_heur stats (set_heur_wl_heur heur S))
   })›

lemma rephase_heur_st_spec:
  ‹(S, S') ∈ twl_st_heur ⟹ rephase_heur_st S ≤ SPEC(λS. (S, S') ∈ twl_st_heur)›
  unfolding rephase_heur_st_def
  apply (cases S')
  apply (refine_vcg rephase_heur_spec[THEN order_trans, of ‹all_atms_st S'›])
  apply (simp_all add:  twl_st_heur_def all_atms_st_def)
  done

definition save_rephase_heur_stats :: ‹64 word ⇒ restart_heuristics ⇒ restart_heuristics nres› where
  ‹save_rephase_heur_stats = (λn (fast_ema, slow_ema, restart_info, wasted, φ, relu).
    do {
      φ ← phase_save_phase n φ;
      RETURN (fast_ema, slow_ema, restart_info, wasted, φ, relu)
  })›

definition save_rephase_heur :: ‹64 word ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics nres› where
  ‹save_rephase_heur = (λn heur.
  do {
  φ ← save_rephase_heur_stats n (get_content heur);
  RETURN (Constructor φ)
  })›

lemma save_phase_heur_spec:
  ‹heuristic_rel 𝒜 heur ⟹ save_rephase_heur n heur ≤  ⇓Id (SPEC(heuristic_rel 𝒜))›
  unfolding save_rephase_heur_def save_rephase_heur_stats_def
  apply (refine_vcg phase_save_phase_spec[THEN order_trans])
  apply (auto simp: heuristic_rel_def heuristic_rel_stats_def)
  done


definition save_phase_st :: ‹isasat ⇒ isasat nres› where
  ‹save_phase_st = (λS. do {
      let stats = get_stats_heur S;
      let n = no_conflict_until stats;
      let heur = get_heur S;
      heur ← save_rephase_heur n heur;
      RETURN (set_heur_wl_heur heur S)
   })›

lemma save_phase_st_spec:
  ‹(S, S') ∈ twl_st_heur ⟹ save_phase_st S ≤ SPEC(λS. (S, S') ∈ twl_st_heur)›
  unfolding save_phase_st_def
  apply (cases S')
  apply (refine_vcg save_phase_heur_spec[THEN order_trans, of ‹all_atms_st S'›])
  apply (simp_all add:  twl_st_heur_def isa_length_trail_pre all_atms_st_def flip: all_lits_st_alt_def)
  done

end