AST.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    AST.cs

Abstract:

    Z3 Managed API: ASTs

Author:

    Christoph Wintersteiger (cwinter) 2012-03-16

Notes:
    
--*/

using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace Microsoft.Z3
{
    [ContractVerification(true)]
    public class AST : Z3Object, IComparable
    {
        public static bool operator ==(AST a, AST b)
        {
            return Object.ReferenceEquals(a, b) ||
                   (!Object.ReferenceEquals(a, null) &&
                    !Object.ReferenceEquals(b, null) &&
                    a.Context.nCtx == b.Context.nCtx &&
                    Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
        }

        public static bool operator !=(AST a, AST b)
        {
            return !(a == b);
        }

        public override bool Equals(object o)
        {
            AST casted = o as AST;
            if (casted == null) return false;
            return this == casted;
        }

        public virtual int CompareTo(object other)
        {
            if (other == null) return 1;
            AST oAST = other as AST;
            if (oAST == null)
                return 1;
            else
            {
                if (Id < oAST.Id)
                    return -1;
                else if (Id > oAST.Id)
                    return +1;
                else
                    return 0;
            }
        }

        public override int GetHashCode()
        {
            return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
        }

        public uint Id
        {
            get { return Native.Z3_get_ast_id(Context.nCtx, NativeObject); }
        }

        public AST Translate(Context ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Ensures(Contract.Result<AST>() != null);

            if (ReferenceEquals(Context, ctx))
                return this;
            else
                return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }

        public Z3_ast_kind ASTKind
        {
            get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
        }

        public bool IsExpr
        {
            get
            {
                switch (ASTKind)
                {
                    case Z3_ast_kind.Z3_APP_AST:
                    case Z3_ast_kind.Z3_NUMERAL_AST:
                    case Z3_ast_kind.Z3_QUANTIFIER_AST:
                    case Z3_ast_kind.Z3_VAR_AST: return true;
                    default: return false;
                }
            }
        }

        public bool IsVar
        {
            get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
        }

        public bool IsQuantifier
        {
            get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
        }

        public bool IsSort
        {
            get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
        }

        public bool IsFuncDecl
        {
            get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
        }

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

        public string SExpr()
        {
            Contract.Ensures(Contract.Result<string>() != null);

            return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
        }

        #region Internal
        internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
        internal AST(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_inc_ref(ctx.nCtx, obj);
            }

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

        internal override void IncRef(IntPtr o)
        {            
            // Console.WriteLine("AST IncRef()");
            if (Context == null)
                throw new Z3Exception("inc() called on null context");
            if (o == IntPtr.Zero)
                throw new Z3Exception("inc() called on null AST");
            Context.AST_DRQ.IncAndClear(Context, o);
            base.IncRef(o);
        }

        internal override void DecRef(IntPtr o)
        {
            // Console.WriteLine("AST DecRef()");
            if (Context == null)
                throw new Z3Exception("dec() called on null context");
            if (o == IntPtr.Zero)
                throw new Z3Exception("dec() called on null AST");
            Context.AST_DRQ.Add(o);
            base.DecRef(o);
        }

        internal static AST Create(Context ctx, IntPtr obj)
        {
            Contract.Requires(ctx != null);
            Contract.Ensures(Contract.Result<AST>() != null);

            switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
            {
                case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
                case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
                case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
                case Z3_ast_kind.Z3_APP_AST:
                case Z3_ast_kind.Z3_NUMERAL_AST:
                case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
                default:
                    throw new Z3Exception("Unknown AST kind");
            }
        }
        #endregion
    }
}