From 2e2d6b623c919e086a53fddfbcece9c22d50f5b3 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 1 Apr 2022 04:33:14 -0500 Subject: [PATCH] Fix javadoc custom tag warning (#8502) Fix this warning Note: Custom tags that could override future standard tags: @apiNote. To avoid potential overrides, use at least one period character (.) in custom tag names. --- docs/api/java/CMakeLists.txt | 2 +- src/api/java/io/github/cvc5/Datatype.java | 6 +- .../io/github/cvc5/DatatypeConstructor.java | 2 +- src/api/java/io/github/cvc5/Solver.java | 66 +++++++++---------- src/api/java/io/github/cvc5/Sort.java | 8 +-- src/api/java/io/github/cvc5/Term.java | 6 +- 6 files changed, 45 insertions(+), 45 deletions(-) diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index def6524be..8150deff3 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -31,7 +31,7 @@ if(BUILD_BINDINGS_JAVA) -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/:${CMAKE_BINARY_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} -cp ${CVC5_JAR_FILE} - -tag "apiNote:a:Note:" + -tag "api.note:a:Note:" -notimestamp COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's///' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete diff --git a/src/api/java/io/github/cvc5/Datatype.java b/src/api/java/io/github/cvc5/Datatype.java index 677ae7909..cfe0614ef 100644 --- a/src/api/java/io/github/cvc5/Datatype.java +++ b/src/api/java/io/github/cvc5/Datatype.java @@ -111,7 +111,7 @@ public class Datatype extends AbstractPointer implements Iterable ) * } * - * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and + * @api.note This corresponds to mkUninterpretedSort() const if arity = 0, and * to mkUninterpretedSortConstructorSort() const if arity > 0. * * @param symbol the name of the sort @@ -1830,7 +1830,7 @@ public class Solver implements IPointer, AutoCloseable * ( get-learned-literals ) * } * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return the list of learned literals */ @@ -1936,7 +1936,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires to enable option 'produce-unsat-cores'. * - * @apiNote In contrast to SMT-LIB, the API does not distinguish between + * @api.note In contrast to SMT-LIB, the API does not distinguish between * named and unnamed assertions when producing an unsatisfiable * core. Additionally, the API allows this option to be called after * a check with assumptions. A subset of those assumptions may be @@ -1956,7 +1956,7 @@ public class Solver implements IPointer, AutoCloseable * Get a difficulty estimate for an asserted formula. This method is * intended to be called immediately after any response to a checkSat. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return a map from (a subset of) the input assertions to a real value that * is an estimate of how difficult each assertion was to solve. Unmentioned @@ -1985,7 +1985,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires to enable option 'produce-proofs'. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return a string representing the proof, according to the value of * proof-format-mode. @@ -2054,7 +2054,7 @@ public class Solver implements IPointer, AutoCloseable * current model. This method will only return false (for any v) if * the model-cores option has been set. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param v The term in question * @return true if v is a model core symbol @@ -2074,7 +2074,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires to enable option 'produce-models'. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param sorts The list of uninterpreted sorts that should be printed in the * model. @@ -2100,7 +2100,7 @@ public class Solver implements IPointer, AutoCloseable * Quantifier Elimination is is only complete for logics such as LRA, * LIA and BV. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param q a quantified formula of the form: * Q x1...xn. P( x1...xn, y1...yn ) @@ -2129,7 +2129,7 @@ public class Solver implements IPointer, AutoCloseable * Quantifier Elimination is is only complete for logics such as LRA, * LIA and BV. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param q a quantified formula of the form: * Q x1...xn. P( x1...xn, y1...yn ) @@ -2162,7 +2162,7 @@ public class Solver implements IPointer, AutoCloseable * datatype sort to the given ones. This method should be invoked exactly * once, before any separation logic constraints are provided. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param locSort The location sort of the heap * @param dataSort The data sort of the heap @@ -2177,7 +2177,7 @@ public class Solver implements IPointer, AutoCloseable /** * When using separation logic, obtain the term for the heap. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return The term for the heap */ @@ -2192,7 +2192,7 @@ public class Solver implements IPointer, AutoCloseable /** * When using separation logic, obtain the term for nil. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return The term for nil */ @@ -2211,7 +2211,7 @@ public class Solver implements IPointer, AutoCloseable * ( declare-pool ( * ) ) * } * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param symbol The name of the pool * @param sort The sort of the elements of the pool. @@ -2265,7 +2265,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires 'produce-interpolants' to be set to a mode different from 'none'. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param conj the conjecture term * @return a Term I such that {@code A->I} and {@code I->B} are valid, where @@ -2288,7 +2288,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires 'produce-interpolants' to be set to a mode different from 'none'. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param conj the conjecture term * @param grammar the grammar for the interpolant I @@ -2321,7 +2321,7 @@ public class Solver implements IPointer, AutoCloseable * set to a mode different from 'none'. * \endverbatim * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return 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 @@ -2344,7 +2344,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires enabling option 'produce-abducts' * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param conj the conjecture term * @return a term C such that A^C is satisfiable, and A^~B^C is @@ -2367,7 +2367,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires enabling option 'produce-abducts' * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param conj the conjecture term * @param grammar the grammar for the abduct C @@ -2394,7 +2394,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires enabling incremental mode and option 'produce-abducts' * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is @@ -2419,7 +2419,7 @@ public class Solver implements IPointer, AutoCloseable * Requires enabling 'produce-models' option and setting 'block-models' option * to a mode other than "none". * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. */ public void blockModel() { @@ -2437,7 +2437,7 @@ public class Solver implements IPointer, AutoCloseable * } * Requires enabling 'produce-models' option. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. */ public void blockModelValues(Term[] terms) { @@ -2451,7 +2451,7 @@ public class Solver implements IPointer, AutoCloseable * Return a string that contains information about all instantiations made by * the quantifiers module. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. */ public String getInstantiations() { diff --git a/src/api/java/io/github/cvc5/Sort.java b/src/api/java/io/github/cvc5/Sort.java index 64fcbb56b..65ff8e49d 100644 --- a/src/api/java/io/github/cvc5/Sort.java +++ b/src/api/java/io/github/cvc5/Sort.java @@ -283,7 +283,7 @@ public class Sort extends AbstractPointer implements Comparable /** * Is this a record sort? * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @return true if the sort is a record sort */ @@ -426,7 +426,7 @@ public class Sort extends AbstractPointer implements Comparable * * Create sorts parameter with Solver.mkParamSort(). * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param params the list of sort parameters to instantiate with */ @@ -461,7 +461,7 @@ public class Sort extends AbstractPointer implements Comparable * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param sort the subsort to be substituted within this sort. * @param replacement the sort replacing the substituted subsort. @@ -486,7 +486,7 @@ public class Sort extends AbstractPointer implements Comparable * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will * return (Array (Array C D) B). * - * @apiNote This method is experimental and may change in future versions. + * @api.note This method is experimental and may change in future versions. * * @param sorts the subsorts to be substituted within this sort. * @param replacements the sort replacing the substituted subsorts. diff --git a/src/api/java/io/github/cvc5/Term.java b/src/api/java/io/github/cvc5/Term.java index 46363251f..a0a0620ac 100644 --- a/src/api/java/io/github/cvc5/Term.java +++ b/src/api/java/io/github/cvc5/Term.java @@ -202,7 +202,7 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * @return the Op used to create this term - * @apiNote This is safe to call when hasOp() returns true. + * @api.note This is safe to call when hasOp() returns true. */ public Op getOp() { @@ -395,7 +395,7 @@ public class Term extends AbstractPointer implements Comparable, Iterable< * * Asserts isString(). * - * @apiNote This method is not to be confused with toString() which returns + * @api.note This method is not to be confused with toString() which returns * the term in some string representation, whatever data it may hold. */ public String getStringValue() @@ -671,7 +671,7 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * Asserts isSequenceValue(). - * @apiNote It is usually necessary for sequences to call + * @api.note It is usually necessary for sequences to call * `Solver::simplify()` to turn a sequence that is constructed by, * e.g., concatenation of unit sequences, into a sequence value. * @return the representation of a sequence value as a vector of terms. -- 2.30.2