Theory IsaSAT_Proofs_LLVM

theory IsaSAT_Proofs_LLVM
  imports IsaSAT_Proofs IsaSAT_Setup_LLVM
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN

sepref_def log_literal_impl
  is ‹RETURN o log_literal›
  :: ‹unat_lit_assn⇧^k →⇩_a unit_assn›
  unfolding log_literal_def
  by sepref


sepref_def log_start_new_clause_impl
  is ‹RETURN o log_start_new_clause›
  :: ‹unat64_assn⇧^k →⇩_a unit_assn›
  unfolding log_start_new_clause_def
  by sepref

sepref_def log_start_del_clause_impl
  is ‹RETURN o log_start_del_clause›
  :: ‹unat64_assn⇧^k →⇩_a unit_assn›
  unfolding log_start_del_clause_def
  by sepref

sepref_def log_end_clause_impl
  is ‹RETURN o log_end_clause›
  :: ‹unat64_assn⇧^k →⇩_a unit_assn›
  unfolding log_end_clause_def
  by sepref

sepref_def log_clause_heur_impl
  is ‹uncurry log_clause_heur›
  :: ‹[λ(S, C). length (get_clauses_wl_heur S) ≤ snat64_max]⇩_a isasat_bounded_assn⇧^k *⇩_a snat64_assn⇧^k → unit_assn›
  unfolding log_clause_heur_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref


sepref_def log_new_clause_heur_impl
  is ‹uncurry log_new_clause_heur›
  :: ‹isasat_bounded_assn⇧^k *⇩_a snat64_assn⇧^k →⇩_a unit_assn›
  supply [dest] = isasat_bounded_assn_length_arenaD
  unfolding log_new_clause_heur_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

sepref_def log_del_clause_heur_impl
  is ‹uncurry log_del_clause_heur›
  :: ‹isasat_bounded_assn⇧^k *⇩_a snat64_assn⇧^k →⇩_a unit_assn›
  supply [dest] = isasat_bounded_assn_length_arenaD
  unfolding log_del_clause_heur_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

sepref_register log_del_clause_heur log_new_clause_heur_impl log_unit_clause log_del_binary_clause

sepref_def log_unit_clause_impl
  is ‹RETURN o log_unit_clause›
  :: ‹unat_lit_assn⇧^k →⇩_a unit_assn›
  unfolding log_unit_clause_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

sepref_def log_del_binary_clause_impl
  is ‹uncurry (RETURN oo log_del_binary_clause)›
  ::  ‹unat_lit_assn⇧^k *⇩_a unat_lit_assn⇧^k →⇩_a unit_assn›
  unfolding log_del_binary_clause_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

sepref_def mark_literal_for_unit_deletion_impl
  is ‹RETURN o mark_literal_for_unit_deletion›
  :: ‹unat_lit_assn⇧^k →⇩_a unit_assn›
  unfolding mark_literal_for_unit_deletion_def
  by sepref


sepref_def mark_clause_for_unit_as_unchanged_impl
  is ‹RETURN o mark_clause_for_unit_as_unchanged›
  :: ‹unat64_assn⇧^k →⇩_a unit_assn›
  unfolding mark_clause_for_unit_as_unchanged_def
  by sepref

sepref_def mark_clause_for_unit_as_changed_impl
  is ‹RETURN o mark_clause_for_unit_as_changed›
  :: ‹unat64_assn⇧^k →⇩_a unit_assn›
  unfolding mark_clause_for_unit_as_changed_def
  by sepref

end