From f66cbabd6b67462ebbf9bbba5d3ccfb08b69ff25 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Sep 2021 00:28:22 -0500 Subject: Minimal fixing version for tuple update parsing (#7228) This takes the essential changes from #7218 so that the current ANTLR issues are avoided. --- src/parser/smt2/Smt2.g | 43 +++++++++++++++++++---- src/parser/smt2/smt2.cpp | 42 +++++++++++----------- src/parser/smt2/smt2.h | 8 ++--- src/printer/smt2/smt2_printer.cpp | 18 +++++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/datatypes/tuple_update.smt2 | 6 ++++ 6 files changed, 81 insertions(+), 37 deletions(-) create mode 100644 test/regress/regress0/datatypes/tuple_update.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8f9e01c6c..674aeca1f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1577,12 +1577,13 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2] * - For declared functions f, we return (2). * - For indexed functions like testers (_ is C) and bitvector extract * (_ extract n m), we return (3) for the appropriate operator. - * - For tuple selectors (_ tupSel n), we return (1) and (3). api::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 - * type information at this point to know the type of the tuple we will be - * selecting from. + * - For tuple selectors (_ tuple_select n) and updaters (_ tuple_update n), we + * return (1) and (3). api::Kind is set to APPLY_SELECTOR or APPLY_UPDATER + * respectively, and expr is set to n, which is to be interpreted by the + * caller as the n^th generic tuple selector or updater. We do this since there + * is no AST expression representing generic tuple select, and we do not have + * enough type information at this point to know the type of the tuple we will + * be selecting from. * * (Ascripted Identifiers) * @@ -1703,7 +1704,35 @@ identifier[cvc5::ParseOp& p] } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { - p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals); + std::string opName = AntlrInput::tokenText($sym); + api::Kind k = PARSER_STATE->getIndexedOpKind(opName); + if (k == api::APPLY_UPDATER) + { + // we adopt a special syntax (_ tuple_update n) for tuple updaters + if (numerals.size() != 1) + { + PARSER_STATE->parseError( + "Unexpected syntax for tuple selector or updater."); + } + // The operator is dependent upon inferring the type of the arguments, + // and hence the type is not available yet. Hence, we remember the + // index as a numeral in the parse operator. + p.d_kind = k; + p.d_expr = SOLVER->mkInteger(numerals[0]); + } + else if (numerals.size() == 1) + { + p.d_op = SOLVER->mkOp(k, numerals[0]); + } + else if (numerals.size() == 2) + { + p.d_op = SOLVER->mkOp(k, numerals[0], numerals[1]); + } + else + { + PARSER_STATE->parseError( + "Unexpected number of numerals for indexed symbol."); + } } ) RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2fd4a5596..40716d908 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -135,6 +135,7 @@ void Smt2::addDatatypesOperators() { Parser::addOperator(api::APPLY_UPDATER); addOperator(api::DT_SIZE, "dt.size"); + addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update"); } } @@ -382,25 +383,15 @@ api::Term Smt2::mkIndexedConstant(const std::string& name, return api::Term(); } -api::Op Smt2::mkIndexedOp(const std::string& name, - const std::vector& numerals) +api::Kind Smt2::getIndexedOpKind(const std::string& name) { const auto& kIt = d_indexedOpKindMap.find(name); if (kIt != d_indexedOpKindMap.end()) { - api::Kind k = (*kIt).second; - if (numerals.size() == 1) - { - return d_solver->mkOp(k, numerals[0]); - } - else if (numerals.size() == 2) - { - return d_solver->mkOp(k, numerals[0], numerals[1]); - } + return (*kIt).second; } - parseError(std::string("Unknown indexed function `") + name + "'"); - return api::Op(); + return api::UNDEFINED_KIND; } api::Term Smt2::bindDefineFunRec( @@ -1037,22 +1028,24 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) Debug("parser") << "applyParseOp: return store all " << ret << std::endl; return ret; } - else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull()) + else if ((p.d_kind == api::APPLY_SELECTOR || p.d_kind == api::APPLY_UPDATER) + && !p.d_expr.isNull()) { // tuple selector case if (!p.d_expr.isUInt64Value()) { - parseError("index of tupSel is larger than size of uint64_t"); + parseError( + "index of tuple select or update is larger than size of uint64_t"); } uint64_t n = p.d_expr.getUInt64Value(); - if (args.size() != 1) + if (args.size() != (p.d_kind == api::APPLY_SELECTOR ? 1 : 2)) { - parseError("tupSel should only be applied to one tuple argument"); + parseError("wrong number of arguments for tuple select or update"); } api::Sort t = args[0].getSort(); if (!t.isTuple()) { - parseError("tupSel applied to non-tuple"); + parseError("tuple select or update applied to non-tuple"); } size_t length = t.getTupleLength(); if (n >= length) @@ -1062,8 +1055,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) parseError(ss.str()); } const api::Datatype& dt = t.getDatatype(); - api::Term ret = d_solver->mkTerm( - api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); + api::Term ret; + if (p.d_kind == api::APPLY_SELECTOR) + { + ret = d_solver->mkTerm( + api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); + } + else + { + ret = d_solver->mkTerm( + api::APPLY_UPDATER, dt[0][n].getUpdaterTerm(), args[0], args[1]); + } Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 97eb95c00..fd68732fe 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -121,15 +121,13 @@ class Smt2 : public Parser const std::vector& numerals); /** - * Creates an indexed operator term, e.g. (_ extract 5 0). + * Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract". * * @param name The name of the operator (e.g. "extract") - * @param numerals The parameters for the operator (e.g. [5, 0]) - * @return The operator term corresponding to the indexed operator or a parse + * @return The kind corresponding to the indexed operator or a parse * error if the name is not valid. */ - api::Op mkIndexedOp(const std::string& name, - const std::vector& numerals); + api::Kind getIndexedOpKind(const std::string& name); /** * Returns the expression that name should be interpreted as. diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6217276b1..3c0fe838b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -791,11 +791,19 @@ void Smt2Printer::toStream(std::ostream& out, size_t index = DType::indexOf(op); const DType& dt = DType::datatypeOf(op); size_t cindex = DType::cindexOf(op); - out << "(_ update "; - toStream(out, - dt[cindex][index].getSelector(), - toDepth < 0 ? toDepth : toDepth - 1); - out << ") "; + if (dt.isTuple()) + { + stillNeedToPrintParams = false; + out << "(_ tuple_update " << DType::indexOf(op) << ") "; + } + else + { + out << "(_ update "; + toStream(out, + dt[cindex][index].getSelector(), + toDepth < 0 ? toDepth : toDepth - 1); + out << ") "; + } } break; case kind::APPLY_SELECTOR_TOTAL: diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 301e26bf9..47d352695 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -522,6 +522,7 @@ set(regress_0_tests regress0/datatypes/tuple-no-clash.cvc regress0/datatypes/tuple-record-bug.cvc regress0/datatypes/tuple.cvc + regress0/datatypes/tuple_update.smt2 regress0/datatypes/tuples-empty.smt2 regress0/datatypes/tuples-multitype.smt2 regress0/datatypes/typed_v10l30054.cvc diff --git a/test/regress/regress0/datatypes/tuple_update.smt2 b/test/regress/regress0/datatypes/tuple_update.smt2 new file mode 100644 index 000000000..9812da728 --- /dev/null +++ b/test/regress/regress0/datatypes/tuple_update.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(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))) +(check-sat) -- cgit v1.2.3