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.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 419d5422758d578ad554efdc4a24c72002c9c0b8..f561c101962c0402b163528b7e8f3c0a47ec0871 100644 (file)
--- 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<uint32_t> 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 f4c318da4d12fc7260f594170d67d954a0a8d31b..4a0b75460f02203ba9e19d97b129db162a24c0b3 100644 (file)
--- 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 (file)
index 0000000..8eac0ec
--- /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)