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)));
187 getContext().checkContextMatch(rule);
189 rule.getNativeObject(),
AST.getNativeObject(name));
201 return (ans == 0) ? null :
Expr.create(getContext(), ans);
219 predicate.getNativeObject());
230 getNativeObject(), level, predicate.getNativeObject());
231 return (res == 0) ? null :
Expr.create(getContext(), res);
242 predicate.getNativeObject(),
property.getNativeObject());
263 getNativeObject(), f.getNativeObject(),
AST.arrayLength(kinds),
264 Symbol.arrayToNative(kinds));
275 AST.arrayLength(queries),
AST.arrayToNative(queries));
308 getContext().nCtx(), getNativeObject()));
339 Fixedpoint(Context ctx)
341 super(ctx, Native.mkFixedpoint(ctx.nCtx()));
346 Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
350 void addToReferenceQueue() {
355 void checkNativeObject(
long obj) { }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
BoolExpr [] ParseString(String s)
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
void addFact(FuncDecl pred, int ... args)
void updateRule(BoolExpr rule, Symbol name)
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
BoolExpr [] getAssertions()
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
static void fixedpointAssert(long a0, long a1, long a2)
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
static void fixedpointSetParams(long a0, long a1, long a2)
static long fixedpointGetAnswer(long a0, long a1)
Status query(BoolExpr query)
static long fixedpointFromString(long a0, long a1, String a2)
void add(BoolExpr ... constraints)
Status query(FuncDecl[] relations)
void addCover(int level, FuncDecl predicate, Expr property)
BoolExpr [] ToBoolExprArray()
static long fixedpointGetParamDescrs(long a0, long a1)
void setParameters(Params value)
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
void storeReference(Context ctx, T obj)
static long fixedpointGetRules(long a0, long a1)
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Expr getCoverDelta(int level, FuncDecl predicate)
static long fixedpointFromFile(long a0, long a1, String a2)
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)
BoolExpr [] ParseFile(String file)
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 long fixedpointGetStatistics(long a0, long a1)
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)
def String(name, ctx=None)
static final Z3_lbool fromInt(int v)
static String fixedpointGetReasonUnknown(long a0, long a1)
Statistics getStatistics()