Some minor improvements to the theory references (#7881)

diff --git a/docs/index.rst b/docs/index.rst
index 27b7b728dfaee32696642a0e90c41b35b32c1ce2..133ad958c0f5388b24ce0bcb0180fec1ff82802d 100644 (file)
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -18,6 +18,6 @@ Table of Contents
    binary/binary
    api/api
    examples/examples
-   theory
+   theories/theories
    references
    genindex

diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst
index 1211a43ee63ddeeeff23f5a780840fc0b7667049..c9a15ad24e9222247e31ff32d3525b11e803cb6e 100644 (file)
--- a/docs/theories/datatypes.rst
+++ b/docs/theories/datatypes.rst
@@ -1,6 +1,8 @@
 Theory Reference: Datatypes
 ===========================
 
+cvc5 implements some extensions to the support for datatypes in SMT-LIB 2.
+
 Logic
 -----
 

diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index 8dd76dbfb9ae4992df297a3375180733901218e0..5184603be2ce668fe5e368a335f12051b7bfd5c4 100644 (file)
--- a/docs/theories/sets-and-relations.rst
+++ b/docs/theories/sets-and-relations.rst
@@ -4,25 +4,8 @@ Theory Reference: Sets and Relations
 Finite Sets
 -----------
 
-cvc5 supports the theory of finite sets.
-The simplest way to get a sense of the syntax is to look at an example:
-
-.. api-examples::
-    <examples>/api/cpp/sets.cpp
-    <examples>/api/java/Sets.java
-    <examples>/api/python/sets.py
-    <examples>/api/smtlib/sets.smt2
-
-The source code of these examples is available at:
-
-* `SMT-LIB 2 language example <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/sets.smt2>`__
-* `C++ API example <https://github.com/cvc5/cvc5/blob/master/examples/api/cpp/sets.cpp>`__
-* `Java API example <https://github.com/cvc5/cvc5/blob/master/examples/api/java/Sets.java>`__
-* `Python API example <https://github.com/cvc5/cvc5/blob/master/examples/api/python/sets.py>`__
-
-
-Below is a short summary of the sorts, constants, functions and
-predicates.  More details can be found in :cite:`BansalBRT17`.
+cvc5 supports the theory of finite sets using the following sorts, constants,
+functions and predicates.  More details can be found in :cite:`BansalBRT17`.
 
 For the C++ API examples in the table below, we assume that we have created
 a `cvc5::api::Solver solver` object.
@@ -144,16 +127,21 @@ Above, notice that we were able to find a model for the universe set of sort
   The reason for that is that making this formula (and similar ones) `unsat` is
   counter-intuitive when quantifiers are present.
 
-Finite Relations
-----------------
 
-Example:
+Below is a more extensive example on how to use finite sets:
 
 .. api-examples::
-    <examples>/api/smtlib/relations.smt2
+    <examples>/api/cpp/sets.cpp
+    <examples>/api/java/Sets.java
+    <examples>/api/python/sets.py
+    <examples>/api/smtlib/sets.smt2
 
-For reference, below is a short summary of the sorts, constants, functions and
-predicates.
+
+Finite Relations
+----------------
+
+cvc5 also supports the theory of finite relations, using the following sorts,
+constants, functions and predicates.
 More details can be found in :cite:`MengRTB17`.
 
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
@@ -173,7 +161,7 @@ More details can be found in :cite:`MengRTB17`.
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 | Tuple Constructor    | ``(tuple <Term_1>, ..., <Term_n>)``          | ``Term t = solver.mkTuple({<Sort_1>, ..., <Sort_n>}, {Term_1>, ..., <Term_n>});``  |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Tuple Selector       | ``((_ tuple_select i) t)``                         | ``Sort s = solver.mkTupleSort(sorts);``                                            |
+| Tuple Selector       | ``((_ tuple_select i) t)``                   | ``Sort s = solver.mkTupleSort(sorts);``                                            |
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Datatype dt = s.getDatatype();``                                                 |
 |                      |                                              |                                                                                    |
@@ -195,3 +183,8 @@ More details can be found in :cite:`MengRTB17`.
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 | Product              | ``(rel.product X Y)``                        | ``Term t = solver.mkTerm(Kind::RELATION_PRODUCT, X, Y);``                          |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
+
+Example:
+
+.. api-examples::
+    <examples>/api/smtlib/relations.smt2

diff --git a/docs/theories/theories.rst b/docs/theories/theories.rst
new file mode 100644 (file)
index 0000000..dd4f2c8
--- /dev/null
+++ b/docs/theories/theories.rst
@@ -0,0 +1,13 @@
+Theory References
+=================
+
+cvc5 implements several theories that are not (yet) standardized in SMT-LIB, or
+that extend beyond the respective standardized theory.
+
+.. toctree::
+   :maxdepth: 1
+
+   datatypes
+   separation-logic
+   sets-and-relations
+   transcendentals

diff --git a/docs/theory.rst b/docs/theory.rst
deleted file mode 100644 (file)
index 075de8b..0000000
--- a/docs/theory.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-Theory References
-=================
-
-.. toctree::
-   :maxdepth: 1
-
-   theories/datatypes
-   theories/separation-logic
-   theories/sets-and-relations
-   theories/transcendentals