sig
  exception Divide_by_zero
  type 'a value =
      [ `Bool of bool
      | `Fun of ('a, Syntax.typ_fo) Syntax.expr
      | `Real of QQ.t ]
  type 'a interpretation
  val pp : Format.formatter -> 'a Interpretation.interpretation -> unit
  val empty : 'a Syntax.context -> 'a Interpretation.interpretation
  val wrap :
    ?symbols:Syntax.symbol list ->
    'a Syntax.context ->
    (Syntax.symbol -> 'a Interpretation.value) ->
    'a Interpretation.interpretation
  val add_real :
    Syntax.symbol ->
    QQ.t ->
    'a Interpretation.interpretation -> 'a Interpretation.interpretation
  val add_bool :
    Syntax.symbol ->
    bool ->
    'a Interpretation.interpretation -> 'a Interpretation.interpretation
  val add_fun :
    Syntax.symbol ->
    ('a, Syntax.typ_fo) Syntax.expr ->
    'a Interpretation.interpretation -> 'a Interpretation.interpretation
  val add :
    Syntax.symbol ->
    'a Interpretation.value ->
    'a Interpretation.interpretation -> 'a Interpretation.interpretation
  val real : 'a Interpretation.interpretation -> Syntax.symbol -> QQ.t
  val bool : 'a Interpretation.interpretation -> Syntax.symbol -> bool
  val value :
    'a Interpretation.interpretation ->
    Syntax.symbol -> 'a Interpretation.value
  val enum :
    'a Interpretation.interpretation ->
    (Syntax.symbol *
     [ `Bool of bool
     | `Fun of ('a, Syntax.typ_fo) Syntax.expr
     | `Real of QQ.t ])
    BatEnum.t
  val substitute :
    'a Interpretation.interpretation ->
    ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
  val evaluate_term :
    'a Interpretation.interpretation ->
    ?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t ->
    'a Syntax.term -> QQ.t
  val evaluate_formula :
    'a Interpretation.interpretation ->
    ?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t ->
    'a Syntax.formula -> bool
  val get_context : 'a Interpretation.interpretation -> 'a Syntax.context
  val select_implicant :
    'a Interpretation.interpretation ->
    ?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t ->
    'a Syntax.formula -> 'a Syntax.formula list option
  val select_ite :
    'a Interpretation.interpretation ->
    ?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t ->
    ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr * 'a Syntax.formula list
  val destruct_atom :
    'a Syntax.context ->
    'a Syntax.formula ->
    [ `Comparison of [ `Eq | `Leq | `Lt ] * 'a Syntax.term * 'a Syntax.term
    | `Literal of [ `Neg | `Pos ] * [ `Const of Syntax.symbol | `Var of int ] ]
end