Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Model.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Model.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Models
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Model : Z3Object
30  {
36  public Expr ConstInterp(Expr a)
37  {
38  Contract.Requires(a != null);
39 
40  Context.CheckContextMatch(a);
41  return ConstInterp(a.FuncDecl);
42  }
43 
50  {
51  Contract.Requires(f != null);
52 
53  Context.CheckContextMatch(f);
54  if (f.Arity != 0 ||
55  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)Z3_sort_kind.Z3_ARRAY_SORT)
56  throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
57 
58  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
59  if (n == IntPtr.Zero)
60  return null;
61  else
62  return Expr.Create(Context, n);
63  }
64 
71  {
72  Contract.Requires(f != null);
73 
74  Context.CheckContextMatch(f);
75 
77 
78  if (f.Arity == 0)
79  {
80  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
81 
82  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
83  {
84  if (n == IntPtr.Zero)
85  return null;
86  else
87  {
88  if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
89  throw new Z3Exception("Argument was not an array constant");
90  IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
91  return FuncInterp(new FuncDecl(Context, fd));
92  }
93  }
94  else
95  {
96  throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
97  }
98  }
99  else
100  {
101  IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
102  if (n == IntPtr.Zero)
103  return null;
104  else
105  return new FuncInterp(Context, n);
106  }
107  }
108 
112  public uint NumConsts
113  {
114  get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
115  }
116 
120  public FuncDecl[] ConstDecls
121  {
122  get
123  {
124  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
125 
126  uint n = NumConsts;
127  FuncDecl[] res = new FuncDecl[n];
128  for (uint i = 0; i < n; i++)
129  res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
130  return res;
131  }
132  }
133 
137  public uint NumFuncs
138  {
139  get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
140  }
141 
145  public FuncDecl[] FuncDecls
146  {
147  get
148  {
149  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
150 
151  uint n = NumFuncs;
152  FuncDecl[] res = new FuncDecl[n];
153  for (uint i = 0; i < n; i++)
154  res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
155  return res;
156  }
157  }
158 
162  public FuncDecl[] Decls
163  {
164  get
165  {
166  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
167 
168  uint nFuncs = NumFuncs;
169  uint nConsts = NumConsts;
170  uint n = nFuncs + nConsts;
171  FuncDecl[] res = new FuncDecl[n];
172  for (uint i = 0; i < nConsts; i++)
173  res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
174  for (uint i = 0; i < nFuncs; i++)
175  res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
176  return res;
177  }
178  }
179 
184  {
188  public ModelEvaluationFailedException() : base() { }
189  }
190 
205  public Expr Eval(Expr t, bool completion = false)
206  {
207  Contract.Requires(t != null);
208  Contract.Ensures(Contract.Result<Expr>() != null);
209 
210  IntPtr v = IntPtr.Zero;
211  if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
212  throw new ModelEvaluationFailedException();
213  else
214  return Expr.Create(Context, v);
215  }
216 
220  public Expr Evaluate(Expr t, bool completion = false)
221  {
222  Contract.Requires(t != null);
223  Contract.Ensures(Contract.Result<Expr>() != null);
224 
225  return Eval(t, completion);
226  }
227 
231  public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }
232 
243  public Sort[] Sorts
244  {
245  get
246  {
247  Contract.Ensures(Contract.Result<Sort[]>() != null);
248 
249  uint n = NumSorts;
250  Sort[] res = new Sort[n];
251  for (uint i = 0; i < n; i++)
252  res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
253  return res;
254  }
255  }
256 
263  public Expr[] SortUniverse(Sort s)
264  {
265  Contract.Requires(s != null);
266  Contract.Ensures(Contract.Result<Expr[]>() != null);
267 
268  ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
269  uint n = nUniv.Size;
270  Expr[] res = new Expr[n];
271  for (uint i = 0; i < n; i++)
272  res[i] = Expr.Create(Context, nUniv[i].NativeObject);
273  return res;
274  }
275 
280  public override string ToString()
281  {
282  return Native.Z3_model_to_string(Context.nCtx, NativeObject);
283  }
284 
285  #region Internal
286  internal Model(Context ctx, IntPtr obj)
287  : base(ctx, obj)
288  {
289  Contract.Requires(ctx != null);
290  }
291 
292  internal class DecRefQueue : IDecRefQueue
293  {
294  public override void IncRef(Context ctx, IntPtr obj)
295  {
296  Native.Z3_model_inc_ref(ctx.nCtx, obj);
297  }
298 
299  public override void DecRef(Context ctx, IntPtr obj)
300  {
301  Native.Z3_model_dec_ref(ctx.nCtx, obj);
302  }
303  };
304 
305  internal override void IncRef(IntPtr o)
306  {
307  Context.Model_DRQ.IncAndClear(Context, o);
308  base.IncRef(o);
309  }
310 
311  internal override void DecRef(IntPtr o)
312  {
313  Context.Model_DRQ.Add(o);
314  base.DecRef(o);
315  }
316  #endregion
317  }
318 }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model...
Definition: Model.cs:183
static Z3_ast_vector Z3_model_get_sort_universe(Z3_context a0, Z3_model a1, Z3_sort a2)
Definition: Native.cs:3700
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
Definition: Model.cs:205
static uint Z3_model_get_num_sorts(Z3_context a0, Z3_model a1)
Definition: Native.cs:3684
Expr ConstInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of f in the model.
Definition: Model.cs:49
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2950
static uint Z3_model_get_num_consts(Z3_context a0, Z3_model a1)
Definition: Native.cs:3652
Z3_sort_kind
Z3_sort_kind
Definition: Enumerations.cs:34
Expr[] SortUniverse(Sort s)
The finite set of distinct values that represent the interpretation for sort s .
Definition: Model.cs:263
static int Z3_model_eval(Z3_context a0, Z3_model a1, Z3_ast a2, int a3, [In, Out] ref Z3_ast a4)
Definition: Native.cs:3620
static Z3_func_decl Z3_model_get_func_decl(Z3_context a0, Z3_model a1, uint a2)
Definition: Native.cs:3676
uint Arity
The arity of the function declaration
Definition: FuncDecl.cs:91
static Z3_func_interp Z3_model_get_func_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
Definition: Native.cs:3644
static int Z3_is_as_array(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3708
static Z3_ast Z3_model_get_const_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
Definition: Native.cs:3628
Expressions are terms.
Definition: Expr.cs:29
static Z3_func_decl Z3_get_as_array_func_decl(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3716
static uint Z3_model_get_num_funcs(Z3_context a0, Z3_model a1)
Definition: Native.cs:3668
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
Definition: Model.cs:36
static Z3_sort Z3_model_get_sort(Z3_context a0, Z3_model a1, uint a2)
Definition: Native.cs:3692
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Definition: Model.cs:70
Expr Evaluate(Expr t, bool completion=false)
Alias for Eval.
Definition: Model.cs:220
static Z3_func_decl Z3_model_get_const_decl(Z3_context a0, Z3_model a1, uint a2)
Definition: Native.cs:3660
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3126
override string ToString()
Conversion of models to strings.
Definition: Model.cs:280
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
ModelEvaluationFailedException()
An exception that is thrown when model evaluation fails.
Definition: Model.cs:188
Function declarations.
Definition: FuncDecl.cs:29
static string Z3_model_to_string(Z3_context a0, Z3_model a1)
Definition: Native.cs:3864
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
Definition: FuncInterp.cs:30