19 package com.microsoft.z3;
43 getContext().checkContextMatch(value);
45 value.getNativeObject());
56 getContext().nCtx(), getNativeObject()));
95 public void pop(
int n)
127 getContext().checkContextMatch(constraints);
131 a.getNativeObject());
152 getContext().checkContextMatch(constraints);
153 getContext().checkContextMatch(ps);
154 if (constraints.length != ps.length) {
158 for (
int i = 0; i < constraints.length; i++) {
160 constraints[i].getNativeObject(), ps[i].getNativeObject());
179 getContext().checkContextMatch(constraint);
180 getContext().checkContextMatch(p);
183 constraint.getNativeObject(), p.getNativeObject());
211 return assrts.
size();
235 if (assumptions ==
null) {
240 .nCtx(), getNativeObject(), assumptions.length,
AST
243 return lboolToStatus(r);
275 for (
Expr v : variables) vars.
push(v);
276 int r =
Native.
solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
277 for (
int i = 0; i < result.
size(); ++i) consequences.add((
BoolExpr)
Expr.create(getContext(), result.
get(i).getNativeObject()));
297 return new Model(getContext(), x);
316 return Expr.create(getContext(), x);
362 getContext().nCtx(), getNativeObject()));
391 Solver(Context ctx,
long obj)
398 Native.solverIncRef(getContext().nCtx(), getNativeObject());
402 void addToReferenceQueue() {