From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 2 Mar 2022 00:44:03 +0000 (+0100)
Subject: Add standard theories to documentation (#8192)
X-Git-Tag: cvc5-1.0.0~351
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd6e741246876d6debdace1913ce00209fba26c0;p=cvc5.git

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 dd4f2c8a1..6a7a78398 100644
--- 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