Z3
Data Structures | 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 29 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 52 of file Tactic.java.

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

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

◆ apply() [2/2]

ApplyResult apply ( Goal  g,
Params  p 
)
inline

Execute the tactic over the goal.

Exceptions
Z3Exception

Definition at line 61 of file Tactic.java.

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

Referenced by Tactic.__call__().

◆ getHelp()

String getHelp ( )
inline

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

Definition at line 33 of file Tactic.java.

34  {
35  return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
36  }

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for Tactics.

Exceptions
Z3Exception

Definition at line 42 of file Tactic.java.

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

◆ getSolver()

Solver getSolver ( )
inline

Creates a solver that is implemented using the given tactic.

See also
Context::mkSolver(Tactic)
Exceptions
Z3Exception

Definition at line 81 of file Tactic.java.

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