Update datatypes.rst (#8009)

diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py
index 04c70133ee9c99528c6abf20fc8cd9c395a5285e..132b029f97ca6a4dfe60f5da73acb7415820407a 100644 (file)
--- a/docs/ext/smtliblexer.py
+++ b/docs/ext/smtliblexer.py
@@ -47,7 +47,7 @@ class SmtLibLexer(RegexLexer):
         '=>', '=', 'true', 'false', 'not', 'and', 'or', 'xor', 'distinct',
         'ite',
         # datatypes
-        'mkTuple', 'tupSel',
+        'tuple', 'tuple_select',
         # fp
         'RNE', 'RNA', 'RTP', 'RTN', 'RTZ', 'fp', 'NaN', 'fp\.abs', 'fp\.neg',
         'fp\.add', 'fp\.sub', 'fp\.mul', 'fp\.div', 'fp\.fma', 'fp\.sqrt',

diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst
index c9a15ad24e9222247e31ff32d3525b11e803cb6e..e99fff89557e49dd1ea175a28ac8c9416a3e53eb 100644 (file)
--- a/docs/theories/datatypes.rst
+++ b/docs/theories/datatypes.rst
@@ -145,8 +145,8 @@ For example:
 .. code:: smtlib
 
   (declare-const t (Tuple Int Int))
-  (assert (= ((_ tupSel 0) t) 3))
-  (assert (not (= t (mkTuple 3 4))))
+  (assert (= ((_ tuple_select 0) t) 3))
+  (assert (not (= t (tuple 3 4))))
 
 
 Codatatypes
@@ -183,11 +183,11 @@ a `cvc5::api::Solver solver` object.
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
 |                    | ``(declare-const t (Tuple Int Int))``  | ``Sort s_int = solver.getIntegerSort();``                                                                                       |
 |                    |                                        |                                                                                                                                 |
-|                    |                                        | ``Sort s = solver.mkTypleSort({s_int, s_int});``                                                                                |
+|                    |                                        | ``Sort s = solver.mkTupleSort({s_int, s_int});``                                                                                |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term t = solver.mkConst(s, "t");``                                                                                            |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
-| Tuple Constructor  | ``(mkTuple <Term_1>, ..., <Term_n>)``  | ``Sort s = solver.mkTypleSort(sorts);``                                                                                         |
+| Tuple Constructor  | ``(mkTuple <Term_1>, ..., <Term_n>)``  | ``Sort s = solver.mkTupleSort(sorts);``                                                                                         |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |
@@ -195,7 +195,7 @@ a `cvc5::api::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});``                                              |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
-| Tuple Selector     | ``((_ tupSel i) t)``                   | ``Sort s = solver.mkTypleSort(sorts);``                                                                                         |
+| Tuple Selector     | ``((_ tuple_select i) t)``             | ``Sort s = solver.mkTupleSort(sorts);``                                                                                         |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |

diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h
index 88bf22638ff661771abfe25c9816af9d046649dc..60e2bf6e2c5fea93eb62928f684305a8374dc317 100644 (file)
--- a/src/parser/parse_op.h
+++ b/src/parser/parse_op.h
@@ -42,7 +42,7 @@ namespace cvc5 {
  * - For declared functions f that we have not yet looked up in a symbol table,
  * we store (2). We may store a name in a state if f is overloaded and we have
  * not yet parsed its arguments to know how to disambiguate f.
- * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to
+ * - For tuple selectors (_ tuple_select n), we store (1) and (3). Kind is set to
  * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
  * caller as the n^th generic tuple selector. We do this since there is no
  * AST expression representing generic tuple select, and we do not have enough

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 62b3d7bf6bcbab0b630ce2680fd82a5b8cd74729..0288040cc72557967406d514dc27cd5f550aab72 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -913,7 +913,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   api::Op op;
   if (p.d_kind != api::NULL_EXPR)
   {
-    // It is a special case, e.g. tupSel or array constant specification.
+    // It is a special case, e.g. tuple_select or array constant specification.
     // We have to wait until the arguments are parsed to resolve it.
   }
   else if (!p.d_expr.isNull())

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 44ff5aa18f5a540e70a5cd4dc0163d726e2439e1..a7a479550e8da84a7e47d7cbd0c2e8a26746cc59 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -244,7 +244,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   else if (kind == TUPLE_PROJECT)
   {
     // returns a tuple that represents
-    // (mkTuple ((_ tupSel i_1) t) ... ((_ tupSel i_n) t))
+    // (tuple ((_ tuple_select i_1) t) ... ((_ tuple_select i_n) t))
     // where each i_j is less than the length of t
 
     Trace("dt-rewrite-project") << "Rewrite project: " << in << std::endl;