sig
  type term
  type formula
  type proof
  type level
  val dummy : Plugin_intf.S.level
  val current_level : unit -> Plugin_intf.S.level
  val assume :
    (Plugin_intf.S.term, Plugin_intf.S.formula, Plugin_intf.S.proof)
    Plugin_intf.slice ->
    (Plugin_intf.S.formula, Plugin_intf.S.proof) Plugin_intf.res
  val if_sat :
    (Plugin_intf.S.term, Plugin_intf.S.formula, Plugin_intf.S.proof)
    Plugin_intf.slice ->
    (Plugin_intf.S.formula, Plugin_intf.S.proof) Plugin_intf.res
  val backtrack : Plugin_intf.S.level -> unit
  val assign : Plugin_intf.S.term -> Plugin_intf.S.term
  val iter_assignable :
    (Plugin_intf.S.term -> unit) -> Plugin_intf.S.formula -> unit
  val eval : Plugin_intf.S.formula -> Plugin_intf.S.term Plugin_intf.eval_res
end