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.Diagnostics;
using System;
 
namespace Microsoft.Z3
{
    public class FuncInterp : Z3Object
    {
        public class Entry : Z3Object
        {
            public Expr Value
            {
                get
                {
                    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
                {
 
                    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) { Debug.Assert(ctx != null); }
 
            internal override void IncRef(IntPtr o)
            {
                Native.Z3_func_entry_inc_ref(Context.nCtx, o);
            }
 
            internal override void DecRef(IntPtr o)
            {
                lock (Context)
                {
                    if (Context.nCtx != IntPtr.Zero)
                        Native.Z3_func_entry_dec_ref(Context.nCtx, o);
                }
            }
            #endregion
        };
 
        public uint NumEntries
        {
            get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
        }
 
        public Entry[] Entries
        {
            get
            {
 
                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
            {
 
                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)
        {
            Debug.Assert(ctx != null);
        }
 
        internal override void IncRef(IntPtr o)
        {
            Native.Z3_func_interp_inc_ref(Context.nCtx, o);
        }
 
        internal override void DecRef(IntPtr o)
        {
            lock (Context)
            {
                if (Context.nCtx != IntPtr.Zero)
                    Native.Z3_func_interp_dec_ref(Context.nCtx, o);
            }
        }
        #endregion
    }
}