Z3
src/api/java/Tactic.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00027 public class Tactic extends Z3Object
00028 {
00032     public String getHelp() throws Z3Exception
00033     {
00034         return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
00035     }
00036 
00041     public ParamDescrs getParameterDescriptions() throws Z3Exception
00042     {
00043         return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
00044                 .nCtx(), getNativeObject()));
00045     }
00046 
00051     public ApplyResult apply(Goal g) throws Z3Exception
00052     {   
00053         return apply(g, null);
00054     }
00055 
00060     public ApplyResult apply(Goal g, Params p) throws Z3Exception
00061     {
00062         getContext().checkContextMatch(g);
00063         if (p == null)
00064             return new ApplyResult(getContext(), Native.tacticApply(getContext()
00065                     .nCtx(), getNativeObject(), g.getNativeObject()));
00066         else
00067         {
00068             getContext().checkContextMatch(p);
00069             return new ApplyResult(getContext(),
00070                     Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
00071                             g.getNativeObject(), p.getNativeObject()));
00072         }
00073     }
00074 
00080     public Solver getSolver() throws Z3Exception
00081     {
00082         return getContext().mkSolver(this);
00083     }
00084 
00085     Tactic(Context ctx, long obj) throws Z3Exception
00086     {
00087         super(ctx, obj);
00088     }
00089 
00090     Tactic(Context ctx, String name) throws Z3Exception
00091     {
00092         super(ctx, Native.mkTactic(ctx.nCtx(), name));
00093     }
00094 
00095     void incRef(long o) throws Z3Exception
00096     {
00097         getContext().tactic_DRQ().incAndClear(getContext(), o);
00098         super.incRef(o);
00099     }
00100 
00101     void decRef(long o) throws Z3Exception
00102     {
00103         getContext().tactic_DRQ().add(o);
00104         super.decRef(o);
00105     }
00106 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines