Z3
Model.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Model.cs
7
8Abstract:
9
10 Z3 Managed API: Models
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Collections.Generic;
23
24namespace Microsoft.Z3
25{
29 public class Model : Z3Object
30 {
37 {
38 Debug.Assert(a != null);
39
40 Context.CheckContextMatch(a);
41 return ConstInterp(a.FuncDecl);
42 }
43
50 {
51 Debug.Assert(f != null);
52
53 Context.CheckContextMatch(f);
54 if (f.Arity != 0)
55 throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
56
57 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
58 if (n == IntPtr.Zero)
59 return null;
60 else
61 return Expr.Create(Context, n);
62 }
63
70 {
71 Debug.Assert(f != null);
72
73 Context.CheckContextMatch(f);
74
75 Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));
76
77 if (f.Arity == 0)
78 {
79 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
80
81 if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
82 {
83 if (n == IntPtr.Zero)
84 return null;
85 else
86 {
87 if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
88 throw new Z3Exception("Argument was not an array constant");
89 IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
90 return FuncInterp(new FuncDecl(Context, fd));
91 }
92 }
93 else
94 {
95 throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
96 }
97 }
98 else
99 {
100 IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
101 if (n == IntPtr.Zero)
102 return null;
103 else
104 return new FuncInterp(Context, n);
105 }
106 }
107
111 public uint NumConsts
112 {
113 get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
114 }
115
120 {
121 get
122 {
123
124 uint n = NumConsts;
125 FuncDecl[] res = new FuncDecl[n];
126 for (uint i = 0; i < n; i++)
127 res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
128 return res;
129 }
130 }
131
135 public IEnumerable<KeyValuePair<FuncDecl, Expr>> Consts
136 {
137 get
138 {
139 uint nc = NumConsts;
140 for (uint i = 0; i < nc; ++i)
141 {
142 var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
143 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
144 if (n == IntPtr.Zero) continue;
145 yield return new KeyValuePair<FuncDecl, Expr>(f, Expr.Create(Context, n));
146 }
147 }
148 }
149
153 public uint NumFuncs
154 {
155 get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
156 }
157
162 {
163 get
164 {
165
166 uint n = NumFuncs;
167 FuncDecl[] res = new FuncDecl[n];
168 for (uint i = 0; i < n; i++)
169 res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
170 return res;
171 }
172 }
173
178 {
179 get
180 {
181
182 uint nFuncs = NumFuncs;
183 uint nConsts = NumConsts;
184 uint n = nFuncs + nConsts;
185 FuncDecl[] res = new FuncDecl[n];
186 for (uint i = 0; i < nConsts; i++)
187 res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
188 for (uint i = 0; i < nFuncs; i++)
189 res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
190 return res;
191 }
192 }
193
198 {
202 public ModelEvaluationFailedException() : base() { }
203 }
204
219 public Expr Eval(Expr t, bool completion = false)
220 {
221 Debug.Assert(t != null);
222
223 IntPtr v = IntPtr.Zero;
224 if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0)
226 else
227 return Expr.Create(Context, v);
228 }
229
233 public Expr Evaluate(Expr t, bool completion = false)
234 {
235 Debug.Assert(t != null);
236
237 return Eval(t, completion);
238 }
239
243 public double Double(Expr t) {
244 var r = Eval(t, true);
245 return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject);
246 }
247
251 public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }
252
263 public Sort[] Sorts
264 {
265 get
266 {
267
268 uint n = NumSorts;
269 Sort[] res = new Sort[n];
270 for (uint i = 0; i < n; i++)
271 res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
272 return res;
273 }
274 }
275
283 {
284 Debug.Assert(s != null);
285
286 ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
287 return av.ToExprArray();
288 }
289
294 public override string ToString()
295 {
296 return Native.Z3_model_to_string(Context.nCtx, NativeObject);
297 }
298
299 #region Internal
300 internal Model(Context ctx, IntPtr obj)
301 : base(ctx, obj)
302 {
303 Debug.Assert(ctx != null);
304 }
305
306 internal class DecRefQueue : IDecRefQueue
307 {
308 public DecRefQueue() : base() { }
309 public DecRefQueue(uint move_limit) : base(move_limit) { }
310 internal override void IncRef(Context ctx, IntPtr obj)
311 {
312 Native.Z3_model_inc_ref(ctx.nCtx, obj);
313 }
314
315 internal override void DecRef(Context ctx, IntPtr obj)
316 {
317 Native.Z3_model_dec_ref(ctx.nCtx, obj);
318 }
319 };
320
321 internal override void IncRef(IntPtr o)
322 {
323 Context.Model_DRQ.IncAndClear(Context, o);
324 base.IncRef(o);
325 }
326
327 internal override void DecRef(IntPtr o)
328 {
329 Context.Model_DRQ.Add(o);
330 base.DecRef(o);
331 }
332 #endregion
333 }
334}
Vectors of ASTs.
Definition: ASTVector.cs:29
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
Definition: ASTVector.cs:115
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue Model_DRQ
Model DRQ
Definition: Context.cs:4760
Expressions are terms.
Definition: Expr.cs:31
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Function declarations.
Definition: FuncDecl.cs:31
uint Arity
The arity of the function declaration
Definition: FuncDecl.cs:92
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
Definition: FuncInterp.cs:30
A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
Definition: Model.cs:198
ModelEvaluationFailedException()
An exception that is thrown when model evaluation fails.
Definition: Model.cs:202
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:30
FuncDecl[] Decls
All symbols that have an interpretation in the model.
Definition: Model.cs:178
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
Definition: Model.cs:36
Expr Evaluate(Expr t, bool completion=false)
Alias for Eval.
Definition: Model.cs:233
FuncDecl[] FuncDecls
The function declarations of the function interpretations in the model.
Definition: Model.cs:162
double Double(Expr t)
Evaluate expression to a double, assuming it is a numeral already.
Definition: Model.cs:243
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Definition: Model.cs:69
Expr[] SortUniverse(Sort s)
The finite set of distinct values that represent the interpretation for sort s .
Definition: Model.cs:282
Sort[] Sorts
The uninterpreted sorts that the model has an interpretation for.
Definition: Model.cs:264
IEnumerable< KeyValuePair< FuncDecl, Expr > > Consts
Enumerate constants in model.
Definition: Model.cs:136
FuncDecl[] ConstDecls
The function declarations of the constants in the model.
Definition: Model.cs:120
override string ToString()
Conversion of models to strings.
Definition: Model.cs:294
uint NumFuncs
The number of function interpretations in the model.
Definition: Model.cs:154
Expr ConstInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of f in the model.
Definition: Model.cs:49
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
Definition: Model.cs:219
uint NumConsts
The number of constants that have an interpretation in the model.
Definition: Model.cs:112
uint NumSorts
The number of uninterpreted sorts that the model has an interpretation for.
Definition: Model.cs:251
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150