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());
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() {