From: mudathirmahgoub Date: Wed, 2 Feb 2022 16:59:28 +0000 (-0600) Subject: Update datatypes.rst (#8009) X-Git-Tag: cvc5-1.0.0~479 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8623b22f6f8d28191f090f8f5456540d9cb0a18;p=cvc5.git Update datatypes.rst (#8009) --- diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index 04c70133e..132b029f9 100644 --- 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 c9a15ad24..e99fff895 100644 --- 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 , ..., )`` | ``Sort s = solver.mkTypleSort(sorts);`` | +| Tuple Constructor | ``(mkTuple , ..., )`` | ``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, , ..., });`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ -| 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 88bf22638..60e2bf6e2 100644 --- 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 62b3d7bf6..0288040cc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -913,7 +913,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& 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 44ff5aa18..a7a479550 100644 --- 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;