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:

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...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object 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.

        {
            Debug.Assert(g != null);
 
            Context.CheckContextMatch(g);
            if (p == null)
                return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
            else
            {
                Context.CheckContextMatch(p);
                return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
            }
        }

Referenced by Goal.Simplify().

Property Documentation

Help

string Help

get

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

Definition at line 36 of file Tactic.cs.

        {
            get
            {
 
                return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
            }
        }

ParameterDescriptions

ParamDescrs ParameterDescriptions

get

Retrieves parameter descriptions for Tactics.

Definition at line 49 of file Tactic.cs.

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

Solver

Solver Solver

get

Creates a solver that is implemented using the given tactic.

See also

Context.MkSolver(Tactic)

Definition at line 89 of file Tactic.cs.

        {
            get
            {
 
                return Context.MkSolver(this);
            }
        }

this[Goal g]

ApplyResult this[Goal g]

get

Apply the tactic to a goal.

Definition at line 75 of file Tactic.cs.

        {
            get
            {
                Debug.Assert(g != null);
 
                return Apply(g);
            }
        }