18 package com.microsoft.z3;
42 getContext().checkContextMatch(value);
44 value.getNativeObject());
55 getContext().nCtx(), getNativeObject()));
110 getContext().checkContextMatch(constraints);
114 a.getNativeObject());
134 getContext().checkContextMatch(constraints);
135 getContext().checkContextMatch(ps);
136 if (constraints.length != ps.length)
139 for (
int i = 0; i < constraints.length; i++)
141 constraints[i].getNativeObject(), ps[i].getNativeObject());
159 getContext().checkContextMatch(constraint);
160 getContext().checkContextMatch(p);
163 constraint.getNativeObject(), p.getNativeObject());
174 getContext().nCtx(), getNativeObject()));
186 getContext().nCtx(), getNativeObject()));
189 for (
int i = 0; i < n; i++)
190 res[i] =
new BoolExpr(getContext(), ass.get(i).getNativeObject());
202 if (assumptions == null)
207 .nCtx(), getNativeObject(), (
int) assumptions.length,
AST
208 .arrayToNative(assumptions)));
244 return new Model(getContext(), x);
261 return Expr.create(getContext(), x);
276 getContext().nCtx(), getNativeObject()));
279 for (
int i = 0; i < n; i++)
280 res[i] =
Expr.create(getContext(), core.get(i).getNativeObject());
302 getContext().nCtx(), getNativeObject()));
316 return "Z3Exception: " + e.getMessage();
325 void incRef(
long o)
throws Z3Exception
327 getContext().solver_DRQ().incAndClear(getContext(), o);
331 void decRef(
long o)
throws Z3Exception
333 getContext().solver_DRQ().add(o);
ParamDescrs getParameterDescriptions()
static String solverGetReasonUnknown(long a0, long a1)
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
static long solverGetParamDescrs(long a0, long a1)
static long solverGetStatistics(long a0, long a1)
static void solverReset(long a0, long a1)
void setParameters(Params value)
Status check(Expr...assumptions)
void assertAndTrack(BoolExpr constraint, BoolExpr p)
static long solverGetProof(long a0, long a1)
void add(BoolExpr...constraints)
String getReasonUnknown()
static int solverGetNumScopes(long a0, long a1)
static void solverPush(long a0, long a1)
static void solverAssert(long a0, long a1, long a2)
static String solverGetHelp(long a0, long a1)
static String solverToString(long a0, long a1)
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
static void solverSetParams(long a0, long a1, long a2)
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
static long solverGetModel(long a0, long a1)
Statistics getStatistics()
static long solverGetAssertions(long a0, long a1)
static long solverGetUnsatCore(long a0, long a1)
static int solverCheck(long a0, long a1)
static void solverPop(long a0, long a1, int a2)
static final Z3_lbool fromInt(int v)
BoolExpr[] getAssertions()