Improve handling of `:named` attributes (#6549)

Currently, when a :named attribute is used in a binder, the parser
complains about an illegal argument. This is because an argument check
in the SymbolManager fails. This is not very user friendly. This
commit makes the error message clearer for the user:

Cannot name a term in a binder (e.g., quantifiers, definitions)

To do this, the commit changes the return type for
SymbolManager::setExpressionName to include more information that can
then be used by the parser to generate an appropriate error message.

The commit also changes define-fun to not push/pop the local scope
if it has zero arguments because it is semantically equivalent to a
define-const, which allows :named terms.

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index c6eb8d08ef03d3e4ac425a60a0d6d22d0e846527..8d48709668de6e9c49e4cdede530764d9d22a025 100644 (file)
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -48,9 +48,9 @@ class SymbolManager::Implementation
 
   ~Implementation() { d_context.pop(); }
   /** set expression name */
-  bool setExpressionName(api::Term t,
-                         const std::string& name,
-                         bool isAssertion = false);
+  NamingResult setExpressionName(api::Term t,
+                                 const std::string& name,
+                                 bool isAssertion = false);
   /** get expression name */
   bool getExpressionName(api::Term t,
                          std::string& name,
@@ -97,15 +97,17 @@ class SymbolManager::Implementation
   CDO<bool> d_hasPushedScope;
 };
 
-bool SymbolManager::Implementation::setExpressionName(api::Term t,
-                                                      const std::string& name,
-                                                      bool isAssertion)
+NamingResult SymbolManager::Implementation::setExpressionName(
+    api::Term t, const std::string& name, bool isAssertion)
 {
   Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
                        << name << ", isAssertion=" << isAssertion << std::endl;
-  // cannot name subexpressions under quantifiers
-  PrettyCheckArgument(
-      !d_hasPushedScope.get(), name, "cannot name function in a scope");
+  if (d_hasPushedScope.get())
+  {
+    // cannot name subexpressions under binders
+    return NamingResult::ERROR_IN_BINDER;
+  }
+
   if (isAssertion)
   {
     d_namedAsserts.insert(t);
@@ -113,10 +115,10 @@ bool SymbolManager::Implementation::setExpressionName(api::Term t,
   if (d_names.find(t) != d_names.end())
   {
     // already named assertion
-    return false;
+    return NamingResult::ERROR_ALREADY_NAMED;
   }
   d_names[t] = name;
-  return true;
+  return NamingResult::SUCCESS;
 }
 
 bool SymbolManager::Implementation::getExpressionName(api::Term t,
@@ -269,9 +271,9 @@ SymbolManager::~SymbolManager() {}
 
 SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
 
-bool SymbolManager::setExpressionName(api::Term t,
-                                      const std::string& name,
-                                      bool isAssertion)
+NamingResult SymbolManager::setExpressionName(api::Term t,
+                                              const std::string& name,
+                                              bool isAssertion)
 {
   return d_implementation->setExpressionName(t, name, isAssertion);
 }

diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 6cd0a1467f219170f415dbe0bc8f90dbce3e59f3..271825e07d9aa9433ad908a94326e593da55225a 100644 (file)
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -28,6 +28,17 @@
 
 namespace cvc5 {
 
+/** Represents the result of a call to `setExpressionName()`. */
+enum class NamingResult
+{
+  /** The expression name was set successfully. */
+  SUCCESS,
+  /** The expression already has a name. */
+  ERROR_ALREADY_NAMED,
+  /** The expression is in a binder. */
+  ERROR_IN_BINDER
+};
+
 /**
  * Symbol manager, which manages:
  * (1) The symbol table used by the parser,
@@ -54,9 +65,9 @@ class CVC5_EXPORT SymbolManager
    * @return true if the name was set. This method may return false if t
    * already has a name.
    */
-  bool setExpressionName(api::Term t,
-                         const std::string& name,
-                         bool isAssertion = false);
+  NamingResult setExpressionName(api::Term t,
+                                 const std::string& name,
+                                 bool isAssertion = false);
   /** Get name for term t
    *
    * @param t The term

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dc9a324bb60b5b4aacb1595ae15ace781244efb3..58f229cfef35458f4886c7a4c2ee959cdf73b664 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -314,7 +314,10 @@ command [std::unique_ptr<cvc5::Command>* cmd]
       }
 
       t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
-      PARSER_STATE->pushScope();
+      if (sortedVarNames.size() > 0)
+      {
+        PARSER_STATE->pushScope();
+      }
       terms = PARSER_STATE->bindBoundVars(sortedVarNames);
     }
     term[expr, expr2]
@@ -325,7 +328,10 @@ command [std::unique_ptr<cvc5::Command>* cmd]
         expr = PARSER_STATE->mkHoApply(expr, flattenVars);
         terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
       }
-      PARSER_STATE->popScope();
+      if (sortedVarNames.size() > 0)
+      {
+        PARSER_STATE->popScope();
+      }
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)
@@ -1007,14 +1013,8 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
-    { /* add variables to parser state before parsing term */
-      Debug("parser") << "define const: '" << name << "'" << std::endl;
-      PARSER_STATE->pushScope();
-      terms = PARSER_STATE->bindBoundVars(sortedVarNames);
-    }
     term[e, e2]
     {
-      PARSER_STATE->popScope();
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a91c713d6ed2459beaca418242faa05d1703d48f..7893dd333de236471886d5d4715186b80d1d379f 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1182,7 +1182,12 @@ void Smt2::notifyNamedExpression(api::Term& expr, std::string name)
 {
   checkUserSymbol(name);
   // remember the expression name in the symbol manager
-  getSymbolManager()->setExpressionName(expr, name, false);
+  if (getSymbolManager()->setExpressionName(expr, name, false)
+      == NamingResult::ERROR_IN_BINDER)
+  {
+    parseError(
+        "Cannot name a term in a binder (e.g., quantifiers, definitions)");
+  }
   // define the variable
   defineVar(name, expr);
   // set the last named term, which ensures that we catch when assertions are

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7358ecca4de421bcddcc9a4b7aa74d1cea6e3768..84ed52991a8e94e89e96019652351b763a61bb68 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -735,6 +735,8 @@ set(regress_0_tests
   regress0/parser/linear_arithmetic_err1.smt2
   regress0/parser/linear_arithmetic_err2.smt2
   regress0/parser/linear_arithmetic_err3.smt2
+  regress0/parser/named-attr-error.smt2
+  regress0/parser/named-attr.smt2
   regress0/parser/shadow_fun_symbol_all.smt2
   regress0/parser/shadow_fun_symbol_nirat.smt2
   regress0/parser/strings20.smt2

diff --git a/test/regress/regress0/parser/named-attr-error.smt2 b/test/regress/regress0/parser/named-attr-error.smt2
new file mode 100644 (file)
index 0000000..2b925b8
--- /dev/null
+++ b/test/regress/regress0/parser/named-attr-error.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Cannot name a term in a binder"
+; EXPECT: Cannot name a term in a binder
+; EXIT: 1
+(set-logic QF_UF)
+(define-fun f ((x Bool)) Bool (! x :named foo))

diff --git a/test/regress/regress0/parser/named-attr.smt2 b/test/regress/regress0/parser/named-attr.smt2
new file mode 100644 (file)
index 0000000..b43573c
--- /dev/null
+++ b/test/regress/regress0/parser/named-attr.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(declare-const x Bool)
+(declare-const y Bool)
+(define-fun f () Bool (! x :named foo))
+(define-const g Bool (! y :named bar))
+(assert (and foo bar))
+(set-info :status sat)
+(check-sat)