Z3 |

FuncInterp.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
25@SuppressWarnings("unchecked")
26public class FuncInterp<R extends Sort> extends Z3Object {
27
32 public static class Entry<R extends Sort> extends Z3Object {
33
40 public Expr<R> getValue()
41 {
42 return (Expr<R>) Expr.create(getContext(),
43 Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
44 }
45
50 public int getNumArgs()
51 {
52 return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
53 }
54
61 public Expr<?>[] getArgs()
62 {
63 int n = getNumArgs();
64 Expr<?>[] res = new Expr[n];
65 for (int i = 0; i < n; i++)
66 res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
67 getContext().nCtx(), getNativeObject(), i));
68 return res;
69 }
70
74 @Override
75 public String toString()
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 }
84
85 Entry(Context ctx, long obj) {
86 super(ctx, obj);
87 }
88
89 @Override
90 void incRef() {
91 Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
92 }
93
94 @Override
95 void addToReferenceQueue() {
96 getContext().getFuncEntryDRQ().storeReference(getContext(), this);
97 }
98 }
99
105 public int getNumEntries()
106 {
107 return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
108 }
109
116 public Entry<R>[] getEntries()
117 {
118 int n = getNumEntries();
119 Entry<R>[] res = new Entry[n];
120 for (int i = 0; i < n; i++)
121 res[i] = new Entry<>(getContext(), Native.funcInterpGetEntry(getContext()
122 .nCtx(), getNativeObject(), i));
123 return res;
124 }
125
133 public Expr<R> getElse()
134 {
135 return (Expr<R>) Expr.create(getContext(),
136 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
137 }
138
144 public int getArity()
145 {
146 return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
147 }
148
152 public String toString()
153 {
154 String res = "";
155 res += "[";
156 for (Entry<R> e : getEntries())
157 {
158 int n = e.getNumArgs();
159 if (n > 1)
160 res += "[";
161 Expr<?>[] args = e.getArgs();
162 for (int i = 0; i < n; i++)
163 {
164 if (i != 0)
165 res += ", ";
166 res += args[i];
167 }
168 if (n > 1)
169 res += "]";
170 res += " -> " + e.getValue() + ", ";
171 }
172 res += "else -> " + getElse();
173 res += "]";
174 return res;
175 }
176
177 FuncInterp(Context ctx, long obj)
178 {
179 super(ctx, obj);
180 }
181
182 @Override
183 void incRef() {
184 Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
185 }
186
187 @Override
188 void addToReferenceQueue() {
189 getContext().getFuncInterpDRQ().storeReference(getContext(), this);
190 }
191}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Expr< R >
com.microsoft.z3.Expr.getArgs
Expr<?>[] getArgs()
Definition: Expr.java:109
com.microsoft.z3.FuncInterp
Definition: FuncInterp.java:26
com.microsoft.z3.FuncInterp.getNumEntries
int getNumEntries()
Definition: FuncInterp.java:105
com.microsoft.z3.FuncInterp.getArity
int getArity()
Definition: FuncInterp.java:144
com.microsoft.z3.FuncInterp.getElse
Expr< R > getElse()
Definition: FuncInterp.java:133
com.microsoft.z3.FuncInterp.getEntries
Entry< R >[] getEntries()
Definition: FuncInterp.java:116
com.microsoft.z3.FuncInterp.toString
String toString()
Definition: FuncInterp.java:152
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693