18package com.microsoft.z3;
33 return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
42 return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
43 .nCtx(), getNativeObject()));
52 return apply(g,
null);
61 getContext().checkContextMatch(g);
63 return new ApplyResult(getContext(), Native.tacticApply(getContext()
64 .nCtx(), getNativeObject(), g.getNativeObject()));
67 getContext().checkContextMatch(p);
69 Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
70 g.getNativeObject(), p.getNativeObject()));
89 Tactic(Context ctx,
String name)
91 super(ctx, Native.mkTactic(ctx.nCtx(), name));
96 Native.tacticIncRef(getContext().nCtx(), getNativeObject());
100 void addToReferenceQueue() {
IDecRefQueue< Tactic > getTacticDRQ()
void storeReference(Context ctx, T obj)
ParamDescrs getParameterDescriptions()
ApplyResult apply(Goal g)
ApplyResult apply(Goal g, Params p)
def String(name, ctx=None)