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.Diagnostics;
21 using System;
22 
23 namespace Microsoft.Z3
24 {
25     /// <summary>
26     ///  A function interpretation is represented as a finite map and an 'else' value.
27     ///  Each entry in the finite map represents the value of a function given a set of arguments.
28     /// </summary>
29     public class FuncInterp : Z3Object
30     {
31         /// <summary>
32         /// An Entry object represents an element in the finite map used to encode
33         /// a function interpretation.
34         /// </summary>
35         public class Entry : Z3Object
36         {
37             /// <summary>
38             /// Return the (symbolic) value of this entry.
39             /// </summary>
40             public Expr Value
41             {
42                 get
43                 {
44                     return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
45                 }
46             }
47 
48             /// <summary>
49             /// The number of arguments of the entry.
50             /// </summary>
51             public uint NumArgs
52             {
53                 get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
54             }
55 
56             /// <summary>
57             /// The arguments of the function entry.
58             /// </summary>
59             public Expr[] Args
60             {
61                 get
62                 {
63 
64                     uint n = NumArgs;
65                     Expr[] res = new Expr[n];
66                     for (uint i = 0; i < n; i++)
67                         res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
68                     return res;
69                 }
70             }
71 
72             /// <summary>
73             /// A string representation of the function entry.
74             /// </summary>
ToString()75             public override string ToString()
76             {
77                 uint n = NumArgs;
78                 string res = "[";
79                 Expr[] args = Args;
80                 for (uint i = 0; i < n; i++)
81                     res += args[i] + ", ";
82                 return res + Value + "]";
83             }
84 
85             #region Internal
Entry(Context ctx, IntPtr obj)86             internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
87 
88             internal class DecRefQueue : IDecRefQueue
89             {
DecRefQueue()90                 public DecRefQueue() : base() { }
DecRefQueue(uint move_limit)91                 public DecRefQueue(uint move_limit) : base(move_limit) { }
IncRef(Context ctx, IntPtr obj)92                 internal override void IncRef(Context ctx, IntPtr obj)
93                 {
94                     Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
95                 }
96 
DecRef(Context ctx, IntPtr obj)97                 internal override void DecRef(Context ctx, IntPtr obj)
98                 {
99                     Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
100                 }
101             };
102 
IncRef(IntPtr o)103             internal override void IncRef(IntPtr o)
104             {
105                 Context.FuncEntry_DRQ.IncAndClear(Context, o);
106                 base.IncRef(o);
107             }
108 
DecRef(IntPtr o)109             internal override void DecRef(IntPtr o)
110             {
111                 Context.FuncEntry_DRQ.Add(o);
112                 base.DecRef(o);
113             }
114             #endregion
115         };
116 
117         /// <summary>
118         /// The number of entries in the function interpretation.
119         /// </summary>
120         public uint NumEntries
121         {
122             get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
123         }
124 
125         /// <summary>
126         /// The entries in the function interpretation
127         /// </summary>
128         public Entry[] Entries
129         {
130             get
131             {
132 
133                 uint n = NumEntries;
134                 Entry[] res = new Entry[n];
135                 for (uint i = 0; i < n; i++)
136                     res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
137                 return res;
138             }
139         }
140 
141         /// <summary>
142         /// The (symbolic) `else' value of the function interpretation.
143         /// </summary>
144         public Expr Else
145         {
146             get
147             {
148 
149                 return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
150             }
151         }
152 
153         /// <summary>
154         /// The arity of the function interpretation
155         /// </summary>
156         public uint Arity
157         {
158             get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
159         }
160 
161         /// <summary>
162         /// A string representation of the function interpretation.
163         /// </summary>
ToString()164         public override string ToString()
165         {
166             string res = "";
167             res += "[";
168             foreach (Entry e in Entries)
169             {
170                 uint n = e.NumArgs;
171                 if (n > 1) res += "[";
172                 Expr[] args = e.Args;
173                 for (uint i = 0; i < n; i++)
174                 {
175                     if (i != 0) res += ", ";
176                     res += args[i];
177                 }
178                 if (n > 1) res += "]";
179                 res += " -> " + e.Value + ", ";
180             }
181             res += "else -> " + Else;
182             res += "]";
183             return res;
184         }
185 
186         #region Internal
FuncInterp(Context ctx, IntPtr obj)187         internal FuncInterp(Context ctx, IntPtr obj)
188             : base(ctx, obj)
189         {
190             Debug.Assert(ctx != null);
191         }
192 
193         internal class DecRefQueue : IDecRefQueue
194         {
DecRefQueue()195             public DecRefQueue() : base() { }
DecRefQueue(uint move_limit)196             public DecRefQueue(uint move_limit) : base(move_limit) { }
IncRef(Context ctx, IntPtr obj)197             internal override void IncRef(Context ctx, IntPtr obj)
198             {
199                 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
200             }
201 
DecRef(Context ctx, IntPtr obj)202             internal override void DecRef(Context ctx, IntPtr obj)
203             {
204                 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
205             }
206         };
207 
IncRef(IntPtr o)208         internal override void IncRef(IntPtr o)
209         {
210             Context.FuncInterp_DRQ.IncAndClear(Context, o);
211             base.IncRef(o);
212         }
213 
DecRef(IntPtr o)214         internal override void DecRef(IntPtr o)
215         {
216             Context.FuncInterp_DRQ.Add(o);
217             base.DecRef(o);
218         }
219         #endregion
220     }
221 }
222