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.

7 files changed, 60 insertions, 26 deletions

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index c6eb8d08e..8d4870966 100644
--- 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 6cd0a1467..271825e07 100644
--- 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 dc9a324bb..58f229cfe 100644
--- 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 a91c713d6..7893dd333 100644
--- 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 7358ecca4..84ed52991 100644
--- 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
index 000000000..2b925b8ce
--- /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
index 000000000..b43573c26
--- /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)