Model.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    Model.cs

Abstract:

    Z3 Managed API: Models

Author:

    Christoph Wintersteiger (cwinter) 2012-03-21

Notes:
    
--*/

using System;
using System.Diagnostics.Contracts;

namespace Microsoft.Z3
{
    [ContractVerification(true)]
    public class Model : Z3Object
    {
        public Expr ConstInterp(Expr a)
        {
            Contract.Requires(a != null);

            Context.CheckContextMatch(a);
            return ConstInterp(a.FuncDecl);
        }

        public Expr ConstInterp(FuncDecl f)
        {
            Contract.Requires(f != null);

            Context.CheckContextMatch(f);
            if (f.Arity != 0 ||
                Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)Z3_sort_kind.Z3_ARRAY_SORT)
                throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");

            IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
            if (n == IntPtr.Zero)
                return null;
            else
                return Expr.Create(Context, n);
        }

        public FuncInterp FuncInterp(FuncDecl f)
        {
            Contract.Requires(f != null);

            Context.CheckContextMatch(f);

            Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));

            if (f.Arity == 0)
            {
                IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);

                if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
                {
                    if (n == IntPtr.Zero)
                        return null;
                    else
                    {
                        if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
                            throw new Z3Exception("Argument was not an array constant");
                        IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
                        return FuncInterp(new FuncDecl(Context, fd));
                    }
                }
                else
                {
                    throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
                }
            }
            else
            {
                IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
                if (n == IntPtr.Zero)
                    return null;
                else
                    return new FuncInterp(Context, n);
            }
        }

        public uint NumConsts
        {
            get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
        }

        public FuncDecl[] ConstDecls
        {
            get
            {
                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);

                uint n = NumConsts;
                FuncDecl[] res = new FuncDecl[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
                return res;
            }
        }

        public uint NumFuncs
        {
            get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
        }

        public FuncDecl[] FuncDecls
        {
            get
            {
                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);

                uint n = NumFuncs;
                FuncDecl[] res = new FuncDecl[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
                return res;
            }
        }

        public FuncDecl[] Decls
        {
            get
            {
                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);

                var nFuncs = NumFuncs;
                var nConsts = NumConsts;
                uint n = nFuncs + nConsts;
                FuncDecl[] res = new FuncDecl[n];
                for (uint i = 0; i < nConsts; i++)
                    res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
                for (uint i = 0; i < nFuncs; i++)
                    res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));                
                return res;
            }
        }

        public class ModelEvaluationFailedException : Z3Exception
        {
            public ModelEvaluationFailedException() : base() { }
        }

        public Expr Eval(Expr t, bool completion = false)
        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            IntPtr v = IntPtr.Zero;
            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
                throw new ModelEvaluationFailedException();
            else
                return Expr.Create(Context, v);
        }

        public Expr Evaluate(Expr t, bool completion = false)
        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            return Eval(t, completion);
        }

        public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }

        public Sort[] Sorts
        {
            get
            {
                Contract.Ensures(Contract.Result<Sort[]>() != null);

                uint n = NumSorts;
                Sort[] res = new Sort[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
                return res;
            }
        }

        public Expr[] SortUniverse(Sort s)
        {
            Contract.Requires(s != null);
            Contract.Ensures(Contract.Result<Expr[]>() != null);

            ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
            uint n = nUniv.Size;
            Expr[] res = new Expr[n];
            for (uint i = 0; i < n; i++)
                res[i] = Expr.Create(Context, nUniv[i].NativeObject);
            return res;
        }

        public override string ToString()
        {
            return Native.Z3_model_to_string(Context.nCtx, NativeObject);
        }

        #region Internal
        internal Model(Context ctx, IntPtr obj)
            : base(ctx, obj)
        {
            Contract.Requires(ctx != null);
        }

        internal class DecRefQueue : Z3.DecRefQueue
        {
            public override void IncRef(Context ctx, IntPtr obj)
            {
                Native.Z3_model_inc_ref(ctx.nCtx, obj);
            }

            public override void DecRef(Context ctx, IntPtr obj)
            {
                Native.Z3_model_dec_ref(ctx.nCtx, obj);
            }
        };        

        internal override void IncRef(IntPtr o)
        {
            Context.Model_DRQ.IncAndClear(Context, o);
            base.IncRef(o);
        }

        internal override void DecRef(IntPtr o)
        {
            Context.Model_DRQ.Add(o);
            base.DecRef(o);
        }
        #endregion
    }
}