Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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-tactics) in the SMT 2.0 front-end. More...

+ Inheritance diagram for Tactic:

Data Structures

class  DecRefQueue

Public Member Functions

ApplyResult Apply (Goal g, Params p=null)
 Execute the tactic over the goal.

Properties

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

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


Member Function Documentation

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

Execute the tactic over the goal.

Definition at line 60 of file Tactic.cs.

Referenced by Goal.Simplify().

        {
            Contract.Requires(g != null);
            Contract.Ensures(Contract.Result<ApplyResult>() != 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));
            }
        }

Property Documentation

string Help [get]

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

Definition at line 38 of file Tactic.cs.

ParamDescrs ParameterDescriptions [get]

Retrieves parameter descriptions for Tactics.

Definition at line 52 of file Tactic.cs.

Solver Solver [get]

Creates a solver that is implemented using the given tactic.

See also:
Context.MkSolver(Tactic)

Definition at line 94 of file Tactic.cs.

ApplyResult this[Goal g] [get]

Apply the tactic to a goal.

Definition at line 79 of file Tactic.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines