mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
57318bab5b
|
@ -3356,7 +3356,7 @@ public class Context implements AutoCloseable {
|
|||
}
|
||||
|
||||
/**
|
||||
* Create a numeral of FloatingPoint sort from a float.
|
||||
* Create a numeral of FloatingPoint sort from a double.
|
||||
* @param v numeral value.
|
||||
* @param s FloatingPoint sort.
|
||||
* @throws Z3Exception
|
||||
|
@ -3368,7 +3368,7 @@ public class Context implements AutoCloseable {
|
|||
|
||||
/**
|
||||
* Create a numeral of FloatingPoint sort from an int.
|
||||
* * @param v numeral value.
|
||||
* @param v numeral value.
|
||||
* @param s FloatingPoint sort.
|
||||
* @throws Z3Exception
|
||||
**/
|
||||
|
@ -3380,8 +3380,8 @@ public class Context implements AutoCloseable {
|
|||
/**
|
||||
* Create a numeral of FloatingPoint sort from a sign bit and two integers.
|
||||
* @param sgn the sign.
|
||||
* @param sig the significand.
|
||||
* @param exp the exponent.
|
||||
* @param sig the significand.
|
||||
* @param s FloatingPoint sort.
|
||||
* @throws Z3Exception
|
||||
**/
|
||||
|
@ -3393,8 +3393,8 @@ public class Context implements AutoCloseable {
|
|||
/**
|
||||
* Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
|
||||
* @param sgn the sign.
|
||||
* @param sig the significand.
|
||||
* @param exp the exponent.
|
||||
* @param sig the significand.
|
||||
* @param s FloatingPoint sort.
|
||||
* @throws Z3Exception
|
||||
**/
|
||||
|
@ -3415,7 +3415,7 @@ public class Context implements AutoCloseable {
|
|||
}
|
||||
|
||||
/**
|
||||
* Create a numeral of FloatingPoint sort from a float.
|
||||
* Create a numeral of FloatingPoint sort from a double.
|
||||
* @param v numeral value.
|
||||
* @param s FloatingPoint sort.
|
||||
* @throws Z3Exception
|
||||
|
@ -3447,7 +3447,7 @@ public class Context implements AutoCloseable {
|
|||
**/
|
||||
public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
|
||||
{
|
||||
return mkFPNumeral(sgn, sig, exp, s);
|
||||
return mkFPNumeral(sgn, exp, sig, s);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -3460,7 +3460,7 @@ public class Context implements AutoCloseable {
|
|||
**/
|
||||
public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
|
||||
{
|
||||
return mkFPNumeral(sgn, sig, exp, s);
|
||||
return mkFPNumeral(sgn, exp, sig, s);
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue