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