From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 14 Apr 2021 21:52:06 +0000 (+0200)
Subject: Improve documentation for FP rounding mode, add bibliography (#6343)
X-Git-Tag: cvc5-1.0.0~1900
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=729b25ea1270344a2ad168f272fd68f53256b661;p=cvc5.git

Improve documentation for FP rounding mode, add bibliography (#6343)

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
---

diff --git a/docs/conf.py b/docs/conf.py
index 5713d3fa3..fbe0e9131 100644
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -29,9 +29,12 @@ author = 'The Authors of cvc5'
 # ones.
 extensions = [
         'breathe',
-        'sphinx.ext.autosectionlabel'
+        'sphinx.ext.autosectionlabel',
+        'sphinxcontrib.bibtex',
 ]
 
+bibtex_bibfiles = ['references.bib']
+
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']
 
diff --git a/docs/cpp/roundingmode.rst b/docs/cpp/roundingmode.rst
index 83e2e003a..fb7a01d79 100644
--- a/docs/cpp/roundingmode.rst
+++ b/docs/cpp/roundingmode.rst
@@ -1,10 +1,10 @@
 RoundingMode
 ============
 
+.. doxygenenum:: cvc5::api::RoundingMode
+    :project: cvc5
+
 .. doxygenstruct:: cvc5::api::RoundingModeHashFunction
     :project: cvc5
     :members:
     :undoc-members:
-
-.. doxygenenum:: cvc5::api::RoundingMode
-    :project: cvc5
diff --git a/docs/index.rst b/docs/index.rst
index b6eb7edac..af8eb498f 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -16,3 +16,4 @@ cvc5 API Documentation
    :maxdepth: 2
 
    cpp
+   references
diff --git a/docs/references.bib b/docs/references.bib
new file mode 100644
index 000000000..50e410e7b
--- /dev/null
+++ b/docs/references.bib
@@ -0,0 +1,8 @@
+@article{IEEE754,
+  author={IEEE},
+  journal={IEEE Std 754-2019 (Revision of IEEE 754-2008)},
+  title={{IEEE Standard for Floating-Point Arithmetic}},
+  year={2019},
+  pages={1-84},
+  doi={10.1109/IEEESTD.2019.8766229}
+}
diff --git a/docs/references.rst b/docs/references.rst
new file mode 100644
index 000000000..7a02493ba
--- /dev/null
+++ b/docs/references.rst
@@ -0,0 +1,4 @@
+References
+==========
+
+.. bibliography::
\ No newline at end of file
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index b541c742e..a7fe9f20a 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2270,18 +2270,56 @@ class CVC4_EXPORT Grammar
 std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT;
 
 /* -------------------------------------------------------------------------- */
-/* Rounding Mode for Floating Points                                          */
+/* Rounding Mode for Floating-Points                                          */
 /* -------------------------------------------------------------------------- */
 
-/*!
- * A CVC4 floating point rounding mode.
+/**
+ * Rounding modes for floating-point numbers.
+ *
+ * For many floating-point operations, infinitely precise results may not be
+ * representable with the number of available bits. Thus, the results are rounded in
+ * a certain way to one of the representable floating-point numbers.
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * These rounding modes directly follow the SMT-LIB theory for floating-point
+ * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
+ * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
+ * Standard 754.
+ * \endverbatim
  */
 enum CVC4_EXPORT RoundingMode
 {
+  /**
+   * Round to the nearest even number.
+   * If the two nearest floating-point numbers bracketing an unrepresentable
+   * infinitely precise result are equally near, the one with an even least
+   * significant digit will be delivered.
+   */
   ROUND_NEAREST_TIES_TO_EVEN,
+  /**
+   * Round towards positive infinity (+oo).
+   * The result shall be the format’s floating-point number (possibly +oo)
+   * closest to and no less than the infinitely precise result.
+   */
   ROUND_TOWARD_POSITIVE,
+  /**
+   * Round towards negative infinity (-oo).
+   * The result shall be the format’s floating-point number (possibly -oo)
+   * closest to and no less than the infinitely precise result.
+   */
   ROUND_TOWARD_NEGATIVE,
+  /**
+   * Round towards zero.
+   * The result shall be the format’s floating-point number closest to and no
+   * greater in magnitude than the infinitely precise result.
+   */
   ROUND_TOWARD_ZERO,
+  /**
+   * Round to the nearest number away from zero.
+   * If the two nearest floating-point numbers bracketing an unrepresentable
+   * infinitely precise result are equally near, the one with larger magnitude
+   * will be selected.
+   */
   ROUND_NEAREST_TIES_TO_AWAY,
 };