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 
94  public void addRule(BoolExpr rule, Symbol name) {
95  getContext().checkContextMatch(rule);
96  Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
97  rule.getNativeObject(), AST.getNativeObject(name));
98  }
99 
105  public void addFact(FuncDecl pred, int ... args) {
106  getContext().checkContextMatch(pred);
107  Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
108  pred.getNativeObject(), args.length, args);
109  }
110 
121  getContext().checkContextMatch(query);
122  Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
123  getNativeObject(), query.getNativeObject()));
124  switch (r)
125  {
126  case Z3_L_TRUE:
127  return Status.SATISFIABLE;
128  case Z3_L_FALSE:
129  return Status.UNSATISFIABLE;
130  default:
131  return Status.UNKNOWN;
132  }
133  }
134 
143  public Status query(FuncDecl[] relations) {
144  getContext().checkContextMatch(relations);
146  .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
147  .arrayToNative(relations)));
148  switch (r)
149  {
150  case Z3_L_TRUE:
151  return Status.SATISFIABLE;
152  case Z3_L_FALSE:
153  return Status.UNSATISFIABLE;
154  default:
155  return Status.UNKNOWN;
156  }
157  }
158 
163  public void push() {
164  Native.fixedpointPush(getContext().nCtx(), getNativeObject());
165  }
166 
174  public void pop() {
175  Native.fixedpointPop(getContext().nCtx(), getNativeObject());
176  }
177 
184  public void updateRule(BoolExpr rule, Symbol name) {
185  getContext().checkContextMatch(rule);
186  Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
187  rule.getNativeObject(), AST.getNativeObject(name));
188  }
189 
196  public Expr getAnswer()
197  {
198  long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
199  return (ans == 0) ? null : Expr.create(getContext(), ans);
200  }
201 
206  {
207  return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
208  getNativeObject());
209  }
210 
214  public int getNumLevels(FuncDecl predicate)
215  {
216  return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
217  predicate.getNativeObject());
218  }
219 
225  public Expr getCoverDelta(int level, FuncDecl predicate)
226  {
227  long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
228  getNativeObject(), level, predicate.getNativeObject());
229  return (res == 0) ? null : Expr.create(getContext(), res);
230  }
231 
236  public void addCover(int level, FuncDecl predicate, Expr property)
237 
238  {
239  Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
240  predicate.getNativeObject(), property.getNativeObject());
241  }
242 
246  @Override
247  public String toString()
248  {
249  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
250  0, null);
251  }
252 
258  {
259 
260  Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
261  getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
262  Symbol.arrayToNative(kinds));
263 
264  }
265 
269  public String toString(BoolExpr[] queries)
270  {
271 
272  return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
273  AST.arrayLength(queries), AST.arrayToNative(queries));
274  }
275 
281  public BoolExpr[] getRules()
282  {
283  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
284  return v.ToBoolExprArray();
285  }
286 
293  {
294  ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
295  return v.ToBoolExprArray();
296  }
297 
304  {
305  return new Statistics(getContext(), Native.fixedpointGetStatistics(
306  getContext().nCtx(), getNativeObject()));
307  }
308 
314  public BoolExpr[] ParseFile(String file)
315  {
316  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
317  return av.ToBoolExprArray();
318  }
319 
326  {
327  ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
328  return av.ToBoolExprArray();
329  }
330 
331 
332  Fixedpoint(Context ctx, long obj) throws Z3Exception
333  {
334  super(ctx, obj);
335  }
336 
337  Fixedpoint(Context ctx)
338  {
339  super(ctx, Native.mkFixedpoint(ctx.nCtx()));
340  }
341 
342  @Override
343  void incRef() {
344  Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
345  }
346 
347  @Override
348  void addToReferenceQueue() {
349  getContext().getFixedpointDRQ().storeReference(getContext(), this);
350  }
351 
352  @Override
353  void checkNativeObject(long obj) { }
354 }
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5101
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:5041
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4004
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:5057
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5074
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:5178
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:5083
Status query(BoolExpr query)
static long fixedpointFromString(long a0, long a1, String a2)
Definition: Native.java:5213
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:5195
void setParameters(Params value)
Definition: Fixedpoint.java:41
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:5118
void storeReference(Context ctx, T obj)
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:5160
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:5144
Expr getCoverDelta(int level, FuncDecl predicate)
static long fixedpointFromFile(long a0, long a1, String a2)
Definition: Native.java:5222
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5204
static void fixedpointIncRef(long a0, long a1)
Definition: Native.java:5025
String toString(BoolExpr[] queries)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:5152
static void fixedpointPop(long a0, long a1)
Definition: Native.java:5239
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:5109
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:5186
static void fixedpointPush(long a0, long a1)
Definition: Native.java:5231
int getNumLevels(FuncDecl predicate)
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:94
static long fixedpointGetStatistics(long a0, long a1)
Definition: Native.java:5135
static long mkFixedpoint(long a0)
Definition: Native.java:5016
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:5049
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:5127
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:5169
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:5065
def String(name, ctx=None)
Definition: z3py.py:9443
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:5092