Z3
Model.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_sort_kind;
21
25public class Model extends Z3Object {
36 {
37 getContext().checkContextMatch(a);
38 return getConstInterp(a.getFuncDecl());
39 }
40
51 {
52 getContext().checkContextMatch(f);
53 if (f.getArity() != 0)
54 throw new Z3Exception(
55 "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
56
57 long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
58 f.getNativeObject());
59 if (n == 0)
60 return null;
61 else
62 return Expr.create(getContext(), n);
63 }
64
74 {
75 getContext().checkContextMatch(f);
76
78 .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
79
80 if (f.getArity() == 0)
81 {
82 long n = Native.modelGetConstInterp(getContext().nCtx(),
83 getNativeObject(), f.getNativeObject());
84
86 {
87 if (n == 0)
88 return null;
89 else
90 {
91 if (Native.isAsArray(getContext().nCtx(), n)) {
92 long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
93 return getFuncInterp(new FuncDecl(getContext(), fd));
94 }
95 return null;
96 }
97 } else
98 {
99 throw new Z3Exception(
100 "Constant functions do not have a function interpretation; use getConstInterp");
101 }
102 } else
103 {
104 long n = Native.modelGetFuncInterp(getContext().nCtx(),
105 getNativeObject(), f.getNativeObject());
106 if (n == 0)
107 return null;
108 else
109 return new FuncInterp(getContext(), n);
110 }
111 }
112
116 public int getNumConsts()
117 {
118 return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
119 }
120
127 {
128 int n = getNumConsts();
129 FuncDecl[] res = new FuncDecl[n];
130 for (int i = 0; i < n; i++)
131 res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
132 .nCtx(), getNativeObject(), i));
133 return res;
134 }
135
139 public int getNumFuncs()
140 {
141 return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
142 }
143
150 {
151 int n = getNumFuncs();
152 FuncDecl[] res = new FuncDecl[n];
153 for (int i = 0; i < n; i++)
154 res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
155 .nCtx(), getNativeObject(), i));
156 return res;
157 }
158
165 {
166 int nFuncs = getNumFuncs();
167 int nConsts = getNumConsts();
168 int n = nFuncs + nConsts;
169 FuncDecl[] res = new FuncDecl[n];
170 for (int i = 0; i < nConsts; i++)
171 res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
172 .nCtx(), getNativeObject(), i));
173 for (int i = 0; i < nFuncs; i++)
174 res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
175 getContext().nCtx(), getNativeObject(), i));
176 return res;
177 }
178
183 @SuppressWarnings("serial")
185 {
190 {
191 super();
192 }
193 }
194
208 public Expr eval(Expr t, boolean completion)
209 {
210 Native.LongPtr v = new Native.LongPtr();
211 if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
212 t.getNativeObject(), (completion), v))
214 else
215 return Expr.create(getContext(), v.value);
216 }
217
223 public Expr evaluate(Expr t, boolean completion)
224 {
225 return eval(t, completion);
226 }
227
232 public int getNumSorts()
233 {
234 return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
235 }
236
248 public Sort[] getSorts()
249 {
250
251 int n = getNumSorts();
252 Sort[] res = new Sort[n];
253 for (int i = 0; i < n; i++)
254 res[i] = Sort.create(getContext(),
255 Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
256 return res;
257 }
258
269 {
270
271 ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
272 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
273 return nUniv.ToExprArray();
274 }
275
281 @Override
282 public String toString() {
283 return Native.modelToString(getContext().nCtx(), getNativeObject());
284 }
285
286 Model(Context ctx, long obj)
287 {
288 super(ctx, obj);
289 }
290
291 @Override
292 void incRef() {
293 Native.modelIncRef(getContext().nCtx(), getNativeObject());
294 }
295
296 @Override
297 void addToReferenceQueue() {
298 getContext().getModelDRQ().storeReference(getContext(), this);
299 }
300}
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:4063
FuncDecl getFuncDecl()
Definition: Expr.java:72
void storeReference(Context ctx, T obj)
FuncDecl[] getConstDecls()
Definition: Model.java:126
Expr eval(Expr t, boolean completion)
Definition: Model.java:208
Expr getConstInterp(FuncDecl f)
Definition: Model.java:50
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:73
Expr evaluate(Expr t, boolean completion)
Definition: Model.java:223
Expr getConstInterp(Expr a)
Definition: Model.java:35
Expr[] getSortUniverse(Sort s)
Definition: Model.java:268
FuncDecl[] getDecls()
Definition: Model.java:164
FuncDecl[] getFuncDecls()
Definition: Model.java:149
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:3591
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:3546
static int getSortKind(long a0, long a1)
Definition: Native.java:2693
static long modelGetSortUniverse(long a0, long a1, long a2)
Definition: Native.java:3627
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:3573
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:3600
static String modelToString(long a0, long a1)
Definition: Native.java:3856
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:3582
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
Definition: Native.java:3537
static long getRange(long a0, long a1)
Definition: Native.java:2945
static long modelGetSort(long a0, long a1, int a2)
Definition: Native.java:3618
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:3564
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:3654
static int modelGetNumSorts(long a0, long a1)
Definition: Native.java:3609
static boolean isAsArray(long a0, long a1)
Definition: Native.java:3645
static final Z3_sort_kind fromInt(int v)
def String(name, ctx=None)
Definition: z3py.py:10085