Module Z3.Model

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.
Returns An expression if the function has an interpretation in the model, null otherwise.
val get_const_interp_e : model -> Expr.expr -> Expr.expr option
Retrieves the interpretation (the assignment) of an expression in the model.
Returns An expression if the constant has an interpretation in the model, null otherwise.
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.
Returns A FunctionInterpretation if the function has an interpretation in the model, null otherwise.
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 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
The finite set of distinct values that represent the interpretation of a sort. Model.get_sorts
Returns A list of expressions, where each is an element of the universe of the sort
val to_string : model -> string
Conversion of models to strings.
Returns A string representation of the model.