Refactor handling of global declarations (#5577)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 3 Dec 2020 16:49:08 +0000 (10:49 -0600)
committerGitHub <noreply@github.com>
Thu, 3 Dec 2020 16:49:08 +0000 (10:49 -0600)
commita0b0aebf36c2ba54edc3ae58dc8270a74560d840
tree213e4c6a1c078370ff5268f5d6f4cc55e7be0da1
parentb0dda401af311ffee78936c8b8924b106b92b0c3
Refactor handling of global declarations (#5577)

This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally.

This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API.

This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring.

This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now.
20 files changed:
src/expr/symbol_manager.cpp
src/expr/symbol_manager.h
src/expr/symbol_table.cpp
src/expr/symbol_table.h
src/parser/antlr_input.cpp
src/parser/cvc/Cvc.g
src/parser/cvc/cvc_input.cpp
src/parser/input.cpp
src/parser/input.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/parser_builder.cpp
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/smt2/smt2_input.cpp
src/parser/smt2/sygus_input.cpp
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp_input.cpp
src/smt/command.cpp