Add standard theories to documentation (#8192)

This PR adds the standardized theories to our theories overview.

diff --git a/docs/theories/theories.rst b/docs/theories/theories.rst
index dd4f2c8a1b986fed1f0d7d24ea38f293caef6b46..6a7a783983072c31662199acd69f459b28eec638 100644 (file)
--- a/docs/theories/theories.rst
+++ b/docs/theories/theories.rst
@@ -1,8 +1,26 @@
 Theory References
 =================
 
-cvc5 implements several theories that are not (yet) standardized in SMT-LIB, or
+cvc5 implements all theories that are currently standardized in SMT-LIB, as well as several theories that are not (yet) standardized, or
 that extend beyond the respective standardized theory.
+Furthermore, cvc5 supports all combinations of those theories as well as combinations with `datatypes, quantifiers, and uninterpreted functions (as defined in the SMT-LIB standard) <https://smtlib.cs.uiowa.edu/language.shtml>`_.
+
+Standardized theories
+---------------------
+
+.. toctree::
+   :maxdepth: 1
+
+   Theory of arrays <https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml>
+   Theory of bit-vectors <https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml>
+   Theory of floating-point numbers <https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>
+   Theory of integer arithmetic <https://smtlib.cs.uiowa.edu/theories-Ints.shtml>
+   Theory of real arithmetic <https://smtlib.cs.uiowa.edu/theories-Reals.shtml>
+   Theory of mixed-integer arithmetic <https://smtlib.cs.uiowa.edu/theories-Reals_Ints.shtml>
+   Theory of strings <https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>
+
+Non-standard or extended theories
+---------------------------------
 
 .. toctree::
    :maxdepth: 1