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 }
com.microsoft.z3.Native.funcInterpGetArity
static int funcInterpGetArity(long a0, long a1)
Definition: Native.java:3731
com.microsoft.z3.Context.getFuncEntryDRQ
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:4048
com.microsoft.z3.Native.funcInterpGetEntry
static long funcInterpGetEntry(long a0, long a1, int a2)
Definition: Native.java:3705
com.microsoft.z3.Native.funcEntryGetValue
static long funcEntryGetValue(long a0, long a1)
Definition: Native.java:3764
com.microsoft.z3.Native.funcEntryGetArg
static long funcEntryGetArg(long a0, long a1, int a2)
Definition: Native.java:3782
com.microsoft.z3.FuncInterp.getElse
Expr getElse()
Definition: FuncInterp.java:132
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Context.getFuncInterpDRQ
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
Definition: Context.java:4053
com.microsoft.z3.FuncInterp.getNumEntries
int getNumEntries()
Definition: FuncInterp.java:104
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Expr.getArgs
Expr[] getArgs()
Definition: Expr.java:105
com.microsoft.z3.Native.funcInterpGetNumEntries
static int funcInterpGetNumEntries(long a0, long a1)
Definition: Native.java:3696
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.Native.funcInterpGetElse
static long funcInterpGetElse(long a0, long a1)
Definition: Native.java:3714
com.microsoft.z3.FuncInterp.getEntries
Entry[] getEntries()
Definition: FuncInterp.java:115
com.microsoft.z3.FuncInterp.getArity
int getArity()
Definition: FuncInterp.java:143
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Native.funcEntryIncRef
static void funcEntryIncRef(long a0, long a1)
Definition: Native.java:3748
com.microsoft.z3.FuncInterp.toString
String toString()
Definition: FuncInterp.java:151
com.microsoft.z3.FuncInterp
Definition: FuncInterp.java:25
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Native.funcEntryGetNumArgs
static int funcEntryGetNumArgs(long a0, long a1)
Definition: Native.java:3773
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10085