mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

FPA API cosmetics

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-11 18:28:07 +00:00
parent ee0ec7fe3a
commit 4bd8e0f497
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/api/dotnet/Context.cs
View file

@ -3758,11 +3758,11 @@ namespace Microsoft.Z3
/// <summary>
/// Create a numeral of FloatingPoint sort from a sign bit and two integers.
/// </summary>
/// <param name="sgn">the sign.</param>
/// <param name="sig">the significand.</param>
/// <param name="sgn">the sign.</param>
/// <param name="exp">the exponent.</param>
/// <param name="sig">the significand.</param>
/// <param name="s">FloatingPoint sort.</param>
public FPNum MkFP(bool sgn, uint sig, int exp, FPSort s)
public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
{
Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return MkFPNumeral(sgn, sig, exp, s);
@ -3771,11 +3771,11 @@ namespace Microsoft.Z3
/// <summary>
/// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
/// </summary>
/// <param name="sgn">the sign.</param>
/// <param name="sig">the significand.</param>
/// <param name="sgn">the sign.</param>
/// <param name="exp">the exponent.</param>
/// <param name="sig">the significand.</param>
/// <param name="s">FloatingPoint sort.</param>
public FPNum MkFP(bool sgn, UInt64 sig, Int64 exp, FPSort s)
public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
{
Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return MkFPNumeral(sgn, sig, exp, s);

4
src/api/java/Context.java
View file

@ -3170,7 +3170,7 @@ public class Context extends IDisposable
* @param s FloatingPoint sort.
* @throws Z3Exception
**/
public FPNum mkFP(boolean sgn, int sig, int exp, FPSort s) throws Z3Exception
public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s) throws Z3Exception
{
return mkFPNumeral(sgn, sig, exp, s);
}
@ -3183,7 +3183,7 @@ public class Context extends IDisposable
* @param s FloatingPoint sort.
* @throws Z3Exception
**/
public FPNum mkFP(boolean sgn, long sig, long exp, FPSort s) throws Z3Exception
public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s) throws Z3Exception
{
return mkFPNumeral(sgn, sig, exp, s);
}