18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_lbool;
33 return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
44 getContext().checkContextMatch(value);
45 Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
56 return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
68 getContext().checkContextMatch(constraints);
71 Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
83 getContext().checkContextMatch(f);
84 Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
96 getContext().checkContextMatch(rule);
97 Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
98 rule.getNativeObject(),
AST.getNativeObject(name));
107 getContext().checkContextMatch(pred);
108 Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
109 pred.getNativeObject(), args.length, args);
122 getContext().checkContextMatch(
query);
124 getNativeObject(),
query.getNativeObject()));
145 getContext().checkContextMatch(relations);
168 getContext().checkContextMatch(rule);
169 Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
170 rule.getNativeObject(),
AST.getNativeObject(name));
181 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
182 return (ans == 0) ? null :
Expr.create(getContext(), ans);
190 return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
199 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
200 predicate.getNativeObject());
210 long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
211 getNativeObject(), level, predicate.getNativeObject());
212 return (res == 0) ? null :
Expr.create(getContext(), res);
222 Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
223 predicate.getNativeObject(), property.getNativeObject());
232 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
242 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
253 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
264 ASTVector v =
new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
275 ASTVector v =
new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
286 return new Statistics(getContext(), Native.fixedpointGetStatistics(
287 getContext().nCtx(), getNativeObject()));
297 ASTVector av =
new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
308 ASTVector av =
new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
318 Fixedpoint(Context ctx)
320 super(ctx, Native.mkFixedpoint(ctx.nCtx()));
325 Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
329 void addToReferenceQueue() {
334 void checkNativeObject(
long obj) { }
BoolExpr[] ToBoolExprArray()
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
BoolExpr[] ParseString(String s)
void updateRule(Expr< BoolSort > rule, Symbol name)
Status query(Expr< BoolSort > query)
ParamDescrs getParameterDescriptions()
void registerRelation(FuncDecl< BoolSort > f)
void setParameters(Params value)
BoolExpr[] ParseFile(String file)
void setPredicateRepresentation(FuncDecl< BoolSort > f, Symbol[] kinds)
Status query(FuncDecl< BoolSort >[] relations)
int getNumLevels(FuncDecl< BoolSort > predicate)
void addCover(int level, FuncDecl< BoolSort > predicate, Expr<?> property)
String toString(Expr< BoolSort >[] queries)
BoolExpr[] getAssertions()
final void add(Expr< BoolSort >... constraints)
void addFact(FuncDecl< BoolSort > pred, int ... args)
Expr<?> getCoverDelta(int level, FuncDecl< BoolSort > predicate)
String getReasonUnknown()
Statistics getStatistics()
void addRule(Expr< BoolSort > rule, Symbol name)
void storeReference(Context ctx, T obj)
static long[] arrayToNative(Z3Object[] a)
static int arrayLength(Z3Object[] a)
def String(name, ctx=None)
Z3_lbool
Lifted Boolean type: false, undefined, true.