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 }