/**
* 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,
/**
* (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``
* - Create Op of this kind with:
*
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) 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,
* 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
/**
* 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,
*
* \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<lbl-option-arrays-exp>`.
* \endrst
*
* - Arity: ``4``
* \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<lbl-option-arrays-exp>`.
* \endrst
*/
EQ_RANGE,
/**
* Datatype selector application.
*
- * \rst
- * .. note:: Undefined if misapplied.
- * \endrst
- *
* - Arity: ``2``
*
* - ``1:`` DatatypeSelector Term (see DatatypeSelector::getTerm() const)
* - Create Op of this kind with:
*
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. note:: Undefined if misapplied.
+ * \endrst
*/
APPLY_SELECTOR,
/**
/**
* Datatype update application.
*
- * \rst
- * .. note:: Does not change the datatype argument if misapplied.
- * \endrst
- *
* - Arity: ``3``
*
* - ``1:`` Datatype updater Term (see DatatypeSelector::getUpdaterTerm() const)
* - Create Op of this kind with:
*
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. note:: Does not change the datatype argument if misapplied.
+ * \endrst
*/
APPLY_UPDATER,
/**
*
* 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,
/**
/**
* 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<Term>&) const
* 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
* - Create Op of this kind with:
*
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. note:: Should only be used as a child of
+ * :cpp:enumerator:`INST_PATTERN_LIST`.
+ * \endrst
*/
INST_PATTERN,
/**
* 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
* - Create Op of this kind with:
*
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. note:: Should only be used as a child of
+ * :cpp:enumerator:`INST_PATTERN_LIST`.
+ * \endrst
*/
INST_NO_PATTERN,
/**
*
* 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<Term>&) const
*
* \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.
* \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.
* \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,
* 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:
*
* - Create Op of this kind with:
*
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. note:: Should only be used as a child of
+ * :cpp:enumerator:`INST_PATTERN_LIST`.
+ * \endrst
*/
INST_ATTRIBUTE,
/**
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>": "int[]",
r"std::vector<Term>": "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></li>')
+ ul_open -= 1
+ lines.append(' * </ul>')
+ ul_open -= 1
+ ul_open += 2
+ lines.append(' * <ul>')
+ lines.append(' * <li>{}'.format(l.strip()[2:]))
+ lines.append(' * <ul>')
+ elif l.strip().startswith('- '):
+ if not ul_open:
+ lines.append(' * <ul>')
+ ul_open += 1
+ lines.append(' * <li>{}</li>'.format(l.strip()[2:]))
+ elif ul_open > 0 and l.strip() and not l.strip().startswith('- '):
+ if ul_open == 2:
+ lines.append(' * </ul></li>')
+ ul_open -= 1
+ lines.append(' * </ul>')
+ 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
projects / cvc5.git / commitdiff