reset-assertions: Remove all non-global symbols in the parser (#5229)

Fixes #5163. When `:global-declarations` is disabled (the default), then
`(reset-assertions)` should remove all declared and defined symbols. Before
this commit, we would remove the defined function from `SmtEngine` but the
parser would not remove it from its symbol table because the symbol was defined
at (what it considered) level 0. Level 0, however, is reserved for global
symbols that we never want to remove.

This commit adds an additional global `pushScope()`/`popScope()`, similar to
what we have in `SmtEngine`. As a result, user-defined symbols are now defined
at level 1 and get removed from the `SymbolTable` when `(reset-assertions)` is
called. The commit also makes sure that symbols defined by the logic are
asserted at level 0, so that they are not removed by `(reset-assertions)`. It
adds a flag to `defineType` to ignore duplicate definitions because some
symbols are defined by multiple logics, which leads to a failing assertion when
inserting them both at level 0 in the hashmap of the `SymbolTable`. E.g.
strings and integer arithmetic both define `Int`. The commit also fixes
existing unit tests that fail with these stricter semantics of
`(reset-assertions)`.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>

5 files changed, 13 insertions, 1 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cc5c911ff..1eca91a5a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -644,6 +644,7 @@ set(regress_0_tests
   regress0/parser/declarefun-emptyset-uf.smt2
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
+  regress0/parser/issue5163.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/issue5163.smt2 b/test/regress/regress0/parser/issue5163.smt2
new file mode 100644
index 000000000..8bb7c382f
--- /dev/null
+++ b/test/regress/regress0/parser/issue5163.smt2
@@ -0,0 +1,10 @@
+; SCRUBBER: grep -o "Symbol a is not declared"
+; EXPECT: Symbol a is not declared
+; EXIT: 1
+(set-logic ALL)
+(define-fun a () Bool false)
+(reset-assertions)
+(declare-const x Int)
+(assert (and (= (+ x x) 0) true))
+(assert a)
+(check-sat)
diff --git a/test/regress/regress0/smtlib/issue4077.smt2 b/test/regress/regress0/smtlib/issue4077.smt2
index 76a37886b..6ce3f4b01 100644
--- a/test/regress/regress0/smtlib/issue4077.smt2
+++ b/test/regress/regress0/smtlib/issue4077.smt2
@@ -3,6 +3,7 @@
 
 ; Use a quantified logic to make sure that TheoryEngine creates a master
 ; equality engine
+(set-option :global-declarations true)
 (set-logic BV)
 (declare-const x (_ BitVec 4))
 (push)
diff --git a/test/regress/regress0/smtlib/reset-assertions1.smt2 b/test/regress/regress0/smtlib/reset-assertions1.smt2
index 7b4006c5d..244b0ecd9 100644
--- a/test/regress/regress0/smtlib/reset-assertions1.smt2
+++ b/test/regress/regress0/smtlib/reset-assertions1.smt2
@@ -1,5 +1,6 @@
 ; EXPECT: unsat
 ; EXPECT: sat
+(set-option :global-declarations true)
 (set-logic QF_BV)
 (declare-fun v0 () (_ BitVec 4))
 (set-option :produce-models true)
diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2
index 583f94ed4..7e349996d 100644
--- a/test/regress/regress1/sygus/interpol_cosa_1.smt2
+++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2
@@ -12,7 +12,6 @@
 (declare-fun clk@1 () (_ BitVec 1))
 (declare-fun a@1 () (_ BitVec 16))
 (declare-fun b@1 () (_ BitVec 16))
-(reset-assertions)
 (declare-fun cfg@0 () (_ BitVec 1))
 (declare-fun witness_0@0 () Bool)
 (declare-fun counter@0 () (_ BitVec 16))