mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

update input for doxygen #5400

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-05 09:04:18 -08:00
parent c845b22c15
commit 0d055b83eb
2 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/api/java/Context.java
View file

@ -1717,9 +1717,8 @@ public class Context implements AutoCloseable {
* {@code [domain -> range]}, and {@code i} must have the sort * {@code [domain -> range]}, and {@code i} must have the sort
* {@code domain}. The sort of the result is {@code range}. * {@code domain}. The sort of the result is {@code range}.
* *
* @see #mkArraySort * @see #mkArraySort(Sort[], Sort)
* @see #mkStore * @see #mkStore
**/ **/
public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i) public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
{ {
@ -1740,7 +1739,7 @@ public class Context implements AutoCloseable {
* {@code [domains -> range]}, and {@code args} must have the sorts * {@code [domains -> range]}, and {@code args} must have the sorts
* {@code domains}. The sort of the result is {@code range}. * {@code domains}. The sort of the result is {@code range}.
* *
* @see #mkArraySort * @see #mkArraySort(Sort[], Sort)
* @see #mkStore * @see #mkStore
**/ **/
public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args) public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
@ -1764,7 +1763,7 @@ public class Context implements AutoCloseable {
* {@code select}) on all indices except for {@code i}, where it * {@code select}) on all indices except for {@code i}, where it
* maps to {@code v} (and the {@code select} of {@code a} * maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code i} may be a different value). * with respect to {@code i} may be a different value).
* @see #mkArraySort * @see #mkArraySort(Sort[], Sort)
* @see #mkSelect * @see #mkSelect
**/ **/
@ -1789,7 +1788,7 @@ public class Context implements AutoCloseable {
* {@code select}) on all indices except for {@code args}, where it * {@code select}) on all indices except for {@code args}, where it
* maps to {@code v} (and the {@code select} of {@code a} * maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code args} may be a different value). * with respect to {@code args} may be a different value).
* @see #mkArraySort * @see #mkArraySort(Sort[], Sort)
* @see #mkSelect * @see #mkSelect
**/ **/
@ -1807,7 +1806,7 @@ public class Context implements AutoCloseable {
* Remarks: The resulting term is an array, such * Remarks: The resulting term is an array, such
* that a {@code select} on an arbitrary index produces the value * that a {@code select} on an arbitrary index produces the value
* {@code v}. * {@code v}.
* @see #mkArraySort * @see #mkArraySort(Sort[], Sort)
* @see #mkSelect * @see #mkSelect
* *
**/ **/
@ -1827,7 +1826,7 @@ public class Context implements AutoCloseable {
* {@code f} must have type {@code range_1 .. range_n -> range}. * {@code f} must have type {@code range_1 .. range_n -> range}.
* {@code v} must have sort range. The sort of the result is * {@code v} must have sort range. The sort of the result is
* {@code [domain_i -> range]}. * {@code [domain_i -> range]}.
* @see #mkArraySort * @see #mkArraySort(Sort[], Sort)
* @see #mkSelect * @see #mkSelect
* @see #mkStore * @see #mkStore

6
src/api/z3_api.h
View file

@ -3488,8 +3488,8 @@ extern "C" {
\brief Create a string constant out of the string that is passed in \brief Create a string constant out of the string that is passed in
The string may contain escape encoding for non-printable characters The string may contain escape encoding for non-printable characters
or characters outside of the basic printable ASCII range. For example, or characters outside of the basic printable ASCII range. For example,
the escape encoding \u{0} represents the character 0 and the encoding the escape encoding \\u{0} represents the character 0 and the encoding
\u{100} represents the character 256. \\u{100} represents the character 256.
def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING))) def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING)))
*/ */
@ -3499,7 +3499,7 @@ extern "C" {
\brief Create a string constant out of the string that is passed in \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 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 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))) def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING)))
*/ */