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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-01-23 17:11:57 +00:00
parent 3bf3de17e9 06051989be
commit 89bfbd38c8
2 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3706,7 +3706,7 @@ namespace Microsoft.Z3
public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != 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));
} }
/// <summary> /// <summary>
@ -3716,10 +3716,10 @@ namespace Microsoft.Z3
/// <param name="sig">the significand.</param> /// <param name="sig">the significand.</param>
/// <param name="exp">the exponent.</param> /// <param name="exp">the exponent.</param>
/// <param name="s">FloatingPoint sort.</param> /// <param name="s">FloatingPoint sort.</param>
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<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != 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));
} }
/// <summary> /// <summary>
@ -3765,7 +3765,7 @@ namespace Microsoft.Z3
public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s) public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return MkFPNumeral(sgn, sig, exp, s); return MkFPNumeral(sgn, exp, sig, s);
} }
/// <summary> /// <summary>
@ -3778,7 +3778,7 @@ namespace Microsoft.Z3
public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s) public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return MkFPNumeral(sgn, sig, exp, s); return MkFPNumeral(sgn, exp, sig, s);
} }
#endregion #endregion

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

@ -3043,9 +3043,9 @@ public class Context extends IDisposable
* @param s FloatingPoint sort. * @param s FloatingPoint sort.
* @throws Z3Exception * @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. * @param s FloatingPoint sort.
* @throws Z3Exception * @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()));
} }
/** /**