module Model:sig
..end
A Model contains interpretations (assignments) of constants and functions.
type
model
module FuncInterp:sig
..end
val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option
val get_const_interp_e : model -> Expr.expr -> Expr.expr option
val get_func_interp : model ->
FuncDecl.func_decl -> FuncInterp.func_interp option
val get_num_consts : model -> int
val get_const_decls : model -> FuncDecl.func_decl list
val get_num_funcs : model -> int
val get_func_decls : model -> FuncDecl.func_decl list
val get_decls : model -> FuncDecl.func_decl list
val eval : model -> Expr.expr -> bool -> Expr.expr option
This function may fail if the argument contains quantifiers,
is partial (MODEL_PARTIAL enabled), or if it is not well-sorted.
In this case a ModelEvaluationFailedException
is thrown.
val evaluate : model -> Expr.expr -> bool -> Expr.expr option
eval
.val get_num_sorts : model -> int
val get_sorts : model -> Sort.sort list
Z3 also provides an intepretation for uninterpreted sorts used in a formula.
The interpretation for a sort is a finite set of distinct values. We say this finite set is
the "universe" of the sort.
Model.get_num_sorts
Model.sort_universe
val sort_universe : model -> Sort.sort -> Expr.expr list
Model.get_sorts
val to_string : model -> string