diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-03 10:49:08 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-03 10:49:08 -0600 |
| commit | a0b0aebf36c2ba54edc3ae58dc8270a74560d840 (patch) | |
| tree | 213e4c6a1c078370ff5268f5d6f4cc55e7be0da1 /src/parser/smt2/smt2_input.cpp | |
| parent | b0dda401af311ffee78936c8b8924b106b92b0c3 (diff) | |
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.
Diffstat (limited to 'src/parser/smt2/smt2_input.cpp')
| -rw-r--r-- | src/parser/smt2/smt2_input.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 99907b51a..01eaf7096 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -18,7 +18,6 @@ #include <antlr3.h> -#include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" |