Z3
Fixedpoint.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_lbool;
21
25public class Fixedpoint extends Z3Object
26{
27
31 public String getHelp()
32 {
33 return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
34 }
35
41 public void setParameters(Params value)
42 {
43
44 getContext().checkContextMatch(value);
45 Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
47 }
48
55 {
56 return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
58 }
59
65 @SafeVarargs
66 public final void add(Expr<BoolSort>... constraints)
67 {
68 getContext().checkContextMatch(constraints);
69 for (Expr<BoolSort> a : constraints)
70 {
71 Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
72 a.getNativeObject());
73 }
74 }
75
82 {
83 getContext().checkContextMatch(f);
84 Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
85 f.getNativeObject());
86 }
87
95 public void addRule(Expr<BoolSort> rule, Symbol name) {
96 getContext().checkContextMatch(rule);
97 Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
98 rule.getNativeObject(), AST.getNativeObject(name));
99 }
100
106 public void addFact(FuncDecl<BoolSort> pred, int ... args) {
107 getContext().checkContextMatch(pred);
108 Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
109 pred.getNativeObject(), args.length, args);
110 }
111
122 getContext().checkContextMatch(query);
123 Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
124 getNativeObject(), query.getNativeObject()));
125 switch (r)
126 {
127 case Z3_L_TRUE:
128 return Status.SATISFIABLE;
129 case Z3_L_FALSE:
130 return Status.UNSATISFIABLE;
131 default:
132 return Status.UNKNOWN;
133 }
134 }
135
144 public Status query(FuncDecl<BoolSort>[] relations) {
145 getContext().checkContextMatch(relations);
146 Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
147 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
148 .arrayToNative(relations)));
149 switch (r)
150 {
151 case Z3_L_TRUE:
152 return Status.SATISFIABLE;
153 case Z3_L_FALSE:
154 return Status.UNSATISFIABLE;
155 default:
156 return Status.UNKNOWN;
157 }
158 }
159
167 public void updateRule(Expr<BoolSort> rule, Symbol name) {
168 getContext().checkContextMatch(rule);
169 Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
170 rule.getNativeObject(), AST.getNativeObject(name));
171 }
172
180 {
181 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
182 return (ans == 0) ? null : Expr.create(getContext(), ans);
183 }
184
189 {
190 return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
191 getNativeObject());
192 }
193
197 public int getNumLevels(FuncDecl<BoolSort> predicate)
198 {
199 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
200 predicate.getNativeObject());
201 }
202
208 public Expr<?> getCoverDelta(int level, FuncDecl<BoolSort> predicate)
209 {
210 long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
211 getNativeObject(), level, predicate.getNativeObject());
212 return (res == 0) ? null : Expr.create(getContext(), res);
213 }
214
219 public void addCover(int level, FuncDecl<BoolSort> predicate, Expr<?> property)
220
221 {
222 Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
223 predicate.getNativeObject(), property.getNativeObject());
224 }
225
229 @Override
231 {
232 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
233 0, null);
234 }
235
241 {
242 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
243 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
244 Symbol.arrayToNative(kinds));
245
246 }
247
252 {
253 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
254 AST.arrayLength(queries), AST.arrayToNative(queries));
255 }
256
263 {
264 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
265 return v.ToBoolExprArray();
266 }
267
274 {
275 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
276 return v.ToBoolExprArray();
277 }
278
285 {
286 return new Statistics(getContext(), Native.fixedpointGetStatistics(
287 getContext().nCtx(), getNativeObject()));
288 }
289
295 public BoolExpr[] ParseFile(String file)
296 {
297 ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
298 return av.ToBoolExprArray();
299 }
300
307 {
308 ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
309 return av.ToBoolExprArray();
310 }
311
312
313 Fixedpoint(Context ctx, long obj) throws Z3Exception
314 {
315 super(ctx, obj);
316 }
317
318 Fixedpoint(Context ctx)
319 {
320 super(ctx, Native.mkFixedpoint(ctx.nCtx()));
321 }
322
323 @Override
324 void incRef() {
325 Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
326 }
327
328 @Override
329 void addToReferenceQueue() {
330 getContext().getFixedpointDRQ().storeReference(getContext(), this);
331 }
332
333 @Override
334 void checkNativeObject(long obj) { }
335}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4140
BoolExpr[] ParseString(String s)
void updateRule(Expr< BoolSort > rule, Symbol name)
Status query(Expr< BoolSort > query)
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
void registerRelation(FuncDecl< BoolSort > f)
Definition: Fixedpoint.java:81
void setParameters(Params value)
Definition: Fixedpoint.java:41
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)
final void add(Expr< BoolSort >... constraints)
Definition: Fixedpoint.java:66
void addFact(FuncDecl< BoolSort > pred, int ... args)
Expr<?> getCoverDelta(int level, FuncDecl< BoolSort > predicate)
void addRule(Expr< BoolSort > rule, Symbol name)
Definition: Fixedpoint.java:95
void storeReference(Context ctx, T obj)
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
static int arrayLength(Z3Object[] a)
Definition: Z3Object.java:83
def String(name, ctx=None)
Definition: z3py.py:10693
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
@ Z3_L_TRUE
Definition: z3_api.h:105
@ Z3_L_FALSE
Definition: z3_api.h:103