Z3
src/api/dotnet/Model.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Model.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Models
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 {
00028     [ContractVerification(true)]
00029     public class Model : Z3Object
00030     {
00036         public Expr ConstInterp(Expr a)
00037         {
00038             Contract.Requires(a != null);
00039 
00040             Context.CheckContextMatch(a);
00041             return ConstInterp(a.FuncDecl);
00042         }
00043 
00049         public Expr ConstInterp(FuncDecl f)
00050         {
00051             Contract.Requires(f != null);
00052 
00053             Context.CheckContextMatch(f);
00054             if (f.Arity != 0 ||
00055                 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)Z3_sort_kind.Z3_ARRAY_SORT)
00056                 throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
00057 
00058             IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
00059             if (n == IntPtr.Zero)
00060                 return null;
00061             else
00062                 return Expr.Create(Context, n);
00063         }
00064 
00070         public FuncInterp FuncInterp(FuncDecl f)
00071         {
00072             Contract.Requires(f != null);
00073 
00074             Context.CheckContextMatch(f);
00075 
00076             Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));
00077 
00078             if (f.Arity == 0)
00079             {
00080                 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
00081 
00082                 if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
00083                 {
00084                     if (n == IntPtr.Zero)
00085                         return null;
00086                     else
00087                     {
00088                         if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
00089                             throw new Z3Exception("Argument was not an array constant");
00090                         IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
00091                         return FuncInterp(new FuncDecl(Context, fd));
00092                     }
00093                 }
00094                 else
00095                 {
00096                     throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
00097                 }
00098             }
00099             else
00100             {
00101                 IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
00102                 if (n == IntPtr.Zero)
00103                     return null;
00104                 else
00105                     return new FuncInterp(Context, n);
00106             }
00107         }
00108 
00112         public uint NumConsts
00113         {
00114             get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
00115         }
00116 
00120         public FuncDecl[] ConstDecls
00121         {
00122             get
00123             {
00124                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
00125 
00126                 uint n = NumConsts;
00127                 FuncDecl[] res = new FuncDecl[n];
00128                 for (uint i = 0; i < n; i++)
00129                     res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
00130                 return res;
00131             }
00132         }
00133 
00137         public uint NumFuncs
00138         {
00139             get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
00140         }
00141 
00145         public FuncDecl[] FuncDecls
00146         {
00147             get
00148             {
00149                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
00150 
00151                 uint n = NumFuncs;
00152                 FuncDecl[] res = new FuncDecl[n];
00153                 for (uint i = 0; i < n; i++)
00154                     res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
00155                 return res;
00156             }
00157         }
00158 
00162         public FuncDecl[] Decls
00163         {
00164             get
00165             {
00166                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
00167 
00168                 uint nFuncs = NumFuncs;
00169                 uint nConsts = NumConsts;
00170                 uint n = nFuncs + nConsts;
00171                 FuncDecl[] res = new FuncDecl[n];
00172                 for (uint i = 0; i < nConsts; i++)
00173                     res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
00174                 for (uint i = 0; i < nFuncs; i++)
00175                     res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));                
00176                 return res;
00177             }
00178         }
00179 
00183         public class ModelEvaluationFailedException : Z3Exception
00184         {
00188             public ModelEvaluationFailedException() : base() { }
00189         }
00190 
00205         public Expr Eval(Expr t, bool completion = false)
00206         {
00207             Contract.Requires(t != null);
00208             Contract.Ensures(Contract.Result<Expr>() != null);
00209 
00210             IntPtr v = IntPtr.Zero;
00211             if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
00212                 throw new ModelEvaluationFailedException();
00213             else
00214                 return Expr.Create(Context, v);
00215         }
00216 
00220         public Expr Evaluate(Expr t, bool completion = false)
00221         {
00222             Contract.Requires(t != null);
00223             Contract.Ensures(Contract.Result<Expr>() != null);
00224 
00225             return Eval(t, completion);
00226         }
00227 
00231         public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }
00232 
00243         public Sort[] Sorts
00244         {
00245             get
00246             {
00247                 Contract.Ensures(Contract.Result<Sort[]>() != null);
00248 
00249                 uint n = NumSorts;
00250                 Sort[] res = new Sort[n];
00251                 for (uint i = 0; i < n; i++)
00252                     res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
00253                 return res;
00254             }
00255         }
00256 
00263         public Expr[] SortUniverse(Sort s)
00264         {
00265             Contract.Requires(s != null);
00266             Contract.Ensures(Contract.Result<Expr[]>() != null);
00267 
00268             ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
00269             uint n = nUniv.Size;
00270             Expr[] res = new Expr[n];
00271             for (uint i = 0; i < n; i++)
00272                 res[i] = Expr.Create(Context, nUniv[i].NativeObject);
00273             return res;
00274         }
00275 
00280         public override string ToString()
00281         {
00282             return Native.Z3_model_to_string(Context.nCtx, NativeObject);
00283         }
00284 
00285         #region Internal
00286         internal Model(Context ctx, IntPtr obj)
00287             : base(ctx, obj)
00288         {
00289             Contract.Requires(ctx != null);
00290         }
00291 
00292         internal class DecRefQueue : IDecRefQueue
00293         {
00294             public override void IncRef(Context ctx, IntPtr obj)
00295             {
00296                 Native.Z3_model_inc_ref(ctx.nCtx, obj);
00297             }
00298 
00299             public override void DecRef(Context ctx, IntPtr obj)
00300             {
00301                 Native.Z3_model_dec_ref(ctx.nCtx, obj);
00302             }
00303         };        
00304 
00305         internal override void IncRef(IntPtr o)
00306         {
00307             Context.Model_DRQ.IncAndClear(Context, o);
00308             base.IncRef(o);
00309         }
00310 
00311         internal override void DecRef(IntPtr o)
00312         {
00313             Context.Model_DRQ.Add(o);
00314             base.DecRef(o);
00315         }
00316         #endregion
00317     }
00318 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines