18 package com.microsoft.z3;
44 getContext().checkContextMatch(value);
46 value.getNativeObject());
57 getContext().nCtx(), getNativeObject()));
67 getContext().checkContextMatch(constraints);
83 getContext().checkContextMatch(f);
96 getContext().checkContextMatch(rule);
98 rule.getNativeObject(),
AST.getNativeObject(name));
107 getContext().checkContextMatch(pred);
109 pred.getNativeObject(), args.length, args);
122 getContext().checkContextMatch(
query);
124 getNativeObject(),
query.getNativeObject()));
145 getContext().checkContextMatch(relations);
168 getContext().checkContextMatch(rule);
170 rule.getNativeObject(),
AST.getNativeObject(name));
182 return (ans == 0) ? null :
Expr.create(getContext(), ans);
200 predicate.getNativeObject());
211 getNativeObject(), level, predicate.getNativeObject());
212 return (res == 0) ? null :
Expr.create(getContext(), res);
223 predicate.getNativeObject(), property.getNativeObject());
289 getContext().nCtx(), getNativeObject()));
320 Fixedpoint(Context ctx)
322 super(ctx, Native.mkFixedpoint(ctx.nCtx()));
327 Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
331 void addToReferenceQueue() {
336 void checkNativeObject(
long obj) { }