Theory IsaSAT_Inprocessing_LLVM

theory IsaSAT_Inprocessing_LLVM
  imports
    IsaSAT_Restart_Inprocessing_Defs
    IsaSAT_Simplify_Units_LLVM
    IsaSAT_Simplify_Binaries_LLVM
    IsaSAT_Simplify_Forward_Subsumption_LLVM
    IsaSAT_Simplify_Pure_Literals_LLVM
begin

sepref_register 0 1

sepref_register mop_arena_update_lit isa_pure_literal_count_occs_wl
    isa_pure_literal_elimination_round_wl incr_purelit_rounds_st


sepref_def should_inprocess_st
  is ‹RETURN o should_inprocess_st›
  :: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
  unfolding should_inprocess_st_def
  by sepref

lemma [simp]: ‹get_clauses_wl_heur (incr_purelit_rounds_st S) = get_clauses_wl_heur S›
  ‹learned_clss_count (incr_purelit_rounds_st S) = learned_clss_count S›
  by (auto simp: incr_purelit_rounds_st_def)


sepref_def isa_pure_literal_elimination_round_wl_code
  is isa_pure_literal_elimination_round_wl
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]⇩a
     isasat_bounded_assn⇧d → word64_assn ×⇩a isasat_bounded_assn›
  unfolding isa_pure_literal_elimination_round_wl_def
  by sepref

lemma schedule_next_pure_lits_st_alt_def:
  ‹schedule_next_pure_lits_st S =
      (let (heur, S) = extract_heur_wl_heur S;
        heur = (schedule_next_pure_lits (heur))in
     update_heur_wl_heur heur S)›
  by (auto simp: schedule_next_pure_lits_st_def state_extractors split: isasat_int_splits
    intro!: ext)

sepref_def schedule_next_pure_lits_st_impl
  is ‹RETURN o schedule_next_pure_lits_st›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  unfolding schedule_next_pure_lits_st_alt_def
  by sepref

sepref_def isa_pure_literal_elimination_wl_code
  is isa_pure_literal_elimination_wl
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]⇩a
     isasat_bounded_assn⇧d → isasat_bounded_assn›
  unfolding isa_pure_literal_elimination_wl_def Let_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_def isa_pure_literal_eliminate_code
  is isa_pure_literal_eliminate
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]⇩a
     isasat_bounded_assn⇧d → isasat_bounded_assn›
  unfolding isa_pure_literal_eliminate_def
  by sepref

(*TODO Move*)
lemmas [llvm_code] = is_NONE_impl_def is_subsumed_impl_def is_strengthened_impl_def
  STRENGTHENED_BY_impl_def SUBSUMED_BY_impl_def NONE_impl_def subsumed_by_impl_def
  strengthened_on_lit_impl_def

lemmas [unfolded inline_direct_return_node_case, llvm_code]  =
  get_occs_list_at_impl_def[unfolded read_all_st_code_def]
(*end move*)
experiment
begin
 export_llvm isa_simplify_clauses_with_unit_st2_code
    isa_simplify_clauses_with_units_st_wl2_code
    isa_deduplicate_binary_clauses_code
    isa_forward_subsumption_all_impl
end

end