Z3
Fixedpoint.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
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 
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 
80  public void registerRelation(FuncDecl f)
81  {
82 
83  getContext().checkContextMatch(f);
84  Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
85  f.getNativeObject());
86  }
87 
93  public void addRule(BoolExpr rule, Symbol name)
94  {
95 
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  {
108  getContext().checkContextMatch(pred);
109  Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
110  pred.getNativeObject(), (int) args.length, args);
111  }
112 
123  {
124 
125  getContext().checkContextMatch(query);
126  Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
127  getNativeObject(), query.getNativeObject()));
128  switch (r)
129  {
130  case Z3_L_TRUE:
131  return Status.SATISFIABLE;
132  case Z3_L_FALSE:
133  return Status.UNSATISFIABLE;
134  default:
135  return Status.UNKNOWN;
136  }
137  }
138 
147  public Status query(FuncDecl[] relations)
148  {
149 
150  getContext().checkContextMatch(relations);
152  .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
153  .arrayToNative(relations)));
154  switch (r)
155  {
156  case Z3_L_TRUE:
157  return Status.SATISFIABLE;
158  case Z3_L_FALSE:
159  return Status.UNSATISFIABLE;
160  default:
161  return Status.UNKNOWN;
162  }
163  }
164 
169  public void push()
170  {
171  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
172  }
173 
181  public void pop()
182  {
183  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
184  }
185 
191  public void updateRule(BoolExpr rule, Symbol name)
192  {
193 
194  getContext().checkContextMatch(rule);
195  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
196  rule.getNativeObject(), AST.getNativeObject(name));
197  }
198 
205  public Expr getAnswer()
206  {
207  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
208  return (ans == 0) ? null : Expr.create(getContext(), ans);
209  }
210 
214  public String getReasonUnknown()
215  {
216  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
217  getNativeObject());
218  }
219 
223  public int getNumLevels(FuncDecl predicate)
224  {
225  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
226  predicate.getNativeObject());
227  }
228 
234  public Expr getCoverDelta(int level, FuncDecl predicate)
235  {
236  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
237  getNativeObject(), level, predicate.getNativeObject());
238  return (res == 0) ? null : Expr.create(getContext(), res);
239  }
240 
245  public void addCover(int level, FuncDecl predicate, Expr property)
246 
247  {
248  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
249  predicate.getNativeObject(), property.getNativeObject());
250  }
251 
255  public String toString()
256  {
257  try
258  {
259  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
260  0, null);
261  } catch (Z3Exception e)
262  {
263  return "Z3Exception: " + e.getMessage();
264  }
265  }
266 
272  {
273 
274  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
275  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
276  Symbol.arrayToNative(kinds));
277 
278  }
279 
283  public String toString(BoolExpr[] queries)
284  {
285 
286  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
287  AST.arrayLength(queries), AST.arrayToNative(queries));
288  }
289 
295  public BoolExpr[] getRules()
296  {
297  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
298  return v.ToBoolExprArray();
299  }
300 
307  {
308  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
309  return v.ToBoolExprArray();
310  }
311 
318  {
319  return new Statistics(getContext(), Native.fixedpointGetStatistics(
320  getContext().nCtx(), getNativeObject()));
321  }
322 
328  public BoolExpr[] ParseFile(String file)
329  {
330  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
331  return av.ToBoolExprArray();
332  }
333 
339  public BoolExpr[] ParseString(String s)
340  {
341  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
342  return av.ToBoolExprArray();
343  }
344 
345 
346  Fixedpoint(Context ctx, long obj) throws Z3Exception
347  {
348  super(ctx, obj);
349  }
350 
351  Fixedpoint(Context ctx)
352  {
353  super(ctx, Native.mkFixedpoint(ctx.nCtx()));
354  }
355 
356  void incRef(long o)
357  {
358  getContext().getFixedpointDRQ().incAndClear(getContext(), o);
359  super.incRef(o);
360  }
361 
362  void decRef(long o)
363  {
364  getContext().getFixedpointDRQ().add(o);
365  super.decRef(o);
366  }
367 }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:3420
BoolExpr[] ParseString(String s)
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
void updateRule(BoolExpr rule, Symbol name)
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
Definition: Native.java:3360
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:3376
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3393
void add(BoolExpr...constraints)
Definition: Fixedpoint.java:65
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:3497
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:3402
Status query(BoolExpr query)
static long fixedpointFromString(long a0, long a1, String a2)
Definition: Native.java:3532
Status query(FuncDecl[] relations)
void addCover(int level, FuncDecl predicate, Expr property)
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:149
static long fixedpointGetParamDescrs(long a0, long a1)
Definition: Native.java:3514
void setParameters(Params value)
Definition: Fixedpoint.java:41
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:3437
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:3479
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:3463
void addFact(FuncDecl pred, int...args)
Expr getCoverDelta(int level, FuncDecl predicate)
static long fixedpointFromFile(long a0, long a1, String a2)
Definition: Native.java:3541
void incAndClear(Context ctx, long o)
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3523
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:3471
static void fixedpointPop(long a0, long a1)
Definition: Native.java:3558
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:3428
BoolExpr[] ParseFile(String file)
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
void registerRelation(FuncDecl f)
Definition: Fixedpoint.java:80
static String fixedpointGetHelp(long a0, long a1)
Definition: Native.java:3505
static void fixedpointPush(long a0, long a1)
Definition: Native.java:3550
int getNumLevels(FuncDecl predicate)
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:93
static long fixedpointGetStatistics(long a0, long a1)
Definition: Native.java:3454
static long mkFixedpoint(long a0)
Definition: Native.java:3335
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:3368
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:3446
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:3488
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:3384
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:3411
IDecRefQueue getFixedpointDRQ()
Definition: Context.java:3754