Theory IsaSAT_Setup

theory IsaSAT_Setup
  imports
    Tuple17
    IsaSAT_Phasing
    Watched_Literals.Watched_Literals_Watch_List_Initialisation
    IsaSAT_Lookup_Conflict
    IsaSAT_Clauses IsaSAT_Arena IsaSAT_Watch_List LBD
    IsaSAT_Options
    IsaSAT_Rephase
    IsaSAT_EMA
    IsaSAT_Stats
    IsaSAT_Profile
    IsaSAT_VDom
    IsaSAT_Occurence_List
    IsaSAT_Bump_Heuristics_State
begin

chapter ‹Complete state›

hide_const (open) IsaSAT_VDom.get_aivdom

hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.SPEC

text ‹We here define the last step of our refinement: the step with all the heuristics and fully
  deterministic code.

  After the result of benchmarking, we concluded that the use of \<^typ>‹nat› leads to worse performance
  than using ‹sint64›. As, however, the later is not complete, we do so with a switch: as long
  as it fits, we use the faster (called 'bounded') version. After that we switch to the 'unbounded'
  version (which is still bounded by memory anyhow) if we generate Standard ML code.

  We have successfully killed all natural numbers when generating LLVM. However, the LLVM binding
  does not have a binding to GMP integers.
›
(*TODO Move*)
fun get_unkept_unit_init_clss_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
  ‹get_unkept_unit_init_clss_wl (M, N, D, NE, UE, NEk, UEk, NS, US, Q, W) = NE›

fun get_unkept_unit_learned_clss_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
  ‹get_unkept_unit_learned_clss_wl (M, N, D, NE, UE, NEk, UEk, NS, US, Q, W) = UE›

fun get_kept_unit_init_clss_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
  ‹get_kept_unit_init_clss_wl (M, N, D, NE, UE, NEk, UEk, NS, US, Q, W) = NEk›

fun get_kept_unit_learned_clss_wl :: ‹'v twl_st_wl ⇒ 'v clauses› where
  ‹get_kept_unit_learned_clss_wl (M, N, D, NE, UE, NEk, UEk, NS, US, Q, W) = UEk›

lemma get_unit_init_clss_wl_alt_def:
  ‹get_unit_init_clss_wl T = get_unkept_unit_init_clss_wl T + get_kept_unit_init_clss_wl T›
  by (cases T) auto

lemma get_unit_learned_clss_wl_alt_def:
  ‹get_unit_learned_clss_wl T = get_unkept_unit_learned_clss_wl T + get_kept_unit_learned_clss_wl T›
  by (cases T) auto


section ‹VMTF›

type_synonym out_learned = ‹nat clause_l›


subsection ‹Conflict›

definition size_conflict_wl :: ‹nat twl_st_wl ⇒ nat› where
  ‹size_conflict_wl S = size (the (get_conflict_wl S))›

definition size_conflict :: ‹nat clause option ⇒ nat› where
  ‹size_conflict D = size (the D)›

definition size_conflict_int :: ‹conflict_option_rel ⇒ nat› where
  ‹size_conflict_int = (λ(_, n, _). n)›


section ‹Full state›

text ‹∗‹heur› stands for heuristic.›

paragraph ‹Definition›



type_synonym isasat = ‹(trail_pol, arena,
      conflict_option_rel, nat, (nat watcher) list list, bump_heuristics,
      nat, conflict_min_cach_l, lbd, out_learned, isasat_stats, isasat_restart_heuristics,
     isasat_aivdom, clss_size, opts, arena, occurences_ref) tuple17›

abbreviation IsaSAT where
  ‹IsaSAT a b c d e f g h i j k l m n xo p occs ≡ Tuple17 a b c d e f g h i j k l m n xo p occs :: isasat›


lemmas isasat_int_splits = Tuple17.tuple17.splits
hide_fact tuple17.splits

abbreviation case_isasat_int :: ‹_ ⇒ isasat ⇒ _› where
  ‹case_isasat_int ≡ case_tuple17›

abbreviation get_trail_wl_heur :: ‹isasat ⇒ trail_pol› where
  ‹get_trail_wl_heur ≡ Tuple17_get_a›

abbreviation get_clauses_wl_heur :: ‹isasat ⇒ arena› where
  ‹get_clauses_wl_heur ≡ Tuple17_get_b›

abbreviation get_conflict_wl_heur :: ‹isasat ⇒ conflict_option_rel› where
  ‹get_conflict_wl_heur ≡ Tuple17_get_c›

abbreviation literals_to_update_wl_heur :: ‹isasat ⇒ nat› where
  ‹literals_to_update_wl_heur ≡ Tuple17_get_d›

abbreviation get_watched_wl_heur :: ‹isasat ⇒ (nat watcher) list list› where
  ‹get_watched_wl_heur ≡ Tuple17_get_e›

abbreviation get_vmtf_heur :: ‹isasat ⇒ bump_heuristics› where
  ‹get_vmtf_heur ≡ Tuple17_get_f›

abbreviation get_count_max_lvls_heur :: ‹isasat ⇒ nat› where
  ‹get_count_max_lvls_heur ≡ Tuple17_get_g›

abbreviation get_conflict_cach :: ‹isasat ⇒ conflict_min_cach_l› where
  ‹get_conflict_cach ≡ Tuple17_get_h›

abbreviation get_lbd :: ‹isasat ⇒ lbd› where
  ‹get_lbd ≡ Tuple17_get_i›

abbreviation get_outlearned_heur :: ‹isasat ⇒ out_learned› where
  ‹get_outlearned_heur ≡ Tuple17_get_j›

abbreviation get_stats_heur :: ‹isasat ⇒ isasat_stats› where
  ‹get_stats_heur ≡ Tuple17_get_k›

abbreviation get_heur :: ‹isasat ⇒ isasat_restart_heuristics› where
  ‹get_heur ≡ Tuple17_get_l›

abbreviation get_aivdom :: ‹isasat ⇒ isasat_aivdom› where
  ‹get_aivdom ≡ Tuple17_get_m›

abbreviation get_learned_count :: ‹isasat ⇒ clss_size› where
  ‹get_learned_count ≡ Tuple17_get_n›

abbreviation get_opts :: ‹isasat ⇒ opts› where
  ‹get_opts ≡ Tuple17_get_o›

abbreviation get_old_arena :: ‹isasat ⇒ arena› where
  ‹get_old_arena ≡ Tuple17_get_p›

abbreviation get_occs :: ‹isasat ⇒ occurences_ref› where
  ‹get_occs ≡ Tuple17_get_q›

abbreviation set_trail_wl_heur :: ‹trail_pol ⇒isasat ⇒ _› where
  ‹set_trail_wl_heur ≡ Tuple17.set_a›

abbreviation set_clauses_wl_heur :: ‹arena ⇒isasat ⇒ _› where
  ‹set_clauses_wl_heur ≡ Tuple17.set_b›

abbreviation set_conflict_wl_heur :: ‹conflict_option_rel ⇒isasat ⇒ _› where
  ‹set_conflict_wl_heur ≡ Tuple17.set_c›

abbreviation set_literals_to_update_wl_heur :: ‹nat ⇒isasat ⇒ _› where
  ‹set_literals_to_update_wl_heur ≡ Tuple17.set_d›

abbreviation set_watched_wl_heur :: ‹nat watcher list list ⇒isasat ⇒ _› where
  ‹set_watched_wl_heur ≡ Tuple17.set_e›

abbreviation set_vmtf_wl_heur :: ‹bump_heuristics ⇒isasat ⇒ _› where
  ‹set_vmtf_wl_heur ≡ Tuple17.set_f›

abbreviation set_count_max_wl_heur :: ‹nat ⇒isasat ⇒ _› where
  ‹set_count_max_wl_heur ≡ Tuple17.set_g›

abbreviation set_ccach_max_wl_heur :: ‹conflict_min_cach_l ⇒isasat ⇒ _› where
  ‹set_ccach_max_wl_heur ≡ Tuple17.set_h›

abbreviation set_lbd_wl_heur :: ‹lbd ⇒isasat ⇒ _› where
  ‹set_lbd_wl_heur ≡ Tuple17.set_i›

abbreviation set_outl_wl_heur :: ‹out_learned ⇒isasat ⇒ _› where
  ‹set_outl_wl_heur ≡ Tuple17.set_j›

abbreviation set_stats_wl_heur :: ‹isasat_stats ⇒ isasat ⇒ isasat› where
  ‹set_stats_wl_heur ≡ Tuple17.set_k›

abbreviation set_heur_wl_heur :: ‹isasat_restart_heuristics ⇒isasat ⇒ isasat› where
  ‹set_heur_wl_heur ≡ Tuple17.set_l›

abbreviation set_aivdom_wl_heur :: ‹isasat_aivdom ⇒isasat ⇒ _› where
  ‹set_aivdom_wl_heur ≡ Tuple17.set_m›

abbreviation set_learned_count_wl_heur :: ‹clss_size ⇒isasat ⇒ _› where
  ‹set_learned_count_wl_heur ≡ Tuple17.set_n›

abbreviation set_opts_wl_heur :: ‹opts ⇒isasat ⇒ _› where
  ‹set_opts_wl_heur ≡ Tuple17.set_o›

abbreviation set_old_arena_wl_heur :: ‹arena ⇒isasat ⇒ _› where
  ‹set_old_arena_wl_heur ≡ Tuple17.set_p›

abbreviation set_occs_wl_heur :: ‹occurences_ref ⇒isasat ⇒ _› where
  ‹set_occs_wl_heur ≡ Tuple17.set_q›

fun watched_by_int :: ‹isasat ⇒ nat literal ⇒ nat watched› where
  ‹watched_by_int S L = get_watched_wl_heur S ! nat_of_lit L›

definition watched_by_app_heur_pre where
  ‹watched_by_app_heur_pre = (λ((S, L), K). nat_of_lit L < length (get_watched_wl_heur S) ∧
          K < length (watched_by_int S L))›

definition watched_by_app_heur :: ‹isasat ⇒ nat literal ⇒ nat ⇒ nat watcher› where
  ‹watched_by_app_heur S L K = watched_by_int S L ! K›

definition mop_watched_by_app_heur :: ‹isasat ⇒ nat literal ⇒ nat ⇒ nat watcher nres› where
  ‹mop_watched_by_app_heur S L K = do {
     ASSERT(K < length (watched_by_int S L));
     ASSERT(nat_of_lit L < length (get_watched_wl_heur S));
     RETURN (watched_by_int S L ! K)}›

definition watched_by_app :: ‹nat twl_st_wl ⇒ nat literal ⇒ nat ⇒ nat watcher› where
  ‹watched_by_app S L K = watched_by S L ! K›

fun get_fast_ema_heur :: ‹isasat ⇒ ema› where
  ‹get_fast_ema_heur S = fast_ema_of (get_heur S)›

fun get_slow_ema_heur :: ‹isasat ⇒ ema› where
  ‹get_slow_ema_heur S = slow_ema_of (get_heur S)›

fun get_conflict_count_heur :: ‹isasat ⇒ restart_info› where
  ‹get_conflict_count_heur S = restart_info_of (get_heur S)›

abbreviation get_vdom :: ‹isasat ⇒ nat list› where
  ‹get_vdom S ≡ get_vdom_aivdom (get_aivdom S)›

abbreviation get_avdom :: ‹isasat ⇒ nat list› where
  ‹get_avdom S ≡ get_avdom_aivdom (get_aivdom S)›

abbreviation get_ivdom :: ‹isasat ⇒ nat list› where
  ‹get_ivdom S ≡ get_ivdom_aivdom (get_aivdom S)›

abbreviation get_tvdom :: ‹isasat ⇒ nat list› where
  ‹get_tvdom S ≡ get_tvdom_aivdom (get_aivdom S)›

abbreviation get_learned_count_number :: ‹isasat ⇒ nat› where
  ‹get_learned_count_number S ≡ clss_size_lcount (get_learned_count S)›

definition get_restart_phase :: ‹isasat ⇒ 64 word› where
  ‹get_restart_phase = (λS.
     current_restart_phase (get_heur S))›

definition cach_refinement_empty where
  ‹cach_refinement_empty 𝒜 cach ⟷
       (cach, λ_. SEEN_UNKNOWN) ∈ cach_refinement 𝒜›

paragraph ‹VMTF›

(*
definition bump_heur where
  ‹bump_heur 𝒜 M =
    ((Id ×⇩r nat_rel ×⇩r nat_rel ×⇩r nat_rel ×⇩r ⟨nat_rel⟩option_rel) ×⇩f distinct_atoms_rel 𝒜)¯
      `` vmtf 𝒜 M›

lemma isa_vmtfI:
  ‹(vm, to_remove') ∈ vmtf 𝒜 M ⟹ (to_remove, to_remove') ∈ distinct_atoms_rel 𝒜 ⟹
    (vm, to_remove) ∈ bump_heur 𝒜 M›
  by (auto simp: Image_iff intro!: bexI[of _ ‹(vm, to_remove')›])

lemma isa_vmtf_consD:
  ‹((ns, m, fst_As, lst_As, next_search), remove) ∈ bump_heur 𝒜 M ⟹
     ((ns, m, fst_As, lst_As, next_search), remove) ∈ bump_heur 𝒜 (L # M)›
  by (auto simp: dest: vmtf_consD)

lemma isa_vmtf_consD:
  ‹f ∈ bump_heur 𝒜 M ⟹
     f ∈ bump_heur 𝒜 (L # M)›
  by (auto simp: dest: vmtf_consD)
    *)

text ‹\<^term>‹vdom› is an upper bound on all the address of the clauses that are used in the
state. \<^term>‹avdom› includes the active clauses.
›

definition twl_st_heur :: ‹(isasat × nat twl_st_wl) set› where
[unfolded Let_def]: ‹twl_st_heur =
  {(S, T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S;
    occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_atms_st T) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', D) ∈ option_lookup_clause_rel (all_atms_st T) ∧
    (D = None ⟶ j ≤ length M) ∧
    Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st T)) ∧
    vm ∈ bump_heur (all_atms_st T) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M D ∧
    cach_refinement_empty (all_atms_st T) cach ∧
    out_learned M D outl ∧
    clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
    vdom_m (all_atms_st T) W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_atms_st T) ∧
    isasat_input_nempty (all_atms_st T) ∧
    old_arena = [] ∧
    heuristic_rel (all_atms_st T) heur ∧
    (occs, empty_occs_list (all_atms_st T)) ∈ occurrence_list_ref
  }›


lemma twl_st_heur_state_simp:
  assumes ‹(S, S') ∈ twl_st_heur›
  shows
     ‹(get_trail_wl_heur S, get_trail_wl S') ∈ trail_pol (all_atms_st S')› and
     twl_st_heur_state_simp_watched: ‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹
       watched_by_int S C = watched_by S' C›
      ‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹
       get_watched_wl_heur S ! (nat_of_lit C) =  get_watched_wl S' C›and
     ‹literals_to_update_wl S' =
         uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev (get_trail_wl S')))› and
     twl_st_heur_state_simp_watched2: ‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹
       nat_of_lit C < length(get_watched_wl_heur S)›
  using assms unfolding twl_st_heur_def by (solves ‹cases S; cases S'; auto simp add: Let_def map_fun_rel_def ac_simps all_atms_st_def›)+

text ‹
  This is the version of the invariants where some informations are already lost. For example,
  losing statistics does not matter if UNSAT was derived.
  ›
definition twl_st_heur_loop :: ‹(isasat × nat twl_st_wl) set› where
[unfolded Let_def]: ‹twl_st_heur_loop =
  {(S, T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S; occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_atms_st T) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', D) ∈ option_lookup_clause_rel (all_atms_st T) ∧
    (D = None ⟶ j ≤ length M) ∧
    Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st T)) ∧
    vm ∈ bump_heur (all_atms_st T) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M D ∧
    cach_refinement_empty (all_atms_st T) cach ∧
    out_learned M D outl ∧
    (D = None ⟶ clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount) ∧
    vdom_m (all_atms_st T)  W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_atms_st T) ∧
    isasat_input_nempty (all_atms_st T) ∧
    old_arena = [] ∧
    heuristic_rel (all_atms_st T) heur∧
    (occs, empty_occs_list (all_atms_st T)) ∈ occurrence_list_ref
  }›

abbreviation learned_clss_count_lcount :: ‹_› where
  ‹learned_clss_count_lcount S ≡ clss_size_lcount (S) +
  clss_size_lcountUE (S) + clss_size_lcountUEk (S) +
  clss_size_lcountUS (S) +
    clss_size_lcountU0 (S)›

definition learned_clss_count :: ‹isasat ⇒ nat› where
  ‹learned_clss_count S = learned_clss_count_lcount (get_learned_count S)›

lemma get_learned_count_learned_clss_countD:
  ‹get_learned_count S = clss_size_resetUS (get_learned_count T) ⟹
       learned_clss_count S ≤ learned_clss_count T›
  ‹get_learned_count S = clss_size_resetUS0 (get_learned_count T) ⟹
       learned_clss_count S ≤ learned_clss_count T›
  by (cases S; cases T; auto simp: learned_clss_count_def; fail)+

lemma get_learned_count_learned_clss_countD2:
  ‹get_learned_count S = (get_learned_count T) ⟹
       learned_clss_count S = learned_clss_count T›
  by (cases S; cases T) (auto simp: learned_clss_count_def)

abbreviation twl_st_heur'''
   :: ‹nat ⇒ (isasat × nat twl_st_wl) set›
where
‹twl_st_heur''' r ≡ {(S, T). (S, T) ∈ twl_st_heur ∧
           length (get_clauses_wl_heur S) = r}›

abbreviation twl_st_heur''''u
   :: ‹nat ⇒ nat ⇒ (isasat × nat twl_st_wl) set›
where
‹twl_st_heur''''u r u ≡ {(S, T). (S, T) ∈ twl_st_heur ∧
           length (get_clauses_wl_heur S) = r ∧
           learned_clss_count S ≤ u}›

lemma twl_st_heur'''_twl_st_heur''''uD:
  ‹(x, y) ∈ twl_st_heur''' r ⟹
  (x, y) ∈ twl_st_heur''''u r (learned_clss_count x)›
  by auto

definition twl_st_heur' :: ‹nat multiset ⇒ (isasat × nat twl_st_wl) set› where
‹twl_st_heur' N = {(S, S'). (S, S') ∈ twl_st_heur ∧ dom_m (get_clauses_wl S') = N}›

definition twl_st_heur_conflict_ana
  :: ‹(isasat × nat twl_st_wl) set›
where
[unfolded Let_def]: ‹twl_st_heur_conflict_ana =
  {(S, T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S; occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_atms_st T) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', D) ∈ option_lookup_clause_rel (all_atms_st T) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st T)) ∧
    vm ∈ bump_heur (all_atms_st T) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M D ∧
    cach_refinement_empty (all_atms_st T) cach ∧
    out_learned M D outl ∧
    clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
    vdom_m (all_atms_st T) W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_atms_st T) ∧
    isasat_input_nempty (all_atms_st T) ∧
    old_arena = [] ∧
    heuristic_rel (all_atms_st T) heur∧
    (occs, empty_occs_list (all_atms_st T)) ∈ occurrence_list_ref
  }›

lemma twl_st_heur_twl_st_heur_conflict_ana:
  ‹(S, T) ∈ twl_st_heur ⟹ (S, T) ∈ twl_st_heur_conflict_ana›
  by (cases S; cases T; auto simp: twl_st_heur_def twl_st_heur_conflict_ana_def Let_def ac_simps all_atms_st_def)

lemma twl_st_heur_ana_state_simp:
  assumes ‹(S, S') ∈ twl_st_heur_conflict_ana›
  shows
    ‹(get_trail_wl_heur S, get_trail_wl S') ∈ trail_pol (all_atms_st S')› and
    ‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹ watched_by_int S C = watched_by S' C›
  using assms unfolding twl_st_heur_conflict_ana_def by (solves ‹cases S; cases S'; auto simp: map_fun_rel_def ac_simps
    all_atms_st_def Let_def›)+

text ‹This relations decouples the conflict that has been minimised and appears abstractly
from the refined state, where the conflict has been removed from the data structure to a
separate array.›
definition twl_st_heur_bt :: ‹(isasat × nat twl_st_wl) set› where
[unfolded Let_def]: ‹twl_st_heur_bt =
  {(S, T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S; occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_atms_st T) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', None) ∈ option_lookup_clause_rel (all_atms_st T) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st T)) ∧
    vm ∈ bump_heur (all_atms_st T) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M None ∧
    cach_refinement_empty (all_atms_st T) cach ∧
    out_learned M None outl ∧
    clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
    vdom_m (all_atms_st T) W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_atms_st T) ∧
    isasat_input_nempty (all_atms_st T) ∧
    old_arena = [] ∧
    heuristic_rel (all_atms_st T) heur ∧
    (occs, empty_occs_list (all_atms_st T)) ∈ occurrence_list_ref
  }›


text ‹
  The difference between \<^term>‹isasat_unbounded_assn› and \<^term>‹isasat_bounded_assn› corresponds to the
  following condition:
›
definition isasat_fast :: ‹isasat ⇒ bool› where
  ‹isasat_fast S ⟷ (length (get_clauses_wl_heur S) ≤ snat64_max - (unat32_max div 2 + MAX_HEADER_SIZE+1) ∧
  learned_clss_count S < unat64_max)›

lemma isasat_fast_length_leD: ‹isasat_fast S ⟹ length (get_clauses_wl_heur S) ≤ snat64_max› and
  isasat_fast_countD:
    ‹isasat_fast S ⟹ clss_size_lcount (get_learned_count S) < unat64_max›
    ‹isasat_fast S ⟹ clss_size_lcountUS (get_learned_count S) < unat64_max›
    ‹isasat_fast S ⟹ clss_size_lcountUE (get_learned_count S) < unat64_max›
    ‹isasat_fast S ⟹ clss_size_lcountU0 (get_learned_count S) < unat64_max›
  by (solves ‹cases S; auto simp: isasat_fast_def clss_size_lcountUS_def
    clss_size_lcountUE_def clss_size_lcount_def clss_size_lcountU0_def
    clss_size_allcount_def learned_clss_count_def›)+


section ‹Lift Operations to State›

definition polarity_st :: ‹'v twl_st_wl ⇒ 'v literal ⇒ bool option› where
  ‹polarity_st S = polarity (get_trail_wl S)›

definition get_conflict_wl_is_None_heur :: ‹isasat ⇒ bool› where
  ‹get_conflict_wl_is_None_heur S = (λ(b, _). b) (get_conflict_wl_heur S)›

lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None:
  ‹(RETURN o get_conflict_wl_is_None_heur,  RETURN o get_conflict_wl_is_None) ∈
    twl_st_heur →⇩f ⟨Id⟩nres_rel›
  unfolding get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def comp_def
  apply (intro frefI nres_relI) apply refine_rcg
  by (auto simp: twl_st_heur_def get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def
      option_lookup_clause_rel_def Let_def
     split: option.splits prod.splits)

definition count_decided_st :: ‹nat twl_st_wl ⇒ nat› where
  ‹count_decided_st = (λ(M, _). count_decided M)›


lemma count_decided_st_alt_def: ‹count_decided_st S = count_decided (get_trail_wl S)›
  unfolding count_decided_st_def
  by (cases S) auto

definition (in -) is_in_conflict_st :: ‹nat literal ⇒ nat twl_st_wl ⇒ bool› where
  ‹is_in_conflict_st L S ⟷ is_in_conflict L (get_conflict_wl S)›

definition atm_is_in_conflict_st_heur :: ‹nat literal ⇒ isasat ⇒ bool nres› where
  ‹atm_is_in_conflict_st_heur L S = (λ(_, D). do {
     ASSERT (atm_in_conflict_lookup_pre (atm_of L) D); RETURN (¬atm_in_conflict_lookup (atm_of L) D) }) (get_conflict_wl_heur S)›

lemma atm_is_in_conflict_st_heur_alt_def:
  ‹atm_is_in_conflict_st_heur = (λL S. case (get_conflict_wl_heur S) of (_, (_, D)) ⇒ do {ASSERT ((atm_of L) < length D); RETURN (D ! (atm_of L) = None)})›
  unfolding atm_is_in_conflict_st_heur_def by (auto intro!: ext simp: atm_in_conflict_lookup_def atm_in_conflict_lookup_pre_def split:option.splits
    intro!: prod.case_cong)

lemma all_lits_st_alt_def: ‹set_mset (all_lits_st S) =  set_mset (ℒ⇩a⇩l⇩l (all_atms_st S))›
  by (auto simp: all_lits_st_def all_lits_def all_lits_of_mm_union
    in_all_lits_of_mm_ain_atms_of_iff in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n all_atms_st_def
    all_atms_def)

lemma atm_is_in_conflict_st_heur_is_in_conflict_st:
  ‹(uncurry (atm_is_in_conflict_st_heur), uncurry (mop_lit_notin_conflict_wl)) ∈
   [λ(L, S). True]⇩f
   Id ×⇩r twl_st_heur → ⟨Id⟩ nres_rel›
proof -
  have 1: ‹aaa ∈# ℒ⇩a⇩l⇩l A ⟹ atm_of aaa  ∈ atms_of (ℒ⇩a⇩l⇩l A)› for aaa A
    by (auto simp: atms_of_def)
  show ?thesis
  unfolding atm_is_in_conflict_st_heur_def twl_st_heur_def option_lookup_clause_rel_def uncurry_def comp_def
    mop_lit_notin_conflict_wl_def all_lits_st_alt_def Let_def
  apply (intro frefI nres_relI)
  apply refine_rcg
  apply clarsimp
  subgoal
     by (rule atm_in_conflict_lookup_pre)
  subgoal for x y x1 x2
    apply (subst atm_in_conflict_lookup_atm_in_conflict[THEN fref_to_Down_unRET_uncurry_Id, of ‹all_atms_st x2›  ‹atm_of x1› ‹the (get_conflict_wl (snd y))›])
    apply (simp add: ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def)[]
    apply (auto simp add: ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def option_lookup_clause_rel_def
      ac_simps)[]
    apply (simp add: atm_in_conflict_def atm_of_in_atms_of)
    done
  done
qed


abbreviation nat_lit_lit_rel where
  ‹nat_lit_lit_rel ≡ Id :: (nat literal × _) set›


section ‹More theorems›

lemma valid_arena_DECISION_REASON:
  ‹valid_arena arena NU vdom ⟹ DECISION_REASON ∉# dom_m NU›
  using arena_lifting[of arena NU vdom DECISION_REASON]
  by (auto simp: DECISION_REASON_def SHIFTS_def)

definition count_decided_st_heur :: ‹isasat ⇒ _› where
   ‹count_decided_st_heur S = count_decided_pol (get_trail_wl_heur S)›

lemma count_decided_st_count_decided_st:
  ‹(RETURN o count_decided_st_heur, RETURN o count_decided_st) ∈ twl_st_heur →⇩f ⟨nat_rel⟩nres_rel›
  by (intro frefI nres_relI)
     (auto simp: count_decided_st_def twl_st_heur_def count_decided_st_heur_def Let_def
       count_decided_trail_ref[THEN fref_to_Down_unRET_Id])

lemma twl_st_heur_count_decided_st_alt_def:
  fixes S :: isasat
  shows ‹(S, T) ∈ twl_st_heur ⟹ count_decided_st_heur S = count_decided (get_trail_wl T)›
  unfolding count_decided_st_def twl_st_heur_def trail_pol_def
  by (cases S) (auto simp: count_decided_st_heur_def count_decided_pol_def)

lemma twl_st_heur_isa_length_trail_get_trail_wl:
  fixes S :: isasat
  shows ‹(S, T) ∈ twl_st_heur ⟹ isa_length_trail (get_trail_wl_heur S) = length (get_trail_wl T)›
  unfolding isa_length_trail_def twl_st_heur_def trail_pol_def
  by (cases S) (auto dest: ann_lits_split_reasons_map_lit_of)

lemma trail_pol_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ trail_pol 𝒜 ⟹ L ∈ trail_pol ℬ›
  using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: trail_pol_def ann_lits_split_reasons_def)

lemma distinct_atoms_rel_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ distinct_atoms_rel 𝒜 ⟹ L ∈ distinct_atoms_rel ℬ›
  using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def distinct_atoms_rel_def distinct_hash_atoms_rel_def
    atoms_hash_rel_def
  by (auto simp: )

lemma phase_saving_rel_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ phase_saving 𝒜 heur ⟹ phase_saving ℬ heur›
  using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: phase_save_heur_rel_def phase_saving_def)

lemma phase_save_heur_rel_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ phase_save_heur_rel 𝒜 heur ⟹ phase_save_heur_rel ℬ heur›
  using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: phase_save_heur_rel_def phase_saving_def)

lemma heuristic_rel_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ heuristic_rel 𝒜 heur ⟹ heuristic_rel ℬ heur›
  using phase_save_heur_rel_cong[of 𝒜 ℬ ‹(λ(_, _, _, _, a, _). a) (get_restart_heuristics heur)›]
  using phase_saving_rel_cong[of 𝒜 ℬ ‹(λ(_, _, _, _, _, _, _, a, _). a) (get_restart_heuristics heur)›]
  by (auto simp: heuristic_rel_def heuristic_rel_stats_def)

lemma vmtf_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ vmtf 𝒜 M ⟹ L ∈ vmtf ℬ M›
  using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def
  by auto

lemma acids_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ acids 𝒜 M ⟹ L ∈ acids ℬ M›
  using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  unfolding acids_def vmtf_ℒ⇩a⇩l⇩l_def
  apply (auto simp: distinct_subseteq_iff)
  by (metis distinct_subseteq_iff)

lemma isa_vmtf_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ bump_heur 𝒜 M ⟹ L ∈ bump_heur ℬ M›
  using vmtf_cong[of 𝒜 ℬ]  distinct_atoms_rel_cong[of 𝒜 ℬ]
    acids_cong
  apply (subst (asm) bump_heur_def)
  apply (subst bump_heur_def)
  by blast

lemma isa_vmtf_cong':
  ‹set_mset 𝒜 = set_mset ℬ ⟹ bump_heur 𝒜 = bump_heur ℬ›
  using isa_vmtf_cong[of 𝒜 ℬ] isa_vmtf_cong[of ℬ 𝒜]
  by blast

lemma option_lookup_clause_rel_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ option_lookup_clause_rel 𝒜 ⟹ L ∈ option_lookup_clause_rel ℬ›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  unfolding option_lookup_clause_rel_def lookup_clause_rel_def
  by (cases L) auto


lemma D⇩0_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ D⇩0 𝒜 = D⇩0 ℬ›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by auto

lemma phase_saving_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ phase_saving 𝒜 = phase_saving ℬ›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: phase_saving_def)

lemma cach_refinement_empty_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ cach_refinement_empty 𝒜 = cach_refinement_empty ℬ›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (force simp: cach_refinement_empty_def cach_refinement_alt_def
    distinct_subseteq_iff[symmetric] intro!: ext)

lemma vdom_m_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ vdom_m 𝒜 x y = vdom_m ℬ x y›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: vdom_m_def intro!: ext)


lemma isasat_input_bounded_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ isasat_input_bounded 𝒜 = isasat_input_bounded ℬ›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: intro!: ext)

lemma isasat_input_nempty_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ isasat_input_nempty 𝒜 = isasat_input_nempty ℬ›
  using  ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
  by (auto simp: intro!: ext)


section ‹Shared Code Equations›

definition clause_not_marked_to_delete where
  ‹clause_not_marked_to_delete S C ⟷ C ∈# dom_m (get_clauses_wl S)›

definition clause_not_marked_to_delete_pre where
  ‹clause_not_marked_to_delete_pre =
    (λ(S, C). C ∈ vdom_m (all_atms_st S) (get_watched_wl S) (get_clauses_wl S))›

definition clause_not_marked_to_delete_heur_pre where
  ‹clause_not_marked_to_delete_heur_pre =
     (λ(S, C). arena_is_valid_clause_vdom (get_clauses_wl_heur S) C)›

definition clause_not_marked_to_delete_heur :: ‹_ ⇒ nat ⇒ bool›
where
  ‹clause_not_marked_to_delete_heur S C ⟷
    arena_status (get_clauses_wl_heur S) C ≠ DELETED›

lemma clause_not_marked_to_delete_rel:
  ‹(uncurry (RETURN oo clause_not_marked_to_delete_heur),
    uncurry (RETURN oo clause_not_marked_to_delete)) ∈
    [clause_not_marked_to_delete_pre]⇩f
     twl_st_heur ×⇩f nat_rel → ⟨bool_rel⟩nres_rel›
  by (intro frefI nres_relI)
    (use arena_dom_status_iff in_dom_in_vdom in
      ‹auto 5 5 simp: clause_not_marked_to_delete_def twl_st_heur_def Let_def
        clause_not_marked_to_delete_heur_def arena_dom_status_iff
        clause_not_marked_to_delete_pre_def ac_simps›)


definition (in -) access_lit_in_clauses_heur_pre where
  ‹access_lit_in_clauses_heur_pre =
      (λ((S, i), j).
           arena_lit_pre (get_clauses_wl_heur S) (i+j))›

definition (in -) access_lit_in_clauses_heur where
  ‹access_lit_in_clauses_heur S i j = arena_lit (get_clauses_wl_heur S) (i + j)›

definition (in -) mop_access_lit_in_clauses_heur where
  ‹mop_access_lit_in_clauses_heur S i j = mop_arena_lit2 (get_clauses_wl_heur S) i j›

lemma access_lit_in_clauses_heur_fast_pre:
  ‹arena_lit_pre (get_clauses_wl_heur a) (ba + b) ⟹
    isasat_fast a ⟹ ba + b ≤ snat64_max›
  by (auto simp: arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
      dest!: arena_lifting(10)
      dest!: isasat_fast_length_leD)[]

(*TODO Move*)
lemma ℒ⇩a⇩l⇩l_add_mset:
  ‹set_mset (ℒ⇩a⇩l⇩l (add_mset L C)) = insert (Pos L) (insert (Neg L) (set_mset (ℒ⇩a⇩l⇩l C)))›
  by (auto simp: ℒ⇩a⇩l⇩l_def)

(*END Move*)


lemma correct_watching_dom_watched:
  assumes ‹correct_watching S› and ‹⋀C. C ∈# ran_mf (get_clauses_wl S) ⟹ C ≠ []›
  shows ‹set_mset (dom_m (get_clauses_wl S)) ⊆
     ⋃(((`) fst) ` set ` (get_watched_wl S) ` set_mset (all_lits_st S))›
    (is ‹?A ⊆ ?B›)
proof
  fix C
  assume ‹C ∈ ?A›
  then obtain D where
    D: ‹D ∈# ran_mf (get_clauses_wl S)› and
    D': ‹D = get_clauses_wl S ∝ C› and
    C: ‹C ∈# dom_m (get_clauses_wl S)›
    by auto
  have ‹(hd D) ∈# all_lits_st S›
    using D D' assms(2)[of D]
    by (cases S; cases D)
      (auto simp: all_lits_def all_lits_st_def all_lits_def
          all_lits_of_mm_add_mset all_lits_of_m_add_mset
        dest!: multi_member_split)
  then show ‹C ∈ ?B›
    using assms(1) assms(2)[of D] D D'
      multi_member_split[OF C]
    by (cases S; cases ‹get_clauses_wl S ∝ C›;
         cases ‹hd (get_clauses_wl S ∝ C)›)
     (auto dest!: multi_member_split simp: ℒ⇩a⇩l⇩l_add_mset correct_watching.simps clause_to_update_def
	  eq_commute[of ‹_ # _›] atm_of_eq_atm_of
      split: if_splits
	dest!: arg_cong[of ‹filter_mset _ _› ‹add_mset _ _› set_mset] eq_insertD)
qed


lemma arena_lit_pre_le_snat64_max:
 ‹length ba ≤ snat64_max ⟹
       arena_lit_pre ba a ⟹ a ≤ snat64_max›
  using arena_lifting(10)[of ba _ _]
  by (fastforce simp: arena_lifting arena_is_valid_clause_idx_def arena_lit_pre_def
      arena_is_valid_clause_idx_and_access_def)

definition rewatch_heur_vdom where
  ‹rewatch_heur_vdom vdom = rewatch_heur (get_tvdom_aivdom vdom)›

definition rewatch_heur_st
 :: ‹isasat ⇒ isasat nres›
where
‹rewatch_heur_st = (λS. do {
  ASSERT(length (get_tvdom_aivdom (get_aivdom S)) ≤ length (get_clauses_wl_heur S));
  W ← rewatch_heur (get_tvdom_aivdom (get_aivdom S)) (get_clauses_wl_heur S) (get_watched_wl_heur S);
  RETURN (set_watched_wl_heur W S)
  })›

definition rewatch_heur_st_fast where
  ‹rewatch_heur_st_fast = rewatch_heur_st›

definition rewatch_heur_st_fast_pre where
  ‹rewatch_heur_st_fast_pre S =
     ((∀x ∈ set (get_tvdom S). x ≤ snat64_max) ∧ length (get_clauses_wl_heur S) ≤ snat64_max)›

definition rewatch_st :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
  ‹rewatch_st S = do{
     (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ← RETURN S;
     W ← rewatch N W;
     RETURN ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))
  }›

definition rewatch_heur_and_reorder_st
 :: ‹isasat ⇒ isasat nres›
where
‹rewatch_heur_and_reorder_st = (λS. do {
  ASSERT(length (get_tvdom_aivdom (get_aivdom S)) ≤ length (get_clauses_wl_heur S));
  W ← rewatch_heur_and_reorder (get_tvdom_aivdom (get_aivdom S)) (get_clauses_wl_heur S) (get_watched_wl_heur S);
  RETURN (set_watched_wl_heur W S)
  })›


fun remove_watched_wl :: ‹'v twl_st_wl ⇒ _› where
  ‹remove_watched_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, _) = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q)›

lemma rewatch_st_correctness:
  assumes ‹get_watched_wl S = (λ_. [])› and
    ‹⋀x. x ∈# dom_m (get_clauses_wl S) ⟹
      distinct ((get_clauses_wl S) ∝ x) ∧ 2 ≤ length ((get_clauses_wl S) ∝ x)›
  shows ‹rewatch_st S ≤ SPEC (λT. remove_watched_wl S = remove_watched_wl T ∧
     correct_watching_init T)›
  apply (rule SPEC_rule_conjI)
  subgoal
    using rewatch_correctness[OF assms]
    unfolding rewatch_st_def
    apply (cases S, case_tac ‹rewatch (get_clauses_wl S) (get_watched_wl S)›)
    by (auto simp: RES_RETURN_RES)
  subgoal
    using rewatch_correctness[OF assms]
    unfolding rewatch_st_def
    apply (cases S, case_tac ‹rewatch (get_clauses_wl S) (get_watched_wl S)›)
    by (force simp: RES_RETURN_RES)+
  done


section ‹Fast to slow conversion›

text ‹Setup to convert a list from \<^typ>‹64 word› to \<^typ>‹nat›.›
definition convert_wlists_to_nat_conv :: ‹'a list list ⇒ 'a list list› where
  ‹convert_wlists_to_nat_conv = id›

abbreviation twl_st_heur''
   :: ‹nat multiset ⇒ nat ⇒ clss_size ⇒ (isasat × nat twl_st_wl) set›
where
‹twl_st_heur'' 𝒟 r lcount ≡ {(S, T). (S, T) ∈ twl_st_heur' 𝒟 ∧
           length (get_clauses_wl_heur S) = r ∧ get_learned_count S = lcount}›

abbreviation twl_st_heur_up''
   :: ‹nat multiset ⇒ nat ⇒ nat ⇒ nat literal ⇒ clss_size ⇒ (isasat × nat twl_st_wl) set›
where
  ‹twl_st_heur_up'' 𝒟 r s L lcount ≡ {(S, T). (S, T) ∈ twl_st_heur'' 𝒟 r lcount ∧
     length (watched_by T L) = s ∧ s ≤ r}›

lemma length_watched_le:
  assumes
    prop_inv: ‹correct_watching x1› and
    xb_x'a: ‹(x1a, x1) ∈ twl_st_heur'' 𝒟1 r lcount› and
    x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
  shows ‹length (watched_by x1 x2) ≤ r - MIN_HEADER_SIZE›
proof -
  have dist: ‹distinct_watched (watched_by x1 x2)›
    using prop_inv x2 unfolding all_atms_def all_lits_def
    by (cases x1; auto simp: correct_watching.simps ac_simps all_lits_st_alt_def[symmetric])
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using xb_x'a
    by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
  have dist_vdom: ‹distinct (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_def twl_st_heur'_def aivdom_inv_dec_alt_def Let_def)
  have x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
    using x2 xb_x'a unfolding all_atms_def
    by auto

  have
      valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
    using xb_x'a unfolding all_atms_def all_lits_def
    by (cases x1)
     (auto simp: twl_st_heur'_def twl_st_heur_def Let_def)

  have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_def twl_st_heur'_def ac_simps Let_def)

  then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
    using x2 unfolding vdom_m_def
    by (cases x1)
      (force simp: twl_st_heur'_def twl_st_heur_def
        dest!: multi_member_split)
  have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
    by (rule distinct_subseteq_iff[THEN iffD1])
      (use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
         ‹simp_all flip: distinct_mset_mset_distinct›)
  have vdom_incl: ‹set (get_vdom x1a) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur x1a)}›
    using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto

  have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - MIN_HEADER_SIZE›
    by (subst distinct_card[OF dist_vdom, symmetric])
      (use card_mono[OF _ vdom_incl] in auto)
  then show ?thesis
    using size_mset_mono[OF watched_incl] xb_x'a
    by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›])
qed

lemma length_watched_le2:
  assumes
    prop_inv: ‹correct_watching_except i j L x1› and
    xb_x'a: ‹(x1a, x1) ∈ twl_st_heur'' 𝒟1 r lcount› and
    x2: ‹x2 ∈# all_lits_st x1› and diff: ‹L ≠ x2›
  shows ‹length (watched_by x1 x2) ≤ r - MIN_HEADER_SIZE›
proof -
  from prop_inv diff have dist: ‹distinct_watched (watched_by x1 x2)›
    using x2 unfolding all_atms_def all_lits_def
    by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching_except.simps ac_simps)
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using xb_x'a
    by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
  have dist_vdom: ‹distinct (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_def twl_st_heur'_def aivdom_inv_dec_alt_def)

  have
      valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
    using xb_x'a unfolding all_atms_def all_lits_def
    by (cases x1)
     (auto simp: twl_st_heur'_def twl_st_heur_def)

  have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_def twl_st_heur'_def ac_simps simp flip: all_atms_def)
  then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
    using x2 unfolding vdom_m_def all_lits_st_alt_def[symmetric]
    by (cases x1)
      (force simp: twl_st_heur'_def twl_st_heur_def ac_simps simp flip: all_atms_def all_lits_alt_def2
        dest!: multi_member_split)
  have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
    by (rule distinct_subseteq_iff[THEN iffD1])
      (use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
         ‹simp_all flip: distinct_mset_mset_distinct›)
  have vdom_incl: ‹set (get_vdom x1a) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur x1a)}›
    using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto

  have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - MIN_HEADER_SIZE›
    by (subst distinct_card[OF dist_vdom, symmetric])
      (use card_mono[OF _ vdom_incl] in auto)
  then show ?thesis
    using size_mset_mono[OF watched_incl] xb_x'a
    by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›])
qed

lemma atm_of_all_lits_of_m: ‹atm_of `# (all_lits_of_m C) = atm_of `# C + atm_of `# C›
   ‹atm_of ` set_mset (all_lits_of_m C) = atm_of `set_mset C ›
  by (induction C; auto simp: all_lits_of_m_add_mset)+

find_theorems ℒ⇩a⇩l⇩l all_lits_st
(* TODO Move in this buffer *)
lemma mop_watched_by_app_heur_mop_watched_by_at:
   ‹(uncurry2 mop_watched_by_app_heur, uncurry2 mop_watched_by_at) ∈
    twl_st_heur ×⇩f nat_lit_lit_rel ×⇩f nat_rel →⇩f ⟨Id⟩nres_rel›
  unfolding mop_watched_by_app_heur_def mop_watched_by_at_def uncurry_def all_lits_def[symmetric]
    all_lits_alt_def[symmetric]
  by (intro frefI nres_relI, refine_rcg)
    (auto simp: twl_st_heur_def map_fun_rel_def all_lits_st_alt_def[symmetric])

lemma mop_watched_by_app_heur_mop_watched_by_at'':
   ‹(uncurry2 mop_watched_by_app_heur, uncurry2 mop_watched_by_at) ∈
    twl_st_heur_up'' 𝒟 r s K lcount ×⇩f nat_lit_lit_rel ×⇩f nat_rel →⇩f ⟨Id⟩nres_rel›
  by (rule fref_mono[THEN set_mp, OF _ _ _ mop_watched_by_app_heur_mop_watched_by_at])
    (auto simp: ℒ⇩a⇩l⇩l_all_atms_all_lits twl_st_heur'_def map_fun_rel_def)

definition polarity_st_pre :: ‹nat twl_st_wl × nat literal ⇒ bool› where
  ‹polarity_st_pre ≡ λ(S, L). L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›

definition mop_polarity_st_heur :: ‹isasat ⇒ nat literal ⇒ bool option nres› where
‹mop_polarity_st_heur S L = do {
    mop_polarity_pol (get_trail_wl_heur S) L
  }›

lemma mop_polarity_st_heur_mop_polarity_wl:
   ‹(uncurry mop_polarity_st_heur, uncurry mop_polarity_wl) ∈
   [λ_. True]⇩f twl_st_heur ×⇩r Id → ⟨⟨bool_rel⟩option_rel⟩nres_rel›
  unfolding mop_polarity_wl_def mop_polarity_st_heur_def uncurry_def mop_polarity_pol_def
  apply (intro frefI nres_relI)
  apply (refine_rcg polarity_pol_polarity[of ‹all_atms_st _›, THEN fref_to_Down_unRET_uncurry])
  apply (auto simp: twl_st_heur_def ℒ⇩a⇩l⇩l_all_atms_all_lits ac_simps all_lits_st_alt_def[symmetric]
    intro!: polarity_pol_pre simp flip: all_atms_def)
  done

lemma mop_polarity_st_heur_mop_polarity_wl'':
   ‹(uncurry mop_polarity_st_heur, uncurry mop_polarity_wl) ∈
   [λ_. True]⇩f twl_st_heur_up'' 𝒟 r s K lcount ×⇩r Id → ⟨⟨bool_rel⟩option_rel⟩nres_rel›
  by (rule fref_mono[THEN set_mp, OF _ _ _ mop_polarity_st_heur_mop_polarity_wl])
    (auto simp: ℒ⇩a⇩l⇩l_all_atms_all_lits twl_st_heur'_def map_fun_rel_def)

(* TODO Kill lhs*)
lemma [simp,iff]: ‹literals_are_ℒ⇩i⇩n (all_atms_st S) S ⟷ blits_in_ℒ⇩i⇩n S›
  unfolding literals_are_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_def ℒ⇩a⇩l⇩l_all_atms_all_lits all_lits_st_alt_def[symmetric]
  by auto


definition length_avdom :: ‹isasat ⇒ nat› where
  ‹length_avdom S = length (get_avdom S)›

definition length_ivdom :: ‹isasat ⇒ nat› where
  ‹length_ivdom S = length (get_ivdom S)›

definition length_tvdom :: ‹isasat ⇒ nat› where
  ‹length_tvdom S = length (get_tvdom S)›

definition clause_is_learned_heur :: ‹isasat ⇒ nat ⇒ bool›
where
  ‹clause_is_learned_heur S C ⟷ arena_status (get_clauses_wl_heur S) C = LEARNED›

definition get_the_propagation_reason_heur
 :: ‹isasat ⇒ nat literal ⇒ nat option nres›
where
  ‹get_the_propagation_reason_heur S = get_the_propagation_reason_pol (get_trail_wl_heur S)›

(* TODO deduplicate arena_lbd = get_clause_LBD *)
definition clause_lbd_heur :: ‹isasat ⇒ nat ⇒ nat›
where
  ‹clause_lbd_heur S C = arena_lbd (get_clauses_wl_heur S) C›

definition (in -) access_length_heur where
  ‹access_length_heur S i = arena_length (get_clauses_wl_heur S) i›

definition marked_as_used_st where
  ‹marked_as_used_st T C =
    marked_as_used (get_clauses_wl_heur T) C›

definition access_avdom_at :: ‹isasat ⇒ nat ⇒ nat› where
  ‹access_avdom_at S i = get_avdom S ! i›

definition access_ivdom_at :: ‹isasat ⇒ nat ⇒ nat› where
  ‹access_ivdom_at S i = get_ivdom S ! i›

definition access_tvdom_at :: ‹isasat ⇒ nat ⇒ nat› where
  ‹access_tvdom_at S i = get_tvdom S ! i›

definition access_avdom_at_pre where
  ‹access_avdom_at_pre S i ⟷ i < length (get_avdom S)›

definition access_ivdom_at_pre where
  ‹access_ivdom_at_pre S i ⟷ i < length (get_ivdom S)›

definition access_tvdom_at_pre where
  ‹access_tvdom_at_pre S i ⟷ i < length (get_tvdom S)›

(*TODO check which of theses variants are used!*)
definition mark_garbage_heur :: ‹nat ⇒ nat ⇒ isasat ⇒ isasat› where
  ‹mark_garbage_heur C i = (λS.
    let N' = extra_information_mark_to_delete (get_clauses_wl_heur S) C in
    let lcount = clss_size_decr_lcount (get_learned_count S) in
    let vdom = remove_inactive_aivdom i (get_aivdom S) in
    set_aivdom_wl_heur vdom (set_clauses_wl_heur N' (set_learned_count_wl_heur lcount S)))›

definition mark_garbage_heur2 :: ‹nat ⇒ isasat ⇒ isasat nres› where
  ‹mark_garbage_heur2 C = (λS. do{
    ASSERT (mark_garbage_pre (get_clauses_wl_heur S, C));
    let N' = get_clauses_wl_heur S;
    let st = arena_status N' C = IRRED;
    let N' = extra_information_mark_to_delete N' C;
    let lcount = get_learned_count S;
    ASSERT(¬st ⟶ clss_size_lcount lcount ≥ 1);
    let lcount = (if st then lcount else clss_size_decr_lcount lcount);
    RETURN (set_clauses_wl_heur N' (set_learned_count_wl_heur lcount S))})›

definition mark_garbage_heur3 :: ‹nat ⇒ nat ⇒ isasat ⇒ isasat› where
  ‹mark_garbage_heur3 C i = (λS.
    let N' = get_clauses_wl_heur S in
    let N' = extra_information_mark_to_delete N' C in
    let lcount = get_learned_count S in
    let vdom = get_aivdom S in
    let vdom = remove_inactive_aivdom_tvdom i vdom in
    let lcount = clss_size_decr_lcount lcount in
    let S = set_clauses_wl_heur N' S in
    let S = set_learned_count_wl_heur lcount S in
    let S = set_aivdom_wl_heur vdom S in
    S)›

definition mark_garbage_heur4 :: ‹nat ⇒ isasat ⇒ isasat nres› where
  ‹mark_garbage_heur4 C S = (do{
    let N' = get_clauses_wl_heur S;
    let st = arena_status N' C = IRRED;
    let N' = extra_information_mark_to_delete (N') C;
    let lcount = get_learned_count S;
    ASSERT(¬st ⟶ clss_size_lcount lcount ≥ 1);
    let lcount = (if st then lcount else clss_size_incr_lcountUEk (clss_size_decr_lcount lcount));
    let stats = get_stats_heur S;
    let stats = (if st then decr_irred_clss stats else stats);
    let S = set_clauses_wl_heur N' S;
    let S = set_learned_count_wl_heur lcount S;
    let S = set_stats_wl_heur stats S;
    RETURN S
   })›

definition delete_index_vdom_heur :: ‹nat ⇒ isasat ⇒ isasat› where
  ‹delete_index_vdom_heur = (λi S.
    let vdom = get_aivdom S in
    let vdom = remove_inactive_aivdom_tvdom i vdom in
    let S = set_aivdom_wl_heur vdom S in
    S)›

lemma arena_act_pre_mark_used:
  ‹arena_act_pre arena C ⟹
  arena_act_pre (mark_unused arena C) C›
  unfolding arena_act_pre_def arena_is_valid_clause_idx_def
  apply clarify
  apply (rule_tac x=N in exI)
  apply (rule_tac x=vdom in exI)
  by (auto simp: arena_act_pre_def
    simp: valid_arena_mark_unused)

definition mop_mark_garbage_heur :: ‹nat ⇒ nat ⇒ isasat ⇒ isasat nres› where
  ‹mop_mark_garbage_heur C i = (λS. do {
    ASSERT(mark_garbage_pre (get_clauses_wl_heur S, C) ∧ clss_size_lcount (get_learned_count S) ≥ 1 ∧ i < length (get_avdom S));
    RETURN (mark_garbage_heur C i S)
  })›

definition mop_mark_garbage_heur3 :: ‹nat ⇒ nat ⇒ isasat ⇒ isasat nres› where
  ‹mop_mark_garbage_heur3 C i = (λS. do {
    ASSERT(mark_garbage_pre (get_clauses_wl_heur S, C) ∧ clss_size_lcount (get_learned_count S) ≥ 1  ∧ i < length (get_tvdom S));
    RETURN (mark_garbage_heur3 C i S)
  })›

definition mark_unused_st_heur :: ‹nat ⇒ isasat ⇒ isasat› where
  ‹mark_unused_st_heur C = (λS.
    let N' = mark_unused (get_clauses_wl_heur S) C in
    let S = set_clauses_wl_heur N' S in
    S)›


definition mop_mark_unused_st_heur :: ‹nat ⇒ isasat ⇒ isasat nres› where
  ‹mop_mark_unused_st_heur C T = do {
     ASSERT(arena_act_pre (get_clauses_wl_heur T) C);
     RETURN (mark_unused_st_heur C T)
  }›

lemma mark_unused_st_heur_simp[simp]:
  ‹get_avdom (mark_unused_st_heur C T) = get_avdom T›
  ‹get_vdom (mark_unused_st_heur C T) = get_vdom T›
  ‹get_ivdom (mark_unused_st_heur C T) = get_ivdom T›
  ‹get_tvdom (mark_unused_st_heur C T) = get_tvdom T›
  by (cases T; auto simp: mark_unused_st_heur_def; fail)+

fun get_conflict_count_since_last_restart_heur :: ‹isasat ⇒ 64 word› where
  ‹get_conflict_count_since_last_restart_heur S = get_conflict_count_since_last_restart (get_heur S)›

definition get_global_conflict_count where
  ‹get_global_conflict_count S = stats_conflicts (get_stats_heur S)›

text ‹
  I also played with \<^term>‹ema_reinit fast_ema› and \<^term>‹ema_reinit slow_ema›. Currently removed,
  to test the performance, I remove it.
›
definition incr_restart_stat :: ‹isasat ⇒ isasat nres› where
  ‹incr_restart_stat = (λS. do{
     let heur = get_heur S;
     let heur = unset_fully_propagated_heur (heuristic_reluctant_untrigger (restart_info_restart_done_heur heur));
     let S = set_heur_wl_heur heur S;
     let stats = get_stats_heur S;
     let S = set_stats_wl_heur (incr_restart (stats)) S;
     RETURN S
  })›

definition incr_reduction_stat :: ‹isasat ⇒ isasat nres› where
  ‹incr_reduction_stat = (λS. do{
     let stats = get_stats_heur S;
     let stats = incr_reduction stats;
     let S = set_stats_wl_heur stats S;
     RETURN S
  })›

definition incr_wasted_st :: ‹64 word ⇒ isasat ⇒ isasat› where
  ‹incr_wasted_st = (λwaste S. do{
  let heur = get_heur S in
  let heur = incr_wasted waste heur in
  let S = set_heur_wl_heur heur S in S
  })›


definition wasted_bytes_st :: ‹isasat ⇒ 64 word› where
  ‹wasted_bytes_st S = wasted_of (get_heur S)›


definition opts_restart_st :: ‹isasat ⇒ bool› where
  ‹opts_restart_st S = opts_restart (get_opts S)›

definition opts_reduction_st :: ‹isasat ⇒ bool› where
  ‹opts_reduction_st S = opts_reduce (get_opts S)›

definition opts_unbounded_mode_st :: ‹isasat ⇒ bool› where
  ‹opts_unbounded_mode_st S = opts_unbounded_mode (get_opts S)›

definition opts_minimum_between_restart_st :: ‹isasat ⇒ 64 word› where
  ‹opts_minimum_between_restart_st S = opts_minimum_between_restart (get_opts S)›

definition opts_restart_coeff1_st :: ‹isasat ⇒ 64 word› where
  ‹opts_restart_coeff1_st S = opts_restart_coeff1 (get_opts S)›

definition opts_restart_coeff2_st :: ‹isasat ⇒ nat› where
  ‹opts_restart_coeff2_st S = opts_restart_coeff2 (get_opts S)›

definition isasat_length_trail_st :: ‹isasat ⇒ nat› where
  ‹isasat_length_trail_st S = isa_length_trail (get_trail_wl_heur S)›

definition mop_isasat_length_trail_st :: ‹isasat ⇒ nat nres› where
  ‹mop_isasat_length_trail_st S = do {
    ASSERT(isa_length_trail_pre (get_trail_wl_heur S));
    RETURN (isa_length_trail (get_trail_wl_heur S))
  }›

definition get_pos_of_level_in_trail_imp_st :: ‹isasat ⇒ nat ⇒ nat nres› where
‹get_pos_of_level_in_trail_imp_st S = get_pos_of_level_in_trail_imp (get_trail_wl_heur S)›

definition mop_clause_not_marked_to_delete_heur :: ‹_ ⇒ nat ⇒ bool nres›
where
  ‹mop_clause_not_marked_to_delete_heur S C = do {
    ASSERT(clause_not_marked_to_delete_heur_pre (S, C));
    RETURN (clause_not_marked_to_delete_heur S C)
  }›

definition mop_arena_lbd_st where
  ‹mop_arena_lbd_st S =
    mop_arena_lbd (get_clauses_wl_heur S)›

definition mop_arena_status_st :: ‹isasat ⇒ _› where
  ‹mop_arena_status_st S =
    mop_arena_status (get_clauses_wl_heur S)›

definition mop_marked_as_used_st :: ‹isasat ⇒ nat ⇒ nat nres› where
  ‹mop_marked_as_used_st S =
    mop_marked_as_used (get_clauses_wl_heur S)›

definition mop_arena_length_st :: ‹isasat ⇒ nat ⇒ nat nres› where
  ‹mop_arena_length_st S =
    mop_arena_length (get_clauses_wl_heur S)›

definition full_arena_length_st :: ‹isasat ⇒ nat› where
  ‹full_arena_length_st S = length (get_clauses_wl_heur S)›

definition (in -) access_lit_in_clauses where
  ‹access_lit_in_clauses S i j = (get_clauses_wl S) ∝ i ! j›

lemma twl_st_heur_get_clauses_access_lit[simp]:
  ‹(S, T) ∈ twl_st_heur ⟹ C ∈# dom_m (get_clauses_wl T) ⟹
    i < length (get_clauses_wl T ∝ C) ⟹
    get_clauses_wl T ∝ C ! i = access_lit_in_clauses_heur S C i›
    for S T C i
    by (cases S; cases T)
      (auto simp: arena_lifting twl_st_heur_def access_lit_in_clauses_heur_def)


abbreviation length_clauses_heur where
  ‹length_clauses_heur ≡ full_arena_length_st›

lemmas length_clauses_heur_def = full_arena_length_st_def

text ‹In an attempt to avoid using @{thm ac_simps} everywhere.›
lemma all_lits_simps[simp]:
  ‹all_lits N ((NE + UE) + (NS + US)) = all_lits N (NE + UE + NS + US)›
  ‹all_atms N ((NE + UE) + (NS + US)) = all_atms N (NE + UE + NS + US)›
  by (auto simp: ac_simps)

lemma learned_clss_count_twl_st_heur: ‹(T, Ta) ∈ twl_st_heur ⟹
                      learned_clss_count T=
                      size (get_learned_clss_wl Ta) +
                      size (get_unit_learned_clss_wl Ta) +
                     size (get_subsumed_learned_clauses_wl Ta) +
                     size (get_learned_clauses0_wl Ta)›
  by (auto simp: twl_st_heur_def clss_size_def learned_clss_count_def clss_size_corr_def
    clss_size_lcount_def clss_size_lcountUE_def clss_size_lcountUS_def clss_size_lcountUEk_def
    get_learned_clss_wl_def clss_size_lcountU0_def get_unit_learned_clss_wl_alt_def)

lemma clss_size_allcount_alt_def:
  ‹clss_size_allcount S = clss_size_lcountUS S + clss_size_lcountU0 S + clss_size_lcountUE S + 
    clss_size_lcountUEk S + clss_size_lcount S›
  by (cases S) (auto simp: clss_size_allcount_def clss_size_lcountUS_def
    clss_size_lcount_def clss_size_lcountUEk_def clss_size_lcountUE_def clss_size_lcountU0_def)

definition isasat_trail_nth_st :: ‹isasat ⇒ nat ⇒ nat literal nres› where
‹isasat_trail_nth_st S i = isa_trail_nth (get_trail_wl_heur S) i›

definition get_the_propagation_reason_pol_st :: ‹isasat⇒ nat literal ⇒ nat option nres› where
‹get_the_propagation_reason_pol_st S i = get_the_propagation_reason_pol (get_trail_wl_heur S) i›

definition empty_US_heur :: ‹isasat ⇒ isasat› where
  ‹empty_US_heur S =
  (let lcount = get_learned_count S in
  let lcount = clss_size_resetUS0 lcount in
  let S = set_learned_count_wl_heur lcount S in S
  )›

lemma get_clauses_wl_heur_empty_US[simp]:
    ‹get_clauses_wl_heur (empty_US_heur xc) = get_clauses_wl_heur xc› and
  get_vdom_empty_US[simp]:
    ‹get_vdom (empty_US_heur xc) = get_vdom xc›
    ‹get_avdom (empty_US_heur xc) = get_avdom xc›
    ‹get_ivdom (empty_US_heur xc) = get_ivdom xc›
    ‹get_tvdom (empty_US_heur xc) = get_tvdom xc›
  by (cases xc; auto simp: empty_US_heur_def; fail)+

definition empty_Q_wl  :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
‹empty_Q_wl = (λ(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, _, W). (M', N, D, NE, UE, NEk, UEk, NS, {#}, N0, {#}, {#}, W))›

definition empty_Q_wl2  :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
‹empty_Q_wl2 = (λ(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, _, W). (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, W))›

definition empty_US_heur_wl  :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
‹empty_US_heur_wl = (λ(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). (M', N, D, NE, UE, NEk, UEk, NS, {#}, N0, {#}, Q, W))›

lemma restart_info_of_stats_simp [simp]: ‹restart_info_of_stats (incr_wasted_stats C heur) = restart_info_of_stats heur›
  by (cases heur; auto; fail)+

lemma incr_wasted_st_twl_st[simp]:
  ‹get_aivdom (incr_wasted_st b T) = get_aivdom T›
  ‹get_avdom (incr_wasted_st w T) = get_avdom T›
  ‹get_vdom (incr_wasted_st w T) = get_vdom T›
  ‹get_ivdom (incr_wasted_st w T) = get_ivdom T›
  ‹get_tvdom (incr_wasted_st w T) = get_tvdom T›
  ‹get_trail_wl_heur (incr_wasted_st w T) = get_trail_wl_heur T›
  ‹get_clauses_wl_heur (incr_wasted_st C T) = get_clauses_wl_heur T›
  ‹get_conflict_wl_heur (incr_wasted_st C T) = get_conflict_wl_heur T›
  ‹get_learned_count (incr_wasted_st C T) = get_learned_count T›
  ‹get_conflict_count_heur (incr_wasted_st C T) = get_conflict_count_heur T›
  ‹literals_to_update_wl_heur (incr_wasted_st C T) = literals_to_update_wl_heur T›
  ‹get_watched_wl_heur (incr_wasted_st C T) = get_watched_wl_heur T›
  ‹get_vmtf_heur (incr_wasted_st C T) = get_vmtf_heur T›
  ‹get_count_max_lvls_heur (incr_wasted_st C T) = get_count_max_lvls_heur T›
  ‹get_conflict_cach (incr_wasted_st C T) = get_conflict_cach T›
  ‹get_lbd (incr_wasted_st C T) = get_lbd T›
  ‹get_outlearned_heur (incr_wasted_st C T) = get_outlearned_heur T›
  ‹get_aivdom (incr_wasted_st C T) = get_aivdom T›
  ‹get_learned_count (incr_wasted_st C T) = get_learned_count T›
  ‹get_opts (incr_wasted_st C T) = get_opts T›
  ‹get_old_arena (incr_wasted_st C T) = get_old_arena T›
  by (cases T; auto simp: incr_wasted_st_def incr_wasted_def restart_info_of_def; fail)+

definition heuristic_reluctant_triggered2_st :: ‹isasat ⇒ bool› where
  ‹heuristic_reluctant_triggered2_st S = heuristic_reluctant_triggered2 (get_heur S)›

definition heuristic_reluctant_untrigger_st :: ‹isasat ⇒ isasat› where
  ‹heuristic_reluctant_untrigger_st S =
  (let heur = get_heur S;
    heur = heuristic_reluctant_untrigger heur;
    S = set_heur_wl_heur heur S in
  S)›

lemma twl_st_heur''D_twl_st_heurD:
  assumes H: ‹(⋀𝒟 r. f ∈ twl_st_heur'' 𝒟 r lcount →⇩f ⟨twl_st_heur'' 𝒟 r lcount⟩ nres_rel)›
  shows ‹f ∈ {(S, T). (S, T) ∈ twl_st_heur ∧ get_learned_count S = lcount} →⇩f
        ⟨{(S, T). (S, T) ∈ twl_st_heur ∧ get_learned_count S = lcount}⟩ nres_rel›  (is ‹_ ∈ ?A B›)
proof -
  obtain f1 f2 where f: ‹f = (f1, f2)›
    by (cases f) auto
  show ?thesis
    unfolding f
    apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
    apply (intro conjI impI allI)
    subgoal for x y
      using assms[of ‹dom_m (get_clauses_wl y)›  ‹length (get_clauses_wl_heur x)›,
        unfolded twl_st_heur'_def nres_rel_def in_pair_collect_simp f,
        rule_format] unfolding f
      apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
      apply (drule spec[of _ x])
      apply (drule spec[of _ y])
      apply simp
      apply (rule "weaken_⇓'"[of _ ‹twl_st_heur'' (dom_m (get_clauses_wl y))
        (length (get_clauses_wl_heur x)) lcount›])
      apply (fastforce simp: twl_st_heur'_def)+
      done
    done
qed


lemma twl_st_heur'''D_twl_st_heurD:
  assumes H: ‹(⋀r. f ∈ twl_st_heur''' r →⇩f ⟨twl_st_heur''' r⟩ nres_rel)›
  shows ‹f ∈ twl_st_heur →⇩f ⟨twl_st_heur⟩ nres_rel›  (is ‹_ ∈ ?A B›)
proof -
  obtain f1 f2 where f: ‹f = (f1, f2)›
    by (cases f) auto
  show ?thesis
    unfolding f
    apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
    apply (intro conjI impI allI)
    subgoal for x y
      using assms[of ‹length (get_clauses_wl_heur x)›,
        unfolded twl_st_heur'_def nres_rel_def in_pair_collect_simp f,
        rule_format] unfolding f
      apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
      apply (drule spec[of _ x])
      apply (drule spec[of _ y])
      apply simp
      apply (rule "weaken_⇓'"[of _ ‹twl_st_heur''' (length (get_clauses_wl_heur x))›])
      apply (fastforce simp: twl_st_heur'_def)+
      done
    done
qed


lemma twl_st_heur'''D_twl_st_heurD_prod:
  assumes H: ‹(⋀r. f ∈ twl_st_heur''' r →⇩f ⟨A ×⇩r twl_st_heur''' r⟩ nres_rel)›
  shows ‹f ∈ twl_st_heur →⇩f ⟨A ×⇩r twl_st_heur⟩ nres_rel›  (is ‹_ ∈ ?A B›)
proof -
  obtain f1 f2 where f: ‹f = (f1, f2)›
    by (cases f) auto
  show ?thesis
    unfolding f
    apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
    apply (intro conjI impI allI)
    subgoal for x y
      using assms[of ‹length (get_clauses_wl_heur x)›,
        unfolded twl_st_heur'_def nres_rel_def in_pair_collect_simp f,
        rule_format] unfolding f
      apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
      apply (drule spec[of _ x])
      apply (drule spec[of _ y])
      apply simp
      apply (rule "weaken_⇓'"[of _ ‹A ×⇩r twl_st_heur''' (length (get_clauses_wl_heur x))›])
      apply (fastforce simp: twl_st_heur'_def)+
      done
    done
qed

definition (in -) lit_of_hd_trail_st_heur :: ‹isasat ⇒ nat literal nres› where
  ‹lit_of_hd_trail_st_heur S = do {
     ASSERT (fst (get_trail_wl_heur S) ≠ []);
     RETURN (lit_of_last_trail_pol (get_trail_wl_heur S))
  }›

subsection ‹Lifting of Options›

definition get_target_opts :: ‹isasat ⇒ opts_target› where
  ‹get_target_opts S = opts_target (get_opts S)›

definition get_subsumption_opts :: ‹isasat ⇒ bool› where
  ‹get_subsumption_opts S = opts_subsumption (get_opts S)›

definition get_GC_units_opt :: ‹isasat ⇒ 64 word› where
  ‹get_GC_units_opt S = opts_GC_units_lim (get_opts S)›

definition units_since_last_GC_st :: ‹isasat ⇒ 64 word› where
  ‹units_since_last_GC_st S = units_since_last_GC (get_stats_heur S)›

definition units_since_beginning_st :: ‹isasat ⇒ 64 word› where
  ‹units_since_beginning_st S = units_since_beginning (get_stats_heur S)›

definition reset_units_since_last_GC_st :: ‹isasat ⇒ isasat› where
  ‹reset_units_since_last_GC_st S =
  (let stats = get_stats_heur S in
  let stats = reset_units_since_last_GC stats in
  let S = set_stats_wl_heur stats S in S
  )›

(*TODO identical to empty_US_heur*)
definition clss_size_resetUS0_st :: ‹isasat ⇒ isasat› where
  ‹clss_size_resetUS0_st S =
  (let lcount = get_learned_count S in
  let lcount = clss_size_resetUS0 lcount in
  let S = set_learned_count_wl_heur lcount S in S
  )›

definition is_fully_propagated_heur_st :: ‹isasat ⇒ bool› where
  ‹is_fully_propagated_heur_st S = is_fully_propagated_heur (get_heur S)›

definition print_trail_st :: ‹isasat ⇒ _› where
  ‹print_trail_st = (λS. print_trail (get_trail_wl_heur S))›

definition print_trail_st2 where
  ‹print_trail_st2 _ = ()›

lemma print_trail_st_print_trail_st2:
  ‹print_trail_st S ≤ ⇓unit_rel (RETURN (print_trail_st2 S))›
  unfolding print_trail_st2_def print_trail_st_def
    print_trail_def
  apply (refine_vcg WHILET_rule[where
       R = ‹measure (λi. Suc (length (fst (get_trail_wl_heur S))) - i)› and
       I = ‹λi. i ≤ length (fst (get_trail_wl_heur S))›])
  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_st_print_trail_st2_rel:
  ‹(print_trail_st, RETURN o print_trail_st2) ∈ Id →⇩f (⟨unit_rel⟩nres_rel)›
  using print_trail_st_print_trail_st2 by (force intro!: frefI nres_relI)

named_theorems isasat_state_simp

lemma [isasat_state_simp]:
  ‹learned_clss_count (Tuple17.set_q occs S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_p old_arena S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_o opts S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_n lcount S) = learned_clss_count_lcount lcount›
  ‹learned_clss_count (Tuple17.set_m aivdom S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_l heur S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_k stats S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_j outl S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_i lbd S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_h ccach S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_g count' S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_f vmtf' S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_e W S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_d j S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_c D S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_b N S) = learned_clss_count S›
  ‹learned_clss_count (Tuple17.set_a M S) = learned_clss_count S›
  ‹get_trail_wl_heur (set_learned_count_wl_heur lcount S) = get_trail_wl_heur S›
  ‹get_clauses_wl_heur (set_learned_count_wl_heur lcount S) = get_clauses_wl_heur S›
  ‹get_conflict_wl_heur (set_learned_count_wl_heur lcount S) = get_conflict_wl_heur S›
  ‹literals_to_update_wl_heur (set_learned_count_wl_heur lcount S) = literals_to_update_wl_heur S›
  ‹get_watched_wl_heur (set_learned_count_wl_heur lcount S) = get_watched_wl_heur S›
  ‹get_vmtf_heur (set_learned_count_wl_heur lcount S) = get_vmtf_heur S›
  ‹get_count_max_lvls_heur (set_learned_count_wl_heur lcount S) = get_count_max_lvls_heur S›
  ‹get_conflict_cach (set_learned_count_wl_heur lcount S) = get_conflict_cach S›
  ‹get_lbd (set_learned_count_wl_heur lcount S) = get_lbd S›
  ‹get_outlearned_heur (set_learned_count_wl_heur lcount S) = get_outlearned_heur S›
  ‹get_stats_heur (set_learned_count_wl_heur lcount S) = get_stats_heur S›
  ‹get_aivdom (set_learned_count_wl_heur lcount S) = get_aivdom S›
  ‹get_heur (set_learned_count_wl_heur lcount S) = get_heur S›
  ‹get_learned_count (set_learned_count_wl_heur lcount S) = lcount›
  ‹get_opts (set_learned_count_wl_heur lcount S) = get_opts S›
  ‹get_old_arena (set_learned_count_wl_heur lcount S) = get_old_arena S›
  ‹get_occs (set_learned_count_wl_heur lcount S) = get_occs S›
  by (solves ‹cases S; auto simp: learned_clss_count_def›)+

lemmas [isasat_state_simp] = tuple17_state_simp
lemmas [simp] = isasat_state_simp


(*TODO Move*)
definition (in -) length_ll_fs_heur :: ‹isasat ⇒ nat literal ⇒ nat› where
  ‹length_ll_fs_heur S L = length (watched_by_int S L)›

definition (in -) length_watchlist :: ‹nat watcher list list ⇒ nat literal ⇒ nat› where
  ‹length_watchlist S L = length_ll S (nat_of_lit L)›

definition mop_length_watched_by_int :: ‹isasat ⇒ nat literal ⇒ nat nres› where
  ‹mop_length_watched_by_int S L = do {
     ASSERT(nat_of_lit L < length (get_watched_wl_heur S));
     RETURN (length (watched_by_int S L))
}›

definition end_of_rephasing_phase_st :: ‹isasat ⇒ 64 word› where
  ‹end_of_rephasing_phase_st = (λS. end_of_rephasing_phase_heur (get_heur S))›

definition end_of_restart_phase_st :: ‹isasat ⇒ 64 word› where
 ‹end_of_restart_phase_st = (λS. end_of_restart_phase (get_heur S))›

definition get_vmtf_heur_array where
  ‹get_vmtf_heur_array S = (fst (get_focused_heuristics (get_vmtf_heur S)))›

definition get_vmtf_heur_fst where
  ‹get_vmtf_heur_fst S = (fst o snd o snd) (get_focused_heuristics (get_vmtf_heur S))›

definition isa_vmtf_heur_fst where
  ‹isa_vmtf_heur_fst x = (case x of Bump_Heuristics hstable focused foc _ ⇒
    RETURN (vmtf_heur_fst focused))›

definition get_bump_heur_array_nth where
  ‹get_bump_heur_array_nth S i = get_vmtf_heur_array S ! i›

definition mop_mark_added_heur_st :: ‹_› where
  ‹mop_mark_added_heur_st L S = do {
    let heur = get_heur S;
    heur ← mop_mark_added_heur L True heur;
    RETURN (set_heur_wl_heur heur S)
  } ›

definition mark_added_clause_heur2 where
  ‹mark_added_clause_heur2 S C = do {
     i ← mop_arena_length_st S C;
     ASSERT (i ≤ length (get_clauses_wl_heur S));
     (_, S) ← WHILE⇩T (λ(j, S). j < i)
       (λ(j, S). do {
          ASSERT (j<i);
          L ← mop_access_lit_in_clauses_heur S C j;
          S ← mop_mark_added_heur_st (atm_of L) S;
          RETURN (j+1, S)
        })
      (0, S);
    RETURN S
  }›
(*TODO: there should be a maybe_mark_added*)

definition mark_added_clause2 where
  ‹mark_added_clause2 S C = do {
     i ← RETURN (length (get_clauses_wl S ∝ C));
     (_, S) ← WHILE⇩T⇗ λ(j, T). j ≤ i ∧ T = S⇖ (λ(j, S). j < i)
       (λ(j, S). do {
          ASSERT (j<i);
          L ← mop_clauses_at (get_clauses_wl S) C j;
          ASSERT (L ∈ set (get_clauses_wl S ∝ C));
          let S = S;
          RETURN (j+1, S)
        })
      (0, S);
    RETURN S
  }›


lemma mop_mark_added_heur_st_it:
  assumes ‹(S,T) ∈ twl_st_heur› and ‹A ∈# all_atms_st T›
  shows ‹mop_mark_added_heur_st A S ≤ SPEC (λc. (c, T) ∈ {(U, V). (U, V) ∈ twl_st_heur ∧ (get_clauses_wl_heur U) = get_clauses_wl_heur S ∧
       learned_clss_count U = learned_clss_count S})›
proof -
  have heur: ‹heuristic_rel (all_atms_st T) (get_heur S)›
    using assms(1)
    by (auto simp: twl_st_heur_def)

  show ?thesis
    unfolding mop_mark_added_heur_st_def mop_mark_added_heur_def
    apply refine_vcg
    subgoal
      using heur assms(2)
      unfolding mark_added_heur_pre_def mark_added_heur_pre_stats_def
      by (auto simp: heuristic_rel_def heuristic_rel_stats_def
        phase_saving_def ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def ℒ⇩a⇩l⇩l_add_mset
        dest!: multi_member_split)
    subgoal by (use assms in ‹auto simp add: twl_st_heur_def›)
    done
qed

lemma mark_added_clause_heur2_id:
  assumes ‹(S,T) ∈ twl_st_heur› and ‹C ∈# dom_m (get_clauses_wl T)›
  shows ‹mark_added_clause_heur2 S C
     ≤ ⇓{(U, V). (U, V) ∈ twl_st_heur ∧ (get_clauses_wl_heur U) = get_clauses_wl_heur S ∧
       learned_clss_count U = learned_clss_count S} (RETURN T)› (is ‹_ ≤⇓?R _›)
proof -
  have 1: ‹mark_added_clause2 T C ≤ ⇓Id (RETURN T)›
    unfolding mark_added_clause2_def mop_clauses_at_def nres_monad3
    apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i,_). length (get_clauses_wl T ∝ C) -i)›])
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (use assms in auto)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
  have [refine]: ‹y' ∈# dom_m x' ⟹
    ((x, y), x', y') ∈ {(N, N'). valid_arena N N' (set (get_vdom S))} ×⇩f nat_rel ⟹
    mop_arena_length x y ≤ SPEC (λy. (y, length (x' ∝ y')) ∈ {(a,b). (a,b)∈nat_rel ∧ a = length (x' ∝ y')})› for x y x' y'
    apply (rule mop_arena_length[THEN fref_to_Down_curry, of _ _ _ _ ‹set (get_vdom S)›, unfolded comp_def conc_fun_RETURN prod.simps, THEN order_trans])
    apply assumption
    apply assumption
    by auto
  have [refine]: ‹((0, S), 0, T) ∈ nat_rel ×⇩r ?R›
    using assms by auto
  have 2: ‹mark_added_clause_heur2 S C ≤ ⇓?R (mark_added_clause2 T C)›
    unfolding mark_added_clause_heur2_def mop_arena_length_st_def mop_access_lit_in_clauses_heur_def
      mark_added_clause2_def
    apply (refine_vcg mop_mark_added_heur_st_it)
    subgoal by (use assms in auto)
    subgoal by (use assms in ‹auto simp: twl_st_heur_def›)
    subgoal using assms by (auto simp: twl_st_heur_def dest: arena_lifting(10))
    subgoal by auto
    subgoal by auto
    apply (rule_tac vdom = ‹set (get_vdom (x2a))› in mop_arena_lit2)
    subgoal by (use assms in ‹auto simp: twl_st_heur_def›)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (use assms in ‹auto simp: all_atms_st_def all_atms_def all_lits_def ran_m_def
        all_lits_of_mm_add_mset image_Un atm_of_all_lits_of_m(2)
      dest!: multi_member_split›)
    subgoal by auto
    subgoal by auto
    done
  show ?thesis
    unfolding mop_arena_length_st_def mop_access_lit_in_clauses_heur_def
    apply (rule order_trans[OF 2])
    apply (rule ref_two_step')
    apply (rule 1[unfolded Down_id_eq])
    done
qed

definition mop_is_marked_added_heur_st where
  ‹mop_is_marked_added_heur_st S = mop_is_marked_added_heur (get_heur S)›

lemma is_marked_added_heur_st_it:
  assumes ‹(S,T) ∈ twl_st_heur› and ‹A ∈# all_atms_st T›
  shows ‹mop_is_marked_added_heur_st S A ≤ SPEC(λc. (c, d) ∈ (UNIV :: (bool × bool) set))›
proof -
  have heur: ‹heuristic_rel (all_atms_st T) (get_heur S)›
    using assms(1)
    by (auto simp: twl_st_heur_def)
  then have ‹is_marked_added_heur_pre (get_heur S) A›
    using assms
    unfolding is_marked_added_heur_pre_def
    by (auto simp: heuristic_rel_def is_marked_added_heur_pre_stats_def
      heuristic_rel_stats_def phase_saving_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
  then show ?thesis
    unfolding mop_is_marked_added_heur_st_def mop_is_marked_added_heur_def
    by auto
qed

definition schedule_next_pure_lits_st :: ‹isasat ⇒ isasat› where
  ‹schedule_next_pure_lits_st S = set_heur_wl_heur (schedule_next_pure_lits (get_heur S)) S›

definition next_pure_lits_schedule_st :: ‹isasat ⇒ _› where
  ‹next_pure_lits_schedule_st S = next_pure_lits_schedule (get_heur S)›

definition schedule_info_of_st :: ‹isasat ⇒ _› where
  ‹schedule_info_of_st S = schedule_info_of (get_heur S)›

definition schedule_next_reduce_st :: ‹64 word ⇒ isasat ⇒ isasat› where
  ‹schedule_next_reduce_st b S = set_heur_wl_heur (schedule_next_reduce b (get_heur S)) S›

definition next_reduce_schedule_st :: ‹isasat ⇒ _› where
  ‹next_reduce_schedule_st S = next_reduce_schedule (get_heur S)›

definition schedule_next_subsume_st :: ‹64 word ⇒ isasat ⇒ isasat› where
  ‹schedule_next_subsume_st b S = set_heur_wl_heur (schedule_next_subsume b (get_heur S)) S›

definition next_subsume_schedule_st :: ‹isasat ⇒ _› where
  ‹next_subsume_schedule_st S = next_subsume_schedule (get_heur S)›

(*TODO move/deduplicate*)
lemma avdom_delete_index_vdom_heur[simp]:
  ‹get_avdom (delete_index_vdom_heur i S) =  (get_avdom S)›
  ‹get_tvdom (delete_index_vdom_heur i S) = delete_index_and_swap (get_tvdom S) i›
  by (cases S; auto simp: delete_index_vdom_heur_def; fail)+
lemma [simp]:
  ‹learned_clss_count (delete_index_vdom_heur C T) = learned_clss_count T›
  ‹learned_clss_count (mark_unused_st_heur C T) = learned_clss_count T›
  by (cases T; auto simp: learned_clss_count_def delete_index_vdom_heur_def
    mark_unused_st_heur_def; fail)+

lemma get_vdom_mark_garbage[simp]:
  ‹get_vdom (mark_garbage_heur C i S) = get_vdom S›
  ‹get_avdom (mark_garbage_heur C i S) = delete_index_and_swap (get_avdom S) i›
  ‹get_ivdom (mark_garbage_heur C i S) = get_ivdom S›
  ‹get_tvdom (mark_garbage_heur C i S) = get_tvdom S›
  ‹get_tvdom (mark_garbage_heur3 C i S) = delete_index_and_swap (get_tvdom S) i›
  ‹get_ivdom (mark_garbage_heur3 C i S) = get_ivdom S›
  ‹get_vdom (mark_garbage_heur3 C i S) = get_vdom S›
  ‹learned_clss_count (mark_garbage_heur3 C i (S)) ≤ learned_clss_count S›
  ‹learned_clss_count (mark_garbage_heur3 C i (incr_wasted_st b S)) ≤ learned_clss_count S›
  by (cases S; auto simp: mark_garbage_heur_def mark_garbage_heur3_def
   learned_clss_count_def incr_wasted_st_def; fail)+

fun get_reductions_count :: ‹isasat ⇒ 64 word› where
  ‹get_reductions_count S = get_reduction_count (get_stats_heur S)›

(*TODO kill*)
abbreviation get_irredundant_count where
  ‹get_irredundant_count ≡ irredundant_clss›

definition get_irredundant_count_st :: ‹isasat ⇒ 64 word› where
  ‹get_irredundant_count_st S = get_irredundant_count (get_stats_heur S)›

(*TODO Move*)

lemma [simp]:
  ‹get_avdom_aivdom (push_to_tvdom C aivdom) = get_avdom_aivdom aivdom›
  ‹get_vdom_aivdom (push_to_tvdom C aivdom) = get_vdom_aivdom aivdom›
  ‹get_ivdom_aivdom (push_to_tvdom C aivdom) = get_ivdom_aivdom aivdom›
  ‹get_tvdom_aivdom (push_to_tvdom C aivdom) = get_tvdom_aivdom aivdom @ [C]›
  by (cases aivdom; auto simp: push_to_tvdom_def push_to_tvdom_int_def; fail)+

lemma aivdom_inv_dec_empty_tvdom[intro!]:
  ‹aivdom_inv_dec aivdom d ⟹ aivdom_inv_dec (empty_tvdom aivdom) d›
  by (cases aivdom) (auto simp: aivdom_inv_dec_alt_def empty_tvdom_def)

lemma [simp]:
  ‹get_avdom_aivdom (empty_tvdom aivdom) = get_avdom_aivdom aivdom›
  ‹get_vdom_aivdom (empty_tvdom aivdom) = get_vdom_aivdom aivdom›
  ‹get_ivdom_aivdom (empty_tvdom aivdom) = get_ivdom_aivdom aivdom›
  ‹get_tvdom_aivdom (empty_tvdom aivdom) = []›
  by (cases aivdom; auto simp: empty_tvdom_def; fail)+

definition isasat_fast_relaxed :: ‹isasat ⇒ bool› where
  ‹isasat_fast_relaxed S ⟷ length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max›

definition isasat_fast_relaxed2 :: ‹isasat ⇒ nat ⇒ bool› where
  ‹isasat_fast_relaxed2 S n  ⟷ isasat_fast_relaxed S ∧ n < unat64_max›


definition  mop_arena_promote_st where
  ‹mop_arena_promote_st S C = do {
    let N' = get_clauses_wl_heur S;
    let lcount = get_learned_count S;
    ASSERT(clss_size_lcount lcount ≥ 1);
    let lcount = clss_size_decr_lcount lcount;
    N' ← mop_arena_set_status N' C IRRED;
    RETURN (set_clauses_wl_heur N' (set_learned_count_wl_heur lcount S))
  }›

definition set_stats_size_limit_st where
  ‹set_stats_size_limit_st lbd sze T = (
     let stats = get_stats_heur T;
         stats = set_stats_size_limit lbd sze stats
     in set_stats_wl_heur stats T
)›

definition get_lsize_limit_stats_st :: ‹_› where
  ‹get_lsize_limit_stats_st T = get_lsize_limit_stats (get_stats_heur T)›

definition maybe_mark_added_clause_heur2 where
  ‹maybe_mark_added_clause_heur2 S C = do {
     let (lbd_limit, size_limit) = get_lsize_limit_stats_st S;
     lbd ← mop_arena_lbd_st S C;
     sze ← mop_arena_length_st S C;
     st ← mop_arena_status_st S C;
     if (st = IRRED ∨ (st = LEARNED ∧ lbd ≤ lbd_limit ∧ sze ≤ size_limit))
     then mark_added_clause_heur2 S C
     else RETURN S
  }›

lemma maybe_mark_added_clause_heur2_id:
  assumes ‹(S,T) ∈ twl_st_heur› and ‹C ∈# dom_m (get_clauses_wl T)›
  shows ‹maybe_mark_added_clause_heur2 S C
     ≤ ⇓{(U, V). (U, V) ∈ twl_st_heur ∧ (get_clauses_wl_heur U) = get_clauses_wl_heur S ∧
       learned_clss_count U = learned_clss_count S} (RETURN T)› (is ‹_ ≤⇓?R _›)
proof -
  have
      valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))›
    using assms unfolding all_atms_def all_lits_def
    by (auto simp: twl_st_heur'_def twl_st_heur_def)
  show ?thesis
    using assms unfolding maybe_mark_added_clause_heur2_def mop_arena_lbd_st_def
      mop_arena_lbd_def mop_arena_length_st_def mop_arena_length_def nres_monad3
      mop_arena_status_st_def mop_arena_status_def
    apply (refine_vcg mark_added_clause_heur2_id[OF assms(1), THEN order_trans])
    subgoal using valid by (auto simp: get_clause_LBD_pre_def
      arena_is_valid_clause_idx_def)
    subgoal using valid by (auto simp: arena_is_valid_clause_idx_def)
    subgoal using valid by (auto simp: arena_is_valid_clause_vdom_def)
    subgoal by (auto simp: Refine_Basic.RETURN_def conc_fun_RES)
    subgoal by auto
    done
qed

definition stats_forward_rounds_st :: ‹isasat ⇒ 64 word› where
  ‹stats_forward_rounds_st S = stats_forward_rounds (get_stats_heur S)›

definition incr_purelit_rounds_st :: ‹_› where
  ‹incr_purelit_rounds_st S = set_stats_wl_heur (incr_purelit_rounds (get_stats_heur S)) S›

lemma all_count_learned[simp]: ‹clss_size_allcount (get_learned_count S) = learned_clss_count S›
    by (auto simp: twl_st_heur'_def clss_size_allcount_def learned_clss_count_def clss_size_lcountU0_def
      clss_size_lcount_def clss_size_lcountUE_def clss_size_lcountUS_def clss_size_lcountUEk_def
      split: prod.splits)
end