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 
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 
164  public void push() {
165  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
166  }
167 
175  public void pop() {
176  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
177  }
178 
186  public void updateRule(BoolExpr rule, Symbol name) {
187  getContext().checkContextMatch(rule);
188  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
189  rule.getNativeObject(), AST.getNativeObject(name));
190  }
191 
198  public Expr getAnswer()
199  {
200  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
201  return (ans == 0) ? null : Expr.create(getContext(), ans);
202  }
203 
208  {
209  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
210  getNativeObject());
211  }
212 
216  public int getNumLevels(FuncDecl predicate)
217  {
218  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
219  predicate.getNativeObject());
220  }
221 
227  public Expr getCoverDelta(int level, FuncDecl predicate)
228  {
229  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
230  getNativeObject(), level, predicate.getNativeObject());
231  return (res == 0) ? null : Expr.create(getContext(), res);
232  }
233 
238  public void addCover(int level, FuncDecl predicate, Expr property)
239 
240  {
241  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
242  predicate.getNativeObject(), property.getNativeObject());
243  }
244 
248  @Override
249  public String toString()
250  {
251  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
252  0, null);
253  }
254 
260  {
261 
262  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
263  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
264  Symbol.arrayToNative(kinds));
265 
266  }
267 
271  public String toString(BoolExpr[] queries)
272  {
273 
274  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
275  AST.arrayLength(queries), AST.arrayToNative(queries));
276  }
277 
283  public BoolExpr[] getRules()
284  {
285  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
286  return v.ToBoolExprArray();
287  }
288 
295  {
296  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
297  return v.ToBoolExprArray();
298  }
299 
306  {
307  return new Statistics(getContext(), Native.fixedpointGetStatistics(
308  getContext().nCtx(), getNativeObject()));
309  }
310 
316  public BoolExpr[] ParseFile(String file)
317  {
318  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
319  return av.ToBoolExprArray();
320  }
321 
328  {
329  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
330  return av.ToBoolExprArray();
331  }
332 
333 
334  Fixedpoint(Context ctx, long obj) throws Z3Exception
335  {
336  super(ctx, obj);
337  }
338 
339  Fixedpoint(Context ctx)
340  {
341  super(ctx, Native.mkFixedpoint(ctx.nCtx()));
342  }
343 
344  @Override
345  void incRef() {
346  Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
347  }
348 
349  @Override
350  void addToReferenceQueue() {
351  getContext().getFixedpointDRQ().storeReference(getContext(), this);
352  }
353 
354  @Override
355  void checkNativeObject(long obj) { }
356 }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5240
BoolExpr [] ParseString(String s)
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
void addFact(FuncDecl pred, int ... args)
void updateRule(BoolExpr rule, Symbol name)
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5180
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4026
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:5196
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5213
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:5317
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:5222
Status query(BoolExpr query)
static long fixedpointFromString(long a0, long a1, String a2)
Definition: Native.java:5352
void add(BoolExpr ... constraints)
Definition: Fixedpoint.java:65
Status query(FuncDecl[] relations)
void addCover(int level, FuncDecl predicate, Expr property)
BoolExpr [] ToBoolExprArray()
Definition: ASTVector.java:140
static long fixedpointGetParamDescrs(long a0, long a1)
Definition: Native.java:5334
void setParameters(Params value)
Definition: Fixedpoint.java:41
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:5257
void storeReference(Context ctx, T obj)
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:5299
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:5283
Expr getCoverDelta(int level, FuncDecl predicate)
static long fixedpointFromFile(long a0, long a1, String a2)
Definition: Native.java:5361
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5343
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:5291
static void fixedpointPop(long a0, long a1)
Definition: Native.java:5378
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:5248
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:5325
static void fixedpointPush(long a0, long a1)
Definition: Native.java:5370
int getNumLevels(FuncDecl predicate)
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:95
static long fixedpointGetStatistics(long a0, long a1)
Definition: Native.java:5274
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:5188
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:5266
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:5308
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:5204
def String(name, ctx=None)
Definition: z3py.py:9738
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:5231