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);
147 .nCtx(), getNativeObject(),
AST.arrayLength(relations),
AST
148 .arrayToNative(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());
244 getNativeObject(), f.getNativeObject(),
AST.arrayLength(kinds),
245 Symbol.arrayToNative(kinds));
256 AST.arrayLength(queries),
AST.arrayToNative(queries));
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) { }