Data Structures | |
class | Entry |
Public Member Functions | |
int | getNumEntries () |
Entry[] | getEntries () |
Expr | getElse () |
int | getArity () |
String | toString () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.
Definition at line 25 of file FuncInterp.java.
|
inline |
The arity of the function interpretation
Z3Exception | on error |
Definition at line 151 of file FuncInterp.java.
|
inline |
The (symbolic) `else' value of the function interpretation.
Z3Exception | |
Z3Exception | on error |
Definition at line 140 of file FuncInterp.java.
Referenced by FuncInterp.toString().
|
inline |
The entries in the function interpretation
Z3Exception | |
Z3Exception | on error |
Definition at line 123 of file FuncInterp.java.
Referenced by FuncInterp.toString().
|
inline |
The number of entries in the function interpretation.
Z3Exception | on error |
Definition at line 112 of file FuncInterp.java.
Referenced by FuncInterp.getEntries().
|
inline |
A string representation of the function interpretation.
Definition at line 159 of file FuncInterp.java.