Public Member Functions | |
String | getHelp () |
ParamDescrs | getParameterDescriptions () |
ApplyResult | apply (Goal g) |
ApplyResult | apply (Goal g, Params p) |
Solver | getSolver () |
Additional Inherited Members | |
Static Public Member Functions inherited from Z3Object | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using
and
. It may also be obtained using the command
in the SMT 2.0 front-end.
Definition at line 27 of file Tactic.java.
|
inline |
Execute the tactic over the goal.
Z3Exception |
Definition at line 50 of file Tactic.java.
Referenced by Tactic.__call__(), and Goal.simplify().
|
inline |
Execute the tactic over the goal.
Z3Exception |
Definition at line 59 of file Tactic.java.
Referenced by Tactic.__call__().
|
inline |
A string containing a description of parameters accepted by the tactic.
Definition at line 31 of file Tactic.java.
|
inline |
Retrieves parameter descriptions for Tactics.
Z3Exception |
Definition at line 40 of file Tactic.java.
|
inline |
Creates a solver that is implemented using the given tactic.
Z3Exception |
Definition at line 79 of file Tactic.java.