From a1d6139547f49cf939494c56cd69396b517bff19 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 5 Apr 2022 16:55:47 -0700 Subject: [PATCH] api: Fix doc generation for kinds in java API. (#8576) Plus some more fixes for docs. --- src/api/cpp/cvc5_kind.h | 146 ++++++++++++------------ src/api/java/genenums.py.in | 83 ++++++++------ src/api/java/io/github/cvc5/Solver.java | 2 +- src/api/python/cvc5.pxi | 2 + src/options/mkoptions.py | 2 +- src/proof/proof_rule.h | 2 +- 6 files changed, 122 insertions(+), 115 deletions(-) diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index a9912f6b3..e1ba67405 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -123,27 +123,27 @@ enum Kind : int32_t /** * Free constant symbol. * - * \rst - * .. note:: Not permitted in bindings (e.g., :cpp:enumerator:`FORALL`, - * :cpp:enumerator:`EXISTS`). - * \endrst - * * - Create Term of this Kind with: * * - Solver::mkConst(const Sort&, const std::string&) const * - Solver::mkConst(const Sort&) const + * + * \rst + * .. note:: Not permitted in bindings (e.g., :cpp:enumerator:`FORALL`, + * :cpp:enumerator:`EXISTS`). + * \endrst */ CONSTANT, /** * (Bound) variable. * - * \rst - * .. note:: Only permitted in bindings and in lambda and quantifier bodies. - * \endrst - * * - Create Term of this Kind with: * * - Solver::mkVar(const Sort&, const std::string&) const + * + * \rst + * .. note:: Only permitted in bindings and in lambda and quantifier bodies. + * \endrst */ VARIABLE, /** @@ -219,19 +219,6 @@ enum Kind : int32_t * (witness ((x Int)) F) * (witness ((x Int)) F)) * - * .. note:: - * - * This kind is primarily used internally, but may be returned in - * models (e.g., for arithmetic terms in non-linear queries). However, - * it is not supported by the parser. Moreover, the user of the API - * should be cautious when using this operator. In general, all witness - * terms ``(witness ((x Int)) F)`` should be such that ``(exists ((x Int)) - * F)`` is a valid formula. If this is not the case, then the semantics - * in formulas that use witness terms may be unintuitive. For example, - * the following formula is unsatisfiable: - * ``(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) - * false) 0))``, whereas notice that ``(or (= z 0) (not (= z 0)))`` is - * true for any :math:`z`. * \endrst * * - Arity: ``3`` @@ -248,6 +235,22 @@ enum Kind : int32_t * - Create Op of this kind with: * * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. note:: + * + * This kind is primarily used internally, but may be returned in + * models (e.g., for arithmetic terms in non-linear queries). However, + * it is not supported by the parser. Moreover, the user of the API + * should be cautious when using this operator. In general, all witness + * terms ``(witness ((x Int)) F)`` should be such that ``(exists ((x Int)) + * F)`` is a valid formula. If this is not the case, then the semantics + * in formulas that use witness terms may be unintuitive. For example, + * the following formula is unsatisfiable: + * ``(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) + * false) 0))``, whereas notice that ``(or (= z 0) (not (= z 0)))`` is + * true for any :math:`z`. + * \endrst */ WITNESS, @@ -396,8 +399,6 @@ enum Kind : int32_t * uinterpreted Sort :math:`S` is less than or equal to an upper bound. * \endrst * - * - Arity: ``0`` - * * - Create Term of this Kind with: * * - Solver::mkCardinalityConstraint(const Sort&, uint32_t) const @@ -1035,15 +1036,15 @@ enum Kind : int32_t /** * Pi constant. * + * - Create Term of this Kind with: + * + * - Solver::mkPi() const + * * \rst * .. note:: :cpp:enumerator:`PI` is considered a special symbol of Sort * Real, but is not a Real value, i.e., * :cpp:func:`Term::isRealValue()` will return ``false``. * \endrst - * - * - Create Term of this Kind with: - * - * - Solver::mkPi() const */ PI, @@ -2499,10 +2500,6 @@ enum Kind : int32_t * * \forall k . i \leq k \leq j \Rightarrow a[k] = b[k] * - * .. note:: We currently support the creation of array equalities over index - * Sorts bit-vector, floating-point, Int and Real. - * Requires to enable option - * :ref:`arrays-exp`. * \endrst * * - Arity: ``4`` @@ -2524,6 +2521,11 @@ enum Kind : int32_t * \rst * .. warning:: This kind is experimental and may be changed or removed in * future versions. + * + * .. note:: We currently support the creation of array equalities over index + * Sorts bit-vector, floating-point, Int and Real. + * Requires to enable option + * :ref:`arrays-exp`. * \endrst */ EQ_RANGE, @@ -2551,10 +2553,6 @@ enum Kind : int32_t /** * Datatype selector application. * - * \rst - * .. note:: Undefined if misapplied. - * \endrst - * * - Arity: ``2`` * * - ``1:`` DatatypeSelector Term (see DatatypeSelector::getTerm() const) @@ -2568,6 +2566,10 @@ enum Kind : int32_t * - Create Op of this kind with: * * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. note:: Undefined if misapplied. + * \endrst */ APPLY_SELECTOR, /** @@ -2591,10 +2593,6 @@ enum Kind : int32_t /** * Datatype update application. * - * \rst - * .. note:: Does not change the datatype argument if misapplied. - * \endrst - * * - Arity: ``3`` * * - ``1:`` Datatype updater Term (see DatatypeSelector::getUpdaterTerm() const) @@ -2609,6 +2607,10 @@ enum Kind : int32_t * - Create Op of this kind with: * * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. note:: Does not change the datatype argument if misapplied. + * \endrst */ APPLY_UPDATER, /** @@ -3021,15 +3023,15 @@ enum Kind : int32_t * * All set variables must be interpreted as subsets of it. * + * - Create Term of this Kind with: + * + * - Solver::mkUniverseSet(const Sort&) const + * * \rst * .. note:: :cpp:enumerator:`SET_UNIVERSE` is considered a special symbol of * the theory of sets and is not considered as a set value, i.e., * Term::isSetValue() will return ``false``. * \endrst - * - * - Create Op of this kind with: - * - * - Solver::mkUniverseSet(const Sort&) const */ SET_UNIVERSE, /** @@ -3391,7 +3393,7 @@ enum Kind : int32_t /** * Bag element multiplicity. * - * Create with: + * - Create Term of this Kind with: * * - Solver::mkTerm(Kind, const Term&, const Term&) const * - Solver::mkTerm(Kind, const std::vector&) const @@ -4897,11 +4899,6 @@ enum Kind : int32_t * Specifies a (list of) terms to be used as a pattern for quantifier * instantiation. * - * \rst - * .. note:: Should only be used as a child of - * :cpp:enumerator:`INST_PATTERN_LIST`. - * \endrst - * * - Arity: ``n > 0`` * * - ``1..n:`` Terms of any Sort @@ -4914,6 +4911,11 @@ enum Kind : int32_t * - Create Op of this kind with: * * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst */ INST_PATTERN, /** @@ -4922,11 +4924,6 @@ enum Kind : int32_t * Specifies a (list of) terms that should not be used as a pattern for * quantifier instantiation. * - * \rst - * .. note:: Should only be used as a child of - * :cpp:enumerator:`INST_PATTERN_LIST`. - * \endrst - * * - Arity: ``n > 0`` * * - ``1..n:`` Terms of any Sort @@ -4939,6 +4936,11 @@ enum Kind : int32_t * - Create Op of this kind with: * * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst */ INST_NO_PATTERN, /** @@ -4946,11 +4948,6 @@ enum Kind : int32_t * * Specifies an annotation for pool based instantiation. * - * \rst - * .. note:: Should only be used as a child of - * :cpp:enumerator:`INST_PATTERN_LIST`. - * \endrst - * * In detail, pool symbols can be declared via the method * - Solver::declarePool(const std::string&, const Sort&, const std::vector&) const * @@ -4987,17 +4984,15 @@ enum Kind : int32_t * \rst * .. warning:: This kind is experimental and may be changed or removed in * future versions. + * + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. * \endrst */ INST_POOL, /** * A instantantiation-add-to-pool annotation. * - * \rst - * .. note:: Should only be used as a child of - * :cpp:enumerator:`INST_PATTERN_LIST`. - * \endrst - * * An instantantiation-add-to-pool annotation indicates that when a quantified * formula is instantiated, the instantiated version of a term should be * added to the given pool. @@ -5032,17 +5027,15 @@ enum Kind : int32_t * \rst * .. warning:: This kind is experimental and may be changed or removed in * future versions. + * + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. * \endrst */ INST_ADD_TO_POOL, /** * A skolemization-add-to-pool annotation. * - * \rst - * .. note:: Should only be used as a child of - * :cpp:enumerator:`INST_PATTERN_LIST`. - * \endrst - * * An skolemization-add-to-pool annotation indicates that when a quantified * formula is skolemized, the skolemized version of a term should be added to * the given pool. @@ -5077,6 +5070,9 @@ enum Kind : int32_t * \rst * .. warning:: This kind is experimental and may be changed or removed in * future versions. + * + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. * \endrst */ SKOLEM_ADD_TO_POOL, @@ -5086,15 +5082,10 @@ enum Kind : int32_t * Specifies a custom property for a quantified formula given by a * term that is ascribed a user attribute. * - * \rst - * .. note:: Should only be used as a child of - * :cpp:enumerator:`INST_PATTERN_LIST`. - * * - Arity: ``n > 0`` * * - ``1:`` Term of Kind :cpp:enumerator:`CONST_STRING` (the keyword of the attribute) * - ``2...n:`` Terms representing the values of the attribute - * \endrst * * - Create Term of this Kind with: * @@ -5104,6 +5095,11 @@ enum Kind : int32_t * - Create Op of this kind with: * * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst */ INST_ATTRIBUTE, /** diff --git a/src/api/java/genenums.py.in b/src/api/java/genenums.py.in index 6d5777c2a..62f9c9277 100644 --- a/src/api/java/genenums.py.in +++ b/src/api/java/genenums.py.in @@ -97,64 +97,73 @@ ENUM_JAVA_BOTTOM = \ CPP_JAVA_MAPPING = \ { r"\bbool\b": "boolean", - r"\bconst\b\s?": "", + r"\bconst\b ?": "", r"\bint32_t\b": "int", r"\bint64_t\b": "long", r"\buint32_t\b": "int", r"\buint64_t\b": "long", r"\bunsigned char\b": "byte", r"cvc5::": "cvc5.", - r"Term::Term\(\)": "{@link Solver#getNullTerm()", - r"Term::": "{@link Term#", - r"Solver::": "{@link Solver#", - r"Datatype::": "{@link Datatype#", - r"DatatypeConstructor::": "{@link DatatypeConstructor#", - r"DatatypeConstructorDecl::": "{@link DatatypeConstructorDecl#", - r"DatatypeDecl::": "{@link DatatypeDecl#", - r"DatatypeSelector::": "{@link DatatypeSelector#", - r"Grammar::": "{@link Grammar#", - r"Op::": "{@link Op#", - r"OptionInfo::": "{@link OptionInfo#", - r"Result::": "{@link Result#", - r"Sort::": "{@link Sort#", - r"Stat::": "{@link Stat#", - r"Statistics::": "{@link Statistics#", - r"SynthResult::": "{@link SynthResult#", + r"Term::Term\(\)": "{@link Solver#getNullTerm()}", + r"([a-zA-Z]*)::(.*?\))": r"{@link \1#\2}", r"std::vector": "int[]", r"std::vector": "Term[]", r"std::string": "String", + r".. note::": "@api.note", + r".. warning::": "@api.note", r"&": "", r"::": ".", r">": ">", r"<": "<", - r"@f\[": "", - r"@f\]": "", - r"@note": "", + r"@note": "@api.note", + r"\\rst": "", + r"\\endrst": "", + r"``(.*?)``": r"{@code \1}", + r":cpp:[a-z]*:`(.*?)`": r"\1", + r":math:`(.*?)`": r"{@code \1}", + r"({@code.*)>": r"\1>", } +def format_list(comment): + lines = [] + ul_open = 0 + for line in comment.split('\n'): + l = line[4:] + if l.strip().startswith('- Arity') or l.strip().startswith('- Create'): + if ul_open > 0: + if ul_open == 2: + lines.append(' * ') + ul_open -= 1 + lines.append(' * ') + ul_open -= 1 + ul_open += 2 + lines.append(' *
    ') + lines.append(' *
  • {}'.format(l.strip()[2:])) + lines.append(' *
      ') + elif l.strip().startswith('- '): + if not ul_open: + lines.append(' *
        ') + ul_open += 1 + lines.append(' *
      • {}
        • '.format(l.strip()[2:])) + elif ul_open > 0 and l.strip() and not l.strip().startswith('- '): + if ul_open == 2: + lines.append(' *
      ') + ul_open -= 1 + lines.append(' *
    ') + lines.append(line) + ul_open -= 1 + else: + lines.append(line) + return '\n'.join(lines) # convert from c++ doc to java doc def format_comment(comment): for pattern, replacement in CPP_JAVA_MAPPING.items(): comment = re.sub(pattern, replacement, comment) - comment = """ /**\n{}\n */""".format(textwrap.indent(comment, ' * ')) - - # e.g. {@link Solver#mkBitVector(int, long) becomes {@link Solver#mkBitVector(int,long)} - def close_link(match): - link = match.group() - link = link.replace(" ", "") - link = link.replace("@link", "@link ") - if "}" in link: - return link - return "{0}}} ".format(link) - - # e.g. {@link Solver#mkBitVector(int, long) - function_pattern = re.compile(r"{@link (.*?\))") - comment = re.sub(function_pattern, close_link, comment) - # e.g. {@link BigInteger#Ten - field_pattern = re.compile(r"{@link [a-zA-Z.#]*\s") - comment = re.sub(field_pattern, close_link, comment) + comment = """ /**\n{}\n */""".format( + textwrap.indent(comment, ' * ', lambda line: True)) comment = comment.replace("- {@link Solver#mkString(std.wstring)}", "") + comment = format_list(comment) return comment diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index 06df020b5..a3fcb4ce4 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -651,7 +651,7 @@ public class Solver implements IPointer, AutoCloseable /** * Create an operator for a builtin Kind * The Kind may not be the Kind for an indexed operator - * (e.g. {@link Kind#BITVECTOR_EXTRACT}). + * (e.g., {@link Kind#BITVECTOR_EXTRACT}). * * @api.note In this case, the Op simply wraps the Kind. The Kind can be used * in mkTerm directly without creating an op first. diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index cfd150e43..4a344316c 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -3984,6 +3984,7 @@ cdef class Term: def getRoundingModeValue(self): """ .. note:: Asserts :py:meth:`isRoundingModeValue()`. + :return: The floating-point rounding mode value held by the term. """ return RoundingMode( self.cterm.getRoundingModeValue()) @@ -4030,6 +4031,7 @@ cdef class Term: def getBitVectorValue(self, base = 2): """ .. note:: Asserts :py:meth:`isBitVectorValue()`. + Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string). diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 2b6469ab8..e30f7093c 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -752,7 +752,7 @@ def _sphinx_help_render_option(res, opt): ''' res.append(desc) - res.append(' ' + opt.help) + res.append(' ' + opt.help.replace("*", "\\*")) if opt.mode: res.append(' ') diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index da0666710..7bfb389d5 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -518,7 +518,7 @@ enum class PfRule : uint32_t * - let :math:`C_1'` be equal, in its set representation, to :math:`C_1`, * - for each :math:`i > 1`, let :math:`C_i'` be equal, it its set * representation, to :math:`C_{i-1} \diamond{L_{i-1},\mathit{pol}_{i-1}} - * C_i'` + * C_i'` * * The result of the chain resolution is :math:`C`, which is equal, in its set * representation, to :math:`C_n'` -- 2.30.2