Data Structures | |
class | Entry |
Public Member Functions | |
int | getNumEntries () throws Z3Exception |
Entry[] | getEntries () throws Z3Exception |
Expr | getElse () throws Z3Exception |
int | getArity () throws Z3Exception |
String | toString () |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () throws Z3Exception |
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
Definition at line 141 of file FuncInterp.java.
|
inline |
The (symbolic) `else' value of the function interpretation.
Z3Exception |
Definition at line 132 of file FuncInterp.java.
Referenced by FuncInterp.toString().
|
inline |
The entries in the function interpretation
Z3Exception |
Definition at line 117 of file FuncInterp.java.
Referenced by FuncInterp.toString().
|
inline |
The number of entries in the function interpretation.
Definition at line 107 of file FuncInterp.java.
Referenced by FuncInterp.getEntries().
|
inline |
A string representation of the function interpretation.
Definition at line 149 of file FuncInterp.java.