Expr.cs

Go to the documentation of this file.

/*++
Copyright (<c>) 2012 Microsoft Corporation
 
Module Name:
 
    Expr.cs
 
Abstract:
 
    Z3 Managed API: Expressions
 
Author:
 
    Christoph Wintersteiger (cwinter) 2012-03-20
 
Notes:
 
--*/
 
using System.Diagnostics;
using System;
using System.Linq;
 
 
namespace Microsoft.Z3
{
    public class Expr : AST
    {
        public Expr Simplify(Params p = null)
        {
 
            if (p == null)
                return Expr.Create(Context, Native.Z3_simplify(Context.nCtx, NativeObject));
            else
                return Expr.Create(Context, Native.Z3_simplify_ex(Context.nCtx, NativeObject, p.NativeObject));
        }
 
        public FuncDecl FuncDecl
        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
            }
        }
 
        public Z3_lbool BoolValue
        {
            get { return (Z3_lbool)Native.Z3_get_bool_value(Context.nCtx, NativeObject); }
        }
 
        public uint NumArgs
        {
            get { return Native.Z3_get_app_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_get_app_arg(Context.nCtx, NativeObject, i));
                return res;
            }
        }
 
        public Expr Arg(uint i)
        {
            return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
        }
 
        public void Update(Expr[] args)
        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            Context.CheckContextMatch<Expr>(args);
            if (IsApp && args.Length != NumArgs)
                throw new Z3Exception("Number of arguments does not match");
            NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
        }
 
        public Expr Substitute(Expr[] from, Expr[] to)
        {
            Debug.Assert(from != null);
            Debug.Assert(to != null);
            Debug.Assert(from.All(f => f != null));
            Debug.Assert(to.All(t => t != null));
 
            Context.CheckContextMatch<Expr>(from);
            Context.CheckContextMatch<Expr>(to);
            if (from.Length != to.Length)
                throw new Z3Exception("Argument sizes do not match");
            return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
        }
 
        public Expr Substitute(Expr from, Expr to)
        {
            Debug.Assert(from != null);
            Debug.Assert(to != null);
 
            return Substitute(new Expr[] { from }, new Expr[] { to });
        }
 
        public Expr SubstituteVars(Expr[] to)
        {
            Debug.Assert(to != null);
            Debug.Assert(to.All(t => t != null));
 
            Context.CheckContextMatch<Expr>(to);
            return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
        }
 
        public Expr SubstituteFuns(FuncDecl[] from, Expr[] to)
        {
            Debug.Assert(from != null);
            Debug.Assert(to != null);
            Debug.Assert(from.All(f => f != null));
            Debug.Assert(to.All(t => t != null));
 
            Context.CheckContextMatch<FuncDecl>(from);
            Context.CheckContextMatch<Expr>(to);
            if (from.Length != to.Length)
                throw new Z3Exception("Arrays 'from' and 'to' must have the same length");
            return Expr.Create(Context, Native.Z3_substitute_funs(Context.nCtx, NativeObject, (uint)from.Length, FuncDecl.ArrayToNative(from), Expr.ArrayToNative(to)));
        }
 
        new public Expr Translate(Context ctx)
        {
            return (Expr)base.Translate(ctx);
        }
        
        public Expr Dup() {
             return Expr.Create(Context, NativeObject);
        }
 
        public override string ToString()
        {
            return base.ToString();
        }
 
        public bool IsNumeral
        {
            get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
        }
 
        public bool IsWellSorted
        {
            get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
        }
 
        public Sort Sort
        {
            get
            {
                return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
            }
        }
 
        #region Constants
        public bool IsConst
        {
            get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
        }
        #endregion
 
        #region Integer Numerals
        public bool IsIntNum
        {
            get { return IsNumeral && IsInt; }
        }
        #endregion
 
        #region Real Numerals
        public bool IsRatNum
        {
            get { return IsNumeral && IsReal; }
        }
        #endregion
 
        #region Algebraic Numbers
        public bool IsAlgebraicNumber
        {
            get { return 0 != Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); }
        }
        #endregion
 
        #region Term Kind Tests
 
        #region Boolean Terms
        public bool IsBool
        {
            get
            {
                return (IsExpr &&
                        Native.Z3_is_eq_sort(Context.nCtx,
                                              Native.Z3_mk_bool_sort(Context.nCtx),
                                              Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
            }
        }
 
        public bool IsTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
 
        public bool IsFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
 
        public bool IsEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
 
        public bool IsDistinct { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
 
        public bool IsITE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
 
        public bool IsAnd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
 
        public bool IsOr { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
 
        public bool IsIff { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
 
        public bool IsXor { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
 
        public bool IsNot { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
 
        public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
 
        public bool IsAtMost { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_MOST; } }
 
        public uint AtMostBound { get { Debug.Assert(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } }
 
        public bool IsAtLeast { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_LEAST; } }
 
        public uint AtLeastBound { get { Debug.Assert(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } }
 
        public bool IsPbEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_EQ; } }
 
        public bool IsPbLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_LE; } }
 
        public bool IsPbGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_GE; } }        
 
        #endregion
 
        #region Arithmetic Terms
        public bool IsInt
        {
            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT; }
        }
 
        public bool IsReal
        {
            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
        }
 
        public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
 
        public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
 
        public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
 
        public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
 
        public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
 
        public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
 
        public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
 
        public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
 
        public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
 
        public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
 
        public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
 
        public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
 
        public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
 
        public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
 
        public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
 
        public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
        #endregion
 
        #region Array Terms
        public bool IsArray
        {
            get
            {
                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
                        (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                        == Z3_sort_kind.Z3_ARRAY_SORT);
            }
        }
 
        public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
 
        public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
 
        public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
 
        public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
 
        public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
 
        public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
        #endregion
 
        #region Set Terms
        public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
 
        public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
 
        public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
 
        public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
 
        public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
        #endregion
 
        #region Bit-vector terms
        public bool IsBV
        {
            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
        }
 
        public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
 
        public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
 
        public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
 
        public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
 
        public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
 
        public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
 
        public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
 
        public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
 
        public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
 
        public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
 
        public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
 
        public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
 
        internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
 
        internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
 
        internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
 
        internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
 
        internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
 
        public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
 
        public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
 
        public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
 
        public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
 
        public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
 
        public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
 
        public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
 
        public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
 
        public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
 
        public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
 
        public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
 
        public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
 
        public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
 
        public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
 
        public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
 
        public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
 
        public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
 
        public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
 
        public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
 
        public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
 
        public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
 
        public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
 
        public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
 
        public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
 
        public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
 
        public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
 
        public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
 
        public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
 
        public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
 
        public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
 
        public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
 
        public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
 
        public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
 
        public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
 
        #endregion
 
        #region Labels
        public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
 
        public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
        #endregion
 
        #region Sequences and Strings
 
        public bool IsString  { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject) != 0; } }
 
        public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
 
        public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }
 
        public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }
 
        public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
 
        public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
 
        public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
 
        public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
 
        public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
 
        public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
 
        public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
 
 
        #endregion
 
        #region Proof Terms
        public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
 
        public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
 
        public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
 
        public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
 
        public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
 
        public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
 
        public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
 
        public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
 
        public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
 
 
        public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
 
        public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
 
        public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
 
        public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
 
        public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
 
        public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
 
        public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
 
        public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
 
 
        public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
 
        public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
 
        public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
 
        public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
 
        public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
 
        public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
 
        public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
 
        public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
 
        public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
 
        public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
 
        public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
 
        public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
 
        public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
 
        public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
 
        public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
 
        public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
 
        public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
 
        public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
 
        public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
        #endregion
 
        #region Relational Terms
        public bool IsRelation
        {
            get
            {
                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
                        Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                        == (uint)Z3_sort_kind.Z3_RELATION_SORT);
            }
        }
 
        public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
 
        public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
 
        public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
 
        public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
 
        public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
 
        public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
 
        public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
 
        public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
 
        public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
 
        public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
 
        public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
 
        public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
 
        public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
        #endregion
 
        #region Finite domain terms
        public bool IsFiniteDomain
        {
            get
            {
                return (Native.Z3_is_app(Context.nCtx, NativeObject)  != 0 &&
                        Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
            }
        }
 
        public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
        #endregion
 
        #region Floating-point terms
        public bool IsFP
        {
            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
        }
 
        public bool IsFPRM
        {
            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
        }
 
        public bool IsFPNumeral { get { return IsFP && IsNumeral; } }
 
        public bool IsFPRMNumeral { get { return IsFPRM && IsNumeral; } }
 
        public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
 
        public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
 
        public bool IsFPRMRoundTowardNegative{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
 
        public bool IsFPRMRoundTowardPositive{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
 
        public bool IsFPRMRoundTowardZero{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
 
        public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
 
        public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
 
        public bool IsFPRMExprRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
 
        public bool IsFPRMExprRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
 
        public bool IsFPRMExprRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
 
        public bool IsFPRMExpr {
            get {
                return IsApp &&
                       (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
            }
        }
 
        public bool IsFPPlusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } }
 
        public bool IsFPMinusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } }
 
        public bool IsFPNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NAN; } }
 
        public bool IsFPPlusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } }
 
        public bool IsFPMinusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } }
 
        public bool IsFPAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ADD; } }
 
 
        public bool IsFPSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SUB; } }
 
        public bool IsFPNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NEG; } }
 
        public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
 
        public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
 
        public bool IsFPRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_REM; } }
 
        public bool IsFPAbs { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ABS; } }
 
        public bool IsFPMin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MIN; } }
 
        public bool IsFPMax { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MAX; } }
 
        public bool IsFPFMA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FMA; } }
 
        public bool IsFPSqrt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SQRT; } }
 
        public bool IsFPRoundToIntegral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } }
 
        public bool IsFPEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_EQ; } }
 
        public bool IsFPLt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LT; } }
 
        public bool IsFPGt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GT; } }
 
        public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
 
        public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
 
        public bool IsFPisNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } }
 
        public bool IsFPisInf { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_INF; } }
 
        public bool IsFPisZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } }
 
        public bool IsFPisNormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } }
 
        public bool IsFPisSubnormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } }
 
        public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }
 
        public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }
 
        public bool IsFPFP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FP; } }
 
        public bool IsFPToFp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP; } }
 
        public bool IsFPToFpUnsigned { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } }
 
        public bool IsFPToUBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } }
 
        public bool IsFPToSBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } }
 
        public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }
 
 
        public bool IsFPToIEEEBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } }
 
        #endregion
        #endregion
 
        #region Bound Variables
        public uint Index
        {
            get
            {
                if (!IsVar)
                    throw new Z3Exception("Term is not a bound variable.");
 
                return Native.Z3_get_index_value(Context.nCtx, NativeObject);
            }
        }
        #endregion
 
        #region Internal
        internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
#if DEBUG
        internal override void CheckNativeObject(IntPtr obj)
        {
            if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
                Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST &&
                Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST)
                throw new Z3Exception("Underlying object is not a term");
            base.CheckNativeObject(obj);
        }
#endif
 
        internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
        {
            Debug.Assert(ctx != null);
            Debug.Assert(f != null);
 
            IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
                                          AST.ArrayLength(arguments),
                                          AST.ArrayToNative(arguments));
            return Create(ctx, obj);
        }
 
        new internal static Expr Create(Context ctx, IntPtr obj)
        {
            Debug.Assert(ctx != null);
 
            Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj);
            if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
                return new Quantifier(ctx, obj);
            IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
            Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
 
            if (0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast?
                return new AlgebraicNum(ctx, obj);
 
            if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
            {
 
                switch (sk)
                {
                    case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
                    case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
                    case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
                    case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
                    case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
                    case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainNum(ctx, obj);
                }
            }
 
            switch (sk)
            {
                case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj);
                case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj);
                case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
                case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
                case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
                case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
                case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
                case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
                case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj);
                case Z3_sort_kind.Z3_RE_SORT: return new ReExpr(ctx, obj);
                case Z3_sort_kind.Z3_SEQ_SORT: return new SeqExpr(ctx, obj);
            }
 
            return new Expr(ctx, obj);
        }
        #endregion
    }
}