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));
108 getContext().checkContextMatch(pred);
110 pred.getNativeObject(), (int) args.length, args);
125 getContext().checkContextMatch(
query);
127 getNativeObject(),
query.getNativeObject()));
150 getContext().checkContextMatch(relations);
152 .nCtx(), getNativeObject(),
AST.arrayLength(relations),
AST
153 .arrayToNative(relations)));
191 getContext().checkContextMatch(rule);
193 rule.getNativeObject(),
AST.getNativeObject(name));
205 return (ans == 0) ? null :
Expr.create(getContext(), ans);
224 predicate.getNativeObject());
235 getNativeObject(), level, predicate.getNativeObject());
236 return (res == 0) ? null :
Expr.create(getContext(), res);
247 predicate.getNativeObject(),
property.getNativeObject());
261 return "Z3Exception: " + e.getMessage();
273 getNativeObject(), f.getNativeObject(),
AST.arrayLength(kinds),
274 Symbol.arrayToNative(kinds));
285 AST.arrayLength(queries),
AST.arrayToNative(queries));
297 getContext().nCtx(), getNativeObject()));
300 for (
int i = 0; i < n; i++)
301 res[i] =
new BoolExpr(getContext(), v.get(i).getNativeObject());
314 getContext().nCtx(), getNativeObject()));
317 for (
int i = 0; i < n; i++)
318 res[i] =
new BoolExpr(getContext(), v.get(i).getNativeObject());
327 Fixedpoint(Context ctx)
throws Z3Exception
329 super(ctx, Native.mkFixedpoint(ctx.nCtx()));
332 void incRef(
long o)
throws Z3Exception
334 getContext().fixedpoint_DRQ().incAndClear(getContext(), o);
338 void decRef(
long o)
throws Z3Exception
340 getContext().fixedpoint_DRQ().add(o);
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
void updateRule(BoolExpr rule, Symbol name)
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
BoolExpr[] getAssertions()
static void fixedpointAssert(long a0, long a1, long a2)
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
void add(BoolExpr...constraints)
static void fixedpointSetParams(long a0, long a1, long a2)
static long fixedpointGetAnswer(long a0, long a1)
Status query(BoolExpr query)
Status query(FuncDecl[] relations)
void addCover(int level, FuncDecl predicate, Expr property)
static long fixedpointGetParamDescrs(long a0, long a1)
void setParameters(Params value)
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
static long fixedpointGetRules(long a0, long a1)
static void fixedpointRegisterRelation(long a0, long a1, long a2)
void addFact(FuncDecl pred, int...args)
Expr getCoverDelta(int level, FuncDecl predicate)
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
static void fixedpointPop(long a0, long a1)
static int fixedpointGetNumLevels(long a0, long a1, long a2)
ParamDescrs getParameterDescriptions()
void registerRelation(FuncDecl f)
static String fixedpointGetHelp(long a0, long a1)
static void fixedpointPush(long a0, long a1)
int getNumLevels(FuncDecl predicate)
void addRule(BoolExpr rule, Symbol name)
String getReasonUnknown()
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
static long fixedpointGetAssertions(long a0, long a1)
static int fixedpointQuery(long a0, long a1, long a2)
static final Z3_lbool fromInt(int v)
static String fixedpointGetReasonUnknown(long a0, long a1)