Theory IsaSAT_Setup2_LLVM

theory IsaSAT_Setup2_LLVM
  imports IsaSAT_Setup
    IsaSAT_Bump_Heuristics_LLVM
    IsaSAT_Setup0_LLVM
begin

definition opts_restart_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹opts_restart_st_fast_code = read_opts_wl_heur_code opts_rel_restart_code›

global_interpretation opts_restart: read_opts_param_adder0 where
  f' = ‹RETURN o opts_restart› and
  f = opts_rel_restart_code and
  x_assn = bool1_assn and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_restart) = RETURN o opts_restart_st› and
    ‹read_opts_wl_heur_code opts_rel_restart_code = opts_restart_st_fast_code›
  apply unfold_locales
  apply (rule opts_refine; assumption)
  subgoal by (auto simp: opts_restart_st_def read_all_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: opts_restart_st_fast_code_def)
  done

definition opts_reduction_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹opts_reduction_st_fast_code = read_opts_wl_heur_code opts_rel_reduce_code›

global_interpretation opts_reduce: read_opts_param_adder0 where
  f' = ‹RETURN o opts_reduce› and
  f = opts_rel_reduce_code and
  x_assn = bool1_assn and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_reduce) = RETURN o opts_reduction_st› and
    ‹read_opts_wl_heur_code opts_rel_reduce_code = opts_reduction_st_fast_code›
  apply unfold_locales
  apply (rule opts_refine; assumption)
  subgoal by (auto simp: opts_reduction_st_fast_code_def read_all_st_def opts_reduction_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: opts_reduction_st_fast_code_def)
  done

definition opts_unbounded_mode_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹opts_unbounded_mode_st_fast_code = read_opts_wl_heur_code opts_rel_unbounded_mode_code›

global_interpretation opts_unbounded_mode: read_opts_param_adder0 where
  f' = ‹RETURN o opts_unbounded_mode› and
  f = opts_rel_unbounded_mode_code and
  x_assn = bool1_assn and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_unbounded_mode) = RETURN o opts_unbounded_mode_st› and
    ‹read_opts_wl_heur_code opts_rel_unbounded_mode_code = opts_unbounded_mode_st_fast_code›
  apply unfold_locales
  apply (rule opts_refine; assumption)
  subgoal by (auto simp: read_all_st_def opts_unbounded_mode_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: opts_unbounded_mode_st_fast_code_def)
  done

definition opts_minimum_between_restart_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹opts_minimum_between_restart_st_fast_code = read_opts_wl_heur_code opts_rel_miminum_between_restart_code›

global_interpretation opts_minimum_between_restart: read_opts_param_adder0 where
  f' = ‹RETURN o opts_minimum_between_restart› and
  f = opts_rel_miminum_between_restart_code and
  x_assn = word_assn and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_minimum_between_restart) = RETURN o opts_minimum_between_restart_st› and
    ‹read_opts_wl_heur_code opts_rel_miminum_between_restart_code = opts_minimum_between_restart_st_fast_code›
  apply unfold_locales
  apply (rule opts_refine; assumption)
  subgoal by (auto simp: read_all_st_def opts_minimum_between_restart_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: opts_minimum_between_restart_st_fast_code_def)
  done

definition opts_restart_coeff1_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹opts_restart_coeff1_st_fast_code = read_opts_wl_heur_code opts_rel_restart_coeff1_code›

global_interpretation opts_restart_coeff1: read_opts_param_adder0 where
  f' = ‹RETURN o opts_restart_coeff1› and
  f = opts_rel_restart_coeff1_code and
  x_assn = word_assn and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_restart_coeff1) = RETURN o opts_restart_coeff1_st› and
    ‹read_opts_wl_heur_code opts_rel_restart_coeff1_code = opts_restart_coeff1_st_fast_code›
  apply unfold_locales
  apply (rule opts_refine; assumption)
  subgoal by (auto simp: read_all_st_def opts_minimum_between_restart_st_def opts_restart_coeff1_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: opts_restart_coeff1_st_fast_code_def)
  done

definition opts_restart_coeff2_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹opts_restart_coeff2_st_fast_code = read_opts_wl_heur_code opts_rel_restart_coeff2_code›

global_interpretation opts_restart_coeff2: read_opts_param_adder0 where
  f' = ‹RETURN o opts_restart_coeff2› and
  f = opts_rel_restart_coeff2_code and
  x_assn = ‹snat_assn' (TYPE(64))› and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_restart_coeff2) = RETURN o opts_restart_coeff2_st› and
    ‹read_opts_wl_heur_code opts_rel_restart_coeff2_code = opts_restart_coeff2_st_fast_code›
  apply unfold_locales
  apply (rule opts_refine; assumption)
  subgoal by (auto simp: read_all_st_def opts_minimum_between_restart_st_def opts_restart_coeff2_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: opts_restart_coeff2_st_fast_code_def)
  done

definition units_since_last_GC_st_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹units_since_last_GC_st_code = read_stats_wl_heur_code units_since_last_GC_stats_impl›

global_interpretation units_since_last_GC: read_stats_param_adder0 where
  f' = ‹RETURN o units_since_last_GC› and
  f = units_since_last_GC_stats_impl and
  x_assn = word_assn and
  P = ‹λ_. True›
  rewrites ‹read_stats_wl_heur (RETURN o units_since_last_GC) = RETURN o units_since_last_GC_st› and
    ‹read_stats_wl_heur_code units_since_last_GC_stats_impl = units_since_last_GC_st_code›
  apply unfold_locales
  apply (rule units_since_last_GC_stats_impl.refine; assumption)
  subgoal by (auto simp: read_all_st_def units_since_last_GC_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: units_since_last_GC_st_code_def)
  done

definition units_since_beginning_st_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹units_since_beginning_st_code = read_stats_wl_heur_code units_since_beginning_stats_impl›

global_interpretation units_since_beginning: read_stats_param_adder0 where
  f' = ‹RETURN o units_since_beginning› and
  f = units_since_beginning_stats_impl and
  x_assn = word_assn and
  P = ‹λ_. True›
  rewrites ‹read_stats_wl_heur (RETURN o units_since_beginning) = RETURN o units_since_beginning_st› and
    ‹read_stats_wl_heur_code units_since_beginning_stats_impl = units_since_beginning_st_code›
  apply unfold_locales
  apply (rule units_since_beginning_stats_impl.refine; assumption)
  subgoal by (auto simp: read_all_st_def units_since_beginning_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: units_since_beginning_st_code_def)
  done

definition get_GC_units_opt_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹get_GC_units_opt_code = read_opts_wl_heur_code opts_rel_GC_units_lim_code›

global_interpretation opts_GC_units_lim: read_opts_param_adder0 where
  f' = ‹RETURN o opts_GC_units_lim› and
  f = opts_rel_GC_units_lim_code and
  x_assn = word_assn and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_GC_units_lim) = RETURN o get_GC_units_opt› and
    ‹read_opts_wl_heur_code opts_rel_GC_units_lim_code = get_GC_units_opt_code›
  apply unfold_locales
  apply (rule opts_refine)
  subgoal by (auto simp: read_all_st_def get_GC_units_opt_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: get_GC_units_opt_code_def)
  done

definition get_target_opts_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹get_target_opts_impl = read_opts_wl_heur_code opts_rel_target_code›

global_interpretation get_target_opts: read_opts_param_adder0 where
  f' = ‹RETURN o opts_target› and
  f = opts_rel_target_code and
  x_assn = ‹word_assn' TYPE(3)› and
  P = ‹λ_. True›
  rewrites ‹read_opts_wl_heur (RETURN o opts_target) = RETURN o get_target_opts› and
    ‹read_opts_wl_heur_code opts_rel_target_code = get_target_opts_impl›
  apply unfold_locales
  apply (rule opts_refine)
  subgoal by (auto simp: get_target_opts_def read_all_st_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: get_target_opts_impl_def)
  done

definition isasat_length_trail_st_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹isasat_length_trail_st_code = read_trail_wl_heur_code isa_length_trail_fast_code›

global_interpretation trail_length: read_trail_param_adder0 where
  f' = ‹RETURN o isa_length_trail› and
  f = isa_length_trail_fast_code and
  x_assn = sint64_nat_assn and
  P = ‹λ_. True›
  rewrites  ‹read_trail_wl_heur (RETURN o isa_length_trail) = RETURN o isasat_length_trail_st› and
    ‹read_trail_wl_heur_code isa_length_trail_fast_code = isasat_length_trail_st_code›
  apply unfold_locales
  apply (rule isa_length_trail_fast_code.refine)
  subgoal by (auto simp: isa_length_trail_def read_all_st_def isasat_length_trail_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: isasat_length_trail_st_code_def)
  done

lemma get_pos_of_level_in_trail_imp_alt_def:
  ‹get_pos_of_level_in_trail_imp = (λS C. do {k ← get_pos_of_level_in_trail_imp S C; RETURN k})›
  by auto

sepref_def get_pos_of_level_in_trail_imp_code
  is ‹uncurry get_pos_of_level_in_trail_imp›
  :: ‹trail_pol_fast_assn⇧k *⇩a uint32_nat_assn⇧k  →⇩a sint64_nat_assn›
  supply [[goals_limit=1]]
  apply (subst get_pos_of_level_in_trail_imp_alt_def)
  apply (rewrite in ‹_› eta_expand[where f = RETURN])
  apply (rewrite in ‹RETURN ⌑› annot_unat_snat_upcast[where 'l=64])
  by sepref

definition get_pos_of_level_in_trail_imp_st_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹get_pos_of_level_in_trail_imp_st_code = (λN C. read_trail_wl_heur_code (λc. get_pos_of_level_in_trail_imp_code c C) N)›

global_interpretation pos_of_level_in_trail: read_trail_param_adder where
  R = ‹unat_rel' TYPE(32)› and
  f' = ‹λM c. get_pos_of_level_in_trail_imp c M› and
  f = ‹λM c. get_pos_of_level_in_trail_imp_code c M› and
  x_assn = sint64_nat_assn and
  P = ‹λ_ _. True›
  rewrites  ‹(λN C'. read_trail_wl_heur (λc. get_pos_of_level_in_trail_imp c C') N) = get_pos_of_level_in_trail_imp_st› and
    ‹(λN C. read_trail_wl_heur_code (λc. get_pos_of_level_in_trail_imp_code c C) N) = get_pos_of_level_in_trail_imp_st_code›
  apply unfold_locales
  apply (subst lambda_comp_true)+
  apply (rule get_pos_of_level_in_trail_imp_code.refine)
  subgoal by (auto simp: get_pos_of_level_in_trail_imp_st_def read_all_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: get_pos_of_level_in_trail_imp_st_code_def)
  done

definition get_global_conflict_count_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
   ‹get_global_conflict_count_impl = read_stats_wl_heur_code stats_conflicts_impl›

global_interpretation stats_conflict: read_stats_param_adder0 where
  f' = ‹RETURN o stats_conflicts› and
  f = stats_conflicts_impl and
  x_assn = word_assn and
  P = ‹λ_. True›
  rewrites ‹read_stats_wl_heur (RETURN o stats_conflicts) = RETURN o get_global_conflict_count› and
    ‹read_stats_wl_heur_code stats_conflicts_impl = get_global_conflict_count_impl›
  apply unfold_locales
  apply (rule stats_conflicts_impl.refine; assumption)
  subgoal by (auto simp: read_all_st_def stats_conflicts_def get_global_conflict_count_def intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: get_global_conflict_count_impl_def)
  done

lemmas [unfolded lambda_comp_true, sepref_fr_rules] =
  opts_restart.refine[unfolded]
  opts_reduce.refine[unfolded]
  opts_unbounded_mode.refine
  opts_minimum_between_restart.refine
  opts_restart_coeff1.refine
  opts_restart_coeff2.refine
  units_since_last_GC.refine
  units_since_beginning.refine
  opts_GC_units_lim.refine
  trail_length.refine
  pos_of_level_in_trail.refine
  stats_conflict.refine
  get_target_opts.refine

sepref_register opts_reduction_st opts_restart_st opts_restart_coeff2_st opts_restart_coeff1_st
    opts_minimum_between_restart_st opts_unbounded_mode_st get_GC_units_opt units_since_last_GC_st
    isasat_length_trail_st get_pos_of_level_in_trail_imp_st units_since_beginning

lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  opts_restart_st_fast_code_def[unfolded read_all_st_code_def]
  opts_reduction_st_fast_code_def[unfolded read_all_st_code_def]
  opts_unbounded_mode_st_fast_code_def[unfolded read_all_st_code_def]
  opts_minimum_between_restart_st_fast_code_def[unfolded read_all_st_code_def]
  opts_restart_coeff1_st_fast_code_def[unfolded read_all_st_code_def]
  opts_restart_coeff2_st_fast_code_def[unfolded read_all_st_code_def]
  units_since_last_GC_st_code_def[unfolded read_all_st_code_def]
  units_since_beginning_st_code_def[unfolded read_all_st_code_def]
  get_GC_units_opt_code_def[unfolded read_all_st_code_def]
  isasat_length_trail_st_code_def[unfolded read_all_st_code_def]
  get_pos_of_level_in_trail_imp_st_code_def[unfolded read_all_st_code_def]
  get_global_conflict_count_impl_def[unfolded read_all_st_code_def]
  get_target_opts_impl_def[unfolded read_all_st_code_def]

sepref_register reset_units_since_last_GC

lemma reset_units_since_last_GC_st_alt_def:
  ‹reset_units_since_last_GC_st S =
  (let (stats, S) = extract_stats_wl_heur S in
  let stats = reset_units_since_last_GC stats in
  let S = update_stats_wl_heur stats S in S
  )›
  by (auto simp: reset_units_since_last_GC_st_def state_extractors split: isasat_int_splits)


sepref_def reset_units_since_last_GC_st_code
  is ‹RETURN o reset_units_since_last_GC_st›
  :: ‹isasat_bounded_assn⇧d  →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding reset_units_since_last_GC_st_alt_def
  by sepref

lemmas [unfolded inline_direct_return_node_case, llvm_code] = units_since_last_GC_st_code_def[unfolded read_all_st_code_def]
lemmas [llvm_code del] = units_since_last_GC_st_code_def

lemma mop_isasat_length_trail_st_alt_def:
  ‹mop_isasat_length_trail_st S = do {
    ASSERT(isa_length_trail_pre (get_trail_wl_heur S));
    RETURN (isasat_length_trail_st S)
  }›
  unfolding isasat_length_trail_st_def mop_isasat_length_trail_st_def
  by auto


sepref_def mop_isasat_length_trail_st_code
  is ‹mop_isasat_length_trail_st›
  :: ‹isasat_bounded_assn⇧k  →⇩a sint64_nat_assn›
  supply [[goals_limit=1]]
  unfolding mop_isasat_length_trail_st_alt_def
  by sepref


definition arena_status_st where
  ‹arena_status_st = (λS. arena_status (get_clauses_wl_heur S))›

definition arena_status_st_impl where
  ‹arena_status_st_impl = (λS C'. read_arena_wl_heur_code (λN. arena_status_impl N C') S)›

global_interpretation arena_is_valid: read_arena_param_adder where
  R = ‹snat_rel' TYPE(64)› and
  f = ‹λC N. arena_status_impl N C› and
  f' = ‹(λC' N.  (RETURN oo arena_status) N C')› and
  x_assn = status_impl_assn and
  P = ‹(λC S. arena_is_valid_clause_vdom S C)›
  rewrites ‹(λS C'. read_arena_wl_heur (λN.  (RETURN oo arena_status) N C') S) = RETURN oo arena_status_st› and
  ‹(λS C'. read_arena_wl_heur_code (λN. arena_status_impl N C') S) = arena_status_st_impl› and
  ‹arena_is_valid.mop = mop_arena_status_st› and
  ‹(λS. arena_is_valid_clause_vdom (get_clauses_wl_heur S)) = curry clause_not_marked_to_delete_heur_pre›
  apply unfold_locales
  apply (rule arena_status_impl.refine)
  subgoal by (auto simp: mop_arena_status_st_def read_all_st_def arena_status_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: arena_status_st_impl_def)
  subgoal by (auto simp: read_arena_param_adder_ops.mop_def mop_arena_status_st_def mop_arena_status_def read_all_st_def arena_status_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: clause_not_marked_to_delete_heur_pre_def)
  done

lemmas [sepref_fr_rules] = arena_is_valid.mop_refine arena_is_valid.refine[unfolded uncurry_curry_id]

sepref_def mop_arena_status_st_impl
  is ‹uncurry mop_arena_status_st›
  :: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a status_impl_assn›
  supply [[goals_limit=1]]
  by sepref

definition arena_length_st_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹arena_length_st_impl = (λS C'. read_arena_wl_heur_code (λN. arena_length_impl N C') S)›

global_interpretation arena_length_clause: read_arena_param_adder where
  R = ‹snat_rel' TYPE(64)› and
  f = ‹λC N. arena_length_impl N C› and
  f' = ‹(λC' N.  (RETURN oo arena_length) N C')› and
  x_assn = sint64_nat_assn and
  P = ‹(λC S. arena_is_valid_clause_idx S C)›
  rewrites ‹(λS C'. read_arena_wl_heur (λN.  (RETURN oo arena_status) N C') S) = RETURN oo arena_status_st› and
  ‹(λS C'. read_arena_wl_heur_code (λN. arena_length_impl N C') S) = arena_length_st_impl› and
  ‹arena_length_clause.mop = mop_arena_length_st›
  apply unfold_locales
  apply (rule arena_length_impl.refine)
  subgoal by (auto simp: mop_arena_status_st_def read_all_st_def arena_status_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: arena_length_st_impl_def)
  subgoal
    by (auto simp: read_arena_param_adder_ops.mop_def mop_arena_length_st_def mop_arena_length_def read_all_st_def
      split: isasat_int_splits intro!: ext)
  done

lemmas [sepref_fr_rules] = arena_length_clause.mop_refine
lemmas [unfolded inline_direct_return_node_case, llvm_code] = arena_length_st_impl_def[unfolded read_all_st_code_def]
  arena_status_st_impl_def[unfolded read_all_st_code_def]

sepref_definition arena_full_length_impl
  is ‹RETURN o length›
  :: ‹arena_fast_assn⇧k →⇩a sint64_nat_assn›
  by sepref

definition full_arena_length_st_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹full_arena_length_st_impl = read_arena_wl_heur_code  (arena_full_length_impl)›

global_interpretation arena_full_length: read_arena_param_adder0 where
  f = ‹arena_full_length_impl› and
  f' = ‹(RETURN o length)› and
  x_assn = sint64_nat_assn and
  P = ‹(λ_. True)›
  rewrites ‹read_arena_wl_heur (RETURN o length) = RETURN o full_arena_length_st› and
    ‹read_arena_wl_heur_code  (arena_full_length_impl) = full_arena_length_st_impl›
  apply unfold_locales
  apply (rule arena_full_length_impl.refine)
  subgoal by (auto simp: mop_arena_status_st_def read_all_st_def full_arena_length_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: full_arena_length_st_impl_def)
  done

lemma incr_wasted_st_alt_def:
  ‹incr_wasted_st = (λwaste S. do{
  let (heur, S) = extract_heur_wl_heur S in
  let heur = incr_wasted waste heur in
  let S = update_heur_wl_heur heur S in S
  })›
    by (auto simp: incr_wasted_st_def state_extractors intro!: ext split: isasat_int_splits)

sepref_def incr_wasted_st_impl
  is ‹uncurry (RETURN oo incr_wasted_st)›
  :: ‹word64_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply[[goals_limit=1]]
  unfolding incr_wasted_st_alt_def
  by sepref

lemma id_clvls_assn: ‹(Mreturn, RETURN) ∈ (uint32_nat_assn)⇧k →⇩a uint32_nat_assn›
  by sepref_to_hoare vcg

definition get_count_max_lvls_heur_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹get_count_max_lvls_heur_impl = read_ccount_wl_heur_code  (Mreturn)›

global_interpretation get_count_max_lvls: read_ccount_param_adder0 where
  f = ‹Mreturn› and
  f' = ‹(RETURN)› and
  x_assn = uint32_nat_assn and
  P = ‹(λ_. True)›
  rewrites ‹read_ccount_wl_heur (RETURN) = RETURN o get_count_max_lvls_heur› and
    ‹read_ccount_wl_heur_code  (Mreturn) = get_count_max_lvls_heur_impl›
  apply unfold_locales
  apply (rule id_clvls_assn)
  subgoal by (auto simp: read_all_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: get_count_max_lvls_heur_impl_def)
  done


lemmas [sepref_fr_rules] = arena_full_length.refine get_count_max_lvls.refine
lemmas [unfolded inline_direct_return_node_case, llvm_code] = full_arena_length_st_impl_def[unfolded read_all_st_code_def]
  arena_full_length_impl_def
   get_count_max_lvls_heur_impl_def[unfolded read_all_st_code_def]

lemma clss_size_resetUS0_st_alt_def:
  ‹clss_size_resetUS0_st S =
  (let (stats, S) = extract_lcount_wl_heur S in
  let stats = clss_size_resetUS0 stats in
  let S = update_lcount_wl_heur stats S in S
  )›
  by (auto simp: clss_size_resetUS0_st_def state_extractors
    split: isasat_int_splits)

sepref_def clss_size_resetUS0_st
  is ‹RETURN o clss_size_resetUS0_st›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  unfolding clss_size_resetUS0_st_alt_def
  by sepref

lemma length_ll[def_pat_rules]: ‹length_ll$xs$i ≡ op_list_list_llen$xs$i›
  by (auto simp: op_list_list_llen_def length_ll_def)

sepref_def length_watchlist_impl
   is ‹uncurry (RETURN oo length_watchlist)›
  :: ‹[uncurry (λS L. nat_of_lit L < length S)]⇩a watchlist_fast_assn⇧k *⇩a unat_lit_assn⇧k → sint64_nat_assn›
  unfolding length_watchlist_def
  by sepref

definition length_ll_fs_heur_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹length_ll_fs_heur_fast_code = (λN C. read_watchlist_wl_heur_code (λN. length_watchlist_impl N C) N)›
global_interpretation watched_by_app: read_watchlist_param_adder where
  R = ‹unat_lit_rel› and
  f = ‹λC N. length_watchlist_impl N C› and
  f' = ‹λC N. (RETURN oo length_watchlist) N C› and
  x_assn = sint64_nat_assn and
  P = ‹(λL S. nat_of_lit L < length (S))›
  rewrites
    ‹(λN C'. read_watchlist_wl_heur (λN. (RETURN ∘∘ length_watchlist) N C') N) = RETURN oo length_ll_fs_heur› and
    ‹(λN C. read_watchlist_wl_heur_code (λN. length_watchlist_impl N C) N) = length_ll_fs_heur_fast_code› and
    ‹watched_by_app.XX.mop = mop_length_watched_by_int›
  apply unfold_locales
  apply (rule length_watchlist_impl.refine)
  subgoal
     by (auto intro!: ext simp: length_ll_fs_heur_def read_all_st_def length_watchlist_def
         length_ll_def
       split: isasat_int_splits)
  subgoal by (auto simp: length_ll_fs_heur_fast_code_def)
  subgoal
    by (auto simp: mop_length_watched_by_int_def read_all_param_adder_ops.mop_def read_all_st_def
        length_watchlist_def length_ll_def split: isasat_int_splits
      intro!: ext)
  done

lemmas [sepref_fr_rules] = watched_by_app.refine watched_by_app.XX.mop_refine
lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  length_ll_fs_heur_fast_code_def[unfolded read_all_st_code_def]

definition get_vmtf_heur_fst_impl where
  ‹get_vmtf_heur_fst_impl = read_vmtf_wl_heur_code (isa_vmtf_heur_fst_code)›

global_interpretation vmtf_fst: read_vmtf_param_adder0 where
  f' = ‹isa_vmtf_heur_fst› and
  f = ‹isa_vmtf_heur_fst_code› and
  x_assn = atom_assn and
  P = ‹(λ_. True)›
  rewrites
    ‹read_vmtf_wl_heur (isa_vmtf_heur_fst) = RETURN o get_vmtf_heur_fst› and
    ‹read_vmtf_wl_heur_code (isa_vmtf_heur_fst_code) = get_vmtf_heur_fst_impl›
  apply unfold_locales
  apply (rule isa_vmtf_heur_fst_code.refine)
  subgoal
    by (auto intro!: ext simp: get_vmtf_heur_fst_def read_all_st_def vmtf_heur_fst_def
      isa_vmtf_heur_fst_def
       split: isasat_int_splits bump_heuristics_splits)
  subgoal by (auto simp: get_vmtf_heur_fst_impl_def)
  done

definition get_bump_heur_array_nth_impl where
  ‹get_bump_heur_array_nth_impl N C' = read_vmtf_wl_heur_code (λM. isa_vmtf_heur_array_nth_code M C') N›

lemma get_vmtf_heur_array_alt_def: ‹get_vmtf_heur_array S = fst (bump_get_heuristics (get_vmtf_heur S))›
  by (auto simp: get_vmtf_heur_array_def bump_get_heuristics_def)

global_interpretation vmtf_array_nth: read_vmtf_param_adder where
  f' = ‹λa b. isa_vmtf_heur_array_nth b a› and
  f = ‹λa b. isa_vmtf_heur_array_nth_code b a› and
  x_assn = vmtf_node_assn and
  P = ‹(λn S. n < length (fst (bump_get_heuristics S)))› and
  R = atom_rel
 rewrites
    ‹(λN C'. read_vmtf_wl_heur (λM. isa_vmtf_heur_array_nth M C') N) = RETURN oo get_bump_heur_array_nth›  and
    ‹(λN C'. read_vmtf_wl_heur_code (λM. isa_vmtf_heur_array_nth_code M C') N) = get_bump_heur_array_nth_impl›
  apply unfold_locales
  apply (subst (3)uncurry_def)
  apply (rule isa_vmtf_heur_array_nth_code.refine)
  subgoal
    by (auto intro!: ext simp: get_bump_heur_array_nth_def read_all_st_def vmtf_heur_array_nth_def
        get_vmtf_heur_array_def isa_vmtf_heur_array_nth_def bump_get_heuristics_def
      split: isasat_int_splits bump_heuristics_splits prod.splits)
  subgoal by (auto simp: get_bump_heur_array_nth_impl_def[abs_def])
  done

lemmas [sepref_fr_rules] = vmtf_fst.refine
  vmtf_array_nth.refine[unfolded get_vmtf_heur_array_def[symmetric, unfolded comp_def] get_vmtf_heur_array_alt_def[symmetric]]

lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  get_vmtf_heur_fst_impl_def[unfolded read_all_st_code_def]
  get_bump_heur_array_nth_impl_def[unfolded read_all_st_code_def]


lemma mop_mark_added_heur_st_alt_def:
  ‹mop_mark_added_heur_st L S = do {
  let (heur, S) = extract_heur_wl_heur S;
  heur ← mop_mark_added_heur L True heur;
  RETURN (update_heur_wl_heur heur S)
  }›
  unfolding mop_mark_added_heur_st_def
  by (auto simp: incr_restart_stat_def state_extractors split: isasat_int_splits
    intro!: ext)

sepref_def mop_mark_added_heur_iml
  is ‹uncurry2 mop_mark_added_heur›
  :: ‹atom_assn⇧k *⇩a bool1_assn⇧k *⇩a heuristic_assn⇧d →⇩a heuristic_assn›
  supply [sepref_fr_rules] = mark_added_heur_impl_refine
  unfolding mop_mark_added_heur_def
  by sepref

sepref_register mop_mark_added_heur mop_mark_added_heur_st mark_added_clause_heur2 maybe_mark_added_clause_heur2

sepref_def mop_mark_added_heur_st_impl
  is ‹uncurry mop_mark_added_heur_st›
  :: ‹atom_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  unfolding mop_mark_added_heur_st_alt_def
  by sepref


experiment
begin

export_llvm opts_reduction_st_fast_code opts_restart_st_fast_code opts_unbounded_mode_st_fast_code
  opts_minimum_between_restart_st_fast_code mop_arena_status_st_impl full_arena_length_st_impl
  get_global_conflict_count_impl get_count_max_lvls_heur_impl clss_size_resetUS0_st
end

end