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.Diagnostics;
using System;
using System.Collections;
using System.Collections.Generic;
 
namespace Microsoft.Z3
{
    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 &&
                    0 != Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject));
        }
 
        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)
        {
            Debug.Assert(ctx != null);
 
            if (ReferenceEquals(Context, ctx))
                return this;
            else
                return Create(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 IsApp
        {
            get { return this.ASTKind == Z3_ast_kind.Z3_APP_AST; }
        }
 
        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()
        {
 
            return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
        }
 
        #region Internal
        internal AST(Context ctx) : base(ctx) { Debug.Assert(ctx != null); }
        internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
        internal override void IncRef(IntPtr o)
        {
            if (Context != null && o != IntPtr.Zero)
                Native.Z3_inc_ref(Context.nCtx, o);
        }
 
        internal override void DecRef(IntPtr o)
        {
            if (Context != null && o != IntPtr.Zero)
            {
                lock (Context)
                {
                    if (Context.nCtx != IntPtr.Zero)
                        Native.Z3_dec_ref(Context.nCtx, o);
                }
            }
        }
 
        internal static AST Create(Context ctx, IntPtr obj)
        {
            Debug.Assert(ctx != 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
    }
}