From a139a1f0ce824fe3e2e38e70baa115150a82a3a6 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 25 Mar 2022 16:09:13 -0700 Subject: [PATCH] [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. --- src/parser/smt2/Smt2.g | 1 + src/parser/smt2/smt2.cpp | 69 +++++++++---------- test/regress/cli/CMakeLists.txt | 1 + .../parser/issue8377-resolve-indexed.smt2 | 6 ++ 4 files changed, 42 insertions(+), 35 deletions(-) create mode 100644 test/regress/cli/regress0/parser/issue8377-resolve-indexed.smt2 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& 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& 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& 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)) -- 2.30.2