From 4eac250cf24968bdf04ed04ec92db1506526b380 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 29 Mar 2022 23:39:29 -0500 Subject: [PATCH] Change tuple tokens and update datatypes theory ref (#8420) Changes tuple_ to tuple. for consistency. Also fixes the lexer list for smt2 and updates the datatypes theory reference with missing content. --- docs/ext/smtliblexer.py | 17 ++-- docs/theories/datatypes.rst | 84 ++++++++++++++++--- src/api/cpp/cvc5_kind.h | 2 +- src/parser/smt2/Smt2.g | 4 +- src/parser/smt2/smt2.cpp | 6 +- src/printer/smt2/smt2_printer.cpp | 12 +-- .../datatypes/some-boolean-tests.cvc.smt2 | 2 +- .../regress0/datatypes/tuple-model.cvc.smt2 | 2 +- .../datatypes/tuple-record-bug.cvc.smt2 | 2 +- .../cli/regress0/datatypes/tuple.cvc.smt2 | 8 +- .../cli/regress0/datatypes/tuple_update.smt2 | 2 +- .../regress0/datatypes/tuples-multitype.smt2 | 2 +- .../printer/tuples_and_records.cvc.smt2 | 4 +- test/regress/cli/regress1/bags/product3.smt2 | 2 +- .../regress1/datatypes/tuple_projection.smt2 | 6 +- .../regress1/sets/sets-tuple-poly.cvc.smt2 | 6 +- test/unit/api/cpp/solver_black.cpp | 2 +- test/unit/api/java/SolverTest.java | 2 +- test/unit/api/python/test_solver.py | 2 +- 19 files changed, 114 insertions(+), 53 deletions(-) diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index cc0792aab..b61cba121 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -48,7 +48,7 @@ class SmtLibLexer(RegexLexer): '=>', '=', 'true', 'false', 'not', 'and', 'or', 'xor', 'distinct', 'ite', # datatypes - 'tuple', 'tuple_project', 'tuple_select', + 'tuple', 'tuple\.project', 'tuple\.select', 'tuple\.update', # fp 'RNE', 'RNA', 'RTP', 'RTN', 'RTZ', 'fp', 'NaN', 'fp\.abs', 'fp\.neg', 'fp\.add', 'fp\.sub', 'fp\.mul', 'fp\.div', 'fp\.fma', 'fp\.sqrt', @@ -62,15 +62,16 @@ class SmtLibLexer(RegexLexer): '<', '>', '<=', '>=', '!=', '\+', '-', '\*', '/', 'div', 'mod', 'abs', 'divisible', 'to_real', 'to_int', 'is_int', 'iand', 'int2bv', # separation logic - 'emp', 'pto', 'sep', 'wand', 'nil', + 'sep\.emp', 'pto', 'sep', 'wand', 'sep\.nil', # sets / relations - 'union', 'setminus', 'member', 'subset', 'emptyset', 'singleton', - 'card', 'insert', 'complement', 'univset', 'transpose', 'tclosure', - 'join', 'product', 'intersection', + 'set\.union', 'set\.minus', 'set\.member', 'set\.subset', 'set\.empty', + 'set\.singleton', 'set\.card', 'set\.insert', 'set\.complement', + 'set\.universe', 'rel\.transpose', 'rel\.tclosure', 'rel\.join', + 'rel\.product', 'set\.inter', # string - 'char', 'str\.\+\+', 'str\.len', 'str\.<', 'str\.to_re', 'str\.in_re', - 're\.none', 're\.all', 're\.allchar', 're\.\+\+', 're\.union', - 're\.inter', 're\.*', 'str\.<=', 'str\.at', 'str\.substr', + 'char', 'str\.\+\+', 'str\.len', 'str\.<', 'str\.<=', 'str\.to_re', + 'str\.in_re', 're\.none', 're\.all', 're\.allchar', 're\.\+\+', + 're\.union', 're\.inter', 're\.*', 'str\.<=', 'str\.at', 'str\.substr', 'str\.prefixof', 'str\.suffixof', 'str\.contains', 'str\.indexof', 'str\.replace', 'str\.replace_all', 'str\.replace_re', 'str\.replace_re_all', 're\.comp', 're\.diff', 're\.\+', 're\.opt', diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 286439653..e0d731d28 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -27,13 +27,13 @@ datatypes in ``*.smt2`` input files in the smt lib 2.6 format: .. code:: smtlib (declare-datatypes ((D1 n1) ... (Dk nk)) - (((C1 (S1 T1) ... (Si Ti)) ... (Cj ... )) + (((C1 (S11 T1) ... (S1i Ti)) ... (Cj ... )) ... ((...) ... (...))) where ``D1 ... Dk`` are datatype types, ``C1 ... Cj`` are the constructors for datatype ``D1``, -``S1 ... Si`` are the selectors (or "destructors") of constructor ``C1``, and +``S11 ... S1i`` are the selectors (or "destructors") of constructor ``C1``, and each ``T1 ... Ti`` is a previously declared type or one of ``D1 ... Dk``. The numbers ``n1 ... nk`` denote the number of type parameters for the datatype, where ``0`` is used for non-parametric datatypes. @@ -144,7 +144,7 @@ For example: .. code:: smtlib (declare-const t (Tuple Int Int)) - (assert (= ((_ tuple_select 0) t) 3)) + (assert (= ((_ tuple.select 0) t) 3)) (assert (not (= t (tuple 3 4)))) @@ -176,6 +176,42 @@ a `cvc5::api::Solver solver` object. +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ | Logic String | ``(set-logic QF_DT)`` | ``solver.setLogic("QF_DT");`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Datatype Sort | ``(declare-datatype ...)`` | ``Sort s = solver.mkDatatypeSort(...);`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Datatype Sorts | ``(declare-datatypes ...)`` | ``std::vector s = solver.mkDatatypeSorts(...);`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Constructor | ``(Ci , ..., )`` | ``Sort s = solver.mkDatatypeSort(...);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term ci = dt[i].getConstructorTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {ci, , ..., });`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Selector | ``(Sij t)`` | ``Sort s = solver.mkDatatypeSort(...);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term sij = dt[i].getSelector(j).getSelectorTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sij, t});`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Updater | ``((_ update Sij) t u)`` | ``Sort s = solver.mkDatatypeSort(...);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term upd = dt[i].getSelector(j).getUpdaterTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Tester | ``((_ is Ci) t)`` | ``Sort s = solver.mkDatatypeSort(...);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term upd = dt[i].getTesterTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_TESTER, {upd, t, u});`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ | Tuple Sort | ``(Tuple , ..., )`` | ``std::vector sorts = { ... };`` | | | | | | | | ``Sort s = solver.mkTupleSort(sorts);`` | @@ -190,17 +226,33 @@ a `cvc5::api::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term c = dt[0].getConstructor();`` | +| | | ``Term c = dt[0].getConstructorTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Tuple Selector | ``((_ tuple.select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term sel = dt[0].getSelector(i).getSelectorTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Tuple Updater | ``((_ tuple.update i) t u)`` | ``Sort s = solver.mkTupleSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term upd = dt[0].getSelector(i).getUpdaterTerm();`` | | | | | -| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | +| | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ -| Tuple Selector | ``((_ tuple_select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` | +| Tuple Projection | ``((_ tuple.project i1 ... in) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` | | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term c = dt[0].getSelector(i);`` | +| | | ``Term proj = solver.mkOp(Kind::TUPLE_PROJECT, {i1, ..., in});`` | | | | | -| | | ``Term s = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});`` | +| | | ``Term r = solver.mkTerm(Kind::TUPLE_PROJECT, {proj, t});`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ | Record Sort | n/a | ``Sort s = mkRecordSort(const std::vector>& fields);`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ @@ -216,15 +268,23 @@ a `cvc5::api::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term c = dt[0].getConstructor();`` | +| | | ``Term c = dt[0].getConstructorTerm();`` | | | | | -| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | +| | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ | Record Selector | n/a | ``Sort s = mkRecordSort(fields);`` | | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term c = dt[0].getSelector(name);`` | +| | | ``Term sel = dt[0].getSelector(name).getSelectorTerm();`` | +| | | | +| | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` | ++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ +| Record Updater | n/a | ``Sort s = solver.mkRecordSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term upd = dt[0].getSelector(name).getUpdaterTerm();`` | | | | | -| | | ``Term s = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});`` | +| | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 93ac21e11..161241466 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2275,7 +2275,7 @@ enum Kind : int32_t * \rst * .. code:: smtlib * - * ((_ tuple_project 1 2 2 3 1) (tuple 10 20 30 40)) + * ((_ tuple.project 1 2 2 3 1) (tuple 10 20 30 40)) * \endrst * yields * \rst diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 86ee80b4c..7361b70a0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1639,7 +1639,7 @@ identifier[cvc5::ParseOp& p] } | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals] { - // we adopt a special syntax (_ tuple_project i_1 ... i_n) where + // we adopt a special syntax (_ tuple.project i_1 ... i_n) where // i_1, ..., i_n are numerals p.d_kind = cvc5::TUPLE_PROJECT; p.d_op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, numerals); @@ -2282,7 +2282,7 @@ FORALL_TOK : 'forall'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple'; -TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple_project'; +TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple.project'; FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card'; HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c4ff3cadf..3538f40d3 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -136,8 +136,8 @@ void Smt2::addDatatypesOperators() // Notice that tuple operators, we use the generic APPLY_SELECTOR and // APPLY_UPDATER kinds. These are processed based on the context // in which they are parsed, e.g. when parsing identifiers. - addIndexedOperator(cvc5::APPLY_SELECTOR, "tuple_select"); - addIndexedOperator(cvc5::APPLY_UPDATER, "tuple_update"); + addIndexedOperator(cvc5::APPLY_SELECTOR, "tuple.select"); + addIndexedOperator(cvc5::APPLY_UPDATER, "tuple.update"); } } @@ -962,7 +962,7 @@ cvc5::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) } else if (p.d_kind != cvc5::NULL_TERM) { - // It is a special case, e.g. tuple_select 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/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 583567e98..0187c2768 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -774,13 +774,13 @@ void Smt2Printer::toStream(std::ostream& out, TupleProjectOp op = n.getOperator().getConst(); if (op.getIndices().empty()) { - // e.g. (tuple_project tuple) - out << "tuple_project " << n[0] << ")"; + // e.g. (tuple.project tuple) + out << "tuple.project " << n[0] << ")"; } else { - // e.g. ((_ tuple_project 2 4 4) tuple) - out << "(_ tuple_project" << op << ") " << n[0] << ")"; + // e.g. ((_ tuple.project 2 4 4) tuple) + out << "(_ tuple.project" << op << ") " << n[0] << ")"; } return; } @@ -797,7 +797,7 @@ void Smt2Printer::toStream(std::ostream& out, if (dt.isTuple()) { stillNeedToPrintParams = false; - out << "(_ tuple_select " << DType::indexOf(op) << ") "; + out << "(_ tuple.select " << DType::indexOf(op) << ") "; } } break; @@ -823,7 +823,7 @@ void Smt2Printer::toStream(std::ostream& out, if (dt.isTuple()) { stillNeedToPrintParams = false; - out << "(_ tuple_update " << DType::indexOf(op) << ") "; + out << "(_ tuple.update " << DType::indexOf(op) << ") "; } else { diff --git a/test/regress/cli/regress0/datatypes/some-boolean-tests.cvc.smt2 b/test/regress/cli/regress0/datatypes/some-boolean-tests.cvc.smt2 index e05a65ad0..d421bc47f 100644 --- a/test/regress/cli/regress0/datatypes/some-boolean-tests.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/some-boolean-tests.cvc.smt2 @@ -5,6 +5,6 @@ (declare-fun x () (list Real)) (declare-fun y () (Tuple Int Bool Int)) (assert (= y (tuple 5 true 4))) -(assert ((_ tuple_select 1) y)) +(assert ((_ tuple.select 1) y)) (assert (= x ((as cons (list Real)) (/ 11 10) true (as nil (list Real))))) (check-sat) diff --git a/test/regress/cli/regress0/datatypes/tuple-model.cvc.smt2 b/test/regress/cli/regress0/datatypes/tuple-model.cvc.smt2 index 7f063a499..a169f492c 100644 --- a/test/regress/cli/regress0/datatypes/tuple-model.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/tuple-model.cvc.smt2 @@ -2,5 +2,5 @@ (set-logic ALL) (set-option :incremental false) (declare-fun x () (Tuple Int Int)) -(assert (= ((_ tuple_select 0) x) 5)) +(assert (= ((_ tuple.select 0) x) 5)) (check-sat) diff --git a/test/regress/cli/regress0/datatypes/tuple-record-bug.cvc.smt2 b/test/regress/cli/regress0/datatypes/tuple-record-bug.cvc.smt2 index f26769ccc..8071abebf 100644 --- a/test/regress/cli/regress0/datatypes/tuple-record-bug.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/tuple-record-bug.cvc.smt2 @@ -8,4 +8,4 @@ (define-fun foo ((x |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)) |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| ((_ update int) x (int x))) (declare-fun m () |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|) (define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) -(check-sat-assuming ( (not (= ((_ tuple_select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) )) +(check-sat-assuming ( (not (= ((_ tuple.select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) )) diff --git a/test/regress/cli/regress0/datatypes/tuple.cvc.smt2 b/test/regress/cli/regress0/datatypes/tuple.cvc.smt2 index 9e6e83c2b..0c5ce70b5 100644 --- a/test/regress/cli/regress0/datatypes/tuple.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/tuple.cvc.smt2 @@ -2,9 +2,9 @@ (set-logic ALL) (set-option :incremental false) (define-fun x () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9))) -(define-fun first_elem () Real ((_ tuple_select 0) (tuple (/ 4 5) 9 (/ 11 9)))) -(define-fun third_elem () Real ((_ tuple_select 2) (tuple (/ 4 5) 9 (/ 11 9)))) +(define-fun first_elem () Real ((_ tuple.select 0) (tuple (/ 4 5) 9 (/ 11 9)))) +(define-fun third_elem () Real ((_ tuple.select 2) (tuple (/ 4 5) 9 (/ 11 9)))) (define-fun y () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9))) -(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3)) -(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple_select 0) _let_1) ((_ tuple_select 0) _let_2))) (= ((_ tuple_select 2) _let_1) ((_ tuple_select 2) _let_2))) (= ((_ tuple_select 1) _let_2) 3))))) )) +(define-fun y1 () (Tuple Real Int Real) ((_ tuple.update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3)) +(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple.update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple.select 0) _let_1) ((_ tuple.select 0) _let_2))) (= ((_ tuple.select 2) _let_1) ((_ tuple.select 2) _let_2))) (= ((_ tuple.select 1) _let_2) 3))))) )) diff --git a/test/regress/cli/regress0/datatypes/tuple_update.smt2 b/test/regress/cli/regress0/datatypes/tuple_update.smt2 index 9812da728..553d5593b 100644 --- a/test/regress/cli/regress0/datatypes/tuple_update.smt2 +++ b/test/regress/cli/regress0/datatypes/tuple_update.smt2 @@ -2,5 +2,5 @@ (set-info :status sat) (declare-fun x () (Tuple Int Int)) (declare-fun y () (Tuple Int Int)) -(assert (= ((_ tuple_update 0) x 1) ((_ tuple_update 1) y 2))) +(assert (= ((_ tuple.update 0) x 1) ((_ tuple.update 1) y 2))) (check-sat) diff --git a/test/regress/cli/regress0/datatypes/tuples-multitype.smt2 b/test/regress/cli/regress0/datatypes/tuples-multitype.smt2 index c6555c5df..b3464127a 100644 --- a/test/regress/cli/regress0/datatypes/tuples-multitype.smt2 +++ b/test/regress/cli/regress0/datatypes/tuples-multitype.smt2 @@ -6,6 +6,6 @@ (declare-fun i () String) (assert (= t (tuple 0 "0"))) -(assert (= i ((_ tuple_select 1) t))) +(assert (= i ((_ tuple.select 1) t))) (check-sat) diff --git a/test/regress/cli/regress0/printer/tuples_and_records.cvc.smt2 b/test/regress/cli/regress0/printer/tuples_and_records.cvc.smt2 index 0c54f5f49..e83751a2c 100644 --- a/test/regress/cli/regress0/printer/tuples_and_records.cvc.smt2 +++ b/test/regress/cli/regress0/printer/tuples_and_records.cvc.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ; EXPECT: (((a r) "active")) -; EXPECT: ((((_ tuple_select 1) y) 9)) +; EXPECT: ((((_ tuple.select 1) y) 9)) (set-logic ALL) (set-option :incremental false) (set-option :produce-models true) @@ -12,4 +12,4 @@ (assert (= y (tuple (/ 4 5) 9 (/ 11 9)))) (check-sat-assuming ( (not (= (a r) "what?")) )) (get-value ( (a r) )) -(get-value ( ((_ tuple_select 1) y) )) +(get-value ( ((_ tuple.select 1) y) )) diff --git a/test/regress/cli/regress1/bags/product3.smt2 b/test/regress/cli/regress1/bags/product3.smt2 index 8f2e8c38f..8e62f55ca 100644 --- a/test/regress/cli/regress1/bags/product3.smt2 +++ b/test/regress/cli/regress1/bags/product3.smt2 @@ -16,6 +16,6 @@ (assert (bag.member y B)) (assert (bag.member z C)) -(assert (distinct x y ((_ tuple_project 0 1 2) z) ((_ tuple_project 3 4 5) z))) +(assert (distinct x y ((_ tuple.project 0 1 2) z) ((_ tuple.project 3 4 5) z))) (check-sat) diff --git a/test/regress/cli/regress1/datatypes/tuple_projection.smt2 b/test/regress/cli/regress1/datatypes/tuple_projection.smt2 index dfe37a9d0..73c298dc4 100644 --- a/test/regress/cli/regress1/datatypes/tuple_projection.smt2 +++ b/test/regress/cli/regress1/datatypes/tuple_projection.smt2 @@ -5,7 +5,7 @@ (declare-fun v () Tuple) (declare-fun x () String) (assert (= t (tuple "a" "b" "c" "d"))) -(assert (= x ((_ tuple_select 0) t))) -(assert (= u ((_ tuple_project 2 3) t))) -(assert (= v (tuple_project t))) +(assert (= x ((_ tuple.select 0) t))) +(assert (= u ((_ tuple.project 2 3) t))) +(assert (= v (tuple.project t))) (check-sat) \ No newline at end of file diff --git a/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2 b/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2 index 64a2306c4..31d64cb49 100644 --- a/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2 +++ b/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2 @@ -7,7 +7,7 @@ (declare-fun b () (Set (Tuple Int Real))) (declare-fun x () (Tuple Real Real)) (assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1))))) -(assert (set.member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a)) -(assert (set.member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b)) -(assert (not (= ((_ tuple_select 0) x) ((_ tuple_select 1) x)))) +(assert (set.member (tuple ((_ tuple.select 0) x) (to_int ((_ tuple.select 1) x))) a)) +(assert (set.member (tuple (to_int ((_ tuple.select 0) x)) ((_ tuple.select 1) x)) b)) +(assert (not (= ((_ tuple.select 0) x) ((_ tuple.select 1) x)))) (check-sat) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index a29f9d268..97129787c 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2880,7 +2880,7 @@ TEST_F(TestApiBlackSolver, tupleProject) } ASSERT_EQ( - "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton " + "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton " "\"Z\")))", projection.toString()); } diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 58fe0d9e7..213979e62 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -2816,7 +2816,7 @@ class SolverTest assertEquals(elements[indices[i]], simplifiedTerm); } - assertEquals("((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" " + assertEquals("((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" " + "(set.singleton \"Z\")))", projection.toString()); } diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 7ad960249..9ba032f0a 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -2585,5 +2585,5 @@ def test_tuple_project(solver): simplifiedTerm = solver.simplify(selectedTerm) assert elements[i] == simplifiedTerm - assert "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str( + assert "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str( projection) -- 2.30.2