From 5ac79f5d2fda1ce189c6470c8201c016e62fe943 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 11 Mar 2022 21:09:45 +0100 Subject: [PATCH] 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. --- docs/api/cpp/CMakeLists.txt | 2 +- docs/index.rst | 1 + docs/proofs/output_alethe.rst | 8 ++++++++ docs/proofs/output_lean.rst | 2 ++ docs/proofs/output_lsfc.rst | 2 ++ docs/proofs/proof_rules.rst | 5 +++++ docs/proofs/proofs.rst | 14 ++++++++++++++ 7 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 docs/proofs/output_alethe.rst create mode 100644 docs/proofs/output_lean.rst create mode 100644 docs/proofs/output_lsfc.rst create mode 100644 docs/proofs/proof_rules.rst create mode 100644 docs/proofs/proofs.rst 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 `, cvc5 can output proofs in the `Alethe proof format `_. + +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 ` :ref:`--dag-thresh=0 `. + +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 + Lean + LSFC + + +some other stuff: :doc:`proof rules `. \ No newline at end of file -- 2.30.2