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  }

Referenced by 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  }

◆ 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  }
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50
com.microsoft.z3.Context.mkSolver
Solver mkSolver()
Definition: Context.java:3089