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 {
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 }