diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 4361cab96..6f12d81a4 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -93,6 +93,9 @@ namespace test_mapi 1, new Pattern[] { p } /* patterns */); + if (q.IsTrue) + Console.WriteLine("is true."); + return q; } diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 48395d8c2..992b0c477 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -89,6 +89,9 @@ class JavaExample names, /* names of quantified variables */ eq, 1, new Pattern[] { p } /* patterns */, null, null, null); + if (q.isTrue()) + System.out.println("is true"); + return q; } diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 49b46edeb..dae4df445 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -269,57 +269,57 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is the constant true. /// - public bool IsTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } } + public bool IsTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } } /// /// Indicates whether the term is the constant false. /// - public bool IsFalse { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } } + public bool IsFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } } /// /// Indicates whether the term is an equality predicate. /// - public bool IsEq { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } } + public bool IsEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } } /// /// Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). /// - public bool IsDistinct { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } } + public bool IsDistinct { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } } /// /// Indicates whether the term is a ternary if-then-else term /// - public bool IsITE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } } + public bool IsITE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } } /// /// Indicates whether the term is an n-ary conjunction /// - public bool IsAnd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } } + public bool IsAnd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } } /// /// Indicates whether the term is an n-ary disjunction /// - public bool IsOr { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } } + public bool IsOr { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } } /// /// Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) /// - public bool IsIff { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } } + public bool IsIff { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } } /// /// Indicates whether the term is an exclusive or /// - public bool IsXor { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } } + public bool IsXor { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } } /// /// Indicates whether the term is a negation /// - public bool IsNot { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } } + public bool IsNot { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } } /// /// Indicates whether the term is an implication /// - public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } } + public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } } #endregion @@ -347,82 +347,82 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is an arithmetic numeral. /// - public bool IsArithmeticNumeral { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } } + public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } } /// /// Indicates whether the term is a less-than-or-equal /// - public bool IsLE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } } + public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } } /// /// Indicates whether the term is a greater-than-or-equal /// - public bool IsGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } } + public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } } /// /// Indicates whether the term is a less-than /// - public bool IsLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } } + public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } } /// /// Indicates whether the term is a greater-than /// - public bool IsGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } } + public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } } /// /// Indicates whether the term is addition (binary) /// - public bool IsAdd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } } + public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } } /// /// Indicates whether the term is subtraction (binary) /// - public bool IsSub { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } } + public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } } /// /// Indicates whether the term is a unary minus /// - public bool IsUMinus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } } + public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } } /// /// Indicates whether the term is multiplication (binary) /// - public bool IsMul { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } } + public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } } /// /// Indicates whether the term is division (binary) /// - public bool IsDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } } + public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } } /// /// Indicates whether the term is integer division (binary) /// - public bool IsIDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } } + public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } } /// /// Indicates whether the term is remainder (binary) /// - public bool IsRemainder { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } } + public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } } /// /// Indicates whether the term is modulus (binary) /// - public bool IsModulus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } } + public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } } /// /// Indicates whether the term is a coercion of integer to real (unary) /// - public bool IsIntToReal { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } } + public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } } /// /// Indicates whether the term is a coercion of real to integer (unary) /// - public bool IsRealToInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } } + public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } } /// /// Indicates whether the term is a check that tests whether a real is integral (unary) /// - public bool IsRealIsInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } } + public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } } #endregion #region Array Terms @@ -444,64 +444,64 @@ namespace Microsoft.Z3 /// /// It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). /// Array store takes at least 3 arguments. - public bool IsStore { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } } + public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } } /// /// Indicates whether the term is an array select. /// - public bool IsSelect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } } + public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } } /// /// Indicates whether the term is a constant array. /// /// For example, select(const(v),i) = v holds for every v and i. The function is unary. - public bool IsConstantArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } } + public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } } /// /// Indicates whether the term is a default array. /// /// For example default(const(v)) = v. The function is unary. - public bool IsDefaultArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } } + public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } } /// /// Indicates whether the term is an array map. /// /// It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. - public bool IsArrayMap { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } } + public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } } /// /// Indicates whether the term is an as-array term. /// /// An as-array term is n array value that behaves as the function graph of the /// function passed as parameter. - public bool IsAsArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } } + public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } } #endregion #region Set Terms /// /// Indicates whether the term is set union /// - public bool IsSetUnion { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } } + public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } } /// /// Indicates whether the term is set intersection /// - public bool IsSetIntersect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } } + public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } } /// /// Indicates whether the term is set difference /// - public bool IsSetDifference { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } } + public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } } /// /// Indicates whether the term is set complement /// - public bool IsSetComplement { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } } + public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } } /// /// Indicates whether the term is set subset /// - public bool IsSetSubset { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } } + public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } } #endregion #region Bit-vector terms @@ -516,266 +516,266 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a bit-vector numeral /// - public bool IsBVNumeral { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } } + public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } } /// /// Indicates whether the term is a one-bit bit-vector with value one /// - public bool IsBVBitOne { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } } + public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } } /// /// Indicates whether the term is a one-bit bit-vector with value zero /// - public bool IsBVBitZero { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } } + public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } } /// /// Indicates whether the term is a bit-vector unary minus /// - public bool IsBVUMinus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } } + public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } } /// /// Indicates whether the term is a bit-vector addition (binary) /// - public bool IsBVAdd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } } + public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } } /// /// Indicates whether the term is a bit-vector subtraction (binary) /// - public bool IsBVSub { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } } + public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } } /// /// Indicates whether the term is a bit-vector multiplication (binary) /// - public bool IsBVMul { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } } + public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } } /// /// Indicates whether the term is a bit-vector signed division (binary) /// - public bool IsBVSDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } } + public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } } /// /// Indicates whether the term is a bit-vector unsigned division (binary) /// - public bool IsBVUDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } } + public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } } /// /// Indicates whether the term is a bit-vector signed remainder (binary) /// - public bool IsBVSRem { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } } + public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } } /// /// Indicates whether the term is a bit-vector unsigned remainder (binary) /// - public bool IsBVURem { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } } + public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } } /// /// Indicates whether the term is a bit-vector signed modulus /// - public bool IsBVSMod { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } } + public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } } /// /// Indicates whether the term is a bit-vector signed division by zero /// - internal bool IsBVSDiv0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } } + internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } } /// /// Indicates whether the term is a bit-vector unsigned division by zero /// - internal bool IsBVUDiv0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } } + internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } } /// /// Indicates whether the term is a bit-vector signed remainder by zero /// - internal bool IsBVSRem0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } } + internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } } /// /// Indicates whether the term is a bit-vector unsigned remainder by zero /// - internal bool IsBVURem0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } } + internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } } /// /// Indicates whether the term is a bit-vector signed modulus by zero /// - internal bool IsBVSMod0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } } + internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } } /// /// Indicates whether the term is an unsigned bit-vector less-than-or-equal /// - public bool IsBVULE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } } + public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } } /// /// Indicates whether the term is a signed bit-vector less-than-or-equal /// - public bool IsBVSLE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } } + public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } } /// /// Indicates whether the term is an unsigned bit-vector greater-than-or-equal /// - public bool IsBVUGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } } + public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } } /// /// Indicates whether the term is a signed bit-vector greater-than-or-equal /// - public bool IsBVSGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } } + public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } } /// /// Indicates whether the term is an unsigned bit-vector less-than /// - public bool IsBVULT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } } + public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } } /// /// Indicates whether the term is a signed bit-vector less-than /// - public bool IsBVSLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } } + public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } } /// /// Indicates whether the term is an unsigned bit-vector greater-than /// - public bool IsBVUGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } } + public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } } /// /// Indicates whether the term is a signed bit-vector greater-than /// - public bool IsBVSGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } } + public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } } /// /// Indicates whether the term is a bit-wise AND /// - public bool IsBVAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } } + public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } } /// /// Indicates whether the term is a bit-wise OR /// - public bool IsBVOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } } + public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } } /// /// Indicates whether the term is a bit-wise NOT /// - public bool IsBVNOT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } } + public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } } /// /// Indicates whether the term is a bit-wise XOR /// - public bool IsBVXOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } } + public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } } /// /// Indicates whether the term is a bit-wise NAND /// - public bool IsBVNAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } } + public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } } /// /// Indicates whether the term is a bit-wise NOR /// - public bool IsBVNOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } } + public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } } /// /// Indicates whether the term is a bit-wise XNOR /// - public bool IsBVXNOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } } + public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } } /// /// Indicates whether the term is a bit-vector concatenation (binary) /// - public bool IsBVConcat { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } } + public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } } /// /// Indicates whether the term is a bit-vector sign extension /// - public bool IsBVSignExtension { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } } + public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } } /// /// Indicates whether the term is a bit-vector zero extension /// - public bool IsBVZeroExtension { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } } + public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } } /// /// Indicates whether the term is a bit-vector extraction /// - public bool IsBVExtract { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } } + public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } } /// /// Indicates whether the term is a bit-vector repetition /// - public bool IsBVRepeat { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } } + public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } } /// /// Indicates whether the term is a bit-vector reduce OR /// - public bool IsBVReduceOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } } + public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } } /// /// Indicates whether the term is a bit-vector reduce AND /// - public bool IsBVReduceAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } } + public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } } /// /// Indicates whether the term is a bit-vector comparison /// - public bool IsBVComp { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } } + public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } } /// /// Indicates whether the term is a bit-vector shift left /// - public bool IsBVShiftLeft { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } } + public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } } /// /// Indicates whether the term is a bit-vector logical shift right /// - public bool IsBVShiftRightLogical { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } } + public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } } /// /// Indicates whether the term is a bit-vector arithmetic shift left /// - public bool IsBVShiftRightArithmetic { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } } + public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } } /// /// Indicates whether the term is a bit-vector rotate left /// - public bool IsBVRotateLeft { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } } + public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } } /// /// Indicates whether the term is a bit-vector rotate right /// - public bool IsBVRotateRight { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } } + public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } } /// /// Indicates whether the term is a bit-vector rotate left (extended) /// /// Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. - public bool IsBVRotateLeftExtended { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } } + public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } } /// /// Indicates whether the term is a bit-vector rotate right (extended) /// /// Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. - public bool IsBVRotateRightExtended { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } } + public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } } /// /// Indicates whether the term is a coercion from integer to bit-vector /// /// This function is not supported by the decision procedures. Only the most /// rudimentary simplification rules are applied to this function. - public bool IsIntToBV { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } } + public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } } /// /// Indicates whether the term is a coercion from bit-vector to integer /// /// This function is not supported by the decision procedures. Only the most /// rudimentary simplification rules are applied to this function. - public bool IsBVToInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } } + public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } } /// /// Indicates whether the term is a bit-vector carry /// /// Compute the carry bit in a full-adder. The meaning is given by the /// equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) - public bool IsBVCarry { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } } + public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } } /// /// Indicates whether the term is a bit-vector ternary XOR /// /// The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) - public bool IsBVXOR3 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } } + public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } } #endregion @@ -784,13 +784,13 @@ namespace Microsoft.Z3 /// Indicates whether the term is a label (used by the Boogie Verification condition generator). /// /// The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. - public bool IsLabel { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } } + public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } } /// /// Indicates whether the term is a label literal (used by the Boogie Verification condition generator). /// /// A label literal has a set of string parameters. It takes no arguments. - public bool IsLabelLit { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } + public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } #endregion #region Proof Terms @@ -799,22 +799,22 @@ namespace Microsoft.Z3 /// /// This binary predicate is used in proof terms. /// It captures equisatisfiability and equivalence modulo renamings. - public bool IsOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } } + public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } } /// /// Indicates whether the term is a Proof for the expression 'true'. /// - public bool IsProofTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } } + public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } } /// /// Indicates whether the term is a proof for a fact asserted by the user. /// - public bool IsProofAsserted { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } } + public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } } /// /// Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. /// - public bool IsProofGoal { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } } + public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } } /// /// Indicates whether the term is proof via modus ponens @@ -825,7 +825,7 @@ namespace Microsoft.Z3 /// T2: (implies p q) /// [mp T1 T2]: q /// The second antecedents may also be a proof for (iff p q). - public bool IsProofModusPonens { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } } + public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } } /// /// Indicates whether the term is a proof for (R t t), where R is a reflexive relation. @@ -834,7 +834,7 @@ namespace Microsoft.Z3 /// The only reflexive relations that are used are /// equivalence modulo namings, equality and equivalence. /// That is, R is either '~', '=' or 'iff'. - public bool IsProofReflexivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } } + public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } } /// /// Indicates whether the term is proof by symmetricity of a relation @@ -845,7 +845,7 @@ namespace Microsoft.Z3 /// [symmetry T1]: (R s t) /// T1 is the antecedent of this proof object. /// - public bool IsProofSymmetry { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } } + public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } } /// /// Indicates whether the term is a proof by transitivity of a relation @@ -857,7 +857,7 @@ namespace Microsoft.Z3 /// T2: (R s u) /// [trans T1 T2]: (R t u) /// - public bool IsProofTransitivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } } + public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } } /// /// Indicates whether the term is a proof by condensed transitivity of a relation @@ -878,7 +878,7 @@ namespace Microsoft.Z3 /// if there is a path from s to t, if we view every /// antecedent (R a b) as an edge between a and b. /// - public bool IsProofTransitivityStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } } + public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } } /// @@ -892,7 +892,7 @@ namespace Microsoft.Z3 /// Remark: if t_i == s_i, then the antecedent Ti is suppressed. /// That is, reflexivity proofs are supressed to save space. /// - public bool IsProofMonotonicity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } } + public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } } /// /// Indicates whether the term is a quant-intro proof @@ -902,7 +902,7 @@ namespace Microsoft.Z3 /// T1: (~ p q) /// [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) /// - public bool IsProofQuantIntro { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } } + public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } } /// /// Indicates whether the term is a distributivity proof object. @@ -920,7 +920,7 @@ namespace Microsoft.Z3 /// Remark. This rule is used by the CNF conversion pass and /// instantiated by f = or, and g = and. /// - public bool IsProofDistributivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } } + public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } } /// /// Indicates whether the term is a proof by elimination of AND @@ -930,7 +930,7 @@ namespace Microsoft.Z3 /// T1: (and l_1 ... l_n) /// [and-elim T1]: l_i /// - public bool IsProofAndElimination { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } } + public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } } /// /// Indicates whether the term is a proof by eliminiation of not-or @@ -940,7 +940,7 @@ namespace Microsoft.Z3 /// T1: (not (or l_1 ... l_n)) /// [not-or-elim T1]: (not l_i) /// - public bool IsProofOrElimination { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } } + public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } } /// /// Indicates whether the term is a proof by rewriting @@ -959,7 +959,7 @@ namespace Microsoft.Z3 /// (= (+ x 1 2) (+ 3 x)) /// (iff (or x false) x) /// - public bool IsProofRewrite { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } } + public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } } /// /// Indicates whether the term is a proof by rewriting @@ -975,7 +975,7 @@ namespace Microsoft.Z3 /// - When converting bit-vectors to Booleans (BIT2BOOL=true) /// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) /// - public bool IsProofRewriteStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } } + public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } } /// /// Indicates whether the term is a proof for pulling quantifiers out. @@ -983,7 +983,7 @@ namespace Microsoft.Z3 /// /// A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. /// - public bool IsProofPullQuant { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } } + public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } } /// /// Indicates whether the term is a proof for pulling quantifiers out. @@ -993,7 +993,7 @@ namespace Microsoft.Z3 /// This proof object is only used if the parameter PROOF_MODE is 1. /// This proof object has no antecedents /// - public bool IsProofPullQuantStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } } + public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } } /// /// Indicates whether the term is a proof for pushing quantifiers in. @@ -1006,7 +1006,7 @@ namespace Microsoft.Z3 /// (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) /// This proof object has no antecedents /// - public bool IsProofPushQuant { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } } + public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } } /// /// Indicates whether the term is a proof for elimination of unused variables. @@ -1018,7 +1018,7 @@ namespace Microsoft.Z3 /// It is used to justify the elimination of unused variables. /// This proof object has no antecedents. /// - public bool IsProofElimUnusedVars { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } } + public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } } /// /// Indicates whether the term is a proof for destructive equality resolution @@ -1032,7 +1032,7 @@ namespace Microsoft.Z3 /// /// Several variables can be eliminated simultaneously. /// - public bool IsProofDER { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } } + public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } } /// /// Indicates whether the term is a proof for quantifier instantiation @@ -1040,13 +1040,13 @@ namespace Microsoft.Z3 /// /// A proof of (or (not (forall (x) (P x))) (P a)) /// - public bool IsProofQuantInst { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } } + public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } } /// /// Indicates whether the term is a hypthesis marker. /// /// Mark a hypothesis in a natural deduction style proof. - public bool IsProofHypothesis { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } } + public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } } /// /// Indicates whether the term is a proof by lemma @@ -1059,7 +1059,7 @@ namespace Microsoft.Z3 /// It converts the proof in a proof for (or (not l_1) ... (not l_n)), /// when T1 contains the hypotheses: l_1, ..., l_n. /// - public bool IsProofLemma { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } } + public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } } /// /// Indicates whether the term is a proof by unit resolution @@ -1071,7 +1071,7 @@ namespace Microsoft.Z3 /// T(n+1): (not l_n) /// [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') /// - public bool IsProofUnitResolution { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } } + public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } } /// /// Indicates whether the term is a proof by iff-true @@ -1080,7 +1080,7 @@ namespace Microsoft.Z3 /// T1: p /// [iff-true T1]: (iff p true) /// - public bool IsProofIFFTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } } + public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } } /// /// Indicates whether the term is a proof by iff-false @@ -1089,7 +1089,7 @@ namespace Microsoft.Z3 /// T1: (not p) /// [iff-false T1]: (iff p false) /// - public bool IsProofIFFFalse { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } } + public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } } /// /// Indicates whether the term is a proof by commutativity @@ -1102,7 +1102,7 @@ namespace Microsoft.Z3 /// This proof object has no antecedents. /// Remark: if f is bool, then = is iff. /// - public bool IsProofCommutativity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } } + public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } } /// /// Indicates whether the term is a proof for Tseitin-like axioms @@ -1138,7 +1138,7 @@ namespace Microsoft.Z3 /// unfolding the Boolean connectives in the axioms a small /// bounded number of steps (=3). /// - public bool IsProofDefAxiom { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } } + public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } } /// /// Indicates whether the term is a proof for introduction of a name @@ -1161,7 +1161,7 @@ namespace Microsoft.Z3 /// Otherwise: /// [def-intro]: (= n e) /// - public bool IsProofDefIntro { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } } + public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } } /// /// Indicates whether the term is a proof for application of a definition @@ -1171,7 +1171,7 @@ namespace Microsoft.Z3 /// F is 'equivalent' to n, given that T1 is a proof that /// n is a name for F. /// - public bool IsProofApplyDef { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } } + public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } } /// /// Indicates whether the term is a proof iff-oeq @@ -1180,7 +1180,7 @@ namespace Microsoft.Z3 /// T1: (iff p q) /// [iff~ T1]: (~ p q) /// - public bool IsProofIFFOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } } + public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } } /// /// Indicates whether the term is a proof for a positive NNF step @@ -1208,7 +1208,7 @@ namespace Microsoft.Z3 /// NNF_NEG furthermore handles the case where negation is pushed /// over Boolean connectives 'and' and 'or'. /// - public bool IsProofNNFPos { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } } + public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } } /// /// Indicates whether the term is a proof for a negative NNF step @@ -1233,7 +1233,7 @@ namespace Microsoft.Z3 /// [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) /// (and (or r_1 r_2) (or r_1' r_2'))) /// - public bool IsProofNNFNeg { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } } + public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } } /// /// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. @@ -1245,7 +1245,7 @@ namespace Microsoft.Z3 /// /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. /// - public bool IsProofNNFStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } } + public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } } /// /// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. @@ -1255,7 +1255,7 @@ namespace Microsoft.Z3 /// This proof object is only used if the parameter PROOF_MODE is 1. /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. /// - public bool IsProofCNFStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } } + public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } } /// /// Indicates whether the term is a proof for a Skolemization step @@ -1268,7 +1268,7 @@ namespace Microsoft.Z3 /// /// This proof object has no antecedents. /// - public bool IsProofSkolemize { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } } + public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } } /// /// Indicates whether the term is a proof by modus ponens for equi-satisfiability. @@ -1279,7 +1279,7 @@ namespace Microsoft.Z3 /// T2: (~ p q) /// [mp~ T1 T2]: q /// - public bool IsProofModusPonensOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } } + public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } } /// /// Indicates whether the term is a proof for theory lemma @@ -1298,7 +1298,7 @@ namespace Microsoft.Z3 /// (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) /// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. /// - public bool IsProofTheoryLemma { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } } + public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } } #endregion #region Relational Terms @@ -1323,40 +1323,40 @@ namespace Microsoft.Z3 /// The function takes n+1 arguments, where the first argument is the relation and the remaining n elements /// correspond to the n columns of the relation. /// - public bool IsRelationStore { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } } + public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } } /// /// Indicates whether the term is an empty relation /// - public bool IsEmptyRelation { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } } + public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } } /// /// Indicates whether the term is a test for the emptiness of a relation /// - public bool IsIsEmptyRelation { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } } + public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } } /// /// Indicates whether the term is a relational join /// - public bool IsRelationalJoin { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } } + public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } } /// /// Indicates whether the term is the union or convex hull of two relations. /// /// The function takes two arguments. - public bool IsRelationUnion { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } } + public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } } /// /// Indicates whether the term is the widening of two relations /// /// The function takes two arguments. - public bool IsRelationWiden { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } } + public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } } /// /// Indicates whether the term is a projection of columns (provided as numbers in the parameters). /// /// The function takes one argument. - public bool IsRelationProject { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } } + public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } } /// /// Indicates whether the term is a relation filter @@ -1368,7 +1368,7 @@ namespace Microsoft.Z3 /// corresponding to the columns of the relation. /// So the first column in the relation has index 0. /// - public bool IsRelationFilter { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } } + public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } } /// /// Indicates whether the term is an intersection of a relation with the negation of another. @@ -1384,7 +1384,7 @@ namespace Microsoft.Z3 /// target are elements in x in pos, such that there is no y in neg that agrees with /// x on the columns c1, d1, .., cN, dN. /// - public bool IsRelationNegationFilter { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } } + public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } } /// /// Indicates whether the term is the renaming of a column in a relation @@ -1393,12 +1393,12 @@ namespace Microsoft.Z3 /// The function takes one argument. /// The parameters contain the renaming as a cycle. /// - public bool IsRelationRename { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } } + public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } } /// /// Indicates whether the term is the complement of a relation /// - public bool IsRelationComplement { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } } + public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } } /// /// Indicates whether the term is a relational select @@ -1408,7 +1408,7 @@ namespace Microsoft.Z3 /// The function takes n+1 arguments, where the first argument is a relation, /// and the remaining n arguments correspond to a record. /// - public bool IsRelationSelect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } } + public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } } /// /// Indicates whether the term is a relational clone (copy) @@ -1420,7 +1420,7 @@ namespace Microsoft.Z3 /// for terms of kind /// to perform destructive updates to the first argument. /// - public bool IsRelationClone { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } } + public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } } #endregion #region Finite domain terms @@ -1439,7 +1439,7 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a less than predicate over a finite domain. /// - public bool IsFiniteDomainLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } } + public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } } #endregion #endregion diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 7793a16e5..5c4f90920 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -245,7 +245,7 @@ public class Expr extends AST **/ public boolean isTrue() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE; } /** @@ -253,7 +253,7 @@ public class Expr extends AST **/ public boolean isFalse() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE; } /** @@ -261,7 +261,7 @@ public class Expr extends AST **/ public boolean isEq() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ; } /** @@ -270,7 +270,7 @@ public class Expr extends AST **/ public boolean isDistinct() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT; } /** @@ -278,7 +278,7 @@ public class Expr extends AST **/ public boolean isITE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE; } /** @@ -286,7 +286,7 @@ public class Expr extends AST **/ public boolean isAnd() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND; } /** @@ -294,7 +294,7 @@ public class Expr extends AST **/ public boolean isOr() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR; } /** @@ -303,7 +303,7 @@ public class Expr extends AST **/ public boolean isIff() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF; } /** @@ -311,7 +311,7 @@ public class Expr extends AST **/ public boolean isXor() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR; } /** @@ -319,7 +319,7 @@ public class Expr extends AST **/ public boolean isNot() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT; } /** @@ -327,7 +327,7 @@ public class Expr extends AST **/ public boolean isImplies() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES; } /** @@ -356,7 +356,7 @@ public class Expr extends AST **/ public boolean isArithmeticNumeral() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM; } /** @@ -364,7 +364,7 @@ public class Expr extends AST **/ public boolean isLE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE; } /** @@ -372,7 +372,7 @@ public class Expr extends AST **/ public boolean isGE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE; } /** @@ -380,7 +380,7 @@ public class Expr extends AST **/ public boolean isLT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT; } /** @@ -388,7 +388,7 @@ public class Expr extends AST **/ public boolean isGT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT; } /** @@ -396,7 +396,7 @@ public class Expr extends AST **/ public boolean isAdd() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD; } /** @@ -404,7 +404,7 @@ public class Expr extends AST **/ public boolean isSub() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB; } /** @@ -412,7 +412,7 @@ public class Expr extends AST **/ public boolean isUMinus() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS; } /** @@ -420,7 +420,7 @@ public class Expr extends AST **/ public boolean isMul() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL; } /** @@ -428,7 +428,7 @@ public class Expr extends AST **/ public boolean isDiv() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV; } /** @@ -436,7 +436,7 @@ public class Expr extends AST **/ public boolean isIDiv() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV; } /** @@ -444,7 +444,7 @@ public class Expr extends AST **/ public boolean isRemainder() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM; } /** @@ -452,7 +452,7 @@ public class Expr extends AST **/ public boolean isModulus() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD; } /** @@ -460,7 +460,7 @@ public class Expr extends AST **/ public boolean isIntToReal() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL; } /** @@ -468,7 +468,7 @@ public class Expr extends AST **/ public boolean isRealToInt() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT; } /** @@ -477,7 +477,7 @@ public class Expr extends AST **/ public boolean isRealIsInt() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT; } /** @@ -497,7 +497,7 @@ public class Expr extends AST **/ public boolean isStore() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE; } /** @@ -505,7 +505,7 @@ public class Expr extends AST **/ public boolean isSelect() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT; } /** @@ -515,7 +515,7 @@ public class Expr extends AST **/ public boolean isConstantArray() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY; } /** @@ -524,7 +524,7 @@ public class Expr extends AST **/ public boolean isDefaultArray() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } /** @@ -533,7 +533,7 @@ public class Expr extends AST **/ public boolean isArrayMap() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP; } /** @@ -543,7 +543,7 @@ public class Expr extends AST **/ public boolean isAsArray() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY; } /** @@ -551,7 +551,7 @@ public class Expr extends AST **/ public boolean isSetUnion() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION; } /** @@ -559,7 +559,7 @@ public class Expr extends AST **/ public boolean isSetIntersect() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT; } /** @@ -567,7 +567,7 @@ public class Expr extends AST **/ public boolean isSetDifference() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } /** @@ -575,7 +575,7 @@ public class Expr extends AST **/ public boolean isSetComplement() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } /** @@ -583,7 +583,7 @@ public class Expr extends AST **/ public boolean isSetSubset() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET; } /** @@ -601,7 +601,7 @@ public class Expr extends AST **/ public boolean isBVNumeral() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM; } /** @@ -609,7 +609,7 @@ public class Expr extends AST **/ public boolean isBVBitOne() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1; } /** @@ -617,7 +617,7 @@ public class Expr extends AST **/ public boolean isBVBitZero() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0; } /** @@ -625,7 +625,7 @@ public class Expr extends AST **/ public boolean isBVUMinus() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG; } /** @@ -633,7 +633,7 @@ public class Expr extends AST **/ public boolean isBVAdd() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD; } /** @@ -641,7 +641,7 @@ public class Expr extends AST **/ public boolean isBVSub() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB; } /** @@ -649,7 +649,7 @@ public class Expr extends AST **/ public boolean isBVMul() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL; } /** @@ -657,7 +657,7 @@ public class Expr extends AST **/ public boolean isBVSDiv() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV; } /** @@ -665,7 +665,7 @@ public class Expr extends AST **/ public boolean isBVUDiv() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV; } /** @@ -673,7 +673,7 @@ public class Expr extends AST **/ public boolean isBVSRem() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM; } /** @@ -681,7 +681,7 @@ public class Expr extends AST **/ public boolean isBVURem() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM; } /** @@ -689,7 +689,7 @@ public class Expr extends AST **/ public boolean isBVSMod() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD; } /** @@ -697,7 +697,7 @@ public class Expr extends AST **/ boolean IsBVSDiv0() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0; } /** @@ -705,7 +705,7 @@ public class Expr extends AST **/ boolean IsBVUDiv0() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0; } /** @@ -713,7 +713,7 @@ public class Expr extends AST **/ boolean IsBVSRem0() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0; } /** @@ -721,7 +721,7 @@ public class Expr extends AST **/ boolean IsBVURem0() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0; } /** @@ -729,7 +729,7 @@ public class Expr extends AST **/ boolean IsBVSMod0() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0; } /** @@ -737,7 +737,7 @@ public class Expr extends AST **/ public boolean isBVULE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ; } /** @@ -745,7 +745,7 @@ public class Expr extends AST **/ public boolean isBVSLE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ; } /** @@ -754,7 +754,7 @@ public class Expr extends AST **/ public boolean isBVUGE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ; } /** @@ -762,7 +762,7 @@ public class Expr extends AST **/ public boolean isBVSGE() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ; } /** @@ -770,7 +770,7 @@ public class Expr extends AST **/ public boolean isBVULT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT; } /** @@ -778,7 +778,7 @@ public class Expr extends AST **/ public boolean isBVSLT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT; } /** @@ -786,7 +786,7 @@ public class Expr extends AST **/ public boolean isBVUGT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT; } /** @@ -794,7 +794,7 @@ public class Expr extends AST **/ public boolean isBVSGT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT; } /** @@ -802,7 +802,7 @@ public class Expr extends AST **/ public boolean isBVAND() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND; } /** @@ -810,7 +810,7 @@ public class Expr extends AST **/ public boolean isBVOR() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR; } /** @@ -818,7 +818,7 @@ public class Expr extends AST **/ public boolean isBVNOT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT; } /** @@ -826,7 +826,7 @@ public class Expr extends AST **/ public boolean isBVXOR() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR; } /** @@ -834,7 +834,7 @@ public class Expr extends AST **/ public boolean isBVNAND() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND; } /** @@ -842,7 +842,7 @@ public class Expr extends AST **/ public boolean isBVNOR() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR; } /** @@ -850,7 +850,7 @@ public class Expr extends AST **/ public boolean isBVXNOR() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR; } /** @@ -858,7 +858,7 @@ public class Expr extends AST **/ public boolean isBVConcat() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT; } /** @@ -866,7 +866,7 @@ public class Expr extends AST **/ public boolean isBVSignExtension() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT; } /** @@ -874,7 +874,7 @@ public class Expr extends AST **/ public boolean isBVZeroExtension() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT; } /** @@ -882,7 +882,7 @@ public class Expr extends AST **/ public boolean isBVExtract() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT; } /** @@ -890,7 +890,7 @@ public class Expr extends AST **/ public boolean isBVRepeat() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT; } /** @@ -898,7 +898,7 @@ public class Expr extends AST **/ public boolean isBVReduceOR() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR; } /** @@ -906,7 +906,7 @@ public class Expr extends AST **/ public boolean isBVReduceAND() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND; } /** @@ -914,7 +914,7 @@ public class Expr extends AST **/ public boolean isBVComp() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP; } /** @@ -922,7 +922,7 @@ public class Expr extends AST **/ public boolean isBVShiftLeft() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL; } /** @@ -930,7 +930,7 @@ public class Expr extends AST **/ public boolean isBVShiftRightLogical() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR; } /** @@ -938,7 +938,7 @@ public class Expr extends AST **/ public boolean isBVShiftRightArithmetic() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR; } /** @@ -946,7 +946,7 @@ public class Expr extends AST **/ public boolean isBVRotateLeft() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } /** @@ -954,7 +954,7 @@ public class Expr extends AST **/ public boolean isBVRotateRight() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } /** @@ -964,7 +964,7 @@ public class Expr extends AST **/ public boolean isBVRotateLeftExtended() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } /** @@ -974,7 +974,7 @@ public class Expr extends AST **/ public boolean isBVRotateRightExtended() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } /** @@ -985,7 +985,7 @@ public class Expr extends AST **/ public boolean isIntToBV() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV; } /** @@ -996,7 +996,7 @@ public class Expr extends AST **/ public boolean isBVToInt() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT; } /** @@ -1006,7 +1006,7 @@ public class Expr extends AST **/ public boolean isBVCarry() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY; } /** @@ -1016,7 +1016,7 @@ public class Expr extends AST **/ public boolean isBVXOR3() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3; } /** @@ -1026,7 +1026,7 @@ public class Expr extends AST **/ public boolean isLabel() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL; } /** @@ -1036,7 +1036,7 @@ public class Expr extends AST **/ public boolean isLabelLit() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT; } /** @@ -1046,7 +1046,7 @@ public class Expr extends AST **/ public boolean isOEQ() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ; } /** @@ -1054,7 +1054,7 @@ public class Expr extends AST **/ public boolean isProofTrue() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE; } /** @@ -1062,7 +1062,7 @@ public class Expr extends AST **/ public boolean isProofAsserted() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED; } /** @@ -1071,7 +1071,7 @@ public class Expr extends AST **/ public boolean isProofGoal() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL; } /** @@ -1082,7 +1082,7 @@ public class Expr extends AST **/ public boolean isProofModusPonens() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } /** @@ -1094,7 +1094,7 @@ public class Expr extends AST **/ public boolean isProofReflexivity() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } /** @@ -1105,7 +1105,7 @@ public class Expr extends AST **/ public boolean isProofSymmetry() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } /** @@ -1116,7 +1116,7 @@ public class Expr extends AST **/ public boolean isProofTransitivity() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } /** @@ -1134,7 +1134,7 @@ public class Expr extends AST **/ public boolean isProofTransitivityStar() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } /** @@ -1146,7 +1146,7 @@ public class Expr extends AST **/ public boolean isProofMonotonicity() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } /** @@ -1156,7 +1156,7 @@ public class Expr extends AST **/ public boolean isProofQuantIntro() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } /** @@ -1172,7 +1172,7 @@ public class Expr extends AST **/ public boolean isProofDistributivity() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } /** @@ -1182,7 +1182,7 @@ public class Expr extends AST **/ public boolean isProofAndElimination() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } /** @@ -1192,7 +1192,7 @@ public class Expr extends AST **/ public boolean isProofOrElimination() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } /** @@ -1209,7 +1209,7 @@ public class Expr extends AST **/ public boolean isProofRewrite() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE; } /** @@ -1225,7 +1225,7 @@ public class Expr extends AST **/ public boolean isProofRewriteStar() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } /** @@ -1235,7 +1235,7 @@ public class Expr extends AST **/ public boolean isProofPullQuant() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } /** @@ -1246,7 +1246,7 @@ public class Expr extends AST **/ public boolean isProofPullQuantStar() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } /** @@ -1258,7 +1258,7 @@ public class Expr extends AST **/ public boolean isProofPushQuant() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } /** @@ -1271,7 +1271,7 @@ public class Expr extends AST **/ public boolean isProofElimUnusedVars() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } /** @@ -1285,7 +1285,7 @@ public class Expr extends AST **/ public boolean isProofDER() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER; } /** @@ -1294,7 +1294,7 @@ public class Expr extends AST **/ public boolean isProofQuantInst() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } /** @@ -1303,7 +1303,7 @@ public class Expr extends AST **/ public boolean isProofHypothesis() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } /** @@ -1316,7 +1316,7 @@ public class Expr extends AST **/ public boolean isProofLemma() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA; } /** @@ -1326,7 +1326,7 @@ public class Expr extends AST **/ public boolean isProofUnitResolution() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } /** @@ -1335,7 +1335,7 @@ public class Expr extends AST **/ public boolean isProofIFFTrue() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } /** @@ -1344,7 +1344,7 @@ public class Expr extends AST **/ public boolean isProofIFFFalse() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } /** @@ -1358,7 +1358,7 @@ public class Expr extends AST **/ public boolean isProofCommutativity() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } /** @@ -1381,7 +1381,7 @@ public class Expr extends AST **/ public boolean isProofDefAxiom() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } /** @@ -1402,7 +1402,7 @@ public class Expr extends AST **/ public boolean isProofDefIntro() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } /** @@ -1412,7 +1412,7 @@ public class Expr extends AST **/ public boolean isProofApplyDef() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } /** @@ -1421,7 +1421,7 @@ public class Expr extends AST **/ public boolean isProofIFFOEQ() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } /** @@ -1446,7 +1446,7 @@ public class Expr extends AST **/ public boolean isProofNNFPos() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS; } /** @@ -1462,7 +1462,7 @@ public class Expr extends AST **/ public boolean isProofNNFNeg() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } /** @@ -1477,7 +1477,7 @@ public class Expr extends AST **/ public boolean isProofNNFStar() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } /** @@ -1489,7 +1489,7 @@ public class Expr extends AST **/ public boolean isProofCNFStar() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } /** @@ -1503,7 +1503,7 @@ public class Expr extends AST **/ public boolean isProofSkolemize() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } /** @@ -1513,7 +1513,7 @@ public class Expr extends AST **/ public boolean isProofModusPonensOEQ() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } /** @@ -1532,7 +1532,7 @@ public class Expr extends AST **/ public boolean isProofTheoryLemma() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } /** @@ -1554,7 +1554,7 @@ public class Expr extends AST **/ public boolean isRelationStore() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE; } /** @@ -1562,7 +1562,7 @@ public class Expr extends AST **/ public boolean isEmptyRelation() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY; } /** @@ -1570,7 +1570,7 @@ public class Expr extends AST **/ public boolean isIsEmptyRelation() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } /** @@ -1578,7 +1578,7 @@ public class Expr extends AST **/ public boolean isRelationalJoin() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN; } /** @@ -1587,7 +1587,7 @@ public class Expr extends AST **/ public boolean isRelationUnion() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION; } /** @@ -1596,7 +1596,7 @@ public class Expr extends AST **/ public boolean isRelationWiden() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN; } /** @@ -1606,7 +1606,7 @@ public class Expr extends AST **/ public boolean isRelationProject() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT; } /** @@ -1618,7 +1618,7 @@ public class Expr extends AST **/ public boolean isRelationFilter() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER; } /** @@ -1635,7 +1635,7 @@ public class Expr extends AST **/ public boolean isRelationNegationFilter() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } /** @@ -1645,7 +1645,7 @@ public class Expr extends AST **/ public boolean isRelationRename() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME; } /** @@ -1653,7 +1653,7 @@ public class Expr extends AST **/ public boolean isRelationComplement() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } /** @@ -1664,7 +1664,7 @@ public class Expr extends AST **/ public boolean isRelationSelect() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT; } /** @@ -1676,7 +1676,7 @@ public class Expr extends AST **/ public boolean isRelationClone() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE; } /** @@ -1695,7 +1695,7 @@ public class Expr extends AST **/ public boolean isFiniteDomainLT() throws Z3Exception { - return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT; + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT; } /**