Z3 |

Fixedpoint.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
20 import com.microsoft.z3.enumerations.Z3_lbool;
21
25 public 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
54 public ParamDescrs getParameterDescriptions()
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
81 public void registerRelation(FuncDecl<BoolSort> f)
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
121 public Status query(Expr<BoolSort> query) {
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
179 public Expr<?> getAnswer()
180 {
181 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
182 return (ans == 0) ? null : Expr.create(getContext(), ans);
183 }
184
188 public String getReasonUnknown()
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
230 public String toString()
231 {
232 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
233 0, null);
234 }
235
240 public void setPredicateRepresentation(FuncDecl<BoolSort> f, Symbol[] kinds)
241 {
242 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
243 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
244 Symbol.arrayToNative(kinds));
245
246 }
247
251 public String toString(Expr<BoolSort>[] queries)
252 {
253 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
254 AST.arrayLength(queries), AST.arrayToNative(queries));
255 }
256
262 public BoolExpr[] getRules()
263 {
264 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
265 return v.ToBoolExprArray();
266 }
267
273 public BoolExpr[] getAssertions()
274 {
275 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
276 return v.ToBoolExprArray();
277 }
278
284 public Statistics getStatistics()
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
306 public BoolExpr[] ParseString(String s)
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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.getFixedpointDRQ
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4140
com.microsoft.z3.Expr< BoolSort >
com.microsoft.z3.Fixedpoint
Definition: Fixedpoint.java:26
com.microsoft.z3.Fixedpoint.ParseString
BoolExpr[] ParseString(String s)
Definition: Fixedpoint.java:306
com.microsoft.z3.Fixedpoint.updateRule
void updateRule(Expr< BoolSort > rule, Symbol name)
Definition: Fixedpoint.java:167
com.microsoft.z3.Fixedpoint.query
Status query(Expr< BoolSort > query)
Definition: Fixedpoint.java:121
com.microsoft.z3.Fixedpoint.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
com.microsoft.z3.Fixedpoint.registerRelation
void registerRelation(FuncDecl< BoolSort > f)
Definition: Fixedpoint.java:81
com.microsoft.z3.Fixedpoint.setParameters
void setParameters(Params value)
Definition: Fixedpoint.java:41
com.microsoft.z3.Fixedpoint.ParseFile
BoolExpr[] ParseFile(String file)
Definition: Fixedpoint.java:295
com.microsoft.z3.Fixedpoint.getHelp
String getHelp()
Definition: Fixedpoint.java:31
com.microsoft.z3.Fixedpoint.setPredicateRepresentation
void setPredicateRepresentation(FuncDecl< BoolSort > f, Symbol[] kinds)
Definition: Fixedpoint.java:240
com.microsoft.z3.Fixedpoint.query
Status query(FuncDecl< BoolSort >[] relations)
Definition: Fixedpoint.java:144
com.microsoft.z3.Fixedpoint.getAnswer
Expr<?> getAnswer()
Definition: Fixedpoint.java:179
com.microsoft.z3.Fixedpoint.getRules
BoolExpr[] getRules()
Definition: Fixedpoint.java:262
com.microsoft.z3.Fixedpoint.getNumLevels
int getNumLevels(FuncDecl< BoolSort > predicate)
Definition: Fixedpoint.java:197
com.microsoft.z3.Fixedpoint.addCover
void addCover(int level, FuncDecl< BoolSort > predicate, Expr<?> property)
Definition: Fixedpoint.java:219
com.microsoft.z3.Fixedpoint.toString
String toString(Expr< BoolSort >[] queries)
Definition: Fixedpoint.java:251
com.microsoft.z3.Fixedpoint.getAssertions
BoolExpr[] getAssertions()
Definition: Fixedpoint.java:273
com.microsoft.z3.Fixedpoint.add
final void add(Expr< BoolSort >... constraints)
Definition: Fixedpoint.java:66
com.microsoft.z3.Fixedpoint.addFact
void addFact(FuncDecl< BoolSort > pred, int ... args)
Definition: Fixedpoint.java:106
com.microsoft.z3.Fixedpoint.getCoverDelta
Expr<?> getCoverDelta(int level, FuncDecl< BoolSort > predicate)
Definition: Fixedpoint.java:208
com.microsoft.z3.Fixedpoint.toString
String toString()
Definition: Fixedpoint.java:230
com.microsoft.z3.Fixedpoint.getReasonUnknown
String getReasonUnknown()
Definition: Fixedpoint.java:188
com.microsoft.z3.Fixedpoint.getStatistics
Statistics getStatistics()
Definition: Fixedpoint.java:284
com.microsoft.z3.Fixedpoint.addRule
void addRule(Expr< BoolSort > rule, Symbol name)
Definition: Fixedpoint.java:95
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.Z3Object.arrayLength
static int arrayLength(Z3Object[] a)
Definition: Z3Object.java:83
com.microsoft.z3.Status
Definition: Status.java:24
com.microsoft.z3.Status.SATISFIABLE
SATISFIABLE
Definition: Status.java:32
com.microsoft.z3.Status.UNSATISFIABLE
UNSATISFIABLE
Definition: Status.java:26
com.microsoft.z3.Status.UNKNOWN
UNKNOWN
Definition: Status.java:29
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:105
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:103