Add doc page about transcendentals (#6755)

This PR adds a theory reference page for the transcendental extension.

4 files changed, 81 insertions, 0 deletions

diff --git a/docs/_static/custom.css b/docs/_static/custom.css
index 9d07edeaf..6934d7017 100644
--- a/docs/_static/custom.css
+++ b/docs/_static/custom.css
@@ -88,6 +88,11 @@ a:hover, a:focus {
   color: #ba2121;
 }
 
+/* Removes margin of code blocks within tabs */
+.sphinx-tabs-panel div[class^="highlight"] {
+  margin: 1px 0 0 0;
+}
+
 #c-api-class-hierarchy code {
   font-size: 100%;
   font-weight: normal;
diff --git a/docs/references.bib b/docs/references.bib
index 8e3fd5e69..12eecc8ba 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -1,3 +1,23 @@
+@article{DBLP:journals/tocl/CimattiGIRS18,
+  author    = {Alessandro Cimatti and
+               Alberto Griggio and
+               Ahmed Irfan and
+               Marco Roveri and
+               Roberto Sebastiani},
+  title     = {Incremental Linearization for Satisfiability and Verification Modulo
+               Nonlinear Arithmetic and Transcendental Functions},
+  journal   = {{ACM} Trans. Comput. Log.},
+  volume    = {19},
+  number    = {3},
+  pages     = {19:1--19:52},
+  year      = {2018},
+  doi       = {10.1145/3230639},
+  timestamp = {Fri, 09 Apr 2021 18:33:35 +0200},
+  biburl    = {https://dblp.org/rec/journals/tocl/CimattiGIRS18.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+
 @article{IEEE754,
   author={IEEE},
   journal={IEEE Std 754-2019 (Revision of IEEE 754-2008)},
diff --git a/docs/theories/transcendentals.rst b/docs/theories/transcendentals.rst
new file mode 100644
index 000000000..cf52b0889
--- /dev/null
+++ b/docs/theories/transcendentals.rst
@@ -0,0 +1,55 @@
+Theory Reference: Transcendentals
+=================================
+
+cvc5 supports transcendental functions that naturally extend the nonlinear real arithmetic theories ``NRA`` and ``NIRA``.
+The theory consists of the constant :math:`\pi` and function symbols for most common transcendental functions like, e.g., ``sin``, ``cos`` and ``tan``.
+
+Logic
+-----
+
+To enable cvc5's decision procedure for transcendentals, append ``T`` to the arithmetic logic that is being used:
+
+.. code:: smtlib
+
+  (set-logic QF_NRAT)
+
+Alternatively, use the ``ALL`` logic:
+
+.. code:: smtlib
+
+  (set-logic ALL)
+
+Syntax
+------
+
+cvc5 internally defines a constant ``real.pi`` of sort ``Real`` and the following unary function symbols from ``Real`` to ``Real``:
+
+* the square root function ``sqrt``
+* the exponential function ``exp``
+* the sine function ``sin``
+* the cosine function ``cos``
+* the tangent function ``tan``
+* the cosecant function ``csc``
+* the secant function ``sec``
+* the cotangent function ``cot``
+* the arcsine function ``arcsin``
+* the arccosine function ``arccos``
+* the arctangent function ``arctan``
+* the arccosecant function ``arccsc``
+* the arcsecant function ``arcsec``
+* the arccotangent function ``arccot``
+
+
+Semantics
+---------
+
+Both the constant ``real.pi`` and all function symbols are defined on real numbers and are thus not subject to limited precision. That being said, cvc5 internally uses inexact techniques based on incremental linearization.
+While ``real.pi`` is specified using a rational enclosing interval that is automatically refined on demand, the function symbols are approximated using tangent planes and secant lines using the techniques described in :cite:`DBLP:journals/tocl/CimattiGIRS18`.
+
+Examples
+--------
+
+.. api-examples::
+    ../../examples/api/cpp/transcendentals.cpp
+    ../../examples/api/python/transcendentals.py
+    ../../examples/api/smtlib/transcendentals.smt2
\ No newline at end of file
diff --git a/docs/theory.rst b/docs/theory.rst
index 2d2a949d5..075de8ba4 100644
--- a/docs/theory.rst
+++ b/docs/theory.rst
@@ -7,3 +7,4 @@ Theory References
    theories/datatypes
    theories/separation-logic
    theories/sets-and-relations
+   theories/transcendentals