From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Fri, 11 Mar 2022 20:09:45 +0000 (+0100)
Subject: Add first step for proofs documentation (#8193)
X-Git-Tag: cvc5-1.0.0~278
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ac79f5d2fda1ce189c6470c8201c016e62fe943;p=cvc5.git

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 511dd6e9c..453809360 100644
--- 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 133ad958c..a533ff4b6 100644
--- 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
index 000000000..ef3cd3633
--- /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
index 000000000..6eaea77bc
--- /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
index 000000000..131a7864d
--- /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
index 000000000..6a0374ba9
--- /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
index 000000000..04044912d
--- /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