sig
  module Solver :
    sig
      type 'a t
      val add : 'a Smt.Solver.t -> 'a Syntax.formula list -> unit
      val push : 'a Smt.Solver.t -> unit
      val pop : 'a Smt.Solver.t -> int -> unit
      val reset : 'a Smt.Solver.t -> unit
      val check :
        'a Smt.Solver.t ->
        'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
      val to_string : 'a Smt.Solver.t -> string
      val get_model :
        ?symbols:Syntax.symbol list ->
        'a Smt.Solver.t ->
        [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
      val get_concrete_model :
        'a Smt.Solver.t ->
        Syntax.symbol list ->
        [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
      val get_unsat_core :
        'a Smt.Solver.t ->
        'a Syntax.formula list ->
        [ `Sat | `Unknown | `Unsat of 'a Syntax.formula list ]
    end
  val mk_solver : ?theory:string -> 'a Syntax.context -> 'a Smt.Solver.t
  val get_model :
    ?symbols:Syntax.symbol list ->
    'a Syntax.context ->
    'a Syntax.formula ->
    [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
  val get_concrete_model :
    'a Syntax.context ->
    Syntax.symbol list ->
    'a Syntax.formula ->
    [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
  val is_sat :
    'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
  val entails :
    'a Syntax.context ->
    'a Syntax.formula -> 'a Syntax.formula -> [ `No | `Unknown | `Yes ]
  val equiv :
    'a Syntax.context ->
    'a Syntax.formula -> 'a Syntax.formula -> [ `No | `Unknown | `Yes ]
  val affine_interpretation :
    'a Syntax.context ->
    'a Interpretation.interpretation ->
    'a Syntax.formula ->
    [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
end