Data Structures | |
class | ModelEvaluationFailedException |
Public Member Functions | |
Expr | getConstInterp (Expr a) throws Z3Exception |
Expr | getConstInterp (FuncDecl f) throws Z3Exception |
FuncInterp | getFuncInterp (FuncDecl f) throws Z3Exception |
int | getNumConsts () throws Z3Exception |
FuncDecl[] | getConstDecls () throws Z3Exception |
int | getNumFuncs () throws Z3Exception |
FuncDecl[] | getFuncDecls () throws Z3Exception |
FuncDecl[] | getDecls () throws Z3Exception |
Expr | eval (Expr t, boolean completion) throws Z3Exception |
Expr | evaluate (Expr t, boolean completion) throws Z3Exception |
int | getNumSorts () throws Z3Exception |
Sort[] | getSorts () throws Z3Exception |
Expr[] | getSortUniverse (Sort s) throws Z3Exception |
String | toString () |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () throws Z3Exception |
A Model contains interpretations (assignments) of constants and functions.
Definition at line 25 of file Model.java.
|
inline |
Evaluates the expression t in the current model.
This function may fail if t contains quantifiers, is partial (MODEL_PARTIAL enabled), or if t is not well-sorted. In this case a
is thrown.
t | An expression |
completion | When this flag is enabled, a model value will be assigned to any constant or function that does not have an interpretation in the model. |
Z3Exception |
Definition at line 211 of file Model.java.
Referenced by Model.evaluate().
|
inline |
|
inline |
The function declarations of the constants in the model.
Z3Exception |
Definition at line 129 of file Model.java.
|
inline |
Retrieves the interpretation (the assignment) of a in the model.
a | A Constant |
Z3Exception |
Definition at line 35 of file Model.java.
|
inline |
Retrieves the interpretation (the assignment) of f in the model.
f | A function declaration of zero arity |
Z3Exception |
Definition at line 49 of file Model.java.
|
inline |
All symbols that have an interpretation in the model.
Z3Exception |
Definition at line 167 of file Model.java.
|
inline |
The function declarations of the function interpretations in the model.
Z3Exception |
Definition at line 152 of file Model.java.
|
inline |
Retrieves the interpretation (the assignment) of a non-constant f in the model.
f | A function declaration of non-zero arity |
Z3Exception |
Definition at line 76 of file Model.java.
|
inline |
The number of constants that have an interpretation in the model.
Definition at line 119 of file Model.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
|
inline |
The number of function interpretations in the model.
Definition at line 142 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.
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 249 of file Model.java.
|
inline |
The finite set of distinct values that represent the interpretation for sort s .
s | An uninterpreted sort |
Z3Exception |
Definition at line 269 of file Model.java.
|
inline |
Conversion of models to strings.
Definition at line 286 of file Model.java.