Z3
Public Member Functions
Tactic Class Reference
+ Inheritance diagram for Tactic:

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)
 

Detailed Description

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-tactic) in the SMT 2.0 front-end.

Definition at line 27 of file Tactic.java.

Member Function Documentation

◆ apply() [1/2]

ApplyResult apply ( Goal  g)
inline

Execute the tactic over the goal.

Exceptions
Z3Exception

Definition at line 50 of file Tactic.java.

51 {
52 return apply(g, null);
53 }
ApplyResult apply(Goal g)
Definition: Tactic.java:50

Referenced by Tactic.__call__(), Tactic.apply(), and Goal.simplify().

◆ apply() [2/2]

ApplyResult apply ( Goal  g,
Params  p 
)
inline

Execute the tactic over the goal.

Exceptions
Z3Exception

Definition at line 59 of file Tactic.java.

60 {
61 getContext().checkContextMatch(g);
62 if (p == null)
63 return new ApplyResult(getContext(), Native.tacticApply(getContext()
64 .nCtx(), getNativeObject(), g.getNativeObject()));
65 else
66 {
67 getContext().checkContextMatch(p);
68 return new ApplyResult(getContext(),
69 Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
70 g.getNativeObject(), p.getNativeObject()));
71 }
72 }

Referenced by Tactic.__call__().

◆ getHelp()

String getHelp ( )
inline

A string containing a description of parameters accepted by the tactic.

Definition at line 31 of file Tactic.java.

32 {
33 return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
34 }

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for Tactics.

Exceptions
Z3Exception

Definition at line 40 of file Tactic.java.

41 {
42 return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
43 .nCtx(), getNativeObject()));
44 }

◆ getSolver()

Solver getSolver ( )
inline

Creates a solver that is implemented using the given tactic.

See also
Context::mkSolver(Tactic)
Exceptions
Z3Exception

Definition at line 79 of file Tactic.java.

80 {
81 return getContext().mkSolver(this);
82 }