18 package com.microsoft.z3;
43 .nCtx(), getNativeObject()));
52 return apply(g, null);
61 getContext().checkContextMatch(g);
64 .nCtx(), getNativeObject(), g.getNativeObject()));
67 getContext().checkContextMatch(p);
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() {
101 getContext().
getTacticDRQ().storeReference(getContext(),
this);
static String tacticGetHelp(long a0, long a1)
static long tacticApplyEx(long a0, long a1, long a2, long a3)
IDecRefQueue< Tactic > getTacticDRQ()
ApplyResult apply(Goal g, Params p)
ApplyResult apply(Goal g)
static long tacticGetParamDescrs(long a0, long a1)
static long tacticApply(long a0, long a1, long a2)
ParamDescrs getParameterDescriptions()