18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_goal_prec;
81 getContext().checkContextMatch(constraints);
132 for (
int i = 0; i < n; i++)
172 getNativeObject(), ctx.nCtx()));
224 return getContext().
mkTrue();
237 Goal(Context ctx,
boolean models,
boolean unsatCores,
boolean proofs) {
238 super(ctx, Native.mkGoal(ctx.nCtx(), (models),
239 (unsatCores), (proofs)));
251 return new Model(getContext(),
263 void addToReferenceQueue() {
IDecRefQueue< Goal > getGoalDRQ()
BoolExpr mkAnd(BoolExpr... t)
Tactic mkTactic(String name)
boolean isOverApproximation()
boolean isUnderApproximation()
Z3_goal_prec getPrecision()
Goal translate(Context ctx)
Model convertModel(Model m)
void add(BoolExpr ... constraints)
void storeReference(Context ctx, T obj)
static boolean goalIsDecidedSat(long a0, long a1)
static boolean goalInconsistent(long a0, long a1)
static void goalReset(long a0, long a1)
static void goalAssert(long a0, long a1, long a2)
static int goalSize(long a0, long a1)
static void goalIncRef(long a0, long a1)
static String goalToString(long a0, long a1)
static int goalDepth(long a0, long a1)
static long goalFormula(long a0, long a1, int a2)
static long goalConvertModel(long a0, long a1, long a2)
static int goalNumExprs(long a0, long a1)
static long goalTranslate(long a0, long a1, long a2)
static int goalPrecision(long a0, long a1)
static boolean goalIsDecidedUnsat(long a0, long a1)
ApplyResult apply(Goal g)
static final Z3_goal_prec fromInt(int v)
def String(name, ctx=None)