19package com.microsoft.z3;
21import com.microsoft.z3.enumerations.Z3_lbool;
42 getContext().checkContextMatch(value);
44 value.getNativeObject());
55 getContext().nCtx(), getNativeObject()));
94 public void pop(
int n)
116 getContext().checkContextMatch(constraints);
120 a.getNativeObject());
141 getContext().checkContextMatch(constraints);
142 getContext().checkContextMatch(ps);
143 if (constraints.length != ps.length) {
147 for (
int i = 0; i < constraints.length; i++) {
149 constraints[i].getNativeObject(), ps[i].getNativeObject());
168 getContext().checkContextMatch(constraint);
169 getContext().checkContextMatch(p);
172 constraint.getNativeObject(), p.getNativeObject());
200 return assrts.
size();
224 if (assumptions ==
null) {
229 .nCtx(), getNativeObject(), assumptions.length,
AST
230 .arrayToNative(assumptions)));
270 return new Model(getContext(), x);
289 return Expr.create(getContext(), x);
335 getContext().nCtx(), getNativeObject()));
355 Native.solverIncRef(getContext().nCtx(), getNativeObject());
359 void addToReferenceQueue() {
BoolExpr[] ToBoolExprArray()
IDecRefQueue< Solver > getSolverDRQ()
void storeReference(Context ctx, T obj)
static long solverGetModel(long a0, long a1)
static int solverCheck(long a0, long a1)
static void solverFromString(long a0, long a1, String a2)
static long solverGetParamDescrs(long a0, long a1)
static void solverFromFile(long a0, long a1, String a2)
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
static long solverGetAssertions(long a0, long a1)
static String solverGetHelp(long a0, long a1)
static void solverPush(long a0, long a1)
static String solverToString(long a0, long a1)
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
static String solverGetReasonUnknown(long a0, long a1)
static long solverTranslate(long a0, long a1, long a2)
static int solverGetNumScopes(long a0, long a1)
static long solverGetUnsatCore(long a0, long a1)
static void solverAssert(long a0, long a1, long a2)
static void solverSetParams(long a0, long a1, long a2)
static long solverGetProof(long a0, long a1)
static void solverPop(long a0, long a1, int a2)
static void solverReset(long a0, long a1)
static long solverGetStatistics(long a0, long a1)
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Solver translate(Context ctx)
ParamDescrs getParameterDescriptions()
void add(BoolExpr... constraints)
void assertAndTrack(BoolExpr constraint, BoolExpr p)
void setParameters(Params value)
BoolExpr[] getUnsatCore()
Status check(Expr... assumptions)
BoolExpr[] getAssertions()
void fromString(String str)
Load solver assertions from a string.
void fromFile(String file)
Load solver assertions from a file.
String getReasonUnknown()
Statistics getStatistics()
static final Z3_lbool fromInt(int v)
def String(name, ctx=None)