Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00029 [ContractVerification(true)]
00030 public class FuncInterp : Z3Object
00031 {
00036 public class Entry : Z3Object
00037 {
00041 public Expr Value
00042 {
00043 get
00044 {
00045 Contract.Ensures(Contract.Result<Expr>() != null);
00046 return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
00047 }
00048 }
00049
00053 public uint NumArgs
00054 {
00055 get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
00056 }
00057
00061 public Expr[] Args
00062 {
00063 get
00064 {
00065 Contract.Ensures(Contract.Result<Expr[]>() != null);
00066 Contract.Ensures(Contract.Result<Expr[]>().Length == this.NumArgs);
00067
00068 uint n = NumArgs;
00069 Expr[] res = new Expr[n];
00070 for (uint i = 0; i < n; i++)
00071 res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
00072 return res;
00073 }
00074 }
00075
00079 public override string ToString()
00080 {
00081 uint n = NumArgs;
00082 string res = "[";
00083 Expr[] args = Args;
00084 for (uint i = 0; i < n; i++)
00085 res += args[i] + ", ";
00086 return res + Value + "]";
00087 }
00088
00089 #region Internal
00090 internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00091
00092 internal class DecRefQueue : IDecRefQueue
00093 {
00094 public override void IncRef(Context ctx, IntPtr obj)
00095 {
00096 Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
00097 }
00098
00099 public override void DecRef(Context ctx, IntPtr obj)
00100 {
00101 Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
00102 }
00103 };
00104
00105 internal override void IncRef(IntPtr o)
00106 {
00107 Context.FuncEntry_DRQ.IncAndClear(Context, o);
00108 base.IncRef(o);
00109 }
00110
00111 internal override void DecRef(IntPtr o)
00112 {
00113 Context.FuncEntry_DRQ.Add(o);
00114 base.DecRef(o);
00115 }
00116 #endregion
00117 };
00118
00122 public uint NumEntries
00123 {
00124 get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
00125 }
00126
00130 public Entry[] Entries
00131 {
00132 get
00133 {
00134 Contract.Ensures(Contract.Result<Entry[]>() != null);
00135 Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
00136
00137 uint n = NumEntries;
00138 Entry[] res = new Entry[n];
00139 for (uint i = 0; i < n; i++)
00140 res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
00141 return res;
00142 }
00143 }
00144
00148 public Expr Else
00149 {
00150 get
00151 {
00152 Contract.Ensures(Contract.Result<Expr>() != null);
00153
00154 return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
00155 }
00156 }
00157
00161 public uint Arity
00162 {
00163 get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
00164 }
00165
00169 public override string ToString()
00170 {
00171 string res = "";
00172 res += "[";
00173 foreach (Entry e in Entries)
00174 {
00175 uint n = e.NumArgs;
00176 if (n > 1) res += "[";
00177 Expr[] args = e.Args;
00178 for (uint i = 0; i < n; i++)
00179 {
00180 if (i != 0) res += ", ";
00181 res += args[i];
00182 }
00183 if (n > 1) res += "]";
00184 res += " -> " + e.Value + ", ";
00185 }
00186 res += "else -> " + Else;
00187 res += "]";
00188 return res;
00189 }
00190
00191 #region Internal
00192 internal FuncInterp(Context ctx, IntPtr obj)
00193 : base(ctx, obj)
00194 {
00195 Contract.Requires(ctx != null);
00196 }
00197
00198 internal class DecRefQueue : IDecRefQueue
00199 {
00200 public override void IncRef(Context ctx, IntPtr obj)
00201 {
00202 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
00203 }
00204
00205 public override void DecRef(Context ctx, IntPtr obj)
00206 {
00207 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
00208 }
00209 };
00210
00211 internal override void IncRef(IntPtr o)
00212 {
00213 Context.FuncInterp_DRQ.IncAndClear(Context, o);
00214 base.IncRef(o);
00215 }
00216
00217 internal override void DecRef(IntPtr o)
00218 {
00219 Context.FuncInterp_DRQ.Add(o);
00220 base.DecRef(o);
00221 }
00222 #endregion
00223 }
00224 }