From 4e6e168a5eb578df2bfd12becf7732cbdd23bc3a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 18 May 2021 18:27:09 -0700 Subject: 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. --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/parser/named-attr-error.smt2 | 6 ++++++ test/regress/regress0/parser/named-attr.smt2 | 8 ++++++++ 3 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/parser/named-attr-error.smt2 create mode 100644 test/regress/regress0/parser/named-attr.smt2 (limited to 'test/regress') 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) -- cgit v1.2.3