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() throws Z3Exception
32  {
33  return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
34  }
35 
41  public void setParameters(Params value) throws Z3Exception
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) throws Z3Exception
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) throws Z3Exception
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) throws Z3Exception
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) throws Z3Exception
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) throws Z3Exception
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 
168  public void push() throws Z3Exception
169  {
170  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
171  }
172 
178  public void pop() throws Z3Exception
179  {
180  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
181  }
182 
188  public void updateRule(BoolExpr rule, Symbol name) throws Z3Exception
189  {
190 
191  getContext().checkContextMatch(rule);
192  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
193  rule.getNativeObject(), AST.getNativeObject(name));
194  }
195 
202  public Expr getAnswer() throws Z3Exception
203  {
204  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
205  return (ans == 0) ? null : Expr.create(getContext(), ans);
206  }
207 
211  public String getReasonUnknown() throws Z3Exception
212  {
213 
214  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
215  getNativeObject());
216  }
217 
221  public int getNumLevels(FuncDecl predicate) throws Z3Exception
222  {
223  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
224  predicate.getNativeObject());
225  }
226 
232  public Expr getCoverDelta(int level, FuncDecl predicate) throws Z3Exception
233  {
234  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
235  getNativeObject(), level, predicate.getNativeObject());
236  return (res == 0) ? null : Expr.create(getContext(), res);
237  }
238 
243  public void addCover(int level, FuncDecl predicate, Expr property)
244  throws Z3Exception
245  {
246  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
247  predicate.getNativeObject(), property.getNativeObject());
248  }
249 
253  public String toString()
254  {
255  try
256  {
257  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
258  0, null);
259  } catch (Z3Exception e)
260  {
261  return "Z3Exception: " + e.getMessage();
262  }
263  }
264 
269  public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exception
270  {
271 
272  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
273  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
274  Symbol.arrayToNative(kinds));
275 
276  }
277 
281  public String toString(BoolExpr[] queries) throws Z3Exception
282  {
283 
284  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
285  AST.arrayLength(queries), AST.arrayToNative(queries));
286  }
287 
293  public BoolExpr[] getRules() throws Z3Exception
294  {
295 
296  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
297  getContext().nCtx(), getNativeObject()));
298  int n = v.size();
299  BoolExpr[] res = new BoolExpr[n];
300  for (int i = 0; i < n; i++)
301  res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
302  return res;
303  }
304 
311  {
312 
313  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
314  getContext().nCtx(), getNativeObject()));
315  int n = v.size();
316  BoolExpr[] res = new BoolExpr[n];
317  for (int i = 0; i < n; i++)
318  res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
319  return res;
320  }
321 
322  Fixedpoint(Context ctx, long obj) throws Z3Exception
323  {
324  super(ctx, obj);
325  }
326 
327  Fixedpoint(Context ctx) throws Z3Exception
328  {
329  super(ctx, Native.mkFixedpoint(ctx.nCtx()));
330  }
331 
332  void incRef(long o) throws Z3Exception
333  {
334  getContext().fixedpoint_DRQ().incAndClear(getContext(), o);
335  super.incRef(o);
336  }
337 
338  void decRef(long o) throws Z3Exception
339  {
340  getContext().fixedpoint_DRQ().add(o);
341  super.decRef(o);
342  }
343 }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:3292
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:3232
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:3248
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3265
void add(BoolExpr...constraints)
Definition: Fixedpoint.java:65
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:3369
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:3274
Status query(BoolExpr query)
Status query(FuncDecl[] relations)
void addCover(int level, FuncDecl predicate, Expr property)
static long fixedpointGetParamDescrs(long a0, long a1)
Definition: Native.java:3386
void setParameters(Params value)
Definition: Fixedpoint.java:41
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:3309
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:3351
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:3335
void addFact(FuncDecl pred, int...args)
Expr getCoverDelta(int level, FuncDecl predicate)
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3395
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:3343
static void fixedpointPop(long a0, long a1)
Definition: Native.java:3430
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:3300
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
void registerRelation(FuncDecl f)
Definition: Fixedpoint.java:80
static String fixedpointGetHelp(long a0, long a1)
Definition: Native.java:3377
static void fixedpointPush(long a0, long a1)
Definition: Native.java:3422
int getNumLevels(FuncDecl predicate)
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:93
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:3240
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:3318
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:3360
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:3256
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:3283