Theory IsaSAT_Profile

theory IsaSAT_Profile
  imports IsaSAT_Literals
begin

chapter ‹Profiling›

text ‹For profiling, we don't do anything except calling some C functions to measure time. As for
printing, the functions to nothing in the refinement and are only removed from the generated code.
The aim is to better understand the behaviour of the generated code and find performance bug.
›
context
begin
  qualified definition start :: ‹8 word ⇒ unit› where ‹start a = ()›
  qualified definition stop :: ‹8 word ⇒ unit› where ‹stop a = ()›
  qualified definition PROPAGATE :: ‹8 word› where ‹PROPAGATE = 0›
  qualified definition ANALYZE :: ‹8 word› where ‹ANALYZE = 1›
  qualified definition GC :: ‹8 word› where ‹GC = 2›
  qualified definition REDUCE :: ‹8 word› where ‹REDUCE = 3›
  qualified definition INITIALISATION :: ‹8 word› where ‹INITIALISATION = 4›
  qualified definition MINIMIZATION :: ‹8 word› where ‹MINIMIZATION = 5›
  qualified definition SUBSUMPTION :: ‹8 word› where ‹SUBSUMPTION = 6›
  qualified definition PURE_LITERAL :: ‹8 word› where ‹PURE_LITERAL = 7›
  qualified definition BINARY_SIMP :: ‹8 word› where ‹BINARY_SIMP = 8›

qualified abbreviation start_propagate :: ‹unit› where
  ‹start_propagate ≡ IsaSAT_Profile.start IsaSAT_Profile.PROPAGATE›
qualified abbreviation stop_propagate :: ‹unit› where
  ‹stop_propagate ≡ IsaSAT_Profile.stop IsaSAT_Profile.PROPAGATE›
  qualified abbreviation start_analyze :: ‹unit› where
  ‹start_analyze ≡ IsaSAT_Profile.start IsaSAT_Profile.ANALYZE›
  qualified abbreviation stop_analyze :: ‹unit› where
  ‹stop_analyze ≡ IsaSAT_Profile.stop IsaSAT_Profile.ANALYZE›
qualified abbreviation start_GC :: ‹unit› where
  ‹start_GC ≡ IsaSAT_Profile.start IsaSAT_Profile.GC›
qualified abbreviation stop_GC :: ‹unit› where
  ‹stop_GC ≡ IsaSAT_Profile.stop IsaSAT_Profile.GC›

qualified abbreviation start_reduce :: ‹unit› where
  ‹start_reduce ≡ IsaSAT_Profile.start IsaSAT_Profile.REDUCE›
qualified abbreviation stop_reduce :: ‹unit› where
  ‹stop_reduce ≡ IsaSAT_Profile.stop IsaSAT_Profile.REDUCE›

qualified abbreviation start_initialisation :: ‹unit› where
  ‹start_initialisation ≡ IsaSAT_Profile.start IsaSAT_Profile.INITIALISATION›
qualified abbreviation stop_initialisation :: ‹unit› where
  ‹stop_initialisation ≡ IsaSAT_Profile.stop IsaSAT_Profile.INITIALISATION›

qualified abbreviation start_minimization :: ‹unit› where
  ‹start_minimization ≡ IsaSAT_Profile.start IsaSAT_Profile.MINIMIZATION›
qualified abbreviation stop_minimization :: ‹unit› where
  ‹stop_minimization ≡ IsaSAT_Profile.stop IsaSAT_Profile.MINIMIZATION›

qualified abbreviation start_subsumption :: ‹unit› where
  ‹start_subsumption ≡ IsaSAT_Profile.start IsaSAT_Profile.SUBSUMPTION›
qualified abbreviation stop_subsumption :: ‹unit› where
  ‹stop_subsumption ≡ IsaSAT_Profile.stop IsaSAT_Profile.SUBSUMPTION›

qualified abbreviation start_binary_simp :: ‹unit› where
  ‹start_binary_simp ≡ IsaSAT_Profile.start IsaSAT_Profile.BINARY_SIMP›
qualified abbreviation stop_binary_simp :: ‹unit› where
  ‹stop_binary_simp ≡ IsaSAT_Profile.stop IsaSAT_Profile.BINARY_SIMP›

qualified abbreviation start_pure_literal :: ‹unit› where
  ‹start_pure_literal ≡ IsaSAT_Profile.start IsaSAT_Profile.PURE_LITERAL›
qualified abbreviation stop_pure_literal :: ‹unit› where
  ‹stop_pure_literal ≡ IsaSAT_Profile.stop IsaSAT_Profile.PURE_LITERAL›

end

end