Theory IsaSAT_Profile_LLVM

theory IsaSAT_Profile_LLVM
  imports IsaSAT_Profile IsaSAT_Literals_LLVM
begin

sepref_register IsaSAT_Profile.start
  IsaSAT_Profile.stop
  IsaSAT_Profile.PROPAGATE
  IsaSAT_Profile.ANALYZE
  IsaSAT_Profile.GC
  IsaSAT_Profile.REDUCE
  IsaSAT_Profile.INITIALISATION
  IsaSAT_Profile.MINIMIZATION

sepref_def start_profile
  is ‹RETURN o IsaSAT_Profile.start›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding IsaSAT_Profile.start_def
  by sepref

sepref_def stop_profile
  is ‹RETURN o IsaSAT_Profile.stop›
  :: ‹word_assn⇧^k →⇩_a unit_assn›
  unfolding IsaSAT_Profile.stop_def
  by sepref


sepref_def IsaSAT_Profile_PROPAGATE
  is ‹uncurry0 (RETURN IsaSAT_Profile.PROPAGATE)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.PROPAGATE_def
  by sepref

sepref_def IsaSAT_Profile_ANALYZE
  is ‹uncurry0 (RETURN IsaSAT_Profile.ANALYZE)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.ANALYZE_def
  by sepref

sepref_def IsaSAT_Profile_GC
  is ‹uncurry0 (RETURN IsaSAT_Profile.GC)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.GC_def
  by sepref

sepref_def IsaSAT_Profile_REDUCE
  is ‹uncurry0 (RETURN IsaSAT_Profile.REDUCE)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.REDUCE_def
  by sepref


sepref_def IsaSAT_Profile_MINIMIZATION
  is ‹uncurry0 (RETURN IsaSAT_Profile.MINIMIZATION)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.MINIMIZATION_def
  by sepref

sepref_def IsaSAT_Profile_INITIALISATION
  is ‹uncurry0 (RETURN IsaSAT_Profile.INITIALISATION)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.INITIALISATION_def
  by sepref

sepref_def IsaSAT_Profile_PURE_LITERAL
  is ‹uncurry0 (RETURN IsaSAT_Profile.PURE_LITERAL)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.PURE_LITERAL_def
  by sepref

sepref_def IsaSAT_Profile_BINARY_SIMP
  is ‹uncurry0 (RETURN IsaSAT_Profile.BINARY_SIMP)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.BINARY_SIMP_def
  by sepref

sepref_def IsaSAT_Profile_SUBSUMPTION
  is ‹uncurry0 (RETURN IsaSAT_Profile.SUBSUMPTION)›
  :: ‹unit_assn⇧^k →⇩_a word_assn›
  unfolding IsaSAT_Profile.SUBSUMPTION_def
  by sepref

experiment begin

export_llvm
    IsaSAT_Profile_PROPAGATE is ‹PROFILE_CST IsaSAT_Profile_PROPAGATE()›
    IsaSAT_Profile_REDUCE is ‹PROFILE_CST IsaSAT_Profile_REDUCE()›
    IsaSAT_Profile_GC is ‹PROFILE_CST IsaSAT_Profile_GC()›
    IsaSAT_Profile_ANALYZE is ‹PROFILE_CST IsaSAT_Profile_ANALYZE()›
    IsaSAT_Profile_MINIMIZATION is ‹PROFILE_CST IsaSAT_Profile_MINIMIZATION()›
    IsaSAT_Profile_INITIALISATION is ‹PROFILE_CST IsaSAT_Profile_INITIALISATION()›
    IsaSAT_Profile_SUBSUMPTION is ‹PROFILE_CST IsaSAT_Profile_SUBSUMPTION()›
    IsaSAT_Profile_PURE_LITERAL is ‹PROFILE_CST IsaSAT_Profile_PURE_LITERAL()›
    IsaSAT_Profile_BINARY_SIMP is ‹PROFILE_CST IsaSAT_Profile_BINARY_SIMP()›
    defines ‹
       typedef int8_t PROFILE_CST;
  ›
end
end