[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 870831dbe4cf3f36b8f19bf0c24841df9183ed84..fc9aab8ef68d6fda7bbe0c86a53cf36f0efdfdc6 100644 (file)
--- 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 f921b6fb561c2a18798548a6bd46691f59dc6ec9..13f7b66132b0f88d6a2e16021b70abe51d6b8d0e 100644 (file)
--- 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 ee249bea42e38956fb211ce85a4f2c07eedac96d..097aa5e32d62f7b7f34d5cbf10fa969ff41735b8 100644 (file)
--- 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 (file)
index 0000000..f20d212
--- /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))