reset-assertions: Remove all non-global symbols in the parser (#5229)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 9 Oct 2020 05:28:42 +0000 (22:28 -0700)
committerGitHub <noreply@github.com>
Fri, 9 Oct 2020 05:28:42 +0000 (22:28 -0700)
commit36addc33791da4b1fbae9fbcec87ac26cfc7a270
treec7eee80da27439ed684a12afe22382bae43b4e35
parente5913461e103bd1c7740e88f748524ae66672b53
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>
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/preprocessing/passes/ho_elim.cpp
src/preprocessing/passes/ho_elim.h
test/regress/CMakeLists.txt
test/regress/regress0/parser/issue5163.smt2 [new file with mode: 0644]
test/regress/regress0/smtlib/issue4077.smt2
test/regress/regress0/smtlib/reset-assertions1.smt2
test/regress/regress1/sygus/interpol_cosa_1.smt2