Theory IsaSAT_Setup4_LLVM

theory IsaSAT_Setup4_LLVM
  imports
    IsaSAT_Setup
    IsaSAT_Setup0_LLVM
begin

definition length_occs where
  ‹length_occs S = length (get_occs S)›

sepref_def length_occs_raw
  is ‹RETURN o length›
  :: ‹occs_assnk →a sint64_nat_assn›
  unfolding op_list_list_len_def[symmetric]
  by sepref
term   op_list_list_llen

definition length_occs_impl where
  ‹length_occs_impl = read_occs_wl_heur_code length_occs_raw›

sepref_register length_occs

global_interpretation length_occs: read_occs_param_adder0 where
  f = ‹length_occs_raw› and
  f' = ‹RETURN o length› and
  x_assn = sint64_nat_assn and
  P = ‹(λS. True)›
  rewrites ‹read_occs_wl_heur (RETURN o length) = RETURN o length_occs› and
  ‹read_occs_wl_heur_code length_occs_raw = length_occs_impl›
  apply unfold_locales
  apply (rule length_occs_raw.refine)
  subgoal
    by (auto simp: read_all_st_def length_occs_def intro!: ext
      split: isasat_int_splits)
  subgoal
    by (auto simp: length_occs_impl_def)
  done

term mop_cocc_list_length

definition length_occs_at where
  ‹length_occs_at S i = mop_cocc_list_length (get_occs S) i›

sepref_def mop_cocc_list_length_impl
  is ‹uncurry (mop_cocc_list_length)›
  :: ‹[uncurry cocc_list_length_pre]a occs_assnk *a unat_lit_assnk → sint64_nat_assn›
  unfolding cocc_list_length_def
    cocc_list_length_pre_def fold_op_list_list_llen mop_cocc_list_length_def
  by sepref

definition length_occs_at_impl where
  ‹length_occs_at_impl = (λN C. read_occs_wl_heur_code (λM. mop_cocc_list_length_impl M C) N)›

sepref_register length_occs_at

global_interpretation length_occs_at: read_occs_param_adder where
  f = ‹λL S. mop_cocc_list_length_impl S L› and
  f' = ‹λL S. mop_cocc_list_length S L› and
  x_assn = sint64_nat_assn and
  P = ‹λL S. cocc_list_length_pre S L› and
  R = ‹unat_lit_rel›
  rewrites ‹(λN C. read_occs_wl_heur_code (λM. mop_cocc_list_length_impl M C) N) = length_occs_at_impl› and
  ‹(λS C'. read_occs_wl_heur (λL. mop_cocc_list_length L C') S) = length_occs_at›
  apply unfold_locales
  apply (rule mop_cocc_list_length_impl.refine)
  subgoal
    by (auto simp: length_occs_at_impl_def)
  subgoal
    by (auto simp: read_all_st_def length_occs_at_def intro!: ext
      split: isasat_int_splits)
  done

lemma length_occs_at_alt_def:
    ‹length_occs_at = length_occs_at.XX.mop›
  by (auto simp: length_occs_at.XX.mop_def length_occs_at_def read_all_param_adder_ops.mop_def
    read_all_st_def summarize_ASSERT_conv
    mop_cocc_list_length_def split: tuple17.splits intro!: ext)

lemmas [sepref_fr_rules] = length_occs.refine[unfolded lambda_comp_true]
   length_occs_at.refine
   length_occs_at.XX.mop_refine[unfolded length_occs_at_alt_def[symmetric]]
lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  length_occs_impl_def[unfolded read_all_st_code_def]
  length_occs_at_impl_def[unfolded read_all_st_code_def]

definition get_occs_list_at :: ‹isasat ⇒ nat literal ⇒ nat ⇒ nat nres› where
  ‹get_occs_list_at S L i = mop_cocc_list_at (get_occs S) L i›

sepref_def mop_cocc_list_at_impl
  is ‹uncurry2 (mop_cocc_list_at)›
  :: ‹[uncurry2 cocc_list_at_pre]a occs_assnk *a unat_lit_assnk *a sint64_nat_assnk → sint64_nat_assn›
  unfolding mop_cocc_list_at_def cocc_list_at_def cocc_list_at_pre_def fold_op_list_list_idx
  by sepref

definition get_occs_list_at_impl :: ‹_ ⇒ _ ⇒ _ ⇒ _› where
  ‹get_occs_list_at_impl = (λN C D. read_occs_wl_heur_code (λM. mop_cocc_list_at_impl M C D) N)›

global_interpretation occs_at_at: read_occs_param_adder2 where
  f = ‹λC D S. mop_cocc_list_at_impl S C D› and
  f' = ‹λC D S. mop_cocc_list_at S C D› and
  x_assn = sint64_nat_assn and
  P = ‹λC D S. cocc_list_at_pre S C D› and
  R = ‹unat_lit_rel› and
  R' = ‹snat_rel' TYPE(64)›
  rewrites
    ‹(λN C D. read_occs_wl_heur (λM. mop_cocc_list_at M C D) N) = get_occs_list_at› and
    ‹(λN C D. read_occs_wl_heur_code (λM. mop_cocc_list_at_impl M C D) N) = get_occs_list_at_impl›
  apply unfold_locales
  apply (rule mop_cocc_list_at_impl.refine)
  subgoal
    by (auto simp: read_all_st_def get_occs_list_at_def intro!: ext
      split: isasat_int_splits)
  subgoal
    by (auto simp: get_occs_list_at_impl_def)
  done

lemma get_occs_list_at_alt_def: ‹get_occs_list_at = (λN C D. occs_at_at.XX.XX.mop N (C, D))›
  by (auto simp: occs_at_at.XX.XX.mop_def get_occs_list_at_def mop_cocc_list_at_def read_all_param_adder_ops.mop_def
    read_all_st_def summarize_ASSERT_conv
    mop_cocc_list_length_def split: tuple17.splits intro!: ext)

lemmas [sepref_fr_rules] = occs_at_at.refine
  occs_at_at.mop_refine[unfolded get_occs_list_at_alt_def[symmetric]]

lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  length_occs_impl_def[unfolded read_all_st_code_def]
  length_occs_at_impl_def[unfolded read_all_st_code_def]

lemma mop_arena_promote_st_alt_def:
    ‹mop_arena_promote_st S C = do {
    let (N', S) = extract_arena_wl_heur S;
    let (lcount, S) = extract_lcount_wl_heur S;
    ASSERT(clss_size_lcount lcount ≥ 1);
    let lcount = clss_size_decr_lcount lcount;
    N' ← mop_arena_set_status N' C IRRED;
    RETURN (update_arena_wl_heur N' (update_lcount_wl_heur lcount S))
  }›
  by (auto simp: mop_arena_promote_st_def state_extractors split: isasat_int_splits)

sepref_def mop_arena_promote_st_impl
  is ‹uncurry mop_arena_promote_st›
  :: ‹isasat_bounded_assnd *a sint64_nat_assnk →a isasat_bounded_assn›
  unfolding mop_arena_promote_st_alt_def
  by sepref

sepref_def get_lsize_limit_stats_impl
  is ‹RETURN o get_lsize_limit_stats›
  :: ‹isasat_stats_assnk →a lbd_size_limit_assn›
  unfolding stats_code_unfold
  by sepref

definition get_lsize_limit_stats_st_impl :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹get_lsize_limit_stats_st_impl = read_stats_wl_heur_code get_lsize_limit_stats_impl›

global_interpretation lsize_limit: read_stats_param_adder0 where
  f' = ‹RETURN o get_lsize_limit_stats› and
  f = get_lsize_limit_stats_impl and
  x_assn = ‹uint32_nat_assn ×a sint64_nat_assn› and
  P = ‹λ_. True›
  rewrites ‹read_stats_wl_heur (RETURN o get_lsize_limit_stats) = RETURN o get_lsize_limit_stats_st› and
    ‹read_stats_wl_heur_code get_lsize_limit_stats_impl = get_lsize_limit_stats_st_impl›
  apply unfold_locales
  apply (rule get_lsize_limit_stats_impl.refine[unfolded lbd_size_limit_assn_def]; assumption)
  subgoal by (auto simp: read_all_st_def get_lsize_limit_stats_def get_lsize_limit_stats_def get_lsize_limit_stats_st_def
    intro!: ext
    split: isasat_int_splits)
  subgoal by (auto simp: get_lsize_limit_stats_st_impl_def)
  done

lemmas [sepref_fr_rules] = lsize_limit.refine

lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  get_lsize_limit_stats_st_impl_def[unfolded read_all_st_code_def]


lemma set_stats_size_limit_st_alt_def:
  ‹RETURN ooo set_stats_size_limit_st = (λlbd sze T.
     let (stats, T) = extract_stats_wl_heur T;
         stats = set_stats_size_limit lbd sze stats
     in RETURN (update_stats_wl_heur stats T)
)›
  by (auto simp: set_stats_size_limit_st_def state_extractors split: isasat_int_splits intro!: ext)

sepref_register ‹LSize_Stats :: nat ⇒ nat ⇒ _›
  IsaSAT_Stats_LLVM.update_f set_stats_size_limit_st stats_forward_rounds_st
  incr_purelit_rounds_st

lemma set_stats_size_limit_alt_def:
  ‹RETURN ooo set_stats_size_limit = (λlbd size' stats. RETURN (set_lsize_limit_stats (LSize_Stats lbd size') stats))›
  unfolding set_stats_size_limit_def LSize_Stats_def
  by (auto intro!: ext)

sepref_def set_stats_size_limit_impl
  is ‹uncurry2 (RETURN ooo set_stats_size_limit)›
  :: ‹uint32_nat_assnk *a sint64_nat_assnk *a isasat_stats_assnd →a isasat_stats_assn›
  unfolding set_stats_size_limit_alt_def stats_code_unfold
  by sepref

sepref_def set_stats_size_limit_st_impl
  is ‹uncurry2 (RETURN ooo set_stats_size_limit_st)›
  :: ‹uint32_nat_assnk *a sint64_nat_assnk *a isasat_bounded_assnd →a isasat_bounded_assn›
  unfolding set_stats_size_limit_st_alt_def
  by sepref

lemma stats_forward_rounds_st_alt_def:
  ‹stats_forward_rounds_st S = (case S of IsaSAT M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena occs ⇒ stats_forward_rounds stats)›
  by (cases S) (auto simp: stats_forward_rounds_st_def)

sepref_def stats_forward_rounds_st_impl
  is ‹RETURN o stats_forward_rounds_st›
  :: ‹isasat_bounded_assnk →a word64_assn›
  unfolding stats_forward_rounds_st_alt_def isasat_bounded_assn_def
  by sepref

lemma incr_purelit_rounds_st_alt_def:
  ‹incr_purelit_rounds_st S = (let (stats, S) = extract_stats_wl_heur S; stats = incr_purelit_rounds stats in update_stats_wl_heur stats S)›
  by (auto simp: incr_purelit_rounds_st_def state_extractors split: isasat_int_splits intro!: ext)

sepref_def incr_purelit_rounds_st_impl
  is ‹RETURN o incr_purelit_rounds_st›
  :: ‹isasat_bounded_assnd →a isasat_bounded_assn›
  unfolding incr_purelit_rounds_st_alt_def
  by sepref

end