Skip to content

Commit

Permalink
update input for doxygen #5400
Browse files Browse the repository at this point in the history
  • Loading branch information
NikolajBjorner committed Dec 5, 2021
1 parent c845b22 commit 0d055b8
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 10 deletions.
13 changes: 6 additions & 7 deletions src/api/java/Context.java
Original file line number Diff line number Diff line change
Expand Up @@ -1717,9 +1717,8 @@ public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(String name
* {@code [domain -> range]}, and {@code i} must have the sort
* {@code domain}. The sort of the result is {@code range}.
*
* @see #mkArraySort
* @see #mkArraySort(Sort[], Sort)
* @see #mkStore
**/
public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
{
Expand All @@ -1740,7 +1739,7 @@ public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a
* {@code [domains -> range]}, and {@code args} must have the sorts
* {@code domains}. The sort of the result is {@code range}.
*
* @see #mkArraySort
* @see #mkArraySort(Sort[], Sort)
* @see #mkStore
**/
public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
Expand All @@ -1764,7 +1763,7 @@ public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] a
* {@code select}) on all indices except for {@code i}, where it
* maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code i} may be a different value).
* @see #mkArraySort
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
**/
Expand All @@ -1789,7 +1788,7 @@ public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore(Expr<ArraySort<D
* {@code select}) on all indices except for {@code args}, where it
* maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code args} may be a different value).
* @see #mkArraySort
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
**/
Expand All @@ -1807,7 +1806,7 @@ public <R extends Sort> ArrayExpr<Sort, R> mkStore(Expr<ArraySort<Sort, R>> a, E
* Remarks: The resulting term is an array, such
* that a {@code select} on an arbitrary index produces the value
* {@code v}.
* @see #mkArraySort
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
*
**/
Expand All @@ -1827,7 +1826,7 @@ public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray(D domain, E
* {@code f} must have type {@code range_1 .. range_n -> range}.
* {@code v} must have sort range. The sort of the result is
* {@code [domain_i -> range]}.
* @see #mkArraySort
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
* @see #mkStore
Expand Down
6 changes: 3 additions & 3 deletions src/api/z3_api.h
Original file line number Diff line number Diff line change
Expand Up @@ -3488,8 +3488,8 @@ extern "C" {
\brief Create a string constant out of the string that is passed in
The string may contain escape encoding for non-printable characters
or characters outside of the basic printable ASCII range. For example,
the escape encoding \u{0} represents the character 0 and the encoding
\u{100} represents the character 256.
the escape encoding \\u{0} represents the character 0 and the encoding
\\u{100} represents the character 256.
def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING)))
*/
Expand All @@ -3499,7 +3499,7 @@ extern "C" {
\brief Create a string constant out of the string that is passed in
It takes the length of the string as well to take into account
0 characters. The string is treated as if it is unescaped so a sequence
of characters \u{0} is treated as 5 characters and not the character 0.
of characters \\u{0} is treated as 5 characters and not the character 0.
def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING)))
*/
Expand Down

0 comments on commit 0d055b8

Please sign in to comment.