From 06051989be4369e4a98707cb04610ee9ecadf5b5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 23 Jan 2015 17:11:12 +0000 Subject: [PATCH] FPA API: Naming consistency Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 10 +++++----- src/api/java/Context.java | 8 ++++---- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 1a36a35dc..96999d2d9 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3706,7 +3706,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_uint_int(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); } /// @@ -3716,10 +3716,10 @@ namespace Microsoft.Z3 /// the significand. /// the exponent. /// FloatingPoint sort. - public FPNum MkFPNumeral(bool sgn, UInt64 sig, Int64 exp, FPSort s) + public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_uint64_int64(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); } /// @@ -3765,7 +3765,7 @@ namespace Microsoft.Z3 public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return MkFPNumeral(sgn, sig, exp, s); + return MkFPNumeral(sgn, exp, sig, s); } /// @@ -3778,7 +3778,7 @@ namespace Microsoft.Z3 public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return MkFPNumeral(sgn, sig, exp, s); + return MkFPNumeral(sgn, exp, sig, s); } #endregion diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 18e1b7b2c..baa84f60a 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3043,9 +3043,9 @@ public class Context extends IDisposable * @param s FloatingPoint sort. * @throws Z3Exception **/ - public FPNum mkFPNumeral(boolean sgn, int sig, int exp, FPSort s) throws Z3Exception + public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s) throws Z3Exception { - return new FPNum(this, Native.mkFpaNumeralUintInt(nCtx(), sgn, sig, exp, s.getNativeObject())); + return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject())); } /** @@ -3056,9 +3056,9 @@ public class Context extends IDisposable * @param s FloatingPoint sort. * @throws Z3Exception **/ - public FPNum mkFPNumeral(boolean sgn, long sig, long exp, FPSort s) throws Z3Exception + public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s) throws Z3Exception { - return new FPNum(this, Native.mkFpaNumeralUint64Int64(nCtx(), sgn, sig, exp, s.getNativeObject())); + return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject())); } /**