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 
167  public void updateRule(BoolExpr 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 
189  {
190  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
191  getNativeObject());
192  }
193 
197  public int getNumLevels(FuncDecl predicate)
198  {
199  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
200  predicate.getNativeObject());
201  }
202 
208  public Expr getCoverDelta(int level, FuncDecl 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 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 
241  {
242 
243  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
244  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
245  Symbol.arrayToNative(kinds));
246 
247  }
248 
252  public String toString(BoolExpr[] queries)
253  {
254 
255  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
256  AST.arrayLength(queries), AST.arrayToNative(queries));
257  }
258 
264  public BoolExpr[] getRules()
265  {
266  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
267  return v.ToBoolExprArray();
268  }
269 
276  {
277  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
278  return v.ToBoolExprArray();
279  }
280 
287  {
288  return new Statistics(getContext(), Native.fixedpointGetStatistics(
289  getContext().nCtx(), getNativeObject()));
290  }
291 
297  public BoolExpr[] ParseFile(String file)
298  {
299  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
300  return av.ToBoolExprArray();
301  }
302 
309  {
310  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
311  return av.ToBoolExprArray();
312  }
313 
314 
315  Fixedpoint(Context ctx, long obj) throws Z3Exception
316  {
317  super(ctx, obj);
318  }
319 
320  Fixedpoint(Context ctx)
321  {
322  super(ctx, Native.mkFixedpoint(ctx.nCtx()));
323  }
324 
325  @Override
326  void incRef() {
327  Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
328  }
329 
330  @Override
331  void addToReferenceQueue() {
332  getContext().getFixedpointDRQ().storeReference(getContext(), this);
333  }
334 
335  @Override
336  void checkNativeObject(long obj) { }
337 }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5509
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:5449
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4096
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:5465
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5482
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:5586
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:5491
Status query(BoolExpr query)
static long fixedpointFromString(long a0, long a1, String a2)
Definition: Native.java:5621
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:5603
void setParameters(Params value)
Definition: Fixedpoint.java:41
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:5526
void storeReference(Context ctx, T obj)
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:5568
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:5552
Expr getCoverDelta(int level, FuncDecl predicate)
static long fixedpointFromFile(long a0, long a1, String a2)
Definition: Native.java:5630
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5612
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:5560
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:5517
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:5594
int getNumLevels(FuncDecl predicate)
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:95
static long fixedpointGetStatistics(long a0, long a1)
Definition: Native.java:5543
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:5457
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:5535
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:5577
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:5473
def String(name, ctx=None)
Definition: z3py.py:10043
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:5500