19package com.microsoft.z3;
21import com.microsoft.z3.enumerations.Z3_lbool;
27@SuppressWarnings(
"unchecked")
34 return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
44 getContext().checkContextMatch(value);
45 Native.solverSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
56 return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
68 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
77 Native.solverPush(getContext().nCtx(), getNativeObject());
96 public void pop(
int n)
98 Native.solverPop(getContext().nCtx(), getNativeObject(), n);
108 Native.solverReset(getContext().nCtx(), getNativeObject());
118 Native.solverInterrupt(getContext().nCtx(), getNativeObject());
128 getContext().checkContextMatch(constraints);
131 Native.solverAssert(getContext().nCtx(), getNativeObject(),
132 a.getNativeObject());
153 getContext().checkContextMatch(constraints);
154 getContext().checkContextMatch(ps);
155 if (constraints.length != ps.length) {
159 for (
int i = 0; i < constraints.length; i++) {
160 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
161 constraints[i].getNativeObject(), ps[i].getNativeObject());
180 getContext().checkContextMatch(constraint);
181 getContext().checkContextMatch(p);
183 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
184 constraint.getNativeObject(), p.getNativeObject());
192 Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
200 Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
211 ASTVector assrts =
new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
212 return assrts.
size();
222 ASTVector assrts =
new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
237 if (assumptions ==
null) {
238 r =
Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
241 r =
Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
242 .nCtx(), getNativeObject(), assumptions.length,
AST
245 return lboolToStatus(r);
255 @SuppressWarnings(
"rawtypes")
258 return check((
Expr[])
null);
279 int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
280 for (
int i = 0; i < result.
size(); ++i) consequences.add((
BoolExpr)
Expr.create(getContext(), result.
get(i).getNativeObject()));
281 return lboolToStatus(
Z3_lbool.fromInt(r));
296 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
300 return new Model(getContext(), x);
315 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
319 return Expr.create(getContext(), x);
335 ASTVector core =
new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
345 return Native.solverGetReasonUnknown(getContext().nCtx(),
354 return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.
nCtx()));
364 return new Statistics(getContext(), Native.solverGetStatistics(
365 getContext().nCtx(), getNativeObject()));
375 .solverToString(getContext().nCtx(), getNativeObject());
394 Solver(Context ctx,
long obj)
401 Native.solverIncRef(getContext().nCtx(), getNativeObject());
405 void addToReferenceQueue() {
406 getContext().getSolverDRQ().storeReference(getContext(),
this);
BoolExpr[] ToBoolExprArray()
Solver translate(Context ctx)
Status getConsequences(Expr< BoolSort >[] assumptions, Expr<?>[] variables, List< Expr< BoolSort > > consequences)
ParamDescrs getParameterDescriptions()
final Status check(Expr< BoolSort >... assumptions)
void assertAndTrack(Expr< BoolSort > constraint, Expr< BoolSort > p)
void setParameters(Params value)
BoolExpr[] getUnsatCore()
BoolExpr[] getAssertions()
void fromString(String str)
Load solver assertions from a string.
void add(Expr< BoolSort >... constraints)
void fromFile(String file)
Load solver assertions from a file.
String getReasonUnknown()
void assertAndTrack(Expr< BoolSort >[] constraints, Expr< BoolSort >[] ps)
Statistics getStatistics()
static long[] arrayToNative(Z3Object[] a)
def String(name, ctx=None)
Z3_lbool
Lifted Boolean type: false, undefined, true.