module Interpretation: sig .. end
An interpretation is a mapping from symbols to values. Interpretations
are a collection of concrete bindings (explicit (symbol, value) pairs)
combined with an optional abstract binding (a symbol -> value function
that can only be inspected by calling).
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
An interpretation is a mapping from symbols to values. Interpretations
are a collection of concrete bindings (explicit (symbol, value) pairs)
combined with an optional abstract binding (a symbol -> value function
that can only be inspected by calling).
val pp : Format.formatter -> 'a interpretation -> unit
val empty : 'a Syntax.context -> 'a interpretation
val wrap : ?symbols:Syntax.symbol list ->
'a Syntax.context ->
(Syntax.symbol -> 'a value) ->
'a interpretation
Wrap a function mapping symbols to values in an interpretation. Calls to
this function are cached. Symbols belonging to the optional symbol list
argument are pre-cached.
val add_real : Syntax.symbol ->
QQ.t -> 'a interpretation -> 'a interpretation
val add_bool : Syntax.symbol ->
bool -> 'a interpretation -> 'a interpretation
val add_fun : Syntax.symbol ->
('a, Syntax.typ_fo) Syntax.expr ->
'a interpretation -> 'a interpretation
val add : Syntax.symbol ->
'a value ->
'a interpretation -> 'a interpretation
val real : 'a interpretation -> Syntax.symbol -> QQ.t
val bool : 'a interpretation -> Syntax.symbol -> bool
val value : 'a interpretation -> Syntax.symbol -> 'a value
val enum : 'a interpretation ->
(Syntax.symbol *
[ `Bool of bool | `Fun of ('a, Syntax.typ_fo) Syntax.expr | `Real of QQ.t ])
BatEnum.t
Enumerate the concrete bindings in an interpretation.
val substitute : 'a interpretation ->
('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
Replace constant symbols by their interpretations within an expression. A
constant symbol that is not defined within the interpretation is not
replaced.
val evaluate_term : 'a interpretation ->
?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t -> 'a Syntax.term -> QQ.t
val evaluate_formula : 'a interpretation ->
?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t ->
'a Syntax.formula -> bool
val get_context : 'a interpretation -> 'a Syntax.context
val select_implicant : 'a interpretation ->
?env:[ `Bool of bool | `Real of QQ.t ] Syntax.Env.t ->
'a Syntax.formula -> 'a Syntax.formula list option
select_implicant srk m ?env phi selects an implicant I of phi such
that m,?env |= I |= phi. The implicant I is a list of atomic
formulas, which can be destructed using destruct_atom.
val select_ite : 'a 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 ] ]