mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

Java API doc fix

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-04-13 17:43:29 +01:00
parent bf00723d37
commit 2948e47240
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3195,7 +3195,7 @@ public class Context extends IDisposable
* @param rm rounding mode term * @param rm rounding mode term
* @param t1 floating-point term * @param t1 floating-point term
* @param t2 floating-point term * @param t2 floating-point term
* @param t3">floating-point term * @param t3 floating-point term
* Remarks: * Remarks:
* The result is round((t1 * t2) + t3) * The result is round((t1 * t2) + t3)
* @throws Z3Exception * @throws Z3Exception
@ -3230,7 +3230,7 @@ public class Context extends IDisposable
/** /**
* Floating-point roundToIntegral. Rounds a floating-point number to * Floating-point roundToIntegral. Rounds a floating-point number to
* the closest integer, again represented as a floating-point number. * the closest integer, again represented as a floating-point number.
* @param rm">term of RoundingMode sort * @param rm term of RoundingMode sort
* @param t floating-point term * @param t floating-point term
* @throws Z3Exception * @throws Z3Exception
**/ **/
@ -3408,7 +3408,7 @@ public class Context extends IDisposable
/** /**
* Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. * Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
* @param bv">bit-vector value (of size m). * @param bv bit-vector value (of size m).
* @param s FloatingPoint sort (ebits+sbits == m) * @param s FloatingPoint sort (ebits+sbits == m)
* Remarks: * Remarks:
* Produces a term that represents the conversion of a bit-vector term bv to a * Produces a term that represents the conversion of a bit-vector term bv to a