FuncInterp.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    FuncInterp.cs

Abstract:

    Z3 Managed API: Function Interpretations

Author:

    Christoph Wintersteiger (cwinter) 2012-03-21

Notes:
    
--*/

using System;
using System.Diagnostics.Contracts;

namespace Microsoft.Z3
{
    [ContractVerification(true)]
    public class FuncInterp : Z3Object
    {
        public class Entry : Z3Object
        {
            public Expr Value
            {
                get
                {
                    Contract.Ensures(Contract.Result<Expr>() != null);
                    return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
                }
            }

            public uint NumArgs
            {
                get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
            }

            public Expr[] Args
            {
                get
                {
                    Contract.Ensures(Contract.Result<Expr[]>() != null);
                    Contract.Ensures(Contract.Result<Expr[]>().Length == this.NumArgs);

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

            public override string ToString()
            {
                uint n = NumArgs;
                string res = "[";
                Expr[] args = Args;
                for (uint i = 0; i < n; i++)
                    res += args[i] + ", ";
                return res + Value + "]";
            }

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

            internal class DecRefQueue : IDecRefQueue
            {
                public DecRefQueue() : base() { }
                public DecRefQueue(uint move_limit) : base(move_limit) { }
                internal override void IncRef(Context ctx, IntPtr obj)
                {
                    Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
                }

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

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

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

        public uint NumEntries
        {
            get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
        }

        public Entry[] Entries
        {
            get
            {
                Contract.Ensures(Contract.Result<Entry[]>() != null);
                Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));

                uint n = NumEntries;
                Entry[] res = new Entry[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
                return res;
            }
        }

        public Expr Else
        {
            get
            {
                Contract.Ensures(Contract.Result<Expr>() != null);

                return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
            }
        }

        public uint Arity
        {
            get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
        }

        public override string ToString()
        {
            string res = "";
            res += "[";
            foreach (Entry e in Entries)
            {
                uint n = e.NumArgs;
                if (n > 1) res += "[";
                Expr[] args = e.Args;
                for (uint i = 0; i < n; i++)
                {
                    if (i != 0) res += ", ";
                    res += args[i];
                }
                if (n > 1) res += "]";
                res += " -> " + e.Value + ", ";
            }
            res += "else -> " + Else;
            res += "]";
            return res;
        }

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

        internal class DecRefQueue : IDecRefQueue
        {
            public DecRefQueue() : base() { }
            public DecRefQueue(uint move_limit) : base(move_limit) { }
            internal override void IncRef(Context ctx, IntPtr obj)
            {
                Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
            }

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

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

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