Z3
FuncInterp.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
25 public class FuncInterp extends Z3Object {
26 
31  public static class Entry extends Z3Object {
32 
39  public Expr getValue()
40  {
41  return Expr.create(getContext(),
42  Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
43  }
44 
49  public int getNumArgs()
50  {
51  return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
52  }
53 
60  public Expr[] getArgs()
61  {
62  int n = getNumArgs();
63  Expr[] res = new Expr[n];
64  for (int i = 0; i < n; i++)
65  res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
66  getContext().nCtx(), getNativeObject(), i));
67  return res;
68  }
69 
73  @Override
74  public String toString()
75  {
76  int n = getNumArgs();
77  String res = "[";
78  Expr[] args = getArgs();
79  for (int i = 0; i < n; i++)
80  res += args[i] + ", ";
81  return res + getValue() + "]";
82  }
83 
84  Entry(Context ctx, long obj) {
85  super(ctx, obj);
86  }
87 
88  @Override
89  void incRef() {
90  Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
91  }
92 
93  @Override
94  void addToReferenceQueue() {
95  getContext().getFuncEntryDRQ().storeReference(getContext(), this);
96  }
97  }
98 
104  public int getNumEntries()
105  {
106  return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
107  }
108 
115  public Entry[] getEntries()
116  {
117  int n = getNumEntries();
118  Entry[] res = new Entry[n];
119  for (int i = 0; i < n; i++)
120  res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
121  .nCtx(), getNativeObject(), i));
122  return res;
123  }
124 
132  public Expr getElse()
133  {
134  return Expr.create(getContext(),
135  Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
136  }
137 
143  public int getArity()
144  {
145  return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
146  }
147 
151  public String toString()
152  {
153  String res = "";
154  res += "[";
155  for (Entry e : getEntries())
156  {
157  int n = e.getNumArgs();
158  if (n > 1)
159  res += "[";
160  Expr[] args = e.getArgs();
161  for (int i = 0; i < n; i++)
162  {
163  if (i != 0)
164  res += ", ";
165  res += args[i];
166  }
167  if (n > 1)
168  res += "]";
169  res += " -> " + e.getValue() + ", ";
170  }
171  res += "else -> " + getElse();
172  res += "]";
173  return res;
174  }
175 
176  FuncInterp(Context ctx, long obj)
177  {
178  super(ctx, obj);
179  }
180 
181  @Override
182  void incRef() {
183  Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
184  }
185 
186  @Override
187  void addToReferenceQueue() {
188  getContext().getFuncInterpDRQ().storeReference(getContext(), this);
189  }
190 }
static long funcInterpGetElse(long a0, long a1)
Definition: Native.java:3289
static int funcInterpGetNumEntries(long a0, long a1)
Definition: Native.java:3271
static long funcEntryGetValue(long a0, long a1)
Definition: Native.java:3323
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:3954
void storeReference(Context ctx, T obj)
static void funcInterpIncRef(long a0, long a1)
Definition: Native.java:3255
static long funcEntryGetArg(long a0, long a1, int a2)
Definition: Native.java:3341
static int funcInterpGetArity(long a0, long a1)
Definition: Native.java:3298
static long funcInterpGetEntry(long a0, long a1, int a2)
Definition: Native.java:3280
Expr [] getArgs()
Definition: Expr.java:105
static int funcEntryGetNumArgs(long a0, long a1)
Definition: Native.java:3332
static void funcEntryIncRef(long a0, long a1)
Definition: Native.java:3307
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
Definition: Context.java:3959
def String(name, ctx=None)
Definition: z3py.py:9443