Theory IsaSAT_Restart_LLVM

theory IsaSAT_Restart_LLVM
  imports IsaSAT_Restart_Simp_Defs IsaSAT_Propagate_Conflict_LLVM IsaSAT_Restart_Heuristics_LLVM
    (*TODO: why do we need IsaSAT_Propagate_Conflict_LLVM here?*)
begin

sepref_register update_all_phases

sepref_def update_all_phases_impl
  is ‹update_all_phases›
  :: ‹isasat_bounded_assnd →a isasat_bounded_assn›
  unfolding update_all_phases_def
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_register mark_to_delete_clauses_wl_D_heur


sepref_register delete_index_and_swap mop_mark_garbage_heur mop_mark_garbage_heur3
  mop_access_lit_in_clauses_heur

(*TODO deduplicate*)
lemma [def_pat_rules]: ‹get_the_propagation_reason_heur ≡ get_the_propagation_reason_pol_st›
proof -
  have ‹get_the_propagation_reason_heur = get_the_propagation_reason_pol_st›
    by (auto intro!: ext simp: get_the_propagation_reason_pol_st_def
      get_the_propagation_reason_heur_def)
  then show  ‹get_the_propagation_reason_heur ≡ get_the_propagation_reason_pol_st›
   by auto
qed

sepref_def mark_to_delete_clauses_wl_D_heur_fast_impl
  is ‹mark_to_delete_clauses_wl_D_heur›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max]a isasat_bounded_assnd → isasat_bounded_assn›
  unfolding mark_to_delete_clauses_wl_D_heur_def
    access_tvdom_at_def[symmetric] length_tvdom_def[symmetric]
    get_the_propagation_reason_heur_def[symmetric]
    clause_is_learned_heur_def[symmetric]
    clause_lbd_heur_def[symmetric]
    access_length_heur_def[symmetric]
    mark_to_delete_clauses_wl_D_heur_is_Some_iff
    marked_as_used_st_def[symmetric] if_conn(4)
    fold_tuple_optimizations
    mop_arena_lbd_st_def[symmetric]
    mop_marked_as_used_st_def[symmetric]
    mop_arena_status_st_def[symmetric]
    mop_arena_length_st_def[symmetric]
  supply [[goals_limit = 1]] of_nat_snat[sepref_import_param]
      length_tvdom_def[symmetric, simp] access_tvdom_at_def[simp]
  apply (rewrite in ‹let _ = ⌑ in _› short_circuit_conv)+
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_def mark_to_delete_clauses_GC_wl_D_heur_heur_fast_impl
  is ‹mark_to_delete_clauses_GC_wl_D_heur›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max]a isasat_bounded_assnd → isasat_bounded_assn›
  unfolding mark_to_delete_clauses_GC_wl_D_heur_def
    access_tvdom_at_def[symmetric] length_tvdom_def[symmetric]
    get_the_propagation_reason_heur_def[symmetric]
    clause_is_learned_heur_def[symmetric]
    clause_lbd_heur_def[symmetric]
    access_length_heur_def[symmetric]
    mark_to_delete_clauses_wl_D_heur_is_Some_iff
    marked_as_used_st_def[symmetric] if_conn(4)
    fold_tuple_optimizations
    mop_arena_lbd_st_def[symmetric]
    mop_marked_as_used_st_def[symmetric]
    mop_arena_status_st_def[symmetric]
    mop_arena_length_st_def[symmetric]
  supply [[goals_limit = 1]] of_nat_snat[sepref_import_param]
      length_avdom_def[symmetric, simp] access_avdom_at_def[simp]
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

definition isasat_fast_bound where
  ‹isasat_fast_bound = snat64_max - (unat32_max div 2 + MAX_HEADER_SIZE + 1)›

lemma isasat_fast_bound_alt_def:
  ‹isasat_fast_bound = 9223372034707292156›
  ‹unat64_max = 18446744073709551615›
  by (auto simp: br_def isasat_fast_bound_def
     snat64_max_def unat32_max_def unat64_max_def)


lemma isasat_fast_alt_def: ‹isasat_fast S = (length_clauses_heur S ≤ 9223372034707292156 ∧
   clss_size_lcount (get_learned_count S) +
    clss_size_lcountUE (get_learned_count S) + clss_size_lcountUS (get_learned_count S) +
      clss_size_lcountU0 (get_learned_count S)+
      clss_size_lcountUEk (get_learned_count S) < 18446744073709551615)›
  by (cases S; auto simp: isasat_fast_def snat64_max_def unat32_max_def length_clauses_heur_def
    unat64_max_def learned_clss_count_def)

sepref_register isasat_fast

(*TODO Move*)
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)

sepref_def isasat_fast_code
  is ‹RETURN o isasat_fast›
  :: ‹[λS. isasat_fast_relaxed S]a isasat_bounded_assnk → bool1_assn›
  unfolding isasat_fast_alt_def isasat_fast_relaxed_def
  apply (rewrite at ‹_ < ⌑› unat_const_fold[where 'a=64])+
  unfolding all_count_learned[symmetric] clss_size_allcount_alt_def
  supply [[goals_limit = 1]]
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_register should_inprocess_st

end