Z3
Data Structures | Public Member Functions | Properties
Tactic Class Reference

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. More...

+ Inheritance diagram for Tactic:

Data Structures

class  DecRefQueue
 DecRefQueue
 

Public Member Functions

ApplyResult Apply (Goal g, Params p=null)
 Execute the tactic over the goal. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

string Help [get]
 A string containing a description of parameters accepted by the tactic. More...
 
ParamDescrs ParameterDescriptions [get]
 Retrieves parameter descriptions for Tactics. More...
 
ApplyResult this[Goal g] [get]
 Apply the tactic to a goal. More...
 
Solver Solver [get]
 Creates a solver that is implemented using the given tactic. More...
 

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 31 of file Tactic.cs.

Member Function Documentation

◆ Apply()

ApplyResult Apply ( Goal  g,
Params  p = null 
)
inline

Execute the tactic over the goal.

Definition at line 58 of file Tactic.cs.

59  {
60  Debug.Assert(g != null);
61 
62  Context.CheckContextMatch(g);
63  if (p == null)
64  return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
65  else
66  {
67  Context.CheckContextMatch(p);
68  return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
69  }
70  }

Referenced by Goal.Simplify().

Property Documentation

◆ Help

string Help
get

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

Definition at line 37 of file Tactic.cs.

37  {
38  get
39  {
40 
41  return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
42  }
43  }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Tactics.

Definition at line 50 of file Tactic.cs.

50  {
51  get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
52  }

◆ Solver

Creates a solver that is implemented using the given tactic.

See also
Context.MkSolver(Tactic)

Definition at line 90 of file Tactic.cs.

90  {
91  get
92  {
93 
94  return Context.MkSolver(this);
95  }
96  }

◆ this[Goal g]

ApplyResult this[Goal g]
get

Apply the tactic to a goal.

Definition at line 76 of file Tactic.cs.

76  {
77  get
78  {
79  Debug.Assert(g != null);
80 
81  return Apply(g);
82  }
83  }
Microsoft.Z3.Tactic.Apply
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:58
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3731