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 -> AST.ast 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.