Integrate javadoc documentation (#7278)

This PR adds the cmake setup to generate javadoc documentation for the java API and integrates it into the sphinx documentation. Right now, we simply link to the javadoc. This PR also modifies a bunch of javadoc comments to use proper javadoc syntax.

10 files changed, 167 insertions, 116 deletions

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 2d8abc8cf..c4cc6c283 100644
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -26,7 +26,7 @@ configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py)
 
 add_custom_target(
   docs ALL
-  DEPENDS docs-cpp docs-python gen-options
+  DEPENDS docs-cpp docs-java docs-python gen-options
   COMMAND
     ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR}
     # Tell Breathe where to find the Doxygen output
diff --git a/docs/api/CMakeLists.txt b/docs/api/CMakeLists.txt
index 3ade7b5b2..73352fd9b 100644
--- a/docs/api/CMakeLists.txt
+++ b/docs/api/CMakeLists.txt
@@ -13,6 +13,7 @@
 # The build system configuration.
 #
 add_subdirectory(cpp)
+add_subdirectory(java)
 add_subdirectory(python)
 
 # tell parent scope where to find the output xml
diff --git a/docs/api/api.rst b/docs/api/api.rst
index 34ee0aec7..a3acdda17 100644
--- a/docs/api/api.rst
+++ b/docs/api/api.rst
@@ -5,4 +5,5 @@ API Documentation
    :maxdepth: 1
 
    cpp/cpp
+   java/index
    python/python
diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt
new file mode 100644
index 000000000..5606357c6
--- /dev/null
+++ b/docs/api/java/CMakeLists.txt
@@ -0,0 +1,42 @@
+###############################################################################
+# Top contributors (to current version):
+#   Gereon Kremer
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# Build system configuration for java API documentation.
+#
+
+add_custom_target(docs-java)
+
+if(BUILD_BINDINGS_JAVA)
+  find_package(Java REQUIRED)
+
+  # put generated doc in a place where sphinx can easily copy from
+  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)
+
+  get_target_property(SOURCES cvc5jar SOURCES)
+  
+  add_custom_command(
+    OUTPUT "${JAVADOC_INDEX_FILE}"
+    COMMAND 
+      ${Java_JAVADOC_EXECUTABLE} cvc5
+      --source-path ${CMAKE_SOURCE_DIR}/src/api/java/
+      -d ${JAVADOC_OUTPUT_DIR}
+      -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar
+    DEPENDS cvc5jar ${SOURCES}
+    COMMENT "Generating javadocs"
+  )
+
+  add_custom_target(docs-java-javadoc DEPENDS ${JAVADOC_INDEX_FILE})
+  add_dependencies(docs-java docs-java-javadoc)
+endif()
+
diff --git a/docs/api/java/index.rst b/docs/api/java/index.rst
new file mode 100644
index 000000000..1aee013fc
--- /dev/null
+++ b/docs/api/java/index.rst
@@ -0,0 +1,4 @@
+Java API Documentation
+======================
+
+This file is just a placeholder that is replaced by javadocs index.html
\ No newline at end of file
diff --git a/docs/conf.py.in b/docs/conf.py.in
index 4447d1441..0df5b2397 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -72,6 +72,10 @@ html_static_path = ['${CMAKE_CURRENT_SOURCE_DIR}/_static/']
 html_css_files = ['custom.css']
 html_show_sourcelink = False
 
+html_extra_path = [
+        "${CMAKE_BINARY_DIR}/docs/api/java/build/"
+]
+
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
 breathe_domain_by_extension = {"h" : "cpp"}
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 293e5c270..bfc266f56 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3830,7 +3830,7 @@ class CVC5_EXPORT Solver
 
   /**
    * Get info from the solver.
-   * SMT-LIB: \verbatim( get-info <info_flag> )\verbatim
+   * SMT-LIB: \verbatim( get-info <info_flag> )\endverbatim
    * @return the info
    */
   std::string getInfo(const std::string& flag) const;
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index a2fc1dba9..12601f397 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -138,5 +138,6 @@ add_jar(cvc5jar
   VERSION ${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}
   OUTPUT_NAME cvc5
 )
+set_target_properties(cvc5jar PROPERTIES SOURCES "${JAVA_FILES}")
 
 add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5-shared)
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index 65efcb170..d295113b0 100644
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -1179,10 +1179,10 @@ public class Solver implements IPointer
   /**
    * Create (first-order) constant (0-arity function symbol).
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( declare-const <symbol> <sort> )
    *   ( declare-fun <symbol> ( ) <sort> )
-   * \endverbatim
+   * }
    *
    * @param sort the sort of the constant
    * @param symbol the name of the constant
@@ -1371,9 +1371,9 @@ public class Solver implements IPointer
   /**
    * Assert a formula.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( assert <term> )
-   * \endverbatim
+   * }
    * @param term the formula to assert
    */
   public void assertFormula(Term term)
@@ -1386,9 +1386,9 @@ public class Solver implements IPointer
   /**
    * Check satisfiability.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( check-sat )
-   * \endverbatim
+   * }
    * @return the result of the satisfiability check.
    */
   public Result checkSat()
@@ -1401,9 +1401,9 @@ public class Solver implements IPointer
   /**
    * Check satisfiability assuming the given formula.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( check-sat-assuming ( <prop_literal> ) )
-   * \endverbatim
+   * }
    * @param assumption the formula to assume
    * @return the result of the satisfiability check.
    */
@@ -1418,9 +1418,9 @@ public class Solver implements IPointer
   /**
    * Check satisfiability assuming the given formulas.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( check-sat-assuming ( <prop_literal>+ ) )
-   * \endverbatim
+   * }
    * @param assumptions the formulas to assume
    * @return the result of the satisfiability check.
    */
@@ -1464,9 +1464,9 @@ public class Solver implements IPointer
   /**
    * Create datatype sort.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( declare-datatype <symbol> <datatype_decl> )
-   * \endverbatim
+   * }
    * @param symbol the name of the datatype sort
    * @param ctors the constructor declarations of the datatype sort
    * @return the datatype sort
@@ -1483,9 +1483,9 @@ public class Solver implements IPointer
   /**
    * Declare n-ary function symbol.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( declare-fun <symbol> ( <sort>* ) <sort> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param sorts the sorts of the parameters to this function
    * @param sort the sort of the return value of this function
@@ -1504,9 +1504,9 @@ public class Solver implements IPointer
   /**
    * Declare uninterpreted sort.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( declare-sort <symbol> <numeral> )
-   * \endverbatim
+   * }
    * @param symbol the name of the sort
    * @param arity the arity of the sort
    * @return the sort
@@ -1523,9 +1523,9 @@ public class Solver implements IPointer
   /**
    * Define n-ary function in the current context.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( define-fun <function_def> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param boundVars the parameters to this function
    * @param sort the sort of the return value of this function
@@ -1540,9 +1540,9 @@ public class Solver implements IPointer
   /**
    * Define n-ary function.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( define-fun <function_def> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param boundVars the parameters to this function
    * @param sort the sort of the return value of this function
@@ -1569,9 +1569,9 @@ public class Solver implements IPointer
   /**
    * Define n-ary function in the current context.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( define-fun <function_def> )
-   * \endverbatim
+   * }
    * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param boundVars the parameters to this function
@@ -1585,9 +1585,9 @@ public class Solver implements IPointer
   /**
    * Define n-ary function.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( define-fun <function_def> )
-   * \endverbatim
+   * }
    * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param boundVars the parameters to this function
@@ -1610,9 +1610,9 @@ public class Solver implements IPointer
   /**
    * Define recursive function in the current context.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( define-fun-rec <function_def> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param boundVars the parameters to this function
    * @param sort the sort of the return value of this function
@@ -1627,9 +1627,9 @@ public class Solver implements IPointer
   /**
    * Define recursive function.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( define-fun-rec <function_def> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param boundVars the parameters to this function
    * @param sort the sort of the return value of this function
@@ -1656,9 +1656,9 @@ public class Solver implements IPointer
   /**
    * Define recursive function in the current context.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( define-fun-rec <function_def> )
-   * \endverbatim
+   * }
    * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param boundVars the parameters to this function
@@ -1674,9 +1674,9 @@ public class Solver implements IPointer
   /**
    * Define recursive function.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( define-fun-rec <function_def> )
-   * \endverbatim
+   * }
    * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param boundVars the parameters to this function
@@ -1699,14 +1699,13 @@ public class Solver implements IPointer
   /**
    * Define recursive functions in the current context.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
-   * \endverbatim
+   * }
    * Create elements of parameter 'funs' with mkConst().
    * @param funs the sorted functions
    * @param boundVars the list of parameters to the functions
    * @param terms the list of function bodies of the functions
-   * @return the function
    */
   public void defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms)
   {
@@ -1715,16 +1714,15 @@ public class Solver implements IPointer
   /**
    * Define recursive functions.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
-   * \endverbatim
+   * }
    * Create elements of parameter 'funs' with mkConst().
    * @param funs the sorted functions
    * @param boundVars the list of parameters to the functions
    * @param terms the list of function bodies of the functions
    * @param global determines whether this definition is global (i.e. persists
    *               when popping the context)
-   * @return the function
    */
   public void defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms, boolean global)
   {
@@ -1743,9 +1741,9 @@ public class Solver implements IPointer
   /**
    * Echo a given string to the given output stream.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( echo <std::string> )
-   * \endverbatim
+   * }
    * @param out the output stream
    * @param str the string to echo
    */
@@ -1754,9 +1752,9 @@ public class Solver implements IPointer
   /**
    * Get the list of asserted formulas.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-assertions )
-   * \endverbatim
+   * }
    * @return the list of asserted formulas
    */
   public Term[] getAssertions()
@@ -1769,7 +1767,7 @@ public class Solver implements IPointer
 
   /**
    * Get info from the solver.
-   * SMT-LIB: \verbatim( get-info <info_flag> )\verbatim
+   * SMT-LIB: {@code ( get-info <info_flag> ) }
    * @return the info
    */
   public String getInfo(String flag)
@@ -1782,9 +1780,9 @@ public class Solver implements IPointer
   /**
    * Get the value of a given option.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-option <keyword> )
-   * \endverbatim
+   * }
    * @param option the option for which the value is queried
    * @return a string representation of the option value
    */
@@ -1798,9 +1796,9 @@ public class Solver implements IPointer
   /**
    * Get the set of unsat ("failed") assumptions.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-unsat-assumptions )
-   * \endverbatim
+   * }
    * Requires to enable option 'produce-unsat-assumptions'.
    * @return the set of unsat assumptions.
    */
@@ -1815,9 +1813,9 @@ public class Solver implements IPointer
   /**
    * Get the unsatisfiable core.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-unsat-core )
-   * \endverbatim
+   * }
    * Requires to enable option 'produce-unsat-cores'.
    * @return a set of terms representing the unsatisfiable core
    */
@@ -1832,9 +1830,9 @@ public class Solver implements IPointer
   /**
    * Get the value of the given term.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-value ( <term> ) )
-   * \endverbatim
+   * }
    * @param term the term for which the value is queried
    * @return the value of the given term
    */
@@ -1849,9 +1847,9 @@ public class Solver implements IPointer
   /**
    * Get the values of the given terms.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-value ( <term>+ ) )
-   * \endverbatim
+   * }
    * @param terms the terms for which the value is queried
    * @return the values of the given terms
    */
@@ -1883,9 +1881,9 @@ public class Solver implements IPointer
   /**
    * Get the model
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-model )
-   * \endverbatim
+   * }
    * Requires to enable option 'produce-models'.
    * @param sorts The list of uninterpreted sorts that should be printed in the
    * model.
@@ -1905,9 +1903,9 @@ public class Solver implements IPointer
   /**
    * Do quantifier elimination.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-qe <q> )
-   * \endverbatim
+   * }
    * Requires a logic that supports quantifier elimination. Currently, the only
    * logics supported by quantifier elimination is LRA and LIA.
    * @param q a quantified formula of the form:
@@ -1931,9 +1929,9 @@ public class Solver implements IPointer
    * Do partial quantifier elimination, which can be used for incrementally
    * computing the result of a quantifier elimination.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-qe-disjunct <q> )
-   * \endverbatim
+   * }
    * Requires a logic that supports quantifier elimination. Currently, the only
    * logics supported by quantifier elimination is LRA and LIA.
    * @param q a quantified formula of the form:
@@ -1941,16 +1939,16 @@ public class Solver implements IPointer
    * where P( x1...xn, y1...yn ) is a quantifier-free formula
    * @return a formula ret such that, given the current set of formulas A
    * asserted to this solver:
-   *   - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
+   *   - {@code (A ^ q) => (A ^ ret)} if Q is forall or {@code (A ^ ret) => (A ^ q)} if Q is
    *     exists,
    *   - ret is quantifier-free formula containing only free variables in
    *     y1...yn,
    *   - If Q is exists, let A^Q_n be the formula
-   *       A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
+   *       {@code A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n}
    *     where for each i=1,...n, formula ret^Q_i is the result of calling
    *     getQuantifierEliminationDisjunct for q with the set of assertions
-   *     A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
-   *       A ^ ret^Q_1 ^ ... ^ ret^Q_n
+   *     {@code A^Q_{i-1}}. Similarly, if Q is forall, then let {@code A^Q_n} be
+   *       {@code A ^ ret^Q_1 ^ ... ^ ret^Q_n }
    *     where ret^Q_i is the same as above. In either case, we have
    *     that ret^Q_j will eventually be true or false, for some finite j.
    */
@@ -2004,9 +2002,9 @@ public class Solver implements IPointer
   /**
    * Pop a level from the assertion stack.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( pop <numeral> )
-   * \endverbatim
+   * }
    */
   public void pop() throws CVC5ApiException
   {
@@ -2016,9 +2014,9 @@ public class Solver implements IPointer
   /**
    * Pop (a) level(s) from the assertion stack.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( pop <numeral> )
-   * \endverbatim
+   * }
    * @param nscopes the number of levels to pop
    */
   public void pop(int nscopes) throws CVC5ApiException
@@ -2032,12 +2030,12 @@ public class Solver implements IPointer
   /**
    * Get an interpolant
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-interpol <conj> )
-   * \endverbatim
+   * }
    * Requires to enable option 'produce-interpols'.
    * @param conj the conjecture term
-   * @param output a Term I such that A->I and I->B are valid, where A is the
+   * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
    *        current set of assertions and B is given in the input by conj.
    * @return true if it gets I successfully, false otherwise.
    */
@@ -2051,13 +2049,13 @@ public class Solver implements IPointer
   /**
    * Get an interpolant
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-interpol <conj> <g> )
-   * \endverbatim
+   * }
    * Requires to enable option 'produce-interpols'.
    * @param conj the conjecture term
    * @param grammar the grammar for the interpolant I
-   * @param output a Term I such that A->I and I->B are valid, where A is the
+   * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
    *        current set of assertions and B is given in the input by conj.
    * @return true if it gets I successfully, false otherwise.
    */
@@ -2072,9 +2070,9 @@ public class Solver implements IPointer
   /**
    * Get an abduct.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-abduct <conj> )
-   * \endverbatim
+   * }
    * Requires enabling option 'produce-abducts'
    * @param conj the conjecture term
    * @param output a term C such that A^C is satisfiable, and A^~B^C is
@@ -2091,9 +2089,9 @@ public class Solver implements IPointer
   /**
    * Get an abduct.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( get-abduct <conj> <g> )
-   * \endverbatim
+   * }
    * Requires enabling option 'produce-abducts'
    * @param conj the conjecture term
    * @param grammar the grammar for the abduct C
@@ -2114,9 +2112,9 @@ public class Solver implements IPointer
    * Block the current model. Can be called only if immediately preceded by a
    * SAT or INVALID query.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( block-model )
-   * \endverbatim
+   * }
    * Requires enabling 'produce-models' option and setting 'block-models' option
    * to a mode other than "none".
    */
@@ -2131,9 +2129,9 @@ public class Solver implements IPointer
    * Block the current model values of (at least) the values in terms. Can be
    * called only if immediately preceded by a SAT or NOT_ENTAILED query.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( block-model-values ( <terms>+ ) )
-   * \endverbatim
+   * }
    * Requires enabling 'produce-models' option and setting 'block-models' option
    * to a mode other than "none".
    */
@@ -2154,9 +2152,9 @@ public class Solver implements IPointer
   /**
    * Push a level to the assertion stack.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( push <numeral> )
-   * \endverbatim
+   * }
    */
   public void push() throws CVC5ApiException
   {
@@ -2166,9 +2164,9 @@ public class Solver implements IPointer
   /**
    * Push (a) level(s) to the assertion stack.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( push <numeral> )
-   * \endverbatim
+   * }
    * @param nscopes the number of levels to push
    */
   public void push(int nscopes) throws CVC5ApiException
@@ -2182,9 +2180,9 @@ public class Solver implements IPointer
   /**
    * Remove all assertions.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( reset-assertions )
-   * \endverbatim
+   * }
    */
   public void resetAssertions()
   {
@@ -2196,9 +2194,9 @@ public class Solver implements IPointer
   /**
    * Set info.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( set-info <attribute> )
-   * \endverbatim
+   * }
    * @param keyword the info flag
    * @param value the value of the info flag
    */
@@ -2212,9 +2210,9 @@ public class Solver implements IPointer
   /**
    * Set logic.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    * ( set-logic <symbol> )
-   * \endverbatim
+   * }
    * @param logic the logic to set
    */
   public void setLogic(String logic) throws CVC5ApiException
@@ -2227,9 +2225,9 @@ public class Solver implements IPointer
   /**
    * Set option.
    * SMT-LIB:
-   * \verbatim
+   * {@code
    *   ( set-option <option> )
-   * \endverbatim
+   * }
    * @param option the option name
    * @param value the option value
    */
@@ -2268,9 +2266,9 @@ public class Solver implements IPointer
   /**
    * Append \p symbol to the current list of universal variables.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( declare-var <symbol> <sort> )
-   * \endverbatim
+   * }
    * @param sort the sort of the universal variable
    * @param symbol the name of the universal variable
    * @return the universal variable
@@ -2305,9 +2303,9 @@ public class Solver implements IPointer
   /**
    * Synthesize n-ary function.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( synth-fun <symbol> ( <boundVars>* ) <sort> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param boundVars the parameters to this function
    * @param sort the sort of the return value of this function
@@ -2326,9 +2324,9 @@ public class Solver implements IPointer
   /**
    * Synthesize n-ary function following specified syntactic constraints.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
-   * \endverbatim
+   * }
    * @param symbol the name of the function
    * @param boundVars the parameters to this function
    * @param sort the sort of the return value of this function
@@ -2349,9 +2347,9 @@ public class Solver implements IPointer
   /**
    * Synthesize invariant.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( synth-inv <symbol> ( <boundVars>* ) )
-   * \endverbatim
+   * }
    * @param symbol the name of the invariant
    * @param boundVars the parameters to this invariant
    * @return the invariant
@@ -2368,9 +2366,9 @@ public class Solver implements IPointer
   /**
    * Synthesize invariant following specified syntactic constraints.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( synth-inv <symbol> ( <boundVars>* ) <g> )
-   * \endverbatim
+   * }
    * @param symbol the name of the invariant
    * @param boundVars the parameters to this invariant
    * @param grammar the syntactic constraints
@@ -2389,9 +2387,9 @@ public class Solver implements IPointer
   /**
    * Add a forumla to the set of Sygus constraints.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( constraint <term> )
-   * \endverbatim
+   * }
    * @param term the formula to add as a constraint
    */
   public void addSygusConstraint(Term term)
@@ -2404,9 +2402,9 @@ public class Solver implements IPointer
    * Add a set of Sygus constraints to the current state that correspond to an
    * invariant synthesis problem.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( inv-constraint <inv> <pre> <trans> <post> )
-   * \endverbatim
+   * }
    * @param inv the function-to-synthesize
    * @param pre the pre-condition
    * @param trans the transition relation
@@ -2426,9 +2424,9 @@ public class Solver implements IPointer
    * current list of functions-to-synthesize, universal variables and
    * constraints.
    * SyGuS v2:
-   * \verbatim
+   * {@code
    *   ( check-synth )
-   * \endverbatim
+   * }
    * @return the result of the synthesis conjecture.
    */
   public Result checkSynth()
diff --git a/src/api/java/cvc5/Stat.java b/src/api/java/cvc5/Stat.java
index 00ea50797..ee7d2095a 100644
--- a/src/api/java/cvc5/Stat.java
+++ b/src/api/java/cvc5/Stat.java
@@ -19,12 +19,12 @@ import java.util.Map;
 
 /**
  * Represents a snapshot of a single statistic value.
- * A value can be of type `long`, `double`, `String` or a histogram
- * (`Map<String, Long>`).
- * The value type can be queried (using `isInt()`, `isDouble()`, etc.) and
- * the stored value can be accessed (using `getInt()`, `getDouble()`, etc.).
+ * A value can be of type {@code long}, {@code double}, {@code String} or a histogram
+ * ({@code Map<String, Long>}).
+ * The value type can be queried (using {@code isInt()}, {@code isDouble()}, etc.) and
+ * the stored value can be accessed (using {@code getInt()}, {@code getDouble()}, etc.).
  * It is possible to query whether this statistic is an expert statistic by
- * `isExpert()` and whether its value is the default value by `isDefault()`.
+ * {@code isExpert()} and whether its value is the default value by {@code isDefault()}.
  */
 public class Stat extends AbstractPointer
 {