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

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
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

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

Definition at line 27 of file Tactic.java.

Member Function Documentation

ApplyResult apply ( Goal  g) throws Z3Exception
inline

Execute the tactic over the goal.

Exceptions
Z3Exception

Definition at line 51 of file Tactic.java.

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

52  {
53  return apply(g, null);
54  }
ApplyResult apply(Goal g)
Definition: Tactic.java:51
ApplyResult apply ( Goal  g,
Params  p 
) throws Z3Exception
inline

Execute the tactic over the goal.

Exceptions
Z3Exception

Definition at line 60 of file Tactic.java.

Referenced by Tactic.__call__().

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

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

Definition at line 32 of file Tactic.java.

33  {
34  return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
35  }
ParamDescrs getParameterDescriptions ( ) throws Z3Exception
inline

Retrieves parameter descriptions for Tactics.

Exceptions
Z3Exception

Definition at line 41 of file Tactic.java.

42  {
43  return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
44  .nCtx(), getNativeObject()));
45  }
Solver getSolver ( ) throws Z3Exception
inline

Creates a solver that is implemented using the given tactic.

See also
Context.MkSolver(Tactic)
Exceptions
Z3Exception

Definition at line 80 of file Tactic.java.

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