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