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 () |
A Model contains interpretations (assignments) of constants and functions.
Definition at line 25 of file Model.java.
|
inline |
The function declarations of the constants in the model.
Z3Exception |
Definition at line 129 of file Model.java.
Retrieves the interpretation (the assignment) of
in the model.
a | A Constant |
Z3Exception |
Definition at line 35 of file Model.java.
Retrieves the interpretation (the assignment) of
in the model.
f | A function declaration of zero arity |
Z3Exception |
Definition at line 50 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
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().