Data Structures | |
class | ModelEvaluationFailedException |
Public Member Functions | |
Expr | getConstInterp (Expr a) |
Expr | getConstInterp (FuncDecl f) |
FuncInterp | getFuncInterp (FuncDecl f) |
int | getNumConsts () |
FuncDecl[] | getConstDecls () |
int | getNumFuncs () |
FuncDecl[] | getFuncDecls () |
FuncDecl[] | getDecls () |
Expr | eval (Expr t, boolean completion) |
Expr | evaluate (Expr t, boolean completion) |
int | getNumSorts () |
Sort[] | getSorts () |
Expr[] | getSortUniverse (Sort s) |
String | toString () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
A Model contains interpretations (assignments) of constants and functions.
Definition at line 25 of file Model.java.
Evaluates the expression
in the current model. Remarks: This function may fail if
contains quantifiers, is partial (MODEL_PARTIAL enabled), or if
is not well-sorted. In this case a
is thrown.
t | An expression completion |
Z3Exception |
Definition at line 211 of file Model.java.
Referenced by Model.evaluate().
|
inline |
The function declarations of the constants in the model.
Z3Exception |
Definition at line 130 of file Model.java.
Retrieves the interpretation (the assignment) of
in the model.
a | A Constant |
Z3Exception |
Definition at line 36 of file Model.java.
Retrieves the interpretation (the assignment) of
in the model.
f | A function declaration of zero arity |
Z3Exception |
Definition at line 51 of file Model.java.
|
inline |
All symbols that have an interpretation in the model.
Z3Exception |
Definition at line 168 of file Model.java.
|
inline |
The function declarations of the function interpretations in the model.
Z3Exception |
Definition at line 153 of file Model.java.
|
inline |
Retrieves the interpretation (the assignment) of a non-constant
in the model.
f | A function declaration of non-zero arity |
Z3Exception |
Definition at line 77 of file Model.java.
|
inline |
The number of constants that have an interpretation in the model.
Definition at line 120 of file Model.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
|
inline |
The number of function interpretations in the model.
Definition at line 143 of file Model.java.
Referenced by Model.getDecls(), and Model.getFuncDecls().
|
inline |
The number of uninterpreted sorts that the model has an interpretation for.
Definition at line 235 of file Model.java.
Referenced by Model.getSorts().
|
inline |
The uninterpreted sorts that the model has an interpretation for. Remarks: 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.
Z3Exception |
Definition at line 251 of file Model.java.
The finite set of distinct values that represent the interpretation for sort
.
s | An uninterpreted sort |
Z3Exception |
Definition at line 271 of file Model.java.
|
inline |
Conversion of models to strings.
Definition at line 284 of file Model.java.