From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 25 Mar 2022 23:09:13 +0000 (-0700)
Subject: [Parser] Fix resolution of indexed symbols (#8383)
X-Git-Tag: cvc5-1.0.0~166
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a139a1f0ce824fe3e2e38e70baa115150a82a3a6;p=cvc5.git

[Parser] Fix resolution of indexed symbols (#8383)

Fixes #8377. Commit 3a97480ffab492f8272ad9c7c192d04b43eeea60 changed how
we handle indexed symbols. In particular, it added the option to resolve
them later when the arguments are known. However, the condition for when
to do this resolution was incorrect: It was applied to _all_ known
indexed symbols and not only the ones that can't immediately be resolved
to a kind. This commit fixes the condition.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 870831dbe..fc9aab8ef 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1661,6 +1661,7 @@ identifier[cvc5::ParseOp& p]
           // We don't know which kind to use until we know the type of the
           // arguments
           p.d_name = opName;
+          p.d_kind = api::UNDEFINED_KIND;
           // convert uint64_t to uint32_t
           for(uint32_t numeral : numerals)
           {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index f921b6fb5..13f7b6613 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -902,32 +902,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
   }
   api::Op op;
-  if (p.d_kind != api::NULL_TERM)
-  {
-    // 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())
-  {
-    // An explicit operator, e.g. an apply function
-    api::Kind fkind = getKindForFunction(p.d_expr);
-    if (fkind != api::UNDEFINED_KIND)
-    {
-      // Some operators may require a specific kind.
-      // Testers are handled differently than other indexed operators,
-      // since they require a kind.
-      kind = fkind;
-      Trace("parser") << "Got function kind " << kind << " for expression "
-                      << std::endl;
-    }
-    args.insert(args.begin(), p.d_expr);
-  }
-  else if (!p.d_op.isNull())
-  {
-    // it was given an operator
-    op = p.d_op;
-  }
-  else if (isIndexedOperatorEnabled(p.d_name))
+  if (p.d_kind == api::UNDEFINED_KIND && isIndexedOperatorEnabled(p.d_name))
   {
     // Resolve indexed symbols that cannot be resolved without knowing the type
     // of the arguments. This is currently limited to `to_fp`.
@@ -935,9 +910,8 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     size_t nchildren = args.size();
     if (nchildren == 1)
     {
-      op = d_solver->mkOp(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
-                          p.d_indices[0],
-                          p.d_indices[1]);
+      kind = api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV;
+      op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
     }
     else if (nchildren > 2)
     {
@@ -960,21 +934,46 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
 
       if (t.isFloatingPoint())
       {
-        op = d_solver->mkOp(
-            api::FLOATINGPOINT_TO_FP_FROM_FP, p.d_indices[0], p.d_indices[1]);
+        kind = api::FLOATINGPOINT_TO_FP_FROM_FP;
+        op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
       }
       else if (t.isInteger() || t.isReal())
       {
-        op = d_solver->mkOp(
-            api::FLOATINGPOINT_TO_FP_FROM_REAL, p.d_indices[0], p.d_indices[1]);
+        kind = api::FLOATINGPOINT_TO_FP_FROM_REAL;
+        op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
       }
       else
       {
-        op = d_solver->mkOp(
-            api::FLOATINGPOINT_TO_FP_FROM_SBV, p.d_indices[0], p.d_indices[1]);
+        kind = api::FLOATINGPOINT_TO_FP_FROM_SBV;
+        op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
       }
     }
   }
+  else if (p.d_kind != api::NULL_TERM)
+  {
+    // 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())
+  {
+    // An explicit operator, e.g. an apply function
+    api::Kind fkind = getKindForFunction(p.d_expr);
+    if (fkind != api::UNDEFINED_KIND)
+    {
+      // Some operators may require a specific kind.
+      // Testers are handled differently than other indexed operators,
+      // since they require a kind.
+      kind = fkind;
+      Trace("parser") << "Got function kind " << kind << " for expression "
+                      << std::endl;
+    }
+    args.insert(args.begin(), p.d_expr);
+  }
+  else if (!p.d_op.isNull())
+  {
+    // it was given an operator
+    op = p.d_op;
+  }
   else
   {
     isBuiltinOperator = isOperatorEnabled(p.d_name);
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index ee249bea4..097aa5e32 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -867,6 +867,7 @@ set(regress_0_tests
   regress0/parser/issue7274.smt2
   regress0/parser/issue7860-parse-only-reset.smt2
   regress0/parser/issue7894-parse-error-assoc.smt2
+  regress0/parser/issue8377-resolve-indexed.smt2
   regress0/parser/linear_arithmetic_err1.smt2
   regress0/parser/linear_arithmetic_err2.smt2
   regress0/parser/linear_arithmetic_err3.smt2
diff --git a/test/regress/cli/regress0/parser/issue8377-resolve-indexed.smt2 b/test/regress/cli/regress0/parser/issue8377-resolve-indexed.smt2
new file mode 100644
index 000000000..f20d21291
--- /dev/null
+++ b/test/regress/cli/regress0/parser/issue8377-resolve-indexed.smt2
@@ -0,0 +1,6 @@
+; SCRUBBER: grep -o "'re.loop' not declared as a variable"
+; EXPECT: 're.loop' not declared as a variable
+; EXIT: 1
+; DISABLE-TESTER: dump
+(set-logic QF_SLIA)
+(assert (re.loop 0))