Z3
FuncInterp.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
25public 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
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}
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
Definition: Context.java:4053
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:4048
Expr[] getArgs()
Definition: Expr.java:105
void storeReference(Context ctx, T obj)
static int funcInterpGetArity(long a0, long a1)
Definition: Native.java:3731
static long funcEntryGetValue(long a0, long a1)
Definition: Native.java:3764
static long funcInterpGetElse(long a0, long a1)
Definition: Native.java:3714
static void funcEntryIncRef(long a0, long a1)
Definition: Native.java:3748
static long funcInterpGetEntry(long a0, long a1, int a2)
Definition: Native.java:3705
static int funcEntryGetNumArgs(long a0, long a1)
Definition: Native.java:3773
static long funcEntryGetArg(long a0, long a1, int a2)
Definition: Native.java:3782
static int funcInterpGetNumEntries(long a0, long a1)
Definition: Native.java:3696
def String(name, ctx=None)
Definition: z3py.py:10085