18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_goal_prec;
37 return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
82 getContext().checkContextMatch(constraints);
85 Native.goalAssert(getContext().nCtx(), getNativeObject(),
95 return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
105 return Native.goalDepth(getContext().nCtx(), getNativeObject());
113 Native.goalReset(getContext().nCtx(), getNativeObject());
121 return Native.goalSize(getContext().nCtx(), getNativeObject());
133 for (
int i = 0; i < n; i++)
134 res[i] = (
BoolExpr)
Expr.create(getContext(), Native.goalFormula(getContext().nCtx(), getNativeObject(), i));
143 return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
152 return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
162 .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
172 return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
173 getNativeObject(), ctx.
nCtx()));
214 return Native.goalToString(getContext().nCtx(), getNativeObject());
225 return getContext().
mkTrue();
238 Goal(Context ctx,
boolean models,
boolean unsatCores,
boolean proofs) {
239 super(ctx, Native.mkGoal(ctx.nCtx(), (models),
240 (unsatCores), (proofs)));
252 return new Model(getContext(),
253 Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
260 Native.goalIncRef(getContext().nCtx(), getNativeObject());
264 void addToReferenceQueue() {
IDecRefQueue< Goal > getGoalDRQ()
Tactic mkTactic(String name)
final BoolExpr mkAnd(Expr< BoolSort >... t)
boolean isOverApproximation()
boolean isUnderApproximation()
Z3_goal_prec getPrecision()
final void add(Expr< BoolSort >... constraints)
Goal translate(Context ctx)
Model convertModel(Model m)
void storeReference(Context ctx, T obj)
ApplyResult apply(Goal g)
def String(name, ctx=None)
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...