Data Structures | |
class | ModelEvaluationFailedException |
Public Member Functions | |
int | getNumConsts () |
FuncDecl<?>[] | getConstDecls () |
int | getNumFuncs () |
FuncDecl<?>[] | getFuncDecls () |
FuncDecl<?>[] | getDecls () |
int | getNumSorts () |
Sort[] | getSorts () |
String | toString () |
Additional Inherited Members | |
Static Public Member Functions inherited from Z3Object | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
A Model contains interpretations (assignments) of constants and functions.
Definition at line 26 of file Model.java.
|
inline |
The function declarations of the constants in the model.
Z3Exception |
Definition at line 127 of file Model.java.
|
inline |
All symbols that have an interpretation in the model.
Z3Exception |
Definition at line 165 of file Model.java.
|
inline |
The function declarations of the function interpretations in the model.
Z3Exception |
Definition at line 150 of file Model.java.
|
inline |
The number of constants that have an interpretation in the model.
Definition at line 117 of file Model.java.
|
inline |
The number of function interpretations in the model.
Definition at line 140 of file Model.java.
|
inline |
The number of uninterpreted sorts that the model has an interpretation for.
Definition at line 233 of file Model.java.
|
inline |
The uninterpreted sorts that the model has an interpretation for. Remarks: 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.
Z3Exception |
Definition at line 249 of file Model.java.
|
inline |
Conversion of models to strings.
Definition at line 283 of file Model.java.