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.

2 files changed, 14 insertions, 0 deletions

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)