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 
217  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
218  getNativeObject());
219  }
220 
224  public int getNumLevels(FuncDecl predicate)
225  {
226  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
227  predicate.getNativeObject());
228  }
229 
235  public Expr getCoverDelta(int level, FuncDecl predicate)
236  {
237  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
238  getNativeObject(), level, predicate.getNativeObject());
239  return (res == 0) ? null : Expr.create(getContext(), res);
240  }
241 
246  public void addCover(int level, FuncDecl predicate, Expr property)
247 
248  {
249  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
250  predicate.getNativeObject(), property.getNativeObject());
251  }
252 
256  public String toString()
257  {
258  try
259  {
260  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
261  0, null);
262  } catch (Z3Exception e)
263  {
264  return "Z3Exception: " + e.getMessage();
265  }
266  }
267 
273  {
274 
275  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
276  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
277  Symbol.arrayToNative(kinds));
278 
279  }
280 
284  public String toString(BoolExpr[] queries)
285  {
286 
287  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
288  AST.arrayLength(queries), AST.arrayToNative(queries));
289  }
290 
296  public BoolExpr[] getRules()
297  {
298 
299  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
300  getContext().nCtx(), getNativeObject()));
301  int n = v.size();
302  BoolExpr[] res = new BoolExpr[n];
303  for (int i = 0; i < n; i++)
304  res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
305  return res;
306  }
307 
314  {
315 
316  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
317  getContext().nCtx(), getNativeObject()));
318  int n = v.size();
319  BoolExpr[] res = new BoolExpr[n];
320  for (int i = 0; i < n; i++)
321  res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
322  return res;
323  }
324 
325  Fixedpoint(Context ctx, long obj)
326  {
327  super(ctx, obj);
328  }
329 
330  Fixedpoint(Context ctx)
331  {
332  super(ctx, Native.mkFixedpoint(ctx.nCtx()));
333  }
334 
335  void incRef(long o)
336  {
337  getContext().getFixedpointDRQ().incAndClear(getContext(), o);
338  super.incRef(o);
339  }
340 
341  void decRef(long o)
342  {
343  getContext().getFixedpointDRQ().add(o);
344  super.decRef(o);
345  }
346 }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:3361
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:3301
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:3317
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3334
void add(BoolExpr...constraints)
Definition: Fixedpoint.java:65
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:3438
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:3343
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:3455
void setParameters(Params value)
Definition: Fixedpoint.java:41
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:3378
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:3420
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:3404
void addFact(FuncDecl pred, int...args)
Expr getCoverDelta(int level, FuncDecl predicate)
void incAndClear(Context ctx, long o)
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:3464
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:3412
static void fixedpointPop(long a0, long a1)
Definition: Native.java:3499
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:3369
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
void registerRelation(FuncDecl f)
Definition: Fixedpoint.java:80
static String fixedpointGetHelp(long a0, long a1)
Definition: Native.java:3446
static void fixedpointPush(long a0, long a1)
Definition: Native.java:3491
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:3309
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:3387
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:3429
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:3325
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:3352
IDecRefQueue getFixedpointDRQ()
Definition: Context.java:3735