From 46e236487be2fa172a021afce577f133e09acd06 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 9 Jan 2015 11:53:18 +0000 Subject: [PATCH] Eliminated FPRMNum classes Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 86 +++++++++++++++++----------------- src/api/dotnet/Expr.cs | 24 +++++----- src/api/dotnet/FPRMExpr.cs | 50 ++++++++++++++++++++ src/api/dotnet/FPRMNum.cs | 96 -------------------------------------- src/api/java/Context.java | 40 ++++++++-------- src/api/java/Expr.java | 2 - 6 files changed, 125 insertions(+), 173 deletions(-) delete mode 100644 src/api/dotnet/FPRMNum.cs diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 9eb544f8a..89a89b959 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3456,91 +3456,91 @@ namespace Microsoft.Z3 /// /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. /// - public FPRMNum MkFPRoundNearestTiesToEven() + public FPRMExpr MkFPRoundNearestTiesToEven() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. /// - public FPRMNum MkFPRNE() + public FPRMExpr MkFPRNE() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_rne(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. /// - public FPRMNum MkFPRoundNearestTiesToAway() + public FPRMExpr MkFPRoundNearestTiesToAway() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. /// - public FPRMNum MkFPRNA() + public FPRMExpr MkFPRNA() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_rna(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. /// - public FPRMNum MkFPRoundTowardPositive() + public FPRMExpr MkFPRoundTowardPositive() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_positive(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. /// - public FPRMNum MkFPRTP() + public FPRMExpr MkFPRTP() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_rtp(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. /// - public FPRMNum MkFPRoundTowardNegative() + public FPRMExpr MkFPRoundTowardNegative() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_negative(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. /// - public FPRMNum MkFPRTN() + public FPRMExpr MkFPRTN() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_rtn(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. /// - public FPRMNum MkFPRoundTowardZero() + public FPRMExpr MkFPRoundTowardZero() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_zero(nCtx)); } /// /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. /// - public FPRMNum MkFPRTZ() + public FPRMExpr MkFPRTZ() { - Contract.Ensures(Contract.Result() != null); - return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx)); + Contract.Ensures(Contract.Result() != null); + return new FPRMExpr(this, Native.Z3_mk_fpa_rtz(nCtx)); } #endregion #endregion @@ -3637,7 +3637,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNaN(FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject)); } @@ -3648,7 +3648,7 @@ namespace Microsoft.Z3 /// indicates whether the result should be negative. public FPNum MkFPInf(FPSort s, bool negative) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0)); } @@ -3659,7 +3659,7 @@ namespace Microsoft.Z3 /// indicates whether the result should be negative. public FPNum MkFPZero(FPSort s, bool negative) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0)); } @@ -3670,7 +3670,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(float v, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject)); } @@ -3681,7 +3681,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(double v, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject)); } @@ -3692,7 +3692,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(int v, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject)); } @@ -3705,7 +3705,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_uint_int(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject)); } @@ -3718,7 +3718,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, UInt64 sig, Int64 exp, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_uint64_int64(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject)); } @@ -3729,7 +3729,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(float v, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return MkFPNumeral(v, s); } @@ -3740,7 +3740,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(double v, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return MkFPNumeral(v, s); } @@ -3751,7 +3751,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(int v, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return MkFPNumeral(v, s); } @@ -3764,7 +3764,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(bool sgn, uint sig, int exp, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return MkFPNumeral(sgn, sig, exp, s); } @@ -3777,7 +3777,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(bool sgn, UInt64 sig, Int64 exp, FPSort s) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); return MkFPNumeral(sgn, sig, exp, s); } diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 97e57b920..eb1d1c02d 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1475,57 +1475,57 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven /// - public bool IsFPRMNumRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } + public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } /// /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway /// - public bool IsFPRMNumRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } + public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative /// - public bool IsFPRMNumRoundTowardNegative{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } + public bool IsFPRMRoundTowardNegative{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive /// - public bool IsFPRMNumRoundTowardPositive{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } + public bool IsFPRMRoundTowardPositive{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardZero /// - public bool IsFPRMNumRoundTowardZero{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } + public bool IsFPRMRoundTowardZero{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } /// /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven /// - public bool IsFPRMNumRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } + public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } /// /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway /// - public bool IsFPRMNumRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } + public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative /// - public bool IsFPRMNumRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } + public bool IsFPRMExprRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive /// - public bool IsFPRMNumRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } + public bool IsFPRMExprRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardZero /// - public bool IsFPRMNumRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } + public bool IsFPRMExprRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } /// /// Indicates whether the term is a floating-point rounding mode numeral /// - public bool IsFPRMNum { + public bool IsFPRMExpr { get { return IsApp && (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY|| @@ -1809,7 +1809,7 @@ namespace Microsoft.Z3 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_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj); } } diff --git a/src/api/dotnet/FPRMExpr.cs b/src/api/dotnet/FPRMExpr.cs index 896c3e6b9..47ea3e670 100644 --- a/src/api/dotnet/FPRMExpr.cs +++ b/src/api/dotnet/FPRMExpr.cs @@ -30,6 +30,56 @@ namespace Microsoft.Z3 /// public class FPRMExpr : Expr { + /// + /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven + /// + public bool isRoundNearestTiesToEven { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven + /// + public bool isRNE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway + /// + public bool isRoundNearestTiesToAway { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway + /// + public bool isRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive + /// + public bool isRoundTowardPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive + /// + public bool isRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative + /// + public bool isRoundTowardNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative + /// + public bool isRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundTowardZero + /// + public bool isRoundTowardZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } + + /// + /// Indicates whether the term is the floating-point rounding numeral roundTowardZero + /// + public bool isRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } + #region Internal /// Constructor for FPRMExpr internal FPRMExpr(Context ctx, IntPtr obj) diff --git a/src/api/dotnet/FPRMNum.cs b/src/api/dotnet/FPRMNum.cs deleted file mode 100644 index 628480d96..000000000 --- a/src/api/dotnet/FPRMNum.cs +++ /dev/null @@ -1,96 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - FPRMNum.cs - -Abstract: - - Z3 Managed API: Floating Point Rounding Mode Numerals - -Author: - - Christoph Wintersteiger (cwinter) 2013-06-10 - -Notes: - ---*/ -using System; -using System.Diagnostics.Contracts; - -namespace Microsoft.Z3 -{ - /// - /// FloatingPoint RoundingMode Numerals - /// - [ContractVerification(true)] - public class FPRMNum : FPRMExpr - { - /// - /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven - /// - public bool isRoundNearestTiesToEven { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven - /// - public bool isRNE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway - /// - public bool isRoundNearestTiesToAway { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway - /// - public bool isRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive - /// - public bool isRoundTowardPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive - /// - public bool isRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative - /// - public bool isRoundTowardNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative - /// - public bool isRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundTowardZero - /// - public bool isRoundTowardZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } - - /// - /// Indicates whether the term is the floating-point rounding numeral roundTowardZero - /// - public bool isRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } } - - #region Internal - internal FPRMNum(Context ctx, IntPtr obj) - : base(ctx, obj) - { - Contract.Requires(ctx != null); - } - #endregion - - /// - /// Returns a string representation of the numeral. - /// - public override string ToString() - { - return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); - } - } -} diff --git a/src/api/java/Context.java b/src/api/java/Context.java index cfbd7c2c8..29be4aae8 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2865,90 +2865,90 @@ public class Context extends IDisposable * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. * @throws Z3Exception on error **/ - public FPRMNum mkFPRoundNearestTiesToEven() throws Z3Exception + public FPRMExpr mkFPRoundNearestTiesToEven() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRoundNearestTiesToEven(nCtx())); + return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRNE() throws Z3Exception + public FPRMExpr mkFPRNE() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRne(nCtx())); + return new FPRMExpr(this, Native.mkFpaRne(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRoundNearestTiesToAway() throws Z3Exception + public FPRMExpr mkFPRoundNearestTiesToAway() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx())); + return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToAway(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRNA() throws Z3Exception + public FPRMExpr mkFPRNA() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRna(nCtx())); + return new FPRMExpr(this, Native.mkFpaRna(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRoundTowardPositive() throws Z3Exception + public FPRMExpr mkFPRoundTowardPositive() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx())); + return new FPRMExpr(this, Native.mkFpaRoundTowardPositive(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRTP() throws Z3Exception + public FPRMExpr mkFPRTP() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRtp(nCtx())); + return new FPRMExpr(this, Native.mkFpaRtp(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRoundTowardNegative() throws Z3Exception + public FPRMExpr mkFPRoundTowardNegative() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx())); + return new FPRMExpr(this, Native.mkFpaRoundTowardNegative(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRTN() throws Z3Exception + public FPRMExpr mkFPRTN() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRtn(nCtx())); + return new FPRMExpr(this, Native.mkFpaRtn(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRoundTowardZero() throws Z3Exception + public FPRMExpr mkFPRoundTowardZero() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx())); + return new FPRMExpr(this, Native.mkFpaRoundTowardZero(nCtx())); } /** * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. * @throws Z3Exception **/ - public FPRMNum mkFPRTZ() throws Z3Exception + public FPRMExpr mkFPRTZ() throws Z3Exception { - return new FPRMNum(this, Native.mkFpaRtz(nCtx())); + return new FPRMExpr(this, Native.mkFpaRtz(nCtx())); } /** FloatingPoint Sorts **/ diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 886c69f08..49f49a295 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2140,8 +2140,6 @@ public class Expr extends AST return new BitVecNum(ctx, obj); case Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj); - case Z3_ROUNDING_MODE_SORT: - return new FPRMNum(ctx, obj); default: ; } }