18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_lbool;
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) { }
BoolExpr[] ToBoolExprArray()
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
BoolExpr[] ParseString(String s)
ParamDescrs getParameterDescriptions()
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
String toString(BoolExpr[] queries)
void setParameters(Params value)
BoolExpr[] ParseFile(String file)
void registerRelation(FuncDecl f)
void addRule(BoolExpr rule, Symbol name)
Status query(FuncDecl[] relations)
Expr getCoverDelta(int level, FuncDecl predicate)
void addCover(int level, FuncDecl predicate, Expr property)
BoolExpr[] getAssertions()
int getNumLevels(FuncDecl predicate)
Status query(BoolExpr query)
void updateRule(BoolExpr rule, Symbol name)
String getReasonUnknown()
void addFact(FuncDecl pred, int ... args)
void add(BoolExpr ... constraints)
Statistics getStatistics()
void storeReference(Context ctx, T obj)
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
static void fixedpointAssert(long a0, long a1, long a2)
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
static String fixedpointGetHelp(long a0, long a1)
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
static String fixedpointGetReasonUnknown(long a0, long a1)
static long fixedpointGetAnswer(long a0, long a1)
static int fixedpointQuery(long a0, long a1, long a2)
static long fixedpointGetRules(long a0, long a1)
static int fixedpointGetNumLevels(long a0, long a1, long a2)
static long fixedpointFromFile(long a0, long a1, String a2)
static void fixedpointSetParams(long a0, long a1, long a2)
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
static void fixedpointRegisterRelation(long a0, long a1, long a2)
static long fixedpointGetStatistics(long a0, long a1)
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
static long fixedpointGetParamDescrs(long a0, long a1)
static long fixedpointFromString(long a0, long a1, String a2)
static long fixedpointGetAssertions(long a0, long a1)
static final Z3_lbool fromInt(int v)
def String(name, ctx=None)