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 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  public String toString()
74  {
75  try
76  {
77  int n = getNumArgs();
78  String res = "[";
79  Expr[] args = getArgs();
80  for (int i = 0; i < n; i++)
81  res += args[i] + ", ";
82  return res + getValue() + "]";
83  } catch (Z3Exception e)
84  {
85  return new String("Z3Exception: " + e.getMessage());
86  }
87  }
88 
89  Entry(Context ctx, long obj)
90  {
91  super(ctx, obj);
92  }
93 
94  void incRef(long o)
95  {
96  getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
97  super.incRef(o);
98  }
99 
100  void decRef(long o)
101  {
102  getContext().getFuncEntryDRQ().add(o);
103  super.decRef(o);
104  }
105  };
106 
112  public int getNumEntries()
113  {
114  return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
115  }
116 
123  public Entry[] getEntries()
124  {
125  int n = getNumEntries();
126  Entry[] res = new Entry[n];
127  for (int i = 0; i < n; i++)
128  res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
129  .nCtx(), getNativeObject(), i));
130  return res;
131  }
132 
140  public Expr getElse()
141  {
142  return Expr.create(getContext(),
143  Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
144  }
145 
151  public int getArity()
152  {
153  return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
154  }
155 
159  public String toString()
160  {
161  try
162  {
163  String res = "";
164  res += "[";
165  for (Entry e : getEntries())
166  {
167  int n = e.getNumArgs();
168  if (n > 1)
169  res += "[";
170  Expr[] args = e.getArgs();
171  for (int i = 0; i < n; i++)
172  {
173  if (i != 0)
174  res += ", ";
175  res += args[i];
176  }
177  if (n > 1)
178  res += "]";
179  res += " -> " + e.getValue() + ", ";
180  }
181  res += "else -> " + getElse();
182  res += "]";
183  return res;
184  } catch (Z3Exception e)
185  {
186  return new String("Z3Exception: " + e.getMessage());
187  }
188  }
189 
190  FuncInterp(Context ctx, long obj)
191  {
192  super(ctx, obj);
193  }
194 
195  void incRef(long o)
196  {
197  getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
198  super.incRef(o);
199  }
200 
201  void decRef(long o)
202  {
203  getContext().getFuncInterpDRQ().add(o);
204  super.decRef(o);
205  }
206 }
Expr[] getArgs()
Definition: FuncInterp.java:60
static long funcInterpGetElse(long a0, long a1)
Definition: Native.java:3022
static int funcInterpGetNumEntries(long a0, long a1)
Definition: Native.java:3004
static long funcEntryGetValue(long a0, long a1)
Definition: Native.java:3056
IDecRefQueue getFuncInterpDRQ()
Definition: Context.java:3709
int getNumArgs()
Definition: FuncInterp.java:49
Definition: FuncInterp.java:31
static long funcEntryGetArg(long a0, long a1, int a2)
Definition: Native.java:3074
String toString()
Definition: FuncInterp.java:73
void incAndClear(Context ctx, long o)
static int funcInterpGetArity(long a0, long a1)
Definition: Native.java:3031
static long funcInterpGetEntry(long a0, long a1, int a2)
Definition: Native.java:3013
Expr[] getArgs()
Definition: Expr.java:105
Expr getValue()
Definition: FuncInterp.java:39
static int funcEntryGetNumArgs(long a0, long a1)
Definition: Native.java:3065
IDecRefQueue getFuncEntryDRQ()
Definition: Context.java:3704