Z3
src/api/dotnet/FuncInterp.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     FuncInterp.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Function Interpretations
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-21
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines