Some random documentation issues (#7921)

This PR fixes a few issues in the documentation, mostly about examples that were not included where they should be.

diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst
index cb3e00fabbcaa20b703f3aafd086d8b5252b1824..88320a508ff9bcbc489939f20f546ec27ce4aee7 100644 (file)
--- a/docs/api/cpp/quickstart.rst
+++ b/docs/api/cpp/quickstart.rst
@@ -177,11 +177,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/cpp/quickstart.cpp <https://github.com/cvc5/cvc5/blob/master/examples/api/cpp/quickstart.cpp>`_.
-
 .. api-examples::
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/api/java/quickstart.rst b/docs/api/java/quickstart.rst
index 2c986ab55877d9e56f28d871561b35c6ba1749be..ccc8a7e13dc8d10620a902bbbb031a1affae47f7 100644 (file)
--- a/docs/api/java/quickstart.rst
+++ b/docs/api/java/quickstart.rst
@@ -181,11 +181,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/java/QuickStart.java <https://github.com/cvc5/cvc5/blob/master/examples/api/java/QuickStart.java>`_.
-
 .. api-examples::
     <examples>/api/java/QuickStart.java
     <examples>/api/cpp/quickstart.cpp
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst
index ba3360db8fd7a485c53ba095dfd48caddf248f8f..e1c2993b5786b7657247949cb8dadf044ad4af7b 100644 (file)
--- a/docs/api/python/base/quickstart.rst
+++ b/docs/api/python/base/quickstart.rst
@@ -165,11 +165,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/python/quickstart.py <https://github.com/cvc5/cvc5/blob/master/examples/api/python/quickstart.py>`_.
-
 .. api-examples::
+    <examples>/api/python/quickstart.py
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
-    <examples>/api/python/quickstart.py
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/binary/options.rst b/docs/binary/options.rst
index 6f9c613e7649c130e8ea12a255bad1c1813acfac..d301c704518a8b43a471db322ca0cce874fc2bac 100644 (file)
--- a/docs/binary/options.rst
+++ b/docs/binary/options.rst
@@ -1,5 +1,7 @@
 Commandline Options
 ===================
 
+Below is an exhaustive list of commandline options supported by cvc5.
+
 .. include-build-file:: options_generated.rst
 

diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst
index ddfc7d9f07cbae862a3de912f6e4919c05c61195..b7b35716b88b05d2f1cfca5d4e1f918c1b531f96 100644 (file)
--- a/docs/binary/quickstart.rst
+++ b/docs/binary/quickstart.rst
@@ -115,11 +115,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-
 .. api-examples::
     <examples>/api/smtlib/quickstart.smt2
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py

diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
index 5f3dd7855cd5b771bad9ee201c8409309c94c3db..7cf4e32dd3da5b0ddeae92f94e2989c6376edb3f 100644 (file)
--- a/docs/examples/floatingpoint.rst
+++ b/docs/examples/floatingpoint.rst
@@ -3,6 +3,7 @@ Theory of Floating-Points
 
 
 .. api-examples::
+    <examples>/api/cpp/floating_point_arith.cpp
     <examples>/api/java/FloatingPointArith.java
     <z3pycompat>/test/pgms/example_floating_point.py
     <examples>/api/python/floating_point.py