19 package com.microsoft.z3;
42 getContext().checkContextMatch(value);
44 value.getNativeObject());
55 getContext().nCtx(), getNativeObject()));
94 public void pop(
int n)
116 getContext().checkContextMatch(constraints);
120 a.getNativeObject());
157 getContext().checkContextMatch(constraints);
158 getContext().checkContextMatch(ps);
159 if (constraints.length != ps.length) {
163 for (
int i = 0; i < constraints.length; i++) {
165 constraints[i].getNativeObject(), ps[i].getNativeObject());
184 getContext().checkContextMatch(constraint);
185 getContext().checkContextMatch(p);
188 constraint.getNativeObject(), p.getNativeObject());
199 return assrts.
size();
223 if (assumptions == null) {
228 .nCtx(), getNativeObject(), assumptions.length,
AST 229 .arrayToNative(assumptions)));
269 return new Model(getContext(), x);
288 return Expr.create(getContext(), x);
334 getContext().nCtx(), getNativeObject()));
354 Native.solverIncRef(getContext().nCtx(), getNativeObject());
358 void addToReferenceQueue() {
ParamDescrs getParameterDescriptions()
static String solverGetReasonUnknown(long a0, long a1)
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Solver translate(Context ctx)
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)
static void solverFromString(long a0, long a1, String a2)
void assertAndTrack(BoolExpr constraint, BoolExpr p)
static long solverGetProof(long a0, long a1)
BoolExpr [] ToBoolExprArray()
static long solverTranslate(long a0, long a1, long a2)
void storeReference(Context ctx, T obj)
String getReasonUnknown()
static int solverGetNumScopes(long a0, long a1)
void fromString(String str)
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)
IDecRefQueue< Solver > getSolverDRQ()
Status check(Expr... assumptions)
static void solverSetParams(long a0, long a1, long a2)
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
void add(BoolExpr... constraints)
void fromFile(String file)
BoolExpr [] getUnsatCore()
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 void solverFromFile(long a0, long a1, String a2)
def String(name, ctx=None)
static final Z3_lbool fromInt(int v)
BoolExpr [] getAssertions()