From 57e5941afc9c4b4513043920bc83c29cc56f8bad Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Mar 2022 17:09:38 -0500 Subject: [PATCH] Handled quoted symbols in indexed operators (#8491) Fixes https://github.com/cvc5/cvc5/issues/8489. The SMT-LIB standard says that symbols and quoted symbols are identical page 24: `This means for instance that abc and |abc| are the same symbol.`. We did not parse quoted symbols in indexed operators, this fixes the issue. --- src/parser/smt2/Smt2.g | 4 ++-- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/quoted-symbols.smt2 | 9 +++++++++ 3 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/quoted-symbols.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 419d54227..f561c1019 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1597,6 +1597,7 @@ identifier[cvc5::ParseOp& p] cvc5::Term f; cvc5::Term f2; std::vector numerals; + std::string opName; } : functionName[p.d_name, CHECK_NONE] @@ -1645,9 +1646,8 @@ identifier[cvc5::ParseOp& p] p.d_kind = cvc5::TUPLE_PROJECT; p.d_op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, numerals); } - | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] + | functionName[opName, CHECK_NONE] nonemptyNumeralList[numerals] { - std::string opName = AntlrInput::tokenText($sym); cvc5::Kind k = PARSER_STATE->getIndexedOpKind(opName); if (k == cvc5::UNDEFINED_KIND) { diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index f4c318da4..4a0b75460 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1098,6 +1098,7 @@ set(regress_0_tests regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/ufnia-fv-delta.smt2 regress0/quantifiers/veqt-delta.smt2 + regress0/quoted-symbols.smt2 regress0/rec-fun-const-parse-bug.smt2 regress0/rels/addr_book_0.cvc.smt2 regress0/rels/atom_univ2.cvc.smt2 diff --git a/test/regress/cli/regress0/quoted-symbols.smt2 b/test/regress/cli/regress0/quoted-symbols.smt2 new file mode 100644 index 000000000..8eac0ecf0 --- /dev/null +++ b/test/regress/cli/regress0/quoted-symbols.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(declare-fun x () Int) +(assert (= |x| 0)) +(declare-fun |y| () Int) +(assert (= y 0)) +(assert (= (|str.len| "ABC") 3)) +(assert (= ((_ |extract| 3 0) #b010101) #b0101)) +(check-sat) -- 2.30.2