Theory IsaSAT_Stats

theory IsaSAT_Stats
  imports IsaSAT_Literals IsaSAT_EMA IsaSAT_Rephase IsaSAT_Reluctant Tuple16
begin


section ‹Statistics›

text ‹
We do some statistics on the run.

NB: the statistics are not proven correct (especially they might
overflow), there are just there to look for regressions, do some comparisons (e.g., to conclude that
we are propagating slower than the other solvers), or to test different option combinations.
›

type_synonym limit = ‹64 word × 64 word›

text ‹The statistics have the following meaning:

  ▸ search information
  (propagations, conflicts, decision, restarts,
  reductions, fixed variables, GCs,
  units since last GC, fixed irredundant clss),

  ▸ binary simplification (binary unit, binary red removed),
  ▸ pure literals (purelit removed, purelit rounds),
  ▸ forward subsumption (forward rounds, forward strengthen, forward subsumed)
  ▸ other: max kept lbd, 
  ▸ ticks
  ▸ average lbds
  ▸ heuristics


At first we used a tuple that became longer and longer. We even had statistics bug because we changed
the wrong element of the tuple. Therefore, we changed to a structure and kept some free spots.
›

type_synonym search_stats = ‹64 word × 64 word ×64 word × 64 word × 64 word × 64 word ×64 word × 64 word × 64 word × 64 word›

definition Search_Stats_propagations :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_propagations = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). propa)›

definition Search_Stats_incr_propagation :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_propagation = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa+1, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_incr_propagation_by :: ‹64 word ⇒ search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_propagation_by = (λp (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa+p, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_conflicts :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_conflicts = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). confl)›

definition Search_Stats_incr_conflicts :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_conflicts = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl+1, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_decisions :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_decisions = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). dec)›

definition Search_Stats_incr_decisions :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_decisions = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec+1, res, reduction, uset, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_restarts :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_restarts = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). res)›

definition Search_Stats_incr_restarts :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_restarts = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res+1, reduction, uset, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_reductions :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_reductions = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). reduction)›

definition Search_Stats_incr_reductions :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_reductions = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction+1, uset, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_fixed :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_fixed = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). uset)›

definition Search_Stats_incr_fixed :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_fixed = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset+1, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_incr_fixed_by :: ‹64 word ⇒ search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_fixed_by = (λp (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset+p, gcs, units, irred_cls, no_conflict_until))›

definition Search_Stats_gcs :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_gcs = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). gcs)›

definition Search_Stats_incr_gcs :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_gcs = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs+1, units, irred_cls, no_conflict_until))›

definition Search_Stats_reset_units_since_gc :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_reset_units_since_gc = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs, 0, irred_cls, no_conflict_until))›

definition Search_Stats_units_since_gcs :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_units_since_gcs = (λ(propa, confl, dec, res, reduction, uset, units_since_gcs, units, irred_cls, no_conflict_until). units_since_gcs)›

definition Search_Stats_incr_units_since_gc :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_units_since_gc = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs, units+1, irred_cls, no_conflict_until))›

definition Search_Stats_incr_units_since_gc_by :: ‹64 word ⇒ search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_units_since_gc_by = (λp (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs, units+p, irred_cls, no_conflict_until))›

definition Search_Stats_incr_irred :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_incr_irred = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls+1, no_conflict_until))›

definition Search_Stats_decr_irred :: ‹search_stats ⇒ search_stats› where
  ‹Search_Stats_decr_irred = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls-1, no_conflict_until))›

definition Search_Stats_irred :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_irred = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). irred_cls)›

definition Search_Stats_no_conflict_until :: ‹search_stats ⇒ 64 word› where
  ‹Search_Stats_no_conflict_until = (λ(propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). no_conflict_until)›

definition Search_Stats_set_no_conflict_until :: ‹64 word ⇒ search_stats ⇒ search_stats› where
  ‹Search_Stats_set_no_conflict_until = (λp (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, no_conflict_until). (propa, confl, dec, res, reduction, uset, gcs, units, irred_cls, p))›

type_synonym inprocessing_binary_stats = ‹64 word × 64 word × 64 word›

definition Binary_Stats_incr_rounds :: ‹inprocessing_binary_stats ⇒ inprocessing_binary_stats› where
  ‹Binary_Stats_incr_rounds = (λ(rounds, units, removed). (rounds + 1, units, removed))›

definition Binary_Stats_incr_units :: ‹inprocessing_binary_stats ⇒ inprocessing_binary_stats› where
  ‹Binary_Stats_incr_units = (λ(rounds, units, removed). (rounds, units+1, removed))›

definition Binary_Stats_incr_removed :: ‹inprocessing_binary_stats ⇒ inprocessing_binary_stats› where
  ‹Binary_Stats_incr_removed = (λ(rounds, units, removed). (rounds, units, removed+1))›



text ‹\<^term>‹ticks› is currently unused: it is supposed to be used as to limit the number of clauses to try.›
type_synonym inprocessing_subsumption_stats = ‹64 word × 64 word × 64 word × 64 word × 64 word›

definition Subsumption_Stats_rounds where
  ‹Subsumption_Stats_rounds = (λ(rounds, strengthened, subsumed, _). rounds)›

definition Subsumption_Stats_subsumed where
  ‹Subsumption_Stats_subsumed = (λ(subsumed, strengthened, subsumed, _). subsumed)›

definition Subsumption_Stats_tried where
  ‹Subsumption_Stats_tried = (λ(subsumed, strengthened, subsumed, _, tried). tried)›

definition Subsumption_Stats_strengthened where
  ‹Subsumption_Stats_strengthened = (λ(rounds, strengethened, subsumed, _). strengethened)›

definition Subsumption_Stats_incr_rounds :: ‹inprocessing_subsumption_stats ⇒ inprocessing_subsumption_stats› where
  ‹Subsumption_Stats_incr_rounds = (λ(rounds, units, removed, ticks, tried). (rounds + 1, units, removed, ticks, tried))›

definition Subsumption_Stats_incr_strengthening :: ‹inprocessing_subsumption_stats ⇒ inprocessing_subsumption_stats› where
  ‹Subsumption_Stats_incr_strengthening = (λ(rounds, units, removed). (rounds, units+1, removed))›

definition Subsumption_Stats_incr_subsumed :: ‹inprocessing_subsumption_stats ⇒ inprocessing_subsumption_stats› where
  ‹Subsumption_Stats_incr_subsumed = (λ(rounds, units, removed, ticks). (rounds, units, removed+1, ticks))›

definition Subsumption_Stats_incr_tried :: ‹inprocessing_subsumption_stats ⇒ inprocessing_subsumption_stats› where
  ‹Subsumption_Stats_incr_tried = (λ(rounds, units, removed, ticks, tried). (rounds, units, removed, ticks, tried+1))›

definition Subsumption_Stats_set_ticks_limit :: ‹64 word ⇒ inprocessing_subsumption_stats ⇒ inprocessing_subsumption_stats› where
  ‹Subsumption_Stats_set_ticks_limit = (λticks (rounds, units, removed, _, tried). (rounds, units, removed+1, ticks, tried))›

definition Subsumption_Stats_ticks_limit :: ‹inprocessing_subsumption_stats ⇒ 64 word› where
  ‹Subsumption_Stats_ticks_limit = (λ(rounds, units, removed, ticks, tried). ticks)›

definition Subsumption_Stats_ticks_tried :: ‹inprocessing_subsumption_stats ⇒ 64 word› where
  ‹Subsumption_Stats_ticks_tried = (λ(rounds, units, removed, ticks, tried). tried)›

type_synonym inprocessing_pure_lits_stats = ‹64 word × 64 word›

definition Pure_lits_Stats_incr_rounds :: ‹inprocessing_pure_lits_stats ⇒ inprocessing_pure_lits_stats› where
  ‹Pure_lits_Stats_incr_rounds = (λ(rounds, removed). (rounds + 1, removed))›

definition Pure_lits_Stats_incr_removed :: ‹inprocessing_pure_lits_stats ⇒ inprocessing_pure_lits_stats› where
  ‹Pure_lits_Stats_incr_removed = (λ(rounds, removed). (rounds, removed+1))›

type_synonym lbd_size_limit_stats = ‹nat × nat›

definition LSize_Stats_lbd where
  ‹LSize_Stats_lbd = (λ(lbd, size). lbd)›

definition LSize_Stats_size where
  ‹LSize_Stats_size = (λ(lbd, size). size)›

definition LSize_Stats where
  ‹LSize_Stats lbd size' = (lbd, size')›


type_synonym rephase_stats = ‹64 word × 64 word × 64 word × 64 word × 64 word × 64 word›

definition Rephase_Stats_total :: ‹rephase_stats ⇒ _› where
  ‹Rephase_Stats_total = (λ(rephased, original, best, invert, flipped, random). rephased)›

definition Rephase_Stats_incr_total :: ‹rephase_stats ⇒ rephase_stats› where
  ‹Rephase_Stats_incr_total = (λ(rephased, original, best, invert, flipped, random). (rephased+1, original, best, invert, flipped, random))›


type_synonym isasat_stats = ‹(search_stats, inprocessing_binary_stats, inprocessing_subsumption_stats, ema,
  inprocessing_pure_lits_stats, lbd_size_limit_stats, rephase_stats, 64 word,
  64 word, 64 word,64 word, 64 word,
  64 word, 64 word, 32 word, 64 word) tuple16›



abbreviation Stats :: ‹_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒ isasat_stats› where
  ‹Stats ≡ Tuple16›

definition get_search_stats :: ‹isasat_stats ⇒ search_stats› where
  ‹get_search_stats ≡ Tuple16.Tuple16_get_a›

definition get_binary_stats :: ‹isasat_stats ⇒ inprocessing_binary_stats› where
  ‹get_binary_stats ≡ Tuple16.Tuple16_get_b›

definition get_subsumption_stats :: ‹isasat_stats ⇒ inprocessing_subsumption_stats› where
  ‹get_subsumption_stats ≡ Tuple16.Tuple16_get_c›

definition get_avg_lbd_stats :: ‹isasat_stats ⇒ ema› where
  ‹get_avg_lbd_stats ≡ Tuple16.Tuple16_get_d›

definition get_pure_lits_stats :: ‹isasat_stats ⇒ inprocessing_pure_lits_stats› where
  ‹get_pure_lits_stats ≡ Tuple16.Tuple16_get_e›

definition get_lsize_limit_stats :: ‹isasat_stats ⇒ lbd_size_limit_stats› where
  ‹get_lsize_limit_stats ≡ Tuple16.Tuple16_get_f›

definition get_rephase_stats :: ‹isasat_stats ⇒ rephase_stats› where
  ‹get_rephase_stats ≡ Tuple16.Tuple16_get_g›

definition set_propagation_stats :: ‹search_stats ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_propagation_stats ≡ Tuple16.set_a›

definition set_binary_stats :: ‹inprocessing_binary_stats ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_binary_stats ≡ Tuple16.set_b›

definition set_subsumption_stats :: ‹inprocessing_subsumption_stats ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_subsumption_stats ≡ Tuple16.set_c›

definition set_avg_lbd_stats :: ‹ema ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_avg_lbd_stats ≡ Tuple16.set_d›

definition set_pure_lits_stats :: ‹inprocessing_pure_lits_stats ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_pure_lits_stats ≡ Tuple16.set_e›

definition set_lsize_limit_stats :: ‹lbd_size_limit_stats ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_lsize_limit_stats ≡ Tuple16.set_f›

definition set_rephase_stats :: ‹rephase_stats ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_rephase_stats ≡ Tuple16.set_g›

definition incr_propagation :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_propagation S = (set_propagation_stats (Search_Stats_incr_propagation (get_search_stats S)) S)›

definition incr_propagation_by :: ‹64 word ⇒ isasat_stats ⇒ isasat_stats› where
  ‹incr_propagation_by p S = (set_propagation_stats (Search_Stats_incr_propagation_by p (get_search_stats S)) S)›

definition incr_conflict :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_conflict S = (set_propagation_stats (Search_Stats_incr_conflicts (get_search_stats S)) S)›

definition incr_decision :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_decision S = (set_propagation_stats (Search_Stats_incr_decisions (get_search_stats S)) S)›

definition incr_restart :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_restart S = (set_propagation_stats (Search_Stats_incr_restarts (get_search_stats S)) S)›

definition incr_reduction :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_reduction S = (set_propagation_stats (Search_Stats_incr_reductions (get_search_stats S)) S)›

definition incr_uset :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_uset S = (set_propagation_stats (Search_Stats_incr_fixed (get_search_stats S)) S)›

definition incr_uset_by :: ‹64 word ⇒ isasat_stats ⇒ isasat_stats› where
  ‹incr_uset_by p S = (set_propagation_stats (Search_Stats_incr_fixed_by p (get_search_stats S)) S)›

definition incr_GC :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_GC S = (set_propagation_stats (Search_Stats_incr_gcs (get_search_stats S)) S)›

definition units_since_last_GC :: ‹isasat_stats ⇒ 64 word› where
  ‹units_since_last_GC = Search_Stats_units_since_gcs o get_search_stats›

definition units_since_beginning :: ‹isasat_stats ⇒ 64 word› where
  ‹units_since_beginning = Search_Stats_fixed o get_search_stats›

definition incr_units_since_last_GC :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_units_since_last_GC S = (set_propagation_stats (Search_Stats_incr_units_since_gc (get_search_stats S)) S)›

definition incr_units_since_last_GC_by :: ‹64 word ⇒ isasat_stats ⇒ isasat_stats› where
  ‹incr_units_since_last_GC_by p S = (set_propagation_stats (Search_Stats_incr_units_since_gc_by p (get_search_stats S)) S)›

definition stats_conflicts :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_conflicts = Search_Stats_conflicts o get_search_stats›

definition incr_binary_unit_derived :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_binary_unit_derived S = set_binary_stats (Binary_Stats_incr_units (get_binary_stats S)) S›

definition incr_binary_red_removed :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_binary_red_removed S = set_binary_stats (Binary_Stats_incr_removed (get_binary_stats S)) S›

definition incr_forward_strengethening :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_forward_strengethening S = set_subsumption_stats (Subsumption_Stats_incr_strengthening (get_subsumption_stats S)) S›

definition incr_forward_subsumed :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_forward_subsumed S = set_subsumption_stats (Subsumption_Stats_incr_subsumed (get_subsumption_stats S)) S›

definition incr_forward_tried :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_forward_tried S = set_subsumption_stats (Subsumption_Stats_incr_tried (get_subsumption_stats S)) S›

definition incr_forward_rounds :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_forward_rounds S = set_subsumption_stats (Subsumption_Stats_incr_rounds (get_subsumption_stats S)) S›

definition stats_forward_rounds :: ‹isasat_stats ⇒ _› where
  ‹stats_forward_rounds = Subsumption_Stats_rounds o get_subsumption_stats›

definition stats_forward_subsumed :: ‹isasat_stats ⇒ _› where
  ‹stats_forward_subsumed = Subsumption_Stats_subsumed o get_subsumption_stats›

definition stats_forward_strengthened :: ‹isasat_stats ⇒ _› where
  ‹stats_forward_strengthened = Subsumption_Stats_strengthened o get_subsumption_stats›

definition stats_forward_tried :: ‹isasat_stats ⇒ _› where
  ‹stats_forward_tried = Subsumption_Stats_tried o get_subsumption_stats›

definition get_restart_count where
  ‹get_restart_count S = Search_Stats_restarts (get_search_stats S)›

definition get_reduction_count where
  ‹get_reduction_count S = Search_Stats_reductions (get_search_stats S)›

definition incr_rephase_total :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_rephase_total S = (set_rephase_stats (Rephase_Stats_incr_total (get_rephase_stats S)) S)›

definition stats_rephase :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_rephase = Rephase_Stats_total o get_rephase_stats›

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

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

definition stats_propagations :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_propagations = Search_Stats_propagations o get_search_stats›

definition stats_restarts :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_restarts = Search_Stats_restarts o get_search_stats›

definition stats_reductions :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_reductions = Search_Stats_reductions o get_search_stats›

definition stats_fixed :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_fixed = Search_Stats_fixed o get_search_stats›

definition stats_gcs :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_gcs = Search_Stats_gcs o get_search_stats›

definition stats_avg_lbd :: ‹isasat_stats ⇒ ema› where
  ‹stats_avg_lbd = get_avg_lbd_stats›


definition stats_decisions :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_decisions = Search_Stats_decisions o get_search_stats›

definition stats_irred :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_irred = Search_Stats_irred o get_search_stats›

definition Binary_Stats_rounds :: ‹inprocessing_binary_stats ⇒ 64 word› where
  ‹Binary_Stats_rounds = (λ(rounds, units, removed). rounds)›

definition stats_binary_rounds :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_binary_rounds = Binary_Stats_rounds o get_binary_stats›

definition Binary_Stats_units :: ‹inprocessing_binary_stats ⇒ 64 word› where
  ‹Binary_Stats_units = (λ(units, units, removed). units)›

definition stats_binary_units :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_binary_units = Binary_Stats_units o get_binary_stats›

definition Binary_Stats_removed :: ‹inprocessing_binary_stats ⇒ 64 word› where
  ‹Binary_Stats_removed = (λ(removed, units, removed). removed)›

definition stats_binary_removed :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_binary_removed = Binary_Stats_removed o get_binary_stats›

definition Pure_Lits_Stats_removed :: ‹inprocessing_pure_lits_stats ⇒ 64 word› where
  ‹Pure_Lits_Stats_removed = (λ(removed, removed). removed)›

definition stats_pure_lits_removed :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_pure_lits_removed = Pure_Lits_Stats_removed o get_pure_lits_stats›

definition Pure_Lits_Stats_rounds :: ‹inprocessing_pure_lits_stats ⇒ 64 word› where
  ‹Pure_Lits_Stats_rounds = (λ(rounds, rounds). rounds)› 

definition stats_pure_lits_rounds :: ‹isasat_stats ⇒ 64 word› where
  ‹stats_pure_lits_rounds = Pure_Lits_Stats_rounds o get_pure_lits_stats›


definition add_lbd :: ‹32 word ⇒ isasat_stats ⇒ isasat_stats› where
  ‹add_lbd lbd S = set_avg_lbd_stats (ema_update (unat lbd) (get_avg_lbd_stats S)) S›

definition incr_purelit_elim :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_purelit_elim S = set_pure_lits_stats (Pure_lits_Stats_incr_removed (get_pure_lits_stats S)) S›

definition incr_purelit_rounds :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_purelit_rounds S = set_pure_lits_stats (Pure_lits_Stats_incr_rounds (get_pure_lits_stats S)) S›


definition reset_units_since_last_GC :: ‹isasat_stats ⇒ isasat_stats› where
  ‹reset_units_since_last_GC S = (set_propagation_stats (Search_Stats_reset_units_since_gc (get_search_stats S)) S)›

definition incr_irred_clss :: ‹isasat_stats ⇒ isasat_stats› where
  ‹incr_irred_clss S = set_propagation_stats (Search_Stats_incr_irred (get_search_stats S)) S›

definition set_no_conflict_until :: ‹64 word ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_no_conflict_until p S = set_propagation_stats (Search_Stats_set_no_conflict_until p (get_search_stats S)) S›

definition no_conflict_until :: ‹isasat_stats ⇒ 64 word› where
  ‹no_conflict_until S = Search_Stats_no_conflict_until (get_search_stats S)›

definition decr_irred_clss :: ‹isasat_stats ⇒ isasat_stats› where
  ‹decr_irred_clss S = set_propagation_stats (Search_Stats_decr_irred (get_search_stats S)) S›

definition irredundant_clss :: ‹isasat_stats ⇒ 64 word› where
  ‹irredundant_clss = Search_Stats_irred o get_search_stats›

abbreviation (input) get_conflict_count :: ‹isasat_stats ⇒ 64 word› where
  ‹get_conflict_count ≡ stats_conflicts›

definition stats_lbd_limit :: ‹isasat_stats ⇒ nat› where
  ‹stats_lbd_limit = LSize_Stats_lbd o get_lsize_limit_stats›

definition stats_size_limit :: ‹isasat_stats ⇒ nat› where
  ‹stats_size_limit = LSize_Stats_size o get_lsize_limit_stats›

definition set_stats_size_limit :: ‹nat ⇒ nat ⇒ isasat_stats ⇒ isasat_stats› where
  ‹set_stats_size_limit lbd size' = set_lsize_limit_stats (lbd, size')›


section ‹Information related to restarts›

definition FOCUSED_MODE :: ‹64 word› where
  ‹FOCUSED_MODE = 0›

definition STABLE_MODE :: ‹64 word› where
  ‹STABLE_MODE = 1›

definition DEFAULT_INIT_PHASE :: ‹64 word› where
  ‹DEFAULT_INIT_PHASE = 10000›

type_synonym restart_info = ‹64 word × 64 word × 64 word × 64 word × 64 word›

definition incr_conflict_count_since_last_restart :: ‹restart_info ⇒ restart_info› where
  ‹incr_conflict_count_since_last_restart = (λ(ccount, ema_lvl, restart_phase, end_of_phase, length_phase).
    (ccount + 1, ema_lvl, restart_phase, end_of_phase, length_phase))›

definition restart_info_update_lvl_avg :: ‹32 word ⇒ restart_info ⇒ restart_info› where
  ‹restart_info_update_lvl_avg = (λlvl (ccount, ema_lvl). (ccount, ema_lvl))›

definition restart_info_init :: ‹restart_info› where
  ‹restart_info_init = (0, 0, FOCUSED_MODE, DEFAULT_INIT_PHASE, 1000)›

definition restart_info_restart_done :: ‹restart_info ⇒ restart_info› where
  ‹restart_info_restart_done = (λ(ccount, lvl_avg). (0, lvl_avg))›

definition empty_stats :: ‹isasat_stats› where
  ‹empty_stats = Tuple16( (0,0,0,0,0,0,0,0,0,0)::search_stats)
  ((0,0,0)::inprocessing_binary_stats) ((0,0,0,0,0)::inprocessing_subsumption_stats)
  (ema_fast_init::ema) ((0,0)::inprocessing_pure_lits_stats) (0,0) (0,0,0,0,0,0) 0 0 0 0 0 0 0 0 0›

definition empty_stats_clss :: ‹64 word ⇒ isasat_stats› where
  ‹empty_stats_clss n = Tuple16( (0,0,0,0,0,0,0,0,n,0)::search_stats)
  ((0,0,0)::inprocessing_binary_stats) ((0,0,0,0,0)::inprocessing_subsumption_stats)
  (ema_fast_init::ema) ((0,0)::inprocessing_pure_lits_stats) (0,0) (0,0,0,0,0,0) 0 0 0 0 0 0 0 0 0›


section ‹Heuristics›

type_synonym schedule_info = ‹64 word × 64 word × 64 word›

definition schedule_next_pure_lits_info :: ‹schedule_info ⇒ schedule_info› where
  ‹schedule_next_pure_lits_info = (λ(inprocess, reduce, forwardsubsumption). (inprocess * 3 >> 1, reduce, forwardsubsumption))›

definition next_pure_lits_schedule_info :: ‹schedule_info ⇒ 64 word› where
  ‹next_pure_lits_schedule_info = (λ(inprocess, reduce, forwardsubsumption). inprocess)›

definition schedule_next_reduce_info :: ‹64 word ⇒ schedule_info ⇒ schedule_info› where
  ‹schedule_next_reduce_info delta = (λ(inprocess, reduce, forwardsubsumption). (inprocess, reduce + delta, forwardsubsumption))›

definition next_reduce_schedule_info :: ‹schedule_info ⇒ 64 word› where
  ‹next_reduce_schedule_info = (λ(inprocess, reduce, forwardsubsumption). reduce)›

definition next_subsume_schedule_info :: ‹schedule_info ⇒ 64 word› where
  ‹next_subsume_schedule_info = (λ(inprocess, reduce, forwardsubsumption). forwardsubsumption)›

definition schedule_next_subsume_info :: ‹64 word ⇒ schedule_info ⇒ schedule_info› where
  ‹schedule_next_subsume_info delta = (λ(inprocess, reduce, forwardsubsumption). (inprocess, reduce, forwardsubsumption + delta))›


datatype 'a code_hider = Constructor (get_content: 'a)

definition code_hider_rel where code_hider_rel_def_internal:
  ‹code_hider_rel R = {(a,b). (a, get_content b) ∈ R}›

lemma code_hider_rel_def[refine_rel_defs]:
  "⟨R⟩code_hider_rel ≡ {(a,b). (a, get_content b) ∈ R}"
  by (simp add: code_hider_rel_def_internal relAPP_def)

type_synonym restart_heuristics = ‹ema × ema × restart_info × 64 word × phase_save_heur × reluctant × bool × phase_saver × schedule_info × ema × ema›

type_synonym isasat_restart_heuristics = ‹restart_heuristics code_hider›


abbreviation Restart_Heuristics :: ‹restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹Restart_Heuristics a ≡ Constructor a›

abbreviation get_restart_heuristics :: ‹isasat_restart_heuristics ⇒ restart_heuristics› where
  ‹get_restart_heuristics a ≡ get_content a›


fun fast_ema_of_stats :: ‹restart_heuristics ⇒ ema› where
  ‹fast_ema_of_stats (fast_ema, slow_ema, restart_info, wasted, φ) = fast_ema›

fun slow_ema_of_stats :: ‹restart_heuristics ⇒ ema› where
  ‹slow_ema_of_stats (fast_ema, slow_ema, restart_info, wasted, φ) = slow_ema›

fun restart_info_of_stats :: ‹restart_heuristics ⇒ restart_info› where
  ‹restart_info_of_stats (fast_ema, slow_ema, restart_info, wasted, φ) = restart_info›

fun schedule_info_of_stats :: ‹restart_heuristics ⇒ schedule_info› where
  ‹schedule_info_of_stats (fast_ema, slow_ema, restart_info, wasted, φ, _, _, _, schedule, _, _) = schedule›

fun current_restart_phase_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹current_restart_phase_stats (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ) =
    restart_phase›

fun incr_restart_phase_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹incr_restart_phase_stats (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ) =
    (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase XOR 1, end_of_phase), wasted, φ)›

fun incr_wasted_stats :: ‹64 word ⇒ restart_heuristics ⇒ restart_heuristics› where
  ‹incr_wasted_stats waste (fast_ema, slow_ema, res_info, wasted, φ) =
    (fast_ema, slow_ema, res_info, wasted + waste, φ)›

fun set_zero_wasted_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹set_zero_wasted_stats (fast_ema, slow_ema, res_info, wasted, φ) =
    (fast_ema, slow_ema, res_info, 0, φ)›

fun wasted_of_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹wasted_of_stats (fast_ema, slow_ema, res_info, wasted, φ) = wasted›

fun get_conflict_count_since_last_restart_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹get_conflict_count_since_last_restart_stats (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ) =
    ccount›

definition swap_emas_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹swap_emas_stats = (λ(fast_ema, slow_ema, restart_info, wasted, φ, a, b, lit_st, schedule, other_fema, other_sema).
  (other_fema, other_sema, restart_info, wasted, φ, a, b, lit_st, schedule, fast_ema, slow_ema))›

definition get_conflict_count_since_last_restart :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹get_conflict_count_since_last_restart = get_conflict_count_since_last_restart_stats o get_content›

definition heuristic_rel_stats :: ‹nat multiset ⇒ restart_heuristics ⇒ bool› where
  ‹heuristic_rel_stats 𝒜 = (λ(fast_ema, slow_ema, res_info, wasted, φ, _, _, lit_st, schedule). phase_save_heur_rel 𝒜 φ ∧ phase_saving 𝒜 lit_st)›

definition save_phase_heur_stats :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ restart_heuristics› where
‹save_phase_heur_stats L b = (λ(fast_ema, slow_ema, res_info, wasted, (φ, target, best), reluctant).
    (fast_ema, slow_ema, res_info, wasted, (φ[L := b], target, best), reluctant))›

definition save_phase_heur_pre_stats :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ bool› where
‹save_phase_heur_pre_stats L b = (λ(fast_ema, slow_ema, res_info, wasted, (φ, _), _). L < length φ)›

definition mop_save_phase_heur_stats :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ restart_heuristics nres› where
‹mop_save_phase_heur_stats L b heur = do {
   ASSERT(save_phase_heur_pre_stats L b heur);
   RETURN (save_phase_heur_stats L b heur)
}›

definition mark_added_heur_stats :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ restart_heuristics› where
‹mark_added_heur_stats L b = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule).
    (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st[L := True], schedule))›

definition mark_added_heur_pre_stats :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ bool› where
‹mark_added_heur_pre_stats L b = (λ(fast_ema, slow_ema, res_info, wasted, φ, _,  fully_proped, lits_st, schedule). L < length lits_st)›

definition mop_mark_added_heur_stats :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ restart_heuristics nres› where
‹mop_mark_added_heur_stats L b heur = do {
   ASSERT(mark_added_heur_pre_stats L b heur);
   RETURN (mark_added_heur_stats L b heur)
}›

definition reset_added_heur_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
‹reset_added_heur_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule).
    (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, replicate (length lits_st) False, schedule))›


definition reset_added_heur_stats2 :: ‹restart_heuristics ⇒ restart_heuristics nres› where
  ‹reset_added_heur_stats2 = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st⇩0, schedule).
  do {
  (_, lits_st) ← WHILE⇩T⇗ λ(i, lits_st). (∀k < i. ¬lits_st ! k) ∧ i ≤ length lits_st ∧ length lits_st = length lits_st⇩0⇖ (λ(i, lits_st). i < length lits_st)
    (λ(i, lits_st). do {ASSERT (i < length lits_st); RETURN (i+1, lits_st[i := False])})
    (0, lits_st⇩0);
  RETURN  (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule)
  })›

lemma reset_added_heur_stats2_reset_added_heur_stats:
  ‹reset_added_heur_stats2 heur ≤⇓Id (RETURN (reset_added_heur_stats heur))›
proof -
  obtain fast_ema slow_ema res_info wasted φ reluctant fully_proped lits_st⇩0 schedule where
    heur: ‹heur = (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st⇩0, schedule)›
    by (cases heur)
  have [refine0]: ‹wf (measure (λ(i, lits_st). length lits_st⇩0 - i))›
    by auto
  show ?thesis
    unfolding reset_added_heur_stats2_def reset_added_heur_stats_def heur
       prod.simps
    apply (refine_vcg)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (auto split: if_splits)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (simp add: list_eq_iff_nth_eq)
    done
qed

definition is_marked_added_heur_stats :: ‹restart_heuristics ⇒ nat ⇒ bool› where
‹is_marked_added_heur_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule) L.
     lits_st ! L)›

definition is_marked_added_heur_pre_stats :: ‹restart_heuristics ⇒nat ⇒ bool› where
‹is_marked_added_heur_pre_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, _,  fully_proped, lits_st, schedule) L. L < length lits_st)›

definition mop_is_marked_added_heur_stats :: ‹restart_heuristics ⇒ nat ⇒ bool nres› where
‹mop_is_marked_added_heur_stats L heur = do {
   ASSERT(is_marked_added_heur_pre_stats L heur);
   RETURN (is_marked_added_heur_stats L heur)
}›

definition get_saved_phase_heur_pre_stats :: ‹nat ⇒ restart_heuristics ⇒ bool› where
‹get_saved_phase_heur_pre_stats L = (λ(fast_ema, slow_ema, res_info, wasted, (φ, _), _). L < length φ)›

definition get_saved_phase_heur_stats :: ‹nat ⇒ restart_heuristics ⇒ bool› where
‹get_saved_phase_heur_stats L = (λ(fast_ema, slow_ema, res_info, wasted, (φ, _), _). φ!L)›

definition current_rephasing_phase_stats :: ‹restart_heuristics ⇒ 64 word› where
‹current_rephasing_phase_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, _). phase_current_rephasing_phase φ)›

definition mop_get_saved_phase_heur_stats :: ‹nat ⇒ restart_heuristics ⇒ bool nres› where
‹mop_get_saved_phase_heur_stats L heur = do {
   ASSERT(get_saved_phase_heur_pre_stats L heur);
   RETURN (get_saved_phase_heur_stats L heur)
}›

definition heuristic_reluctant_tick_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹heuristic_reluctant_tick_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped).
     (fast_ema, slow_ema, res_info, wasted, φ, reluctant_tick reluctant, fullyproped))›

definition heuristic_reluctant_enable_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹heuristic_reluctant_enable_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped).
     (fast_ema, slow_ema, res_info, wasted, φ, reluctant_init, fullyproped))›

definition heuristic_reluctant_disable_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹heuristic_reluctant_disable_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped).
     (fast_ema, slow_ema, res_info, wasted, φ, reluctant_disable reluctant, fullyproped))›

definition heuristic_reluctant_triggered_stats :: ‹restart_heuristics ⇒ restart_heuristics × bool› where
  ‹heuristic_reluctant_triggered_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped).
    let (reluctant, b) = reluctant_triggered reluctant in
     ((fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped), b))›

definition heuristic_reluctant_triggered2_stats :: ‹restart_heuristics ⇒ bool› where
  ‹heuristic_reluctant_triggered2_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped).
    reluctant_triggered2 reluctant)›

definition heuristic_reluctant_untrigger_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹heuristic_reluctant_untrigger_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fullyproped).
    (fast_ema, slow_ema, res_info, wasted, φ, reluctant_untrigger reluctant, fullyproped))›

definition end_of_rephasing_phase_heur_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹end_of_rephasing_phase_heur_stats =
    (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant). end_of_rephasing_phase phasing)›

definition is_fully_propagated_heur_stats :: ‹restart_heuristics ⇒ bool› where
  ‹is_fully_propagated_heur_stats =
    (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, _). fullyproped)›

definition set_fully_propagated_heur_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹set_fully_propagated_heur_stats =
    (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, lit_st). (fast_ema, slow_ema, res_info, wasted, phasing, reluctant, True, lit_st))›

definition unset_fully_propagated_heur_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹unset_fully_propagated_heur_stats =
    (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, lit_st). (fast_ema, slow_ema, res_info, wasted, phasing, reluctant, False, lit_st))›

definition restart_info_restart_done_heur_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹restart_info_restart_done_heur_stats = (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, lit_st). (fast_ema, slow_ema, restart_info_restart_done res_info, wasted, phasing, reluctant, False, lit_st))›

lemma heuristic_rel_statsI[intro!]:
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (incr_wasted_stats wast heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (set_zero_wasted_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (incr_restart_phase_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (save_phase_heur_stats L b heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (mark_added_heur_stats L b heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (heuristic_reluctant_tick_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (heuristic_reluctant_enable_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (heuristic_reluctant_untrigger_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (set_fully_propagated_heur_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (unset_fully_propagated_heur_stats heur)›
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (swap_emas_stats heur)›
  by (clarsimp_all simp: heuristic_rel_stats_def save_phase_heur_stats_def phase_save_heur_rel_def phase_saving_def
    heuristic_reluctant_tick_stats_def heuristic_reluctant_enable_stats_def heuristic_reluctant_untrigger_stats_def
    set_fully_propagated_heur_stats_def unset_fully_propagated_heur_stats_def mark_added_heur_stats_def swap_emas_stats_def)

lemma heuristic_rel_stats_heuristic_reluctant_triggered_statsD:
  ‹heuristic_rel_stats 𝒜 heur ⟹
     heuristic_rel_stats 𝒜 (fst (heuristic_reluctant_triggered_stats heur))›
  by (clarsimp simp: heuristic_reluctant_triggered_stats_def heuristic_rel_stats_def  phase_save_heur_rel_def
    phase_saving_def reluctant_triggered_def)

lemma save_phase_heur_pre_statsI:
  ‹heuristic_rel_stats 𝒜 heur ⟹ a ∈# 𝒜 ⟹ save_phase_heur_pre_stats a b heur›
  by (auto simp: heuristic_rel_stats_def phase_saving_def save_phase_heur_pre_stats_def
     phase_save_heur_rel_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)

definition fast_ema_of :: ‹isasat_restart_heuristics ⇒ ema› where
  ‹fast_ema_of = fast_ema_of_stats o get_restart_heuristics›

definition slow_ema_of :: ‹isasat_restart_heuristics ⇒ ema› where
  ‹slow_ema_of = slow_ema_of_stats o get_restart_heuristics›

definition restart_info_of :: ‹isasat_restart_heuristics ⇒ restart_info› where
  ‹restart_info_of = restart_info_of_stats o get_restart_heuristics›

definition current_restart_phase :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹current_restart_phase = current_restart_phase_stats o get_restart_heuristics›

definition incr_restart_phase :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹incr_restart_phase = Restart_Heuristics o incr_restart_phase_stats o get_restart_heuristics›

definition incr_wasted :: ‹64 word ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹incr_wasted waste = Restart_Heuristics o incr_wasted_stats waste o get_restart_heuristics›

definition set_zero_wasted :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹set_zero_wasted =  Restart_Heuristics o set_zero_wasted_stats o get_restart_heuristics›

definition wasted_of :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹wasted_of = wasted_of_stats o get_restart_heuristics›

definition swap_emas :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹swap_emas = Restart_Heuristics o swap_emas_stats o get_restart_heuristics›

definition heuristic_rel :: ‹nat multiset ⇒ isasat_restart_heuristics ⇒ bool› where
  ‹heuristic_rel 𝒜 = heuristic_rel_stats 𝒜 o get_restart_heuristics›

definition save_phase_heur :: ‹nat ⇒ bool ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
‹save_phase_heur L b = Restart_Heuristics o save_phase_heur_stats L b o get_restart_heuristics›

definition save_phase_heur_pre :: ‹nat ⇒ bool ⇒ isasat_restart_heuristics ⇒ bool› where
  ‹save_phase_heur_pre L b = save_phase_heur_pre_stats L b o get_restart_heuristics›

definition mop_save_phase_heur :: ‹nat ⇒ bool ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics nres› where
‹mop_save_phase_heur L b heur = do {
   ASSERT(save_phase_heur_pre L b heur);
   RETURN (save_phase_heur L b heur)
}›

definition mark_added_heur :: ‹nat ⇒ bool ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
‹mark_added_heur L b = Restart_Heuristics o mark_added_heur_stats L b o get_restart_heuristics›

definition mark_added_heur_pre :: ‹nat ⇒ bool ⇒ isasat_restart_heuristics ⇒ bool› where
‹mark_added_heur_pre L b = mark_added_heur_pre_stats L b o get_restart_heuristics›

definition mop_mark_added_heur :: ‹nat ⇒ bool ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics nres› where
‹mop_mark_added_heur L b heur = do {
   ASSERT(mark_added_heur_pre L b heur);
   RETURN (mark_added_heur L b heur)
}›

definition reset_added_heur :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
‹reset_added_heur = Restart_Heuristics o reset_added_heur_stats o get_restart_heuristics›

definition mop_reset_added_heur :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics nres› where
‹mop_reset_added_heur heur = do {
   RETURN (reset_added_heur heur)
}›

definition is_marked_added_heur :: ‹isasat_restart_heuristics ⇒ nat ⇒ bool› where
‹is_marked_added_heur = is_marked_added_heur_stats o get_restart_heuristics›

definition is_marked_added_heur_pre :: ‹isasat_restart_heuristics ⇒  nat ⇒ bool› where
‹is_marked_added_heur_pre = is_marked_added_heur_pre_stats o get_restart_heuristics›

definition mop_is_marked_added_heur :: ‹isasat_restart_heuristics ⇒ nat ⇒ bool nres› where
‹mop_is_marked_added_heur L heur = do {
   ASSERT(is_marked_added_heur_pre L heur);
   RETURN (is_marked_added_heur L heur)
}›

definition get_saved_phase_heur_pre :: ‹nat ⇒ isasat_restart_heuristics ⇒ bool› where
‹get_saved_phase_heur_pre L = get_saved_phase_heur_pre_stats L o get_restart_heuristics›

definition get_saved_phase_heur :: ‹nat ⇒ isasat_restart_heuristics ⇒ bool› where
‹get_saved_phase_heur L = get_saved_phase_heur_stats L o get_restart_heuristics›

definition current_rephasing_phase :: ‹isasat_restart_heuristics ⇒ 64 word› where
‹current_rephasing_phase = current_rephasing_phase_stats o get_restart_heuristics›

definition mop_get_saved_phase_heur :: ‹nat ⇒ isasat_restart_heuristics ⇒ bool nres› where
‹mop_get_saved_phase_heur L heur = do {
   ASSERT(get_saved_phase_heur_pre L heur);
   RETURN (get_saved_phase_heur L heur)
}›

definition heuristic_reluctant_tick :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹heuristic_reluctant_tick = Restart_Heuristics o heuristic_reluctant_tick_stats o get_restart_heuristics›

definition heuristic_reluctant_enable :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹heuristic_reluctant_enable = Restart_Heuristics o heuristic_reluctant_enable_stats o get_restart_heuristics›

definition heuristic_reluctant_disable :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹heuristic_reluctant_disable = Restart_Heuristics o heuristic_reluctant_disable_stats o get_restart_heuristics›

definition heuristic_reluctant_triggered :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics × bool› where
  ‹heuristic_reluctant_triggered = apfst Restart_Heuristics o heuristic_reluctant_triggered_stats o get_restart_heuristics›

definition heuristic_reluctant_triggered2 :: ‹isasat_restart_heuristics ⇒ bool› where
  ‹heuristic_reluctant_triggered2 = heuristic_reluctant_triggered2_stats o get_restart_heuristics›

definition heuristic_reluctant_untrigger :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹heuristic_reluctant_untrigger = Restart_Heuristics o heuristic_reluctant_untrigger_stats o get_restart_heuristics›

definition end_of_rephasing_phase_heur :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹end_of_rephasing_phase_heur = end_of_rephasing_phase_heur_stats o get_restart_heuristics›

definition is_fully_propagated_heur :: ‹isasat_restart_heuristics ⇒ bool› where
  ‹is_fully_propagated_heur = is_fully_propagated_heur_stats o get_restart_heuristics›

definition set_fully_propagated_heur :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹set_fully_propagated_heur = Restart_Heuristics o set_fully_propagated_heur_stats o get_restart_heuristics›

definition unset_fully_propagated_heur :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹unset_fully_propagated_heur =
  Restart_Heuristics o unset_fully_propagated_heur_stats o get_restart_heuristics›

definition restart_info_restart_done_heur :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹restart_info_restart_done_heur =
  Restart_Heuristics o restart_info_restart_done_heur_stats o get_restart_heuristics›

definition schedule_info_of :: ‹isasat_restart_heuristics ⇒ schedule_info› where
  ‹schedule_info_of = schedule_info_of_stats o get_restart_heuristics›

definition schedule_next_pure_lits_stats :: ‹restart_heuristics ⇒ restart_heuristics› where
  ‹schedule_next_pure_lits_stats = (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, lit_st, schedule, other_fema, other_sema).
  (fast_ema, slow_ema, restart_info_restart_done res_info, wasted, phasing, reluctant, fullyproped, lit_st, schedule_next_pure_lits_info schedule, other_fema, other_sema))›

definition schedule_next_pure_lits :: ‹isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹schedule_next_pure_lits = Restart_Heuristics o schedule_next_pure_lits_stats o get_restart_heuristics›

definition next_pure_lits_schedule_info_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹next_pure_lits_schedule_info_stats = next_pure_lits_schedule_info o schedule_info_of_stats›

definition next_pure_lits_schedule :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹next_pure_lits_schedule = next_pure_lits_schedule_info_stats o get_restart_heuristics›

definition schedule_next_reduce_stats :: ‹64 word ⇒ restart_heuristics ⇒ restart_heuristics› where
  ‹schedule_next_reduce_stats delta = (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, lit_st, schedule, other_fema, other_sema). (fast_ema, slow_ema, restart_info_restart_done res_info, wasted, phasing, reluctant, fullyproped, lit_st, schedule_next_reduce_info delta schedule, other_fema, other_sema))›

definition schedule_next_reduce :: ‹64 word ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹schedule_next_reduce delta = Restart_Heuristics o schedule_next_reduce_stats delta o get_restart_heuristics›

definition next_reduce_schedule_info_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹next_reduce_schedule_info_stats = next_reduce_schedule_info o schedule_info_of_stats›

definition next_reduce_schedule :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹next_reduce_schedule = next_reduce_schedule_info_stats o get_restart_heuristics›

definition schedule_next_subsume_stats :: ‹64 word ⇒ restart_heuristics ⇒ restart_heuristics› where
  ‹schedule_next_subsume_stats delta = (λ(fast_ema, slow_ema, res_info, wasted, phasing, reluctant, fullyproped, lit_st, schedule, other_fema, other_sema). (fast_ema, slow_ema, restart_info_restart_done res_info, wasted, phasing, reluctant, fullyproped, lit_st, schedule_next_subsume_info delta schedule, other_fema, other_sema))›

definition schedule_next_subsume :: ‹64 word ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹schedule_next_subsume delta = Restart_Heuristics o schedule_next_subsume_stats delta o get_restart_heuristics›

definition next_subsume_schedule_info_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹next_subsume_schedule_info_stats = next_subsume_schedule_info o schedule_info_of_stats›

definition next_subsume_schedule :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹next_subsume_schedule = next_subsume_schedule_info_stats o get_restart_heuristics›

lemma heuristic_relI[intro!]:
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (incr_wasted wast heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (set_zero_wasted heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (incr_restart_phase heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (save_phase_heur L b heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (heuristic_reluctant_tick heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (heuristic_reluctant_enable heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (heuristic_reluctant_untrigger heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (set_fully_propagated_heur heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (unset_fully_propagated_heur heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (mark_added_heur L b heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (swap_emas heur)›
  by (auto simp: heuristic_rel_def save_phase_heur_def phase_save_heur_rel_def phase_saving_def
    heuristic_reluctant_tick_def heuristic_reluctant_enable_def heuristic_reluctant_untrigger_def
    set_fully_propagated_heur_def unset_fully_propagated_heur_def set_zero_wasted_def incr_wasted_def
    incr_restart_phase_def mark_added_heur_def swap_emas_def)

lemma heuristic_rel_heuristic_reluctant_triggeredD:
  ‹heuristic_rel 𝒜 heur ⟹
     heuristic_rel 𝒜 (fst (heuristic_reluctant_triggered heur))›
  by (clarsimp simp: heuristic_reluctant_triggered_def heuristic_rel_def  phase_save_heur_rel_def
    phase_saving_def reluctant_triggered_def heuristic_rel_stats_heuristic_reluctant_triggered_statsD)

lemma save_phase_heur_preI:
  ‹heuristic_rel 𝒜 heur ⟹ a ∈# 𝒜 ⟹ save_phase_heur_pre a b heur›
  by (auto simp: heuristic_rel_def phase_saving_def save_phase_heur_pre_def save_phase_heur_pre_statsI
     phase_save_heur_rel_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)

text ‹Using \<^term>‹a + 1› ensures that we do not get stuck with 0.›
fun incr_restart_phase_end_stats :: ‹64 word ⇒ restart_heuristics ⇒ restart_heuristics› where
  ‹incr_restart_phase_end_stats end_of_phase (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, _, length_phase), wasted) =
  (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase + length_phase, (length_phase * 3) >> 1), wasted)›

definition incr_restart_phase_end :: ‹64 word ⇒ isasat_restart_heuristics ⇒ isasat_restart_heuristics› where
  ‹incr_restart_phase_end end_of_phase = Restart_Heuristics o (incr_restart_phase_end_stats end_of_phase) o get_content›

lemma heuristic_rel_incr_restartI[intro!]:
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (incr_restart_phase_end lcount heur)›
  by (auto simp: heuristic_rel_def heuristic_rel_stats_def incr_restart_phase_end_def)

lemma [intro!]:
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (heuristic_reluctant_disable heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (schedule_next_pure_lits heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (heuristic_reluctant_disable heur)›
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (schedule_next_reduce delta heur)›
  by (auto simp: heuristic_rel_def heuristic_reluctant_disable_def heuristic_rel_stats_def heuristic_reluctant_disable_stats_def
     next_pure_lits_schedule_def schedule_next_pure_lits_def schedule_next_pure_lits_stats_def
     next_reduce_schedule_def schedule_next_reduce_def schedule_next_reduce_stats_def)

lemma [simp]:
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (restart_info_restart_done_heur heur)›
  by (auto simp: heuristic_rel_def heuristic_rel_stats_def restart_info_restart_done_heur_def
    restart_info_restart_done_heur_stats_def)


subsection ‹Number of clauses›

type_synonym clss_size = ‹nat × nat × nat × nat × nat›

definition clss_size
  :: ‹'v clauses_l ⇒ 'v clauses ⇒ 'v clauses ⇒ 'v clauses ⇒ 'v clauses ⇒'v clauses ⇒ 'v clauses ⇒
     'v clauses ⇒ 'v clauses ⇒ clss_size›
where
  ‹clss_size N NE UE NEk UEk NS US N0 U0 =
     (size (learned_clss_lf N), size UE, size UEk, size US, size U0)›

definition clss_size_lcount :: ‹clss_size ⇒ nat› where
  ‹clss_size_lcount = (λ(lcount, lcountUE, lcountUEk, lcountUS). lcount)›

definition clss_size_lcountUE :: ‹clss_size ⇒ nat› where
  ‹clss_size_lcountUE = (λ(lcount, lcountUE, lcountUEk, lcountUS). lcountUE)›

definition clss_size_lcountUEk :: ‹clss_size ⇒ nat› where
  ‹clss_size_lcountUEk = (λ(lcount, lcountUE, lcountUEk, lcountUS). lcountUEk)›

definition clss_size_lcountUS :: ‹clss_size ⇒ nat› where
  ‹clss_size_lcountUS = (λ(lcount, lcountUE, lcountUEk, lcountUS, _). lcountUS)›

definition clss_size_lcountU0 :: ‹clss_size ⇒ nat› where
  ‹clss_size_lcountU0 = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). lcountU0)›

definition clss_size_incr_lcount :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_incr_lcount =
     (λ(lcount, lcountUE, lcountUEk, lcountUS). (lcount + 1, lcountUE, lcountUEk, lcountUS))›

definition clss_size_decr_lcount :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_decr_lcount =
     (λ(lcount, lcountUE, lcountUEk, lcountUS). (lcount - 1, lcountUE, lcountUEk, lcountUS))›

definition clss_size_incr_lcountUE :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_incr_lcountUE =
     (λ(lcount, lcountUE, lcountUEk, lcountUS). (lcount, lcountUE + 1, lcountUEk, lcountUS))›

definition clss_size_incr_lcountUEk :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_incr_lcountUEk =
     (λ(lcount, lcountUE, lcountUEk, lcountUS). (lcount, lcountUE, lcountUEk + 1, lcountUS))›

definition clss_size_incr_lcountUS :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_incr_lcountUS =
     (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). (lcount, lcountUE, lcountUEk, lcountUS + 1, lcountU0))›

definition clss_size_incr_lcountU0 :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_incr_lcountU0 =
     (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). (lcount, lcountUE, lcountUEk, lcountUS, lcountU0 + 1))›

definition clss_size_resetUS :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_resetUS =
     (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). (lcount, lcountUE, lcountUEk, 0, lcountU0))›

definition clss_size_resetU0 :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_resetU0 =
     (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). (lcount, lcountUE, lcountUEk, lcountUS, 0))›

definition clss_size_resetUE :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_resetUE =
     (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). (lcount, 0, lcountUEk, lcountUS, lcountU0))›

definition clss_size_resetUEk :: ‹clss_size ⇒ clss_size› where
  ‹clss_size_resetUEk =
     (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). (lcount, lcountUE, 0, lcountUS, lcountU0))›

definition clss_size_allcount :: ‹clss_size ⇒ nat› where
  ‹clss_size_allcount =
    (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). lcount + lcountUE + lcountUEk + lcountUS + lcountU0)›

abbreviation clss_size_resetUS0 :: ‹clss_size ⇒ _› where
  ‹clss_size_resetUS0 lcount ≡ clss_size_resetUE (clss_size_resetUS (clss_size_resetU0 lcount))›

lemma clss_size_add_simp[simp]:
  ‹clss_size N NE (add_mset D UE) NEk UEk NS US N0 U0 = clss_size_incr_lcountUE (clss_size N NE UE NEk UEk NS US N0 U0)›
  ‹clss_size N (add_mset C NE) UE NEk UEk NS US N0 U0 = clss_size N NE UE NEk UEk NS US N0 U0›
  ‹clss_size N NE UE NEk UEk (add_mset C NS) US N0 U0 = clss_size N NE UE NEk UEk NS US N0 U0›
  by (auto simp: clss_size_def ran_m_fmdrop_If clss_size_decr_lcount_def
    clss_size_incr_lcountUE_def size_remove1_mset_If clss_size_resetUS_def)

lemma clss_size_upd_simp[simp]:
  ‹C ∈# dom_m N ⟹  clss_size (N(C ↪ C')) NE UE NEk UEk NS US N0 U0 = clss_size N NE UE NEk UEk NS US N0 U0›
  ‹C ∉# dom_m N ⟹ ¬snd D ⟹ clss_size (fmupd C D N) NE UE NEk UEk NS US N0 U0 = clss_size_incr_lcount (clss_size N NE UE NEk UEk NS US N0 U0)›
  ‹C ∉# dom_m N ⟹ snd D ⟹ clss_size (fmupd C D N) NE UE NEk UEk NS US N0 U0 = (clss_size N NE UE NEk UEk NS US N0 U0)›
  by (auto simp: clss_size_def learned_clss_l_fmupd_if clss_size_incr_lcount_def)

lemma clss_size_del_simp[simp]:
  ‹C ∈# dom_m N ⟹ ¬irred N C ⟹ clss_size (fmdrop C N) NE UE NEk UEk NS US N0 U0 = clss_size_decr_lcount (clss_size N NE UE NEk UEk NS US N0 U0)›
  ‹C ∈# dom_m N ⟹ irred N C ⟹ clss_size (fmdrop C N) NE UE NEk UEk NS US N0 U0 = (clss_size N NE UE NEk UEk NS US N0 U0)›
  by (auto simp: clss_size_def ran_m_fmdrop_If clss_size_decr_lcount_def
     size_remove1_mset_If clss_size_resetUS_def)


lemma clss_size_lcount_clss_size[simp]:
  ‹clss_size_lcount (clss_size N NE UE NEk UEk NS US N0 U0) = size (learned_clss_l N)›
  ‹clss_size_allcount (clss_size N NE UE NEk UEk NS US N0 U0) = size (learned_clss_l N) + size UE + size UEk + size US + size U0›
  by (auto simp: clss_size_lcount_def clss_size_def clss_size_allcount_def)

lemma clss_size_resetUS_simp[simp]:
  ‹clss_size_resetUS (clss_size_decr_lcount (clss_size baa da ea NEk UEk fa ga ha ia)) =
     clss_size_decr_lcount (clss_size baa da ea NEk UEk fa {#} ha ia)›
  ‹clss_size_resetUS (clss_size_incr_lcount (clss_size baa da ea NEk UEk fa ga ha ia)) =
     clss_size_incr_lcount (clss_size baa da ea NEk UEk fa {#} ha ia)›
  ‹clss_size_resetUS  (clss_size_incr_lcountUE (clss_size baa da ea NEk UEk fa ga ha ia)) =
     clss_size_incr_lcountUE (clss_size baa da ea NEk UEk fa {#} ha ia)›
  ‹clss_size_resetUS (clss_size N NE UE NEk UEk NS US N0 U0) = (clss_size N NE UE NEk UEk NS {#} N0 U0)›
  ‹clss_size_lcountU0 (clss_size_resetUS x) = clss_size_lcountU0 x›
  by (auto simp: clss_size_resetUS_def clss_size_decr_lcount_def clss_size_def
    clss_size_incr_lcount_def clss_size_incr_lcountUE_def clss_size_lcountU0_def
    split: prod.splits)

lemma [simp]: ‹clss_size_resetUS (clss_size_incr_lcountUE st) =
         clss_size_incr_lcountUE (clss_size_resetUS st)›
  by (solves ‹cases st; auto simp: clss_size_incr_lcountUE_def clss_size_resetUS_def›)+

lemma clss_size_lcount_simps2[simp]:
  ‹clss_size_lcount (clss_size_resetUS S) = clss_size_lcount S›
  ‹clss_size_lcountUE (clss_size_resetUS S) = clss_size_lcountUE S›
  ‹clss_size_lcountUS (clss_size_resetUS S) = 0›


  ‹clss_size_lcount (clss_size_incr_lcountUE S) = clss_size_lcount S›
  ‹clss_size_lcountUE (clss_size_incr_lcountUE S) = Suc (clss_size_lcountUE S)›
  ‹clss_size_lcountUS (clss_size_incr_lcountUE S) = clss_size_lcountUS S›


  ‹clss_size_lcount (clss_size_decr_lcount S) = clss_size_lcount S - 1›
  ‹clss_size_lcountUE (clss_size_decr_lcount S) = clss_size_lcountUE S›
  ‹clss_size_lcountUS (clss_size_decr_lcount S) = clss_size_lcountUS S›

  ‹clss_size_incr_lcountUE (clss_size_decr_lcount S) =
        clss_size_decr_lcount (clss_size_incr_lcountUE S)›
  ‹clss_size_resetUS (clss_size_decr_lcount S) = 
     clss_size_decr_lcount (clss_size_resetUS S)›
  ‹clss_size_resetUS (clss_size_incr_lcountUE S) = clss_size_incr_lcountUE (clss_size_resetUS S)›
  by (solves ‹cases S; auto simp: clss_size_lcount_def clss_size_resetUS_def
    clss_size_lcountUE_def clss_size_lcountUS_def
    clss_size_incr_lcountUE_def clss_size_decr_lcount_def›)+

lemma [simp]:
  ‹clss_size_lcountU0 (clss_size_decr_lcount S) = clss_size_lcountU0 S›
  ‹clss_size_lcountU0 (clss_size_incr_lcountUE S) = clss_size_lcountU0 S›
  ‹clss_size_lcountU0 (clss_size_incr_lcountUS S) = clss_size_lcountU0 S›
  ‹clss_size_lcountU0 (clss_size_incr_lcountU0 S) = clss_size_lcountU0 S + 1›
  by (auto simp: clss_size_lcountU0_def clss_size_decr_lcount_def clss_size_incr_lcountUE_def
      clss_size_incr_lcountUS_def clss_size_incr_lcountU0_def
    split: prod.splits)

lemma [simp]:
  ‹clss_size_lcount (clss_size_incr_lcountUEk c) = clss_size_lcount c›
  ‹clss_size_lcountUE (clss_size_incr_lcountUEk c) = clss_size_lcountUE c›
  ‹clss_size_lcountUEk (clss_size_incr_lcountUEk c) = clss_size_lcountUEk c+1›
  ‹clss_size_lcountU0 (clss_size_incr_lcountUEk c) = clss_size_lcountU0 c›
  ‹clss_size_lcountUS (clss_size_incr_lcountUEk c) = clss_size_lcountUS c›
  by (auto simp: clss_size_lcountUE_def clss_size_lcount_def clss_size_incr_lcountUEk_def
    clss_size_lcountUEk_def clss_size_lcountU0_def clss_size_lcountUS_def
    split: prod.splits)

lemma clss_size_simps3[simp]:
  ‹clss_size_lcountUE (clss_size baa da ea NEk UEk fa x N0 U0) = size ea›
  ‹clss_size_lcountUEk (clss_size baa da ea NEk UEk fa x N0 U0) = size UEk›
  ‹clss_size_lcountUS (clss_size baa da ea NEk UEk fa x N0 U0) = size x›
  ‹clss_size_lcountU0 (clss_size baa da ea NEk UEk fa x N0 U0) = size U0›
  by (auto simp: clss_size_lcountUE_def clss_size_lcountUS_def clss_size_lcountU0_def clss_size_def
    clss_size_lcountUEk_def)

(*TODO Move inside this file*)
lemma clss_size_lcount_incr_lcount_simps[simp]:
  ‹clss_size_lcount (clss_size_incr_lcount S) = Suc (clss_size_lcount S)›
  ‹clss_size_lcountUE (clss_size_incr_lcount S) = (clss_size_lcountUE S)›
  ‹clss_size_lcountUEk (clss_size_incr_lcount S) = (clss_size_lcountUEk S)›
  ‹clss_size_lcountUS (clss_size_incr_lcount S) = (clss_size_lcountUS S)›
  ‹clss_size_lcountU0 (clss_size_incr_lcount (S)) = clss_size_lcountU0 ( (S))›
  by (cases S; auto simp: clss_size_incr_lcount_def
      clss_size_lcount_def clss_size_def clss_size_lcountUEk_def
    clss_size_lcountUE_def clss_size_lcountUS_def clss_size_lcountU0_def; fail)+

lemma [simp]:
  ‹clss_size_lcount (clss_size_resetU0 c) = clss_size_lcount c›
  ‹clss_size_lcount (clss_size_resetUE c) = clss_size_lcount c›
  ‹clss_size_lcount (clss_size_resetUEk c) = clss_size_lcount c›
  ‹clss_size_lcountUE (clss_size_resetU0 c) = clss_size_lcountUE c›
  ‹clss_size_lcountUE (clss_size_resetUEk c) = clss_size_lcountUE c›
  ‹clss_size_lcountU0 (clss_size_resetUE c) = clss_size_lcountU0 c›
  ‹clss_size_lcountU0 (clss_size_resetUEk c) = clss_size_lcountU0 c›
  ‹clss_size_lcountU0 (clss_size_resetU0 c) = 0›
 ‹clss_size_lcountU0 (clss_size_decr_lcount c) = clss_size_lcountU0 c›
  ‹clss_size_lcountUEk (clss_size_resetUE c) = clss_size_lcountUEk c›
  ‹clss_size_lcountUEk (clss_size_resetUS c) = clss_size_lcountUEk c›
  ‹clss_size_lcountUEk (clss_size_resetU0 c) = clss_size_lcountUEk c›
  ‹clss_size_lcountUEk (clss_size_resetUEk c) = 0›
 ‹clss_size_lcountUEk (clss_size_decr_lcount c) = clss_size_lcountUEk c›
  ‹clss_size_lcountUE (clss_size_resetUE c) = 0›
  ‹clss_size_lcountUS (clss_size_resetUE c) = clss_size_lcountUS c›
  ‹clss_size_lcountUS (clss_size_resetUEk c) = clss_size_lcountUS c›
  by (auto simp: clss_size_resetU0_def clss_size_lcount_def clss_size_lcountU0_def
    clss_size_lcountUS_def clss_size_decr_lcount_def
    clss_size_resetUE_def clss_size_resetUEk_def clss_size_lcountUE_def clss_size_lcountUEk_def
    clss_size_resetUS_def split: prod.splits)

definition print_literal_of_trail where
  ‹print_literal_of_trail _ = RETURN ()›

definition print_trail where
  ‹print_trail = (λ(M, _). do {
  i ← WHILE⇩T(λi. i < length M)
  (λi. do {
  ASSERT(i < length M);
  print_literal_of_trail (M!i);
  RETURN (i+1)})
  0;
  print_literal_of_trail ((0::nat));
  RETURN ()
  })›

definition print_trail2 where
  ‹print_trail2 = (λ(M, _). RETURN ())›

lemma print_trail_print_trail2:
  ‹(M,M')∈Id ⟹ print_trail M ≤ ⇓ Id (print_trail2 M')›
  unfolding print_trail_def print_trail2_def
  apply (refine_vcg WHILET_rule[where
    R = ‹measure (λi. Suc (length (fst M)) - i)› and
    I = ‹λi. i ≤ length (fst M)›])
  subgoal by auto
  subgoal by auto
  subgoal unfolding print_literal_of_trail_def by auto
  subgoal unfolding print_literal_of_trail_def by auto
  done

lemma print_trail_print_trail2_rel:
  ‹(print_trail, print_trail2) ∈ Id →⇩f ⟨unit_rel⟩nres_rel›
  using print_trail_print_trail2 by (fastforce intro: frefI nres_relI)

definition clss_size_corr :: ‹_ ⇒ _ ⇒ _ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ _ ⇒_ ⇒ clss_size ⇒ bool› where
  ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟷ c = clss_size N NE UE NEk UEk NS US N0 U0›

text ‹There is no equivalence because of rounding errors. However, we do not care about that in
  the proofs and we are always safe in IsaSAT.

  However, the intro rule are still too dangerous and make it hard to recognize the original goal.
  Therefore, they are not marked as safe.
›
lemma
  clss_size_corr_intro[intro!]:
    ‹C ∈# dom_m N ⟹ ¬irred N C ⟹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr (fmdrop C N) NE UE NEk UEk NS US N0 U0 (clss_size_decr_lcount c)›
    ‹C ∉# dom_m N ⟹ ¬b ⟹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr (fmupd C (D, b) N) NE UE NEk UEk NS US N0 U0 (clss_size_incr_lcount c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE UE NEk (add_mset E UEk) NS US N0 U0 (clss_size_incr_lcountUEk c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE (add_mset E UE) NEk UEk NS US N0 U0 (clss_size_incr_lcountUE c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE UE NEk UEk NS (add_mset E US) N0 U0 (clss_size_incr_lcountUS c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE UE NEk UEk NS US N0 (add_mset E U0) (clss_size_incr_lcountU0 c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 (clss_size N NE UE NEk UEk NS US N0 U0)›
  and
  clss_size_corr_simp[simp]:
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE UE NEk UEk NS {#} N0 U0 (clss_size_resetUS c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE UE NEk {#} NS US N0 U0 (clss_size_resetUEk c)›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE UE NEk UEk NS US N0 {#} (clss_size_resetU0 c)›
    ‹C ∉# dom_m N ⟹ b ⟹ clss_size_corr (fmupd C (D, b) N) NE UE NEk UEk NS US N0 U0 c ⟷
      clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹C ∈# dom_m N ⟹ irred N C ⟹ clss_size_corr (fmdrop C N) NE UE NEk UEk NS US N0 U0 c = clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹C ∈# dom_m N ⟹ clss_size_corr (N(C ↪ swap (N ∝ C) i j)) NE UE NEk UEk NS US N0 U0 c = clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr N NE UE (add_mset E NEk) UEk NS US N0 U0 c = clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr N (add_mset E NE) UE NEk UEk NS US N0 U0 c = clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr N NE UE NEk UEk (add_mset E NS) US N0 U0 c = clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr N NE UE NEk UEk NS US (add_mset E N0) U0 c = clss_size_corr N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ⟹ clss_size_lcount lcount = size (learned_clss_lf N)›
  by (auto simp: clss_size_def ran_m_fmdrop_If clss_size_decr_lcount_def learned_clss_l_fmupd_if
    clss_size_incr_lcount_def clss_size_incr_lcountUS_def clss_size_incr_lcountU0_def clss_size_incr_lcountUEk_def
    clss_size_incr_lcountUE_def  clss_size_lcount_def clss_size_resetUEk_def clss_size_resetU0_def
      size_remove1_mset_If clss_size_resetUS_def clss_size_corr_def; fail)+

text ‹This version of the counter is incomplete. It is however useful because we do not need to care
about some of the counts during restarts. In particular, it avoids taking care of overflows.
›
definition clss_size_corr_restart :: ‹'v clauses_l ⇒ 'v clauses ⇒ 'v clauses ⇒ 'v clauses ⇒ 'v clauses ⇒
  'v clauses ⇒ 'v clauses ⇒ 'v clauses ⇒ 'v clauses ⇒ clss_size ⇒ bool› where
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟷ (∃UE US U0. c = clss_size N NE UE NEk UEk NS US N0 U0)›

lemma clss_size_corr_restart_clss_size_corr:
  ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE UE' NEk UEk NS US' N0 U0' c›
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr N NE {#} NEk UEk NS {#} N0 {#} (clss_size_resetUS0 c)›
  by (auto simp: clss_size_corr_def clss_size_corr_restart_def clss_size_resetUS_def
    clss_size_resetU0_def clss_size_def clss_size_resetUE_def)

lemma
  clss_size_corr_restart_intro[intro]:
    ‹C ∈# dom_m N ⟹ ¬irred N C ⟹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart (fmdrop C N) NE {#} NEk UEk NS {#} N0 {#} (clss_size_decr_lcount c)›
    ‹C ∉# dom_m N ⟹ ¬b ⟹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart (fmupd C (D, b) N) NE {#} NEk UEk NS {#} N0 {#} (clss_size_incr_lcount c)›
    ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE {#} NEk (add_mset E UEk) NS {#} N0 {#} (clss_size_incr_lcountUEk c)›
    ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 (clss_size N NE {#} NEk UEk NS {#} N0 {#})›
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE {#} NEk UEk NS {#} N0 {#} c›

  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE {#} NEk UEk NS US N0 U0 (c)›
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 {#} (c)›
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE UE NEk UEk NS {#} N0 U0 (c)›
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 {#} (c)›
  and
  clss_size_corr_restart_simp[simp]:
  ‹NO_MATCH {#} UE ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟷ clss_size_corr_restart N NE {#} NEk UEk NS US N0 U0 (c)›
  ‹NO_MATCH {#} U0 ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟷ clss_size_corr_restart N NE UE NEk UEk NS US N0 {#} (c)›
  ‹NO_MATCH {#} US ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟷ clss_size_corr_restart N NE UE NEk UEk NS {#} N0 U0 (c)›
  ‹NO_MATCH {#} UE ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟷ clss_size_corr_restart N NE UE NEk UEk NS US N0 {#} (c)›
    (* ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE UE NEk UEk NS {#} N0 U0 (c)› *)
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹ clss_size_corr_restart N NE UE NEk {#} NS US N0 U0 (clss_size_resetUEk c)›
    ‹clss_size_corr_restart N NE UE NEk UEk NS (add_mset E US) N0 U0 (c) ⟷ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 (add_mset E U0) (c) ⟷ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹C ∉# dom_m N ⟹ b ⟹ clss_size_corr_restart (fmupd C (D, b) N) NE UE NEk UEk NS US N0 U0 c ⟷
      clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹C ∈# dom_m N ⟹ irred N C ⟹ clss_size_corr_restart (fmdrop C N) NE UE NEk UEk NS US N0 U0 c = clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹C ∈# dom_m N ⟹ clss_size_corr_restart (N(C ↪ swap (N ∝ C) i j)) NE UE NEk UEk NS US N0 U0 c = clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr_restart N (add_mset E NE) UE NEk UEk NS US N0 U0 c = clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr_restart N NE UE (add_mset E NEk) UEk NS US N0 U0 c = clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
    ‹clss_size_corr_restart N NE UE NEk UEk (add_mset E NS) US N0 U0 c = clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
  ‹clss_size_corr_restart N NE UE NEk UEk NS US (add_mset E N0) U0 c = clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
  by (auto simp: clss_size_def ran_m_fmdrop_If clss_size_decr_lcount_def learned_clss_l_fmupd_if
    clss_size_incr_lcount_def clss_size_incr_lcountUS_def clss_size_incr_lcountU0_def clss_size_incr_lcountUEk_def
    clss_size_incr_lcountUE_def  clss_size_lcount_def clss_size_resetUEk_def clss_size_resetU0_def
    clss_size_resetUE_def
      size_remove1_mset_If clss_size_resetUS_def clss_size_corr_restart_def; fail)+

text ‹The following lemmas produce loops, but usually only in the next file (!). Hence, we do
  not activate them by default as simp rules.
›
lemma clss_size_corr_restart_rew:
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 lcount ⟹ clss_size_lcount lcount = size (learned_clss_lf N)›
  by (auto simp: clss_size_def ran_m_fmdrop_If clss_size_decr_lcount_def learned_clss_l_fmupd_if
    clss_size_incr_lcount_def clss_size_incr_lcountUS_def clss_size_incr_lcountU0_def clss_size_incr_lcountUEk_def
    clss_size_incr_lcountUE_def  clss_size_lcount_def clss_size_resetUEk_def clss_size_resetU0_def
    clss_size_resetUE_def
      size_remove1_mset_If clss_size_resetUS_def clss_size_corr_restart_def; fail)+

lemma clss_size_corr_restart_simp3:
  ‹clss_size_corr_restart N NE UE NEk (add_mset E UEk) NS US N0 U0 (clss_size_incr_lcountUEk c) ⟷
  clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c›
  by (auto simp: clss_size_corr_restart_def clss_size_incr_lcountUEk_def clss_size_def
    split: prod.splits)

subsection ‹Lifting to heuristic level›
definition get_next_phase_heur_pre_stats :: ‹bool ⇒ nat ⇒ restart_heuristics ⇒ bool› where
  ‹get_next_phase_heur_pre_stats = (λb L (_, _, _, _, rephase, _).
  get_next_phase_pre b L rephase)›

definition get_next_phase_heur_stats :: ‹bool ⇒ nat ⇒ restart_heuristics ⇒ bool nres›  where
  ‹get_next_phase_heur_stats = (λb L (_, _, _, _, rephase, _).
    get_next_phase_stats b L rephase)›

definition get_next_phase_heur :: ‹bool ⇒ nat ⇒ isasat_restart_heuristics ⇒ bool nres›  where
  ‹get_next_phase_heur = (λb L heur.
  let heur = get_restart_heuristics heur in
  get_next_phase_heur_stats b L heur)›

definition end_of_restart_phase_stats :: ‹restart_heuristics ⇒ 64 word› where
  ‹end_of_restart_phase_stats = (λ(_, _, (restart_phase,_ ,_ , end_of_phase, _), _).
    end_of_phase)›

definition end_of_restart_phase :: ‹isasat_restart_heuristics ⇒ 64 word› where
  ‹end_of_restart_phase = end_of_restart_phase_stats o get_content›

end