Z3
FuncInterp.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  FuncInterp.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Function Interpretations
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
22 
23 namespace Microsoft.Z3
24 {
29  [ContractVerification(true)]
30  public class FuncInterp : Z3Object
31  {
36  public class Entry : Z3Object
37  {
41  public Expr Value
42  {
43  get
44  {
45  Contract.Ensures(Contract.Result<Expr>() != null);
46  return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
47  }
48  }
49 
53  public uint NumArgs
54  {
55  get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
56  }
57 
61  public Expr[] Args
62  {
63  get
64  {
65  Contract.Ensures(Contract.Result<Expr[]>() != null);
66  Contract.Ensures(Contract.Result<Expr[]>().Length == this.NumArgs);
67 
68  uint n = NumArgs;
69  Expr[] res = new Expr[n];
70  for (uint i = 0; i < n; i++)
71  res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
72  return res;
73  }
74  }
75 
79  public override string ToString()
80  {
81  uint n = NumArgs;
82  string res = "[";
83  Expr[] args = Args;
84  for (uint i = 0; i < n; i++)
85  res += args[i] + ", ";
86  return res + Value + "]";
87  }
88 
89  #region Internal
90  internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
91 
92  internal class DecRefQueue : IDecRefQueue
93  {
94  public DecRefQueue() : base() { }
95  public DecRefQueue(uint move_limit) : base(move_limit) { }
96  internal override void IncRef(Context ctx, IntPtr obj)
97  {
98  Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
99  }
100 
101  internal override void DecRef(Context ctx, IntPtr obj)
102  {
103  Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
104  }
105  };
106 
107  internal override void IncRef(IntPtr o)
108  {
109  Context.FuncEntry_DRQ.IncAndClear(Context, o);
110  base.IncRef(o);
111  }
112 
113  internal override void DecRef(IntPtr o)
114  {
115  Context.FuncEntry_DRQ.Add(o);
116  base.DecRef(o);
117  }
118  #endregion
119  };
120 
124  public uint NumEntries
125  {
126  get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
127  }
128 
132  public Entry[] Entries
133  {
134  get
135  {
136  Contract.Ensures(Contract.Result<Entry[]>() != null);
137  Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
138 
139  uint n = NumEntries;
140  Entry[] res = new Entry[n];
141  for (uint i = 0; i < n; i++)
142  res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
143  return res;
144  }
145  }
146 
150  public Expr Else
151  {
152  get
153  {
154  Contract.Ensures(Contract.Result<Expr>() != null);
155 
156  return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
157  }
158  }
159 
163  public uint Arity
164  {
165  get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
166  }
167 
171  public override string ToString()
172  {
173  string res = "";
174  res += "[";
175  foreach (Entry e in Entries)
176  {
177  uint n = e.NumArgs;
178  if (n > 1) res += "[";
179  Expr[] args = e.Args;
180  for (uint i = 0; i < n; i++)
181  {
182  if (i != 0) res += ", ";
183  res += args[i];
184  }
185  if (n > 1) res += "]";
186  res += " -> " + e.Value + ", ";
187  }
188  res += "else -> " + Else;
189  res += "]";
190  return res;
191  }
192 
193  #region Internal
194  internal FuncInterp(Context ctx, IntPtr obj)
195  : base(ctx, obj)
196  {
197  Contract.Requires(ctx != null);
198  }
199 
200  internal class DecRefQueue : IDecRefQueue
201  {
202  public DecRefQueue() : base() { }
203  public DecRefQueue(uint move_limit) : base(move_limit) { }
204  internal override void IncRef(Context ctx, IntPtr obj)
205  {
206  Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
207  }
208 
209  internal override void DecRef(Context ctx, IntPtr obj)
210  {
211  Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
212  }
213  };
214 
215  internal override void IncRef(IntPtr o)
216  {
217  Context.FuncInterp_DRQ.IncAndClear(Context, o);
218  base.IncRef(o);
219  }
220 
221  internal override void DecRef(IntPtr o)
222  {
223  Context.FuncInterp_DRQ.Add(o);
224  base.DecRef(o);
225  }
226  #endregion
227  }
228 }
override string ToString()
A string representation of the function entry.
Definition: FuncInterp.cs:79
Expr Value
Return the (symbolic) value of this entry.
Definition: FuncInterp.cs:42
override string ToString()
A string representation of the function interpretation.
Definition: FuncInterp.cs:171
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:71
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
Definition: Context.cs:4903
Expressions are terms.
Definition: Expr.cs:29
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Definition: Context.cs:4908
DecRefQueue interface
Definition: IDecRefQueue.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expr [] Args
The arguments of the function entry.
Definition: FuncInterp.cs:62
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:54
An Entry object represents an element in the finite map used to encode a function interpretation...
Definition: FuncInterp.cs:36
A function interpretation is represented as a finite map and an &#39;else&#39; value. Each entry in the finit...
Definition: FuncInterp.cs:30