Add first step for proofs documentation (#8193)

This PR initializes some documentation for our proofs. It adds some almost empty files and makes sure that we can show documentation for the PfRule enum.

diff --git a/docs/api/cpp/CMakeLists.txt b/docs/api/cpp/CMakeLists.txt
index 511dd6e9c158d031ae885cd7c5f4379a7c9a0508..453809360916b8dcb07c170974489cd5bacfa341 100644 (file)
--- a/docs/api/cpp/CMakeLists.txt
+++ b/docs/api/cpp/CMakeLists.txt
@@ -18,7 +18,7 @@ find_package(Doxygen REQUIRED)
 set(DOXYGEN_INPUT_DIR ${PROJECT_SOURCE_DIR}/src/api/cpp)
 set(DOXYGEN_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/doxygen)
 set(DOXYGEN_INPUT
-    "${DOXYGEN_INPUT_DIR}/cvc5.h ${DOXYGEN_INPUT_DIR}/cvc5_kind.h"
+    "${DOXYGEN_INPUT_DIR}/cvc5.h ${DOXYGEN_INPUT_DIR}/cvc5_kind.h ${PROJECT_SOURCE_DIR}/src/proof/proof_rule.h"
 )
 set(DOXYGEN_INDEX_FILE ${DOXYGEN_OUTPUT_DIR}/xml/index.xml)
 

diff --git a/docs/index.rst b/docs/index.rst
index 133ad958c0f5388b24ce0bcb0180fec1ff82802d..a533ff4b6356b98ad781de18f1d7b6d0259ce08f 100644 (file)
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -17,6 +17,7 @@ Table of Contents
    installation/installation
    binary/binary
    api/api
+   proofs/proofs
    examples/examples
    theories/theories
    references

diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst
new file mode 100644 (file)
index 0000000..ef3cd36
--- /dev/null
+++ b/docs/proofs/output_alethe.rst
@@ -0,0 +1,8 @@
+Proof format: Alethe
+====================
+
+Using the flag :ref:`--proof-format-mode=alethe <lbl-option-proof-format-mode>`, cvc5 can output proofs in the `Alethe proof format <https://verit.loria.fr/documentation/alethe-spec.pdf>`_.
+
+Additonally, the following flags should be used to produce proofs without term sharing (which is not supported for the Alethe backend yet): :ref:`--simplification=none <lbl-option-simplification>` :ref:`--dag-thresh=0 <lbl-option-dag-thresh>`.
+
+Currently, only the theory of equality with uninterpreted functions, parts of the theory of arithmetic and parts of the theory of quantifiers are supported.

diff --git a/docs/proofs/output_lean.rst b/docs/proofs/output_lean.rst
new file mode 100644 (file)
index 0000000..6eaea77
--- /dev/null
+++ b/docs/proofs/output_lean.rst
@@ -0,0 +1,2 @@
+Proof format: Lean
+==================
\ No newline at end of file

diff --git a/docs/proofs/output_lsfc.rst b/docs/proofs/output_lsfc.rst
new file mode 100644 (file)
index 0000000..131a786
--- /dev/null
+++ b/docs/proofs/output_lsfc.rst
@@ -0,0 +1,2 @@
+Proof format: LSFC
+==================
\ No newline at end of file

diff --git a/docs/proofs/proof_rules.rst b/docs/proofs/proof_rules.rst
new file mode 100644 (file)
index 0000000..6a0374b
--- /dev/null
+++ b/docs/proofs/proof_rules.rst
@@ -0,0 +1,5 @@
+Proof rules
+===========
+
+.. doxygenenum:: cvc5::PfRule
+    :project: cvc5

diff --git a/docs/proofs/proofs.rst b/docs/proofs/proofs.rst
new file mode 100644 (file)
index 0000000..0404491
--- /dev/null
+++ b/docs/proofs/proofs.rst
@@ -0,0 +1,14 @@
+Proof generation
+================
+
+cvc5 can generate formal proofs and output it in the following formats:
+
+.. toctree::
+   :maxdepth: 1
+   
+   Alethe <output_alethe>
+   Lean <output_lean>
+   LSFC <output_lsfc>
+
+
+some other stuff: :doc:`proof rules <proof_rules>`.
\ No newline at end of file