18 package com.microsoft.z3;
81 getContext().checkContextMatch(constraints);
131 for (
int i = 0; i < n; i++)
133 .nCtx(), getNativeObject(), i));
173 getNativeObject(), ctx.nCtx()));
186 throw new Z3Exception(
"No subgoals");
218 return "Z3Exception: " + e.getMessage();
227 Goal(Context ctx,
boolean models,
boolean unsatCores,
boolean proofs)
230 super(ctx, Native.mkGoal(ctx.nCtx(), (models) ?
true :
false,
231 (unsatCores) ?
true :
false, (proofs) ?
true :
false));
234 void incRef(
long o)
throws Z3Exception
236 getContext().goal_DRQ().incAndClear(getContext(), o);
240 void decRef(
long o)
throws Z3Exception
242 getContext().goal_DRQ().add(o);
static void goalReset(long a0, long a1)
static boolean goalIsDecidedUnsat(long a0, long a1)
void add(BoolExpr...constraints)
static void goalAssert(long a0, long a1, long a2)
static boolean goalInconsistent(long a0, long a1)
static int goalPrecision(long a0, long a1)
Goal translate(Context ctx)
static long goalTranslate(long a0, long a1, long a2)
static long goalFormula(long a0, long a1, int a2)
static final Z3_goal_prec fromInt(int v)
ApplyResult apply(Goal g)
boolean isOverApproximation()
static int goalNumExprs(long a0, long a1)
static int goalDepth(long a0, long a1)
static String goalToString(long a0, long a1)
boolean isUnderApproximation()
static boolean goalIsDecidedSat(long a0, long a1)
Tactic mkTactic(String name)
static int goalSize(long a0, long a1)
Z3_goal_prec getPrecision()