Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
Tactic Class Reference
+ Inheritance diagram for Tactic:

Public Member Functions

String getHelp () throws Z3Exception
ParamDescrs getParameterDescriptions () throws Z3Exception
ApplyResult apply (Goal g) throws Z3Exception
ApplyResult apply (Goal g, Params p) throws Z3Exception
Solver getSolver () throws Z3Exception

Package Functions

 Tactic (Context ctx, long obj) throws Z3Exception
 Tactic (Context ctx, String name) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) throws Z3Exception

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 27 of file Tactic.java.


Constructor & Destructor Documentation

Tactic ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 85 of file Tactic.java.

    {
        super(ctx, obj);
    }
Tactic ( Context  ctx,
String  name 
) throws Z3Exception [inline, package]

Definition at line 90 of file Tactic.java.

    {
        super(ctx, Native.mkTactic(ctx.nCtx(), name));
    }

Member Function Documentation

ApplyResult apply ( Goal  g) throws Z3Exception [inline]

Execute the tactic over the goal.

Exceptions:
Z3Exception

Definition at line 51 of file Tactic.java.

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

    {   
        return apply(g, null);
    }
ApplyResult apply ( Goal  g,
Params  p 
) throws Z3Exception [inline]

Execute the tactic over the goal.

Exceptions:
Z3Exception

Definition at line 60 of file Tactic.java.

Referenced by Tactic.__call__().

    {
        getContext().checkContextMatch(g);
        if (p == null)
            return new ApplyResult(getContext(), Native.tacticApply(getContext()
                    .nCtx(), getNativeObject(), g.getNativeObject()));
        else
        {
            getContext().checkContextMatch(p);
            return new ApplyResult(getContext(),
                    Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
                            g.getNativeObject(), p.getNativeObject()));
        }
    }
void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 101 of file Tactic.java.

    {
        getContext().tactic_DRQ().add(o);
        super.decRef(o);
    }
String getHelp ( ) throws Z3Exception [inline]

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

Definition at line 32 of file Tactic.java.

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

Retrieves parameter descriptions for Tactics.

Exceptions:
Z3Exception

Definition at line 41 of file Tactic.java.

    {
        return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
                .nCtx(), getNativeObject()));
    }
Solver getSolver ( ) throws Z3Exception [inline]

Creates a solver that is implemented using the given tactic.

See also:
Context.MkSolver(Tactic)
Exceptions:
Z3Exception

Definition at line 80 of file Tactic.java.

    {
        return getContext().mkSolver(this);
    }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 95 of file Tactic.java.

    {
        getContext().tactic_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines