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
25@SuppressWarnings("unchecked")
26public class Model extends Z3Object {
36 public <R extends Sort> Expr<R> getConstInterp(Expr<R> a)
37 {
38 getContext().checkContextMatch(a);
39 return getConstInterp(a.getFuncDecl());
40 }
41
51 public <R extends Sort> Expr<R> getConstInterp(FuncDecl<R> f)
52 {
53 getContext().checkContextMatch(f);
54 if (f.getArity() != 0)
55 throw new Z3Exception(
56 "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
57
58 long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
59 f.getNativeObject());
60 if (n == 0)
61 return null;
62 else
63 return (Expr<R>) Expr.create(getContext(), n);
64 }
65
74 public <R extends Sort> FuncInterp<R> getFuncInterp(FuncDecl<R> f)
75 {
76 getContext().checkContextMatch(f);
77
78 Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext()
79 .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
80
81 if (f.getArity() == 0)
82 {
83 long n = Native.modelGetConstInterp(getContext().nCtx(),
84 getNativeObject(), f.getNativeObject());
85
86 if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
87 {
88 if (n == 0)
89 return null;
90 else
91 {
92 if (Native.isAsArray(getContext().nCtx(), n)) {
93 long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
94 return getFuncInterp(new FuncDecl<>(getContext(), fd));
95 }
96 return null;
97 }
98 } else
99 {
100 throw new Z3Exception(
101 "Constant functions do not have a function interpretation; use getConstInterp");
102 }
103 } else
104 {
105 long n = Native.modelGetFuncInterp(getContext().nCtx(),
106 getNativeObject(), f.getNativeObject());
107 if (n == 0)
108 return null;
109 else
110 return new FuncInterp<>(getContext(), n);
111 }
112 }
113
117 public int getNumConsts()
118 {
119 return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
120 }
121
128 {
129 int n = getNumConsts();
130 FuncDecl<?>[] res = new FuncDecl[n];
131 for (int i = 0; i < n; i++)
132 res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
133 .nCtx(), getNativeObject(), i));
134 return res;
135 }
136
140 public int getNumFuncs()
141 {
142 return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
143 }
144
151 {
152 int n = getNumFuncs();
153 FuncDecl<?>[] res = new FuncDecl[n];
154 for (int i = 0; i < n; i++)
155 res[i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(getContext()
156 .nCtx(), getNativeObject(), i));
157 return res;
158 }
159
166 {
167 int nFuncs = getNumFuncs();
168 int nConsts = getNumConsts();
169 int n = nFuncs + nConsts;
170 FuncDecl<?>[] res = new FuncDecl[n];
171 for (int i = 0; i < nConsts; i++)
172 res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
173 .nCtx(), getNativeObject(), i));
174 for (int i = 0; i < nFuncs; i++)
175 res[nConsts + i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(
176 getContext().nCtx(), getNativeObject(), i));
177 return res;
178 }
179
184 @SuppressWarnings("serial")
186 {
191 {
192 super();
193 }
194 }
195
209 public <R extends Sort> Expr<R> eval(Expr<R> t, boolean completion)
210 {
211 Native.LongPtr v = new Native.LongPtr();
212 if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
213 t.getNativeObject(), (completion), v))
214 throw new ModelEvaluationFailedException();
215 else
216 return (Expr<R>) Expr.create(getContext(), v.value);
217 }
218
224 public <R extends Sort> Expr<R> evaluate(Expr<R> t, boolean completion)
225 {
226 return eval(t, completion);
227 }
228
233 public int getNumSorts()
234 {
235 return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
236 }
237
249 public Sort[] getSorts()
250 {
251
252 int n = getNumSorts();
253 Sort[] res = new Sort[n];
254 for (int i = 0; i < n; i++)
255 res[i] = Sort.create(getContext(),
256 Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
257 return res;
258 }
259
269 public <R extends Sort> Expr<R>[] getSortUniverse(R s)
270 {
271
272 ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
273 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
274 return (Expr<R>[]) nUniv.ToExprArray();
275 }
276
282 @Override
283 public String toString() {
284 return Native.modelToString(getContext().nCtx(), getNativeObject());
285 }
286
287 Model(Context ctx, long obj)
288 {
289 super(ctx, obj);
290 }
291
292 @Override
293 void incRef() {
294 Native.modelIncRef(getContext().nCtx(), getNativeObject());
295 }
296
297 @Override
298 void addToReferenceQueue() {
299 getContext().getModelDRQ().storeReference(getContext(), this);
300 }
301}
FuncDecl< R > getFuncDecl()
Definition: Expr.java:76
FuncDecl<?>[] getFuncDecls()
Definition: Model.java:150
FuncDecl<?>[] getConstDecls()
Definition: Model.java:127
FuncDecl<?>[] getDecls()
Definition: Model.java:165
def String(name, ctx=None)
Definition: z3py.py:10693
def Model(ctx=None)
Definition: z3py.py:6579
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150