Z3
FuncInterp.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 FuncInterp.cs
7
8Abstract:
9
10 Z3 Managed API: Function Interpretations
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
29 public class FuncInterp : Z3Object
30 {
35 public class Entry : Z3Object
36 {
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
51 public uint NumArgs
52 {
53 get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
54 }
55
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
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
86 internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
87
88 internal class DecRefQueue : IDecRefQueue
89 {
90 public DecRefQueue() : base() { }
91 public DecRefQueue(uint move_limit) : base(move_limit) { }
92 internal override void IncRef(Context ctx, IntPtr obj)
93 {
94 Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
95 }
96
97 internal override void DecRef(Context ctx, IntPtr obj)
98 {
99 Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
100 }
101 };
102
103 internal override void IncRef(IntPtr o)
104 {
105 Context.FuncEntry_DRQ.IncAndClear(Context, o);
106 base.IncRef(o);
107 }
108
109 internal override void DecRef(IntPtr o)
110 {
111 Context.FuncEntry_DRQ.Add(o);
112 base.DecRef(o);
113 }
114 #endregion
115 };
116
120 public uint NumEntries
121 {
122 get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
123 }
124
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
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
156 public uint Arity
157 {
158 get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
159 }
160
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
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 {
195 public DecRefQueue() : base() { }
196 public DecRefQueue(uint move_limit) : base(move_limit) { }
197 internal override void IncRef(Context ctx, IntPtr obj)
198 {
199 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
200 }
201
202 internal override void DecRef(Context ctx, IntPtr obj)
203 {
204 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
205 }
206 };
207
208 internal override void IncRef(IntPtr o)
209 {
210 Context.FuncInterp_DRQ.IncAndClear(Context, o);
211 base.IncRef(o);
212 }
213
214 internal override void DecRef(IntPtr o)
215 {
216 Context.FuncInterp_DRQ.Add(o);
217 base.DecRef(o);
218 }
219 #endregion
220 }
221}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
Definition: Context.cs:4745
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Definition: Context.cs:4750
Expressions are terms.
Definition: Expr.cs:31
An Entry object represents an element in the finite map used to encode a function interpretation.
Definition: FuncInterp.cs:36
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:52
Expr Value
Return the (symbolic) value of this entry.
Definition: FuncInterp.cs:41
Expr[] Args
The arguments of the function entry.
Definition: FuncInterp.cs:60
override string ToString()
A string representation of the function entry.
Definition: FuncInterp.cs:75
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
Definition: FuncInterp.cs:30
uint Arity
The arity of the function interpretation
Definition: FuncInterp.cs:157
override string ToString()
A string representation of the function interpretation.
Definition: FuncInterp.cs:164
Entry[] Entries
The entries in the function interpretation
Definition: FuncInterp.cs:129
uint NumEntries
The number of entries in the function interpretation.
Definition: FuncInterp.cs:121
Expr Else
The (symbolic) ‘else’ value of the function interpretation.
Definition: FuncInterp.cs:145
DecRefQueue interface
Definition: IDecRefQueue.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33