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 5713d3fa305548a90b855a6c8e8a42a2f659fffc..fbe0e913108b24800e5eec347381217db8d3a09f 100644 (file)
--- 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 83e2e003ab3d7da8793bbba9d1956c0ebccfe855..fb7a01d79801f4e3c72df33a99994b17dd7b4fdf 100644 (file)
--- 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 b6eb7edac97f25dcc82e55523db5a266001223d7..af8eb498fbaef3fbd6ceddb05544a78be0b31314 100644 (file)
--- 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 (file)
index 0000000..50e410e
--- /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 (file)
index 0000000..7a02493
--- /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 b541c742e7f14cf0f89a32f654233ae3f79157aa..a7fe9f20ad4616ac4391a02e242288b3e09c7608 100644 (file)
--- 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,
 };