Make Proof Rule enum a part of the API (cvc5#9925)

This pull requests makes the enum that lists all proof rules a part of the API. It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule). This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)
ajreynol · Sep 27, 2023 · 0a35879 · 0a35879
1 parent a3f653c
commit 0a35879
Show file tree

Hide file tree

Showing 179 changed files with 2,392 additions and 2,001 deletions.
diff --git a/docs/api/cpp/CMakeLists.txt b/docs/api/cpp/CMakeLists.txt
@@ -21,7 +21,7 @@ set(DOXYGEN_INPUT "\
 ${DOXYGEN_INPUT_DIR}/cvc5.h \
 ${DOXYGEN_INPUT_DIR}/cvc5_kind.h \
 ${DOXYGEN_INPUT_DIR}/cvc5_types.h \
-${PROJECT_SOURCE_DIR}/src/proof/proof_rule.h \
+${DOXYGEN_INPUT_DIR}/cvc5_proof_rule.h
 ")
 set(DOXYGEN_INDEX_FILE ${DOXYGEN_OUTPUT_DIR}/xml/index.xml)
 
@@ -42,7 +42,7 @@ add_custom_command(
     ${DOXYGEN_INPUT_DIR}/cvc5.h
     ${DOXYGEN_INPUT_DIR}/cvc5_kind.h
     ${DOXYGEN_INPUT_DIR}/cvc5_types.h
-    ${PROJECT_SOURCE_DIR}/src/proof/proof_rule.h
+    ${DOXYGEN_INPUT_DIR}/cvc5_proof_rule.h
   COMMENT "Generating doxygen API docs"
 )
 add_custom_target(docs-cpp DEPENDS ${DOXYGEN_INDEX_FILE})

diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt
@@ -22,6 +22,36 @@ if(BUILD_BINDINGS_JAVA)
   set(JAVADOC_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/build/api/java)
   # used to trigger the rebuild
   set(JAVADOC_INDEX_FILE ${JAVADOC_OUTPUT_DIR}/index.html)
+  # HTML added to javadoc to include Mathjax
+  # This is fragile with respect to escapes:
+  #   - The LaTeX sequence '$#1$' must be written as '\$$#1$$'.
+  #   - Whitespaces in some places must be omitted, otherwise
+  #     they become ';'.
+  #   - To make LaTeX commands work they need '\\\\'.
+  set(JAVADOC_MATHJAX [=["
+    <script>
+    window.MathJax = {
+      'loader': {
+        'load': ['[tex]/ams','[tex]/bussproofs'],
+      },
+      'tex': {
+        'packages': {
+          '[+]': ['ams','bussproofs'],
+        },
+        'macros': {
+          'xor': '\\\\mathbin{xor}',
+          'ite': ['#1~\\\\mathbin{?}~#2~\\\\mathbin{:}~#3',3],
+          'inferrule': ['\\\\begin{prooftree}\\\\AxiomC{\$$#1$$}\\\\UnaryInfC{\$$#2$$}\\\\end{prooftree}',2],
+          'inferruleSC': ['\\\\begin{prooftree}\\\\AxiomC{\$$#1$$}\\\\RightLabel{~#3}\\\\UnaryInfC{\$$#2$$}\\\\end{prooftree}',3],
+        }
+      }
+    }
+    </script>
+    <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'>
+    </script>
+  "]=])
+  string(REPLACE "\n" " " JAVADOC_MATHJAX ${JAVADOC_MATHJAX})
+  string(REPLACE " " ";" JAVADOC_MATHJAX ${JAVADOC_MATHJAX})
 
   get_target_property(CVC5_JAR_FILE cvc5jar JAR_FILE)
   add_custom_command(
@@ -32,6 +62,8 @@ if(BUILD_BINDINGS_JAVA)
       -d ${JAVADOC_OUTPUT_DIR}
       -cp ${CVC5_JAR_FILE}
       -tag "api.note:a:Note:"
+      --allow-script-in-comments
+      -header ${JAVADOC_MATHJAX}
       -notimestamp
     COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's/<!-- Generated by javadoc [^>]* -->//' {} "\;"
     COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete

diff --git a/docs/api/java/java.rst b/docs/api/java/java.rst
@@ -79,6 +79,7 @@ Building cvc5 Java API
   * enum `Kind <io/github/cvc5/Kind.html>`_
   * enum `Result.UnknownExplanation <io/github/cvc5/Result.UnknownExplanation.html>`_
   * enum `RoundingMode <io/github/cvc5/RoundingMode.html>`_
+  * enum `ProofRule <io/github/cvc5/ProofRule.html>`_
   * exception `CVC5ApiException <io/github/cvc5/CVC5ApiException.html>`_
   * exception `CVC5ApiOptionException <io/github/cvc5/CVC5ApiOptionException.html>`_
   * exception `CVC5ApiRecoverableException <io/github/cvc5/CVC5ApiRecoverableException.html>`_
diff --git a/docs/api/python/base/proofrule.rst b/docs/api/python/base/proofrule.rst
@@ -0,0 +1,6 @@
+ProofRule
+=========
+
+.. autoclass:: cvc5.ProofRule
+    :members:
+    :undoc-members:
diff --git a/docs/proofs/proof_rules.rst b/docs/proofs/proof_rules.rst
@@ -1,5 +1,5 @@
 Proof rules
 ===========
 
-.. doxygenenum:: cvc5::internal::PfRule
+.. doxygenenum:: cvc5::ProofRule
     :project: cvc5
diff --git a/include/cvc5/cvc5.h b/include/cvc5/cvc5.h
@@ -20,6 +20,7 @@
 
 #include <cvc5/cvc5_kind.h>
 #include <cvc5/cvc5_types.h>
+#include <cvc5/cvc5_proof_rule.h>
 
 #include <functional>
 #include <map>