sig
  type 'a solver
  val mk_solver :
    ?context:SrkZ3.z3_context -> 'a Syntax.context -> 'a SrkZ3.CHC.solver
  val register_relation : 'a SrkZ3.CHC.solver -> Syntax.symbol -> unit
  val add_rule :
    'a SrkZ3.CHC.solver -> 'a Syntax.formula -> 'a Syntax.formula -> unit
  val add : 'a SrkZ3.CHC.solver -> 'a Syntax.formula list -> unit
  val check :
    'a SrkZ3.CHC.solver ->
    'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
  val get_solution :
    'a SrkZ3.CHC.solver -> Syntax.symbol -> 'a Syntax.formula
  val to_string : 'a SrkZ3.CHC.solver -> string
  val push : 'a SrkZ3.CHC.solver -> unit
  val pop : 'a SrkZ3.CHC.solver -> unit
end