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 public void add(BoolExpr ... constraints)
66 {
67 getContext().checkContextMatch(constraints);
68 for (BoolExpr a : constraints)
69 {
70 Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
71 a.getNativeObject());
72 }
73 }
74
81 {
82
83 getContext().checkContextMatch(f);
84 Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
85 f.getNativeObject());
86 }
87
95 public void addRule(BoolExpr 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 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[] relations) {
145 getContext().checkContextMatch(relations);
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(BoolExpr 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 predicate)
198 {
199 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
200 predicate.getNativeObject());
201 }
202
208 public Expr getCoverDelta(int level, FuncDecl 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 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
244 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
245 Symbol.arrayToNative(kinds));
246
247 }
248
252 public String toString(BoolExpr[] queries)
253 {
254
255 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
256 AST.arrayLength(queries), AST.arrayToNative(queries));
257 }
258
265 {
266 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
267 return v.ToBoolExprArray();
268 }
269
276 {
277 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
278 return v.ToBoolExprArray();
279 }
280
287 {
288 return new Statistics(getContext(), Native.fixedpointGetStatistics(
289 getContext().nCtx(), getNativeObject()));
290 }
291
297 public BoolExpr[] ParseFile(String file)
298 {
299 ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
300 return av.ToBoolExprArray();
301 }
302
309 {
310 ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
311 return av.ToBoolExprArray();
312 }
313
314
315 Fixedpoint(Context ctx, long obj) throws Z3Exception
316 {
317 super(ctx, obj);
318 }
319
320 Fixedpoint(Context ctx)
321 {
322 super(ctx, Native.mkFixedpoint(ctx.nCtx()));
323 }
324
325 @Override
326 void incRef() {
327 Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
328 }
329
330 @Override
331 void addToReferenceQueue() {
332 getContext().getFixedpointDRQ().storeReference(getContext(), this);
333 }
334
335 @Override
336 void checkNativeObject(long obj) { }
337}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4098
BoolExpr[] ParseString(String s)
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
String toString(BoolExpr[] queries)
void setParameters(Params value)
Definition: Fixedpoint.java:41
BoolExpr[] ParseFile(String file)
void registerRelation(FuncDecl f)
Definition: Fixedpoint.java:80
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:95
Status query(FuncDecl[] relations)
Expr getCoverDelta(int level, FuncDecl predicate)
void addCover(int level, FuncDecl predicate, Expr property)
int getNumLevels(FuncDecl predicate)
Status query(BoolExpr query)
void updateRule(BoolExpr rule, Symbol name)
void addFact(FuncDecl pred, int ... args)
void add(BoolExpr ... constraints)
Definition: Fixedpoint.java:65
void storeReference(Context ctx, T obj)
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:5565
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:5504
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5521
static String fixedpointGetHelp(long a0, long a1)
Definition: Native.java:5633
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5488
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:5539
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:5530
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:5512
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:5607
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:5556
static long fixedpointFromFile(long a0, long a1, String a2)
Definition: Native.java:5669
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:5625
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5548
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:5574
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:5591
static long fixedpointGetStatistics(long a0, long a1)
Definition: Native.java:5582
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:5496
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:5599
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5651
static long fixedpointGetParamDescrs(long a0, long a1)
Definition: Native.java:5642
static long fixedpointFromString(long a0, long a1, String a2)
Definition: Native.java:5660
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:5616
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
def String(name, ctx=None)
Definition: z3py.py:10085
@ Z3_L_TRUE
Definition: z3_api.h:103
@ Z3_L_FALSE
Definition: z3_api.h:101