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 }
com.microsoft.z3.Fixedpoint.getStatistics
Statistics getStatistics()
Definition: Fixedpoint.java:286
com.microsoft.z3.Native.fixedpointFromFile
static long fixedpointFromFile(long a0, long a1, String a2)
Definition: Native.java:5669
com.microsoft.z3.Native.fixedpointToString
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5651
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Native.fixedpointGetRules
static long fixedpointGetRules(long a0, long a1)
Definition: Native.java:5607
com.microsoft.z3.Fixedpoint.getCoverDelta
Expr getCoverDelta(int level, FuncDecl predicate)
Definition: Fixedpoint.java:208
com.microsoft.z3.Native.fixedpointGetNumLevels
static int fixedpointGetNumLevels(long a0, long a1, long a2)
Definition: Native.java:5556
com.microsoft.z3.Native.fixedpointRegisterRelation
static void fixedpointRegisterRelation(long a0, long a1, long a2)
Definition: Native.java:5591
com.microsoft.z3.Native.fixedpointAddCover
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
Definition: Native.java:5574
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:27
com.microsoft.z3.Fixedpoint.query
Status query(FuncDecl[] relations)
Definition: Fixedpoint.java:144
com.microsoft.z3.Status.SATISFIABLE
SATISFIABLE
Definition: Status.java:32
com.microsoft.z3.Fixedpoint.getHelp
String getHelp()
Definition: Fixedpoint.java:31
com.microsoft.z3.Native.fixedpointSetParams
static void fixedpointSetParams(long a0, long a1, long a2)
Definition: Native.java:5625
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.enumerations.Z3_lbool.fromInt
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
com.microsoft
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Native.fixedpointAssert
static void fixedpointAssert(long a0, long a1, long a2)
Definition: Native.java:5504
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:103
com.microsoft.z3.Native.fixedpointAddRule
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5488
com.microsoft.z3.Fixedpoint.addCover
void addCover(int level, FuncDecl predicate, Expr property)
Definition: Fixedpoint.java:219
com.microsoft.z3.Native.fixedpointGetParamDescrs
static long fixedpointGetParamDescrs(long a0, long a1)
Definition: Native.java:5642
com.microsoft.z3.Native.fixedpointGetReasonUnknown
static String fixedpointGetReasonUnknown(long a0, long a1)
Definition: Native.java:5539
com.microsoft.z3.Native.fixedpointQuery
static int fixedpointQuery(long a0, long a1, long a2)
Definition: Native.java:5512
com.microsoft.z3.Fixedpoint.setParameters
void setParameters(Params value)
Definition: Fixedpoint.java:41
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Fixedpoint.addFact
void addFact(FuncDecl pred, int ... args)
Definition: Fixedpoint.java:106
com.microsoft.z3.Native.fixedpointGetHelp
static String fixedpointGetHelp(long a0, long a1)
Definition: Native.java:5633
com.microsoft.z3.Fixedpoint.setPredicateRepresentation
void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
Definition: Fixedpoint.java:240
com.microsoft.z3.Fixedpoint.ParseString
BoolExpr[] ParseString(String s)
Definition: Fixedpoint.java:308
com.microsoft.z3.Fixedpoint.getReasonUnknown
String getReasonUnknown()
Definition: Fixedpoint.java:188
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Fixedpoint.toString
String toString()
Definition: Fixedpoint.java:230
com.microsoft.z3.Fixedpoint.getAssertions
BoolExpr[] getAssertions()
Definition: Fixedpoint.java:275
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.fixedpointQueryRelations
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5521
com.microsoft.z3.Native.fixedpointGetCoverDelta
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
Definition: Native.java:5565
com.microsoft.z3.Context.getFixedpointDRQ
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4098
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.Native.fixedpointAddFact
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
Definition: Native.java:5496
com.microsoft.z3.Native.fixedpointFromString
static long fixedpointFromString(long a0, long a1, String a2)
Definition: Native.java:5660
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.AST
Definition: AST.java:25
com.microsoft.z3.enumerations.Z3_lbool
Definition: Z3_lbool.java:13
com.microsoft.z3.Native.fixedpointGetAssertions
static long fixedpointGetAssertions(long a0, long a1)
Definition: Native.java:5616
com.microsoft.z3.Native.fixedpointUpdateRule
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
Definition: Native.java:5548
com.microsoft.z3.Status.UNKNOWN
UNKNOWN
Definition: Status.java:29
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:101
com.microsoft.z3.Fixedpoint.addRule
void addRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:95
com.microsoft.z3.Status
Definition: Status.java:23
com
com.microsoft.z3.Native.fixedpointGetStatistics
static long fixedpointGetStatistics(long a0, long a1)
Definition: Native.java:5582
com.microsoft.z3.Fixedpoint.getRules
BoolExpr[] getRules()
Definition: Fixedpoint.java:264
com.microsoft.z3.Fixedpoint.getNumLevels
int getNumLevels(FuncDecl predicate)
Definition: Fixedpoint.java:197
com.microsoft.z3.Fixedpoint
Definition: Fixedpoint.java:25
com.microsoft.z3.Fixedpoint.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Fixedpoint.java:54
com.microsoft.z3.Fixedpoint.getAnswer
Expr getAnswer()
Definition: Fixedpoint.java:179
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Fixedpoint.query
Status query(BoolExpr query)
Definition: Fixedpoint.java:121
com.microsoft.z3.Fixedpoint.updateRule
void updateRule(BoolExpr rule, Symbol name)
Definition: Fixedpoint.java:167
com.microsoft.z3.Fixedpoint.add
void add(BoolExpr ... constraints)
Definition: Fixedpoint.java:65
com.microsoft.z3.Native.fixedpointSetPredicateRepresentation
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
Definition: Native.java:5599
com.microsoft.z3.Status.UNSATISFIABLE
UNSATISFIABLE
Definition: Status.java:26
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Fixedpoint.ParseFile
BoolExpr[] ParseFile(String file)
Definition: Fixedpoint.java:297
com.microsoft.z3.Native.fixedpointGetAnswer
static long fixedpointGetAnswer(long a0, long a1)
Definition: Native.java:5530
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Fixedpoint.toString
String toString(BoolExpr[] queries)
Definition: Fixedpoint.java:252
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10085
com.microsoft.z3.Fixedpoint.registerRelation
void registerRelation(FuncDecl f)
Definition: Fixedpoint.java:80