Add more examples to the documentation (#6569)

This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)

25 files changed, 139 insertions, 16 deletions

diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst
new file mode 100644
index 000000000..d28beab14
--- /dev/null
+++ b/docs/binary/binary.rst
@@ -0,0 +1,7 @@
+Binary Documentation
+====================
+
+.. toctree::
+    :maxdepth: 2
+
+    options
diff --git a/docs/options.rst b/docs/binary/options.rst
index 6f9c613e7..6f9c613e7 100644
--- a/docs/options.rst
+++ b/docs/binary/options.rst
diff --git a/docs/conf.py.in b/docs/conf.py.in
index 9dc5255bd..6a23ff759 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -70,6 +70,7 @@ html_css_files = ['custom.css']
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
 breathe_domain_by_extension = {"h" : "cpp"}
+cpp_index_common_prefix = ["cvc5::api::"]
 
 # where to look for include-build-file
 ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}']
diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst
index a2e928927..8d302d60c 100644
--- a/docs/cpp/cpp.rst
+++ b/docs/cpp/cpp.rst
@@ -1,3 +1,5 @@
+.. _cpp-api:
+
 C++ API Documentation
 =====================
 
diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst
new file mode 100644
index 000000000..354c86751
--- /dev/null
+++ b/docs/examples/bitvectors.rst
@@ -0,0 +1,8 @@
+Theory of Bit-Vectors
+=====================
+
+
+.. api-examples::
+    ../../examples/api/cpp/bitvectors.cpp
+    ../../examples/api/java/BitVectors.java
+    ../../examples/api/python/bitvectors.py
diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst
new file mode 100644
index 000000000..9d63f36bd
--- /dev/null
+++ b/docs/examples/bitvectors_and_arrays.rst
@@ -0,0 +1,8 @@
+Theory of Bit-Vectors and Arrays
+================================
+
+
+.. api-examples::
+    ../../examples/api/cpp/bitvectors_and_arrays.cpp
+    ../../examples/api/java/BitVectorsAndArrays.java
+    ../../examples/api/python/bitvectors_and_arrays.py
diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst
new file mode 100644
index 000000000..5f301a14f
--- /dev/null
+++ b/docs/examples/combination.rst
@@ -0,0 +1,8 @@
+Theory Combination
+==================
+
+
+.. api-examples::
+    ../../examples/api/cpp/combination.cpp
+    ../../examples/api/java/Combination.java
+    ../../examples/api/python/combination.py
diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
index 8200ebb14..abbb16964 100644
--- a/docs/examples/datatypes.rst
+++ b/docs/examples/datatypes.rst
@@ -1,8 +1,8 @@
-Datatypes
-===========
+Theory of Datatypes
+===================
 
 
 .. api-examples::
-    ../../examples/api/datatypes.cpp
+    ../../examples/api/cpp/datatypes.cpp
     ../../examples/api/java/Datatypes.java
     ../../examples/api/python/datatypes.py
diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst
index ff3651857..528566a3e 100644
--- a/docs/examples/examples.rst
+++ b/docs/examples/examples.rst
@@ -1,9 +1,25 @@
 Examples
 ===========
 
+The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) and input languages can be used.
+For every example, the same problem is constructed and solved using different input mechanisms.
+
+
 .. toctree::
     :maxdepth: 2
  
     helloworld
+    exceptions
+    bitvectors
+    bitvectors_and_arrays
+    extract
     datatypes
-    lineararith
\ No newline at end of file
+    floatingpoint
+    lineararith
+    sequences
+    sets
+    strings
+    combination
+    sygus-fun
+    sygus-grammar
+    sygus-inv
\ No newline at end of file
diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst
new file mode 100644
index 000000000..6598e8fb0
--- /dev/null
+++ b/docs/examples/exceptions.rst
@@ -0,0 +1,7 @@
+Exception Handling
+======================================
+
+
+.. api-examples::
+    ../../examples/api/java/Exceptions.java
+    ../../examples/api/python/exceptions.py
diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst
new file mode 100644
index 000000000..0108de948
--- /dev/null
+++ b/docs/examples/extract.rst
@@ -0,0 +1,7 @@
+Theory of Bit-Vectors: :code:`extract`
+======================================
+
+
+.. api-examples::
+    ../../examples/api/cpp/extract.cpp
+    ../../examples/api/python/extract.py
diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
new file mode 100644
index 000000000..1b09102b2
--- /dev/null
+++ b/docs/examples/floatingpoint.rst
@@ -0,0 +1,7 @@
+Theory of Floating-Points
+======================================
+
+
+.. api-examples::
+    ../../examples/api/java/FloatingPointArith.java
+    ../../examples/api/python/floating_point.py
diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst
index 202952bb6..cdc424dfa 100644
--- a/docs/examples/helloworld.rst
+++ b/docs/examples/helloworld.rst
@@ -5,6 +5,7 @@ This example shows the very basic usage of the API.
 We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver).
 
 .. api-examples::
-    ../../examples/api/helloworld.cpp
+    ../../examples/api/cpp/helloworld.cpp
     ../../examples/api/java/HelloWorld.java
     ../../examples/api/python/helloworld.py
+    ../../examples/api/smtlib/helloworld.smt2
diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst
index d772edbb3..29d84cae5 100644
--- a/docs/examples/lineararith.rst
+++ b/docs/examples/lineararith.rst
@@ -1,8 +1,13 @@
-Linear Arithmetic
-=================
+Theory of Linear Arithmetic
+===========================
 
+This example asserts three constraints over an integer variable :code:`x` and a real variable :code:`y`.
+Firstly, it checks that these constraints entail an upper bound on the difference :code:`y - x <= 2/3`.
+Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` and checking for satisfiability.
+The two checks are separated by using :code:`push` and :code:`pop`.
 
 .. api-examples::
-    ../../examples/api/linear_arith.cpp
+    ../../examples/api/cpp/linear_arith.cpp
     ../../examples/api/java/LinearArith.java
     ../../examples/api/python/linear_arith.py
+    ../../examples/api/smtlib/linear_arith.smt2
diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst
new file mode 100644
index 000000000..a6f9e2238
--- /dev/null
+++ b/docs/examples/sequences.rst
@@ -0,0 +1,7 @@
+Theory of Sequences
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sequences.cpp
+    ../../examples/api/python/sequences.py
diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst
new file mode 100644
index 000000000..71a6843c3
--- /dev/null
+++ b/docs/examples/sets.rst
@@ -0,0 +1,7 @@
+Theory of Sets
+=================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sets.cpp
+    ../../examples/api/python/sets.py
diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst
new file mode 100644
index 000000000..87f566363
--- /dev/null
+++ b/docs/examples/strings.rst
@@ -0,0 +1,8 @@
+Theory of Strings
+=================
+
+
+.. api-examples::
+    ../../examples/api/cpp/strings.cpp
+    ../../examples/api/java/Strings.java
+    ../../examples/api/python/strings.py
diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst
new file mode 100644
index 000000000..3d5bddff1
--- /dev/null
+++ b/docs/examples/sygus-fun.rst
@@ -0,0 +1,7 @@
+SyGuS: Functions
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sygus-fun.cpp
+    ../../examples/api/python/sygus-fun.py
diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst
new file mode 100644
index 000000000..3733fe2c3
--- /dev/null
+++ b/docs/examples/sygus-grammar.rst
@@ -0,0 +1,7 @@
+SyGuS: Grammars
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sygus-grammar.cpp
+    ../../examples/api/python/sygus-grammar.py
diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst
new file mode 100644
index 000000000..f9698a720
--- /dev/null
+++ b/docs/examples/sygus-inv.rst
@@ -0,0 +1,7 @@
+SyGuS: Invariants
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sygus-inv.cpp
+    ../../examples/api/python/sygus-inv.py
diff --git a/docs/ext/examples.py b/docs/ext/examples.py
index befb6c175..003726de4 100644
--- a/docs/ext/examples.py
+++ b/docs/ext/examples.py
@@ -22,6 +22,7 @@ class APIExamples(Directive):
         '.cpp': {'title': 'C++', 'lang': 'c++'},
         '.java': {'title': 'Java', 'lang': 'java'},
         '.py': {'title': 'Python', 'lang': 'python'},
+        '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'},
     }
 
     # The "arguments" are actually the content of the directive
diff --git a/docs/genindex.rst b/docs/genindex.rst
new file mode 100644
index 000000000..9e530fa2f
--- /dev/null
+++ b/docs/genindex.rst
@@ -0,0 +1,2 @@
+Index
+=====
diff --git a/docs/index.rst b/docs/index.rst
index 8d77790fb..fc82111e2 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -6,17 +6,13 @@
 cvc5 API Documentation
 ======================
 
-
-* :ref:`genindex`
-
-
----------------
-
 .. toctree::
    :maxdepth: 1
 
+   installation/installation
+   binary/binary
    cpp/cpp
    python/python
-   references
    examples/examples
-   options
+   references
+   genindex
diff --git a/docs/installation/installation.rst b/docs/installation/installation.rst
new file mode 100644
index 000000000..e50cd8d4b
--- /dev/null
+++ b/docs/installation/installation.rst
@@ -0,0 +1,2 @@
+Installation
+============
\ No newline at end of file
diff --git a/docs/python/python.rst b/docs/python/python.rst
index 50d9077df..c3e425a7f 100644
--- a/docs/python/python.rst
+++ b/docs/python/python.rst
@@ -1,3 +1,5 @@
+.. _python-api:
+
 Python API Documentation
 ========================