module Model:sig
..end
Models
A Model contains interpretations (assignments) of constants and functions.
type
model
module FuncInterp:sig
..end
Function interpretations
val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option
Retrieves the interpretation (the assignment) of a func_decl in the model.
val get_const_interp_e : model -> Expr.expr -> Expr.expr option
Retrieves the interpretation (the assignment) of an expression in the model.
val get_func_interp : model ->
FuncDecl.func_decl -> FuncInterp.func_interp option
Retrieves the interpretation (the assignment) of a non-constant func_decl in the model.
val get_num_consts : model -> int
The number of constant interpretations in the model.
val get_const_decls : model -> FuncDecl.func_decl list
The function declarations of the constants in the model.
val get_num_funcs : model -> int
The number of function interpretations in the model.
val get_func_decls : model -> FuncDecl.func_decl list
The function declarations of the function interpretations in the model.
val get_decls : model -> FuncDecl.func_decl list
All symbols that have an interpretation in the model.
val eval : model -> Expr.expr -> bool -> Expr.expr option
Evaluates an expression in the current model.
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
Alias for eval
.
val get_num_sorts : model -> int
The number of uninterpreted sorts that the model has an interpretation for.
val get_sorts : model -> Sort.sort list
The uninterpreted sorts that the model has an interpretation for.
Z3 also provides an interpretation 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
The finite set of distinct values that represent the interpretation of a sort.
Model.get_sorts
val to_string : model -> string
Conversion of models to strings.