Public Member Functions | |
String | getHelp () throws Z3Exception |
ParamDescrs | getParameterDescriptions () throws Z3Exception |
ApplyResult | apply (Goal g) throws Z3Exception |
ApplyResult | apply (Goal g, Params p) throws Z3Exception |
Solver | getSolver () throws Z3Exception |
Package Functions | |
Tactic (Context ctx, long obj) throws Z3Exception | |
Tactic (Context ctx, String name) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics
and Context.TacticNames
. It may also be obtained using the command (help-tactics)
in the SMT 2.0 front-end.
Definition at line 27 of file Tactic.java.
Tactic | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 85 of file Tactic.java.
{ super(ctx, obj); }
Tactic | ( | Context | ctx, |
String | name | ||
) | throws Z3Exception [inline, package] |
Definition at line 90 of file Tactic.java.
{ super(ctx, Native.mkTactic(ctx.nCtx(), name)); }
ApplyResult apply | ( | Goal | g | ) | throws Z3Exception [inline] |
Execute the tactic over the goal.
Z3Exception |
Definition at line 51 of file Tactic.java.
Referenced by Tactic.__call__(), and Goal.simplify().
{ return apply(g, null); }
ApplyResult apply | ( | Goal | g, |
Params | p | ||
) | throws Z3Exception [inline] |
Execute the tactic over the goal.
Z3Exception |
Definition at line 60 of file Tactic.java.
Referenced by Tactic.__call__().
{ getContext().checkContextMatch(g); if (p == null) return new ApplyResult(getContext(), Native.tacticApply(getContext() .nCtx(), getNativeObject(), g.getNativeObject())); else { getContext().checkContextMatch(p); return new ApplyResult(getContext(), Native.tacticApplyEx(getContext().nCtx(), getNativeObject(), g.getNativeObject(), p.getNativeObject())); } }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 101 of file Tactic.java.
{ getContext().tactic_DRQ().add(o); super.decRef(o); }
String getHelp | ( | ) | throws Z3Exception [inline] |
A string containing a description of parameters accepted by the tactic.
Definition at line 32 of file Tactic.java.
{ return Native.tacticGetHelp(getContext().nCtx(), getNativeObject()); }
ParamDescrs getParameterDescriptions | ( | ) | throws Z3Exception [inline] |
Retrieves parameter descriptions for Tactics.
Z3Exception |
Definition at line 41 of file Tactic.java.
{ return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext() .nCtx(), getNativeObject())); }
Solver getSolver | ( | ) | throws Z3Exception [inline] |
Creates a solver that is implemented using the given tactic.
Z3Exception |
Definition at line 80 of file Tactic.java.
{ return getContext().mkSolver(this); }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 95 of file Tactic.java.
{ getContext().tactic_DRQ().incAndClear(getContext(), o); super.incRef(o); }