Previous  Up  Next

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.

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. The Boolean argument indicates whether to apply model completion. When model completion is true it will assign an interpretation for constants and functions that do not have an interpretation in the 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.