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  {
38  public Expr getValue() throws Z3Exception
39  {
40  return Expr.create(getContext(),
41  Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
42  }
43 
47  public int getNumArgs() throws Z3Exception
48  {
49  return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
50  }
51 
57  public Expr[] getArgs() throws Z3Exception
58  {
59  int n = getNumArgs();
60  Expr[] res = new Expr[n];
61  for (int i = 0; i < n; i++)
62  res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
63  getContext().nCtx(), getNativeObject(), i));
64  return res;
65  }
66 
70  public String toString()
71  {
72  try
73  {
74  int n = getNumArgs();
75  String res = "[";
76  Expr[] args = getArgs();
77  for (int i = 0; i < n; i++)
78  res += args[i] + ", ";
79  return res + getValue() + "]";
80  } catch (Z3Exception e)
81  {
82  return new String("Z3Exception: " + e.getMessage());
83  }
84  }
85 
86  Entry(Context ctx, long obj) throws Z3Exception
87  {
88  super(ctx, obj);
89  }
90 
91  void incRef(long o) throws Z3Exception
92  {
93  getContext().funcEntry_DRQ().incAndClear(getContext(), o);
94  super.incRef(o);
95  }
96 
97  void decRef(long o) throws Z3Exception
98  {
99  getContext().funcEntry_DRQ().add(o);
100  super.decRef(o);
101  }
102  };
103 
107  public int getNumEntries() throws Z3Exception
108  {
109  return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
110  }
111 
117  public Entry[] getEntries() throws Z3Exception
118  {
119  int n = getNumEntries();
120  Entry[] res = new Entry[n];
121  for (int i = 0; i < n; i++)
122  res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
123  .nCtx(), getNativeObject(), i));
124  return res;
125  }
126 
132  public Expr getElse() throws Z3Exception
133  {
134  return Expr.create(getContext(),
135  Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
136  }
137 
141  public int getArity() throws Z3Exception
142  {
143  return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
144  }
145 
149  public String toString()
150  {
151  try
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  } catch (Z3Exception e)
175  {
176  return new String("Z3Exception: " + e.getMessage());
177  }
178  }
179 
180  FuncInterp(Context ctx, long obj) throws Z3Exception
181  {
182  super(ctx, obj);
183  }
184 
185  void incRef(long o) throws Z3Exception
186  {
187  getContext().funcInterp_DRQ().incAndClear(getContext(), o);
188  super.incRef(o);
189  }
190 
191  void decRef(long o) throws Z3Exception
192  {
193  getContext().funcInterp_DRQ().add(o);
194  super.decRef(o);
195  }
196 }
Expr[] getArgs()
Definition: FuncInterp.java:57
static long funcInterpGetElse(long a0, long a1)
Definition: Native.java:2899
static int funcInterpGetNumEntries(long a0, long a1)
Definition: Native.java:2881
static long funcEntryGetValue(long a0, long a1)
Definition: Native.java:2933
int getNumArgs()
Definition: FuncInterp.java:47
Definition: FuncInterp.java:31
static long funcEntryGetArg(long a0, long a1, int a2)
Definition: Native.java:2951
String toString()
Definition: FuncInterp.java:70
static int funcInterpGetArity(long a0, long a1)
Definition: Native.java:2908
static long funcInterpGetEntry(long a0, long a1, int a2)
Definition: Native.java:2890
Expr[] getArgs()
Definition: Expr.java:90
Expr getValue()
Definition: FuncInterp.java:38
static int funcEntryGetNumArgs(long a0, long a1)
Definition: Native.java:2942