Eliminate CDHashMap::insertAtContextLevelZero (#8173)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Mar 2022 21:11:05 +0000 (15:11 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Mar 2022 21:11:05 +0000 (21:11 +0000)
commitbcf90d561a60ebce1417950fd570e95199061111
treed70ea88238665507d5bc6b0ffe4d98d45b590afa
parentedfcb4be0617bd28eb9379d8bfe49524ecde3ec1
Eliminate CDHashMap::insertAtContextLevelZero (#8173)

This method unnecessarily complicates the usage of CDHashMap. It had one usage in the current code, for dealing with global declarations. However, this was an entirely artificial use case, as one should properly manage scopes when this option is true (i.e. global-declarations simply disables user-level scoping in the symbol table).

It also simplifies the symbol table so that it doesn't automatically push a global outermost scope. Instead, this scope is pushed when the logic is declared, so that background symbols are correctly added at level 0.

Fixes #4767.
13 files changed:
src/context/cdhashmap.h
src/context/cdhashset.h
src/context/cdinsert_hashmap.h
src/expr/symbol_manager.cpp
src/expr/symbol_table.cpp
src/expr/symbol_table.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp.h
test/unit/context/cdhashmap_black.cpp