From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Mar 2022 22:09:38 +0000 (-0500)
Subject: Handled quoted symbols in indexed operators (#8491)
X-Git-Tag: cvc5-1.0.0~83
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57e5941afc9c4b4513043920bc83c29cc56f8bad;p=cvc5.git

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 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<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 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)