Add symbol manager (#5380)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 9 Nov 2020 22:51:04 +0000 (16:51 -0600)
committerGitHub <noreply@github.com>
Mon, 9 Nov 2020 22:51:04 +0000 (16:51 -0600)
commitb5eb623ea33eeb257d61a18c44e9aa1b2aafabbb
tree4c1e3ff13161d844569349a17e06761cedfc3ceb
parentbf98dd46aa92241d33901e84a437536ad5010be1
Add symbol manager (#5380)

This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.

The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.

This PR adds the basic interface for the symbol manager and passes it to the parser.

Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.

Marking "complex" since this impacts further design of the parser and the code that lives in src/main.

FYI @4tXJ7f
23 files changed:
src/CMakeLists.txt
src/main/command_executor.cpp
src/main/command_executor.h
src/main/driver_unified.cpp
src/main/interactive_shell.cpp
src/main/interactive_shell.h
src/parser/CMakeLists.txt
src/parser/cvc/cvc.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/parser_builder.cpp
src/parser/parser_builder.h
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/symbol_manager.cpp [new file with mode: 0644]
src/parser/symbol_manager.h [new file with mode: 0644]
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp.h
test/api/ouroborous.cpp
test/api/smt2_compliance.cpp
test/unit/main/interactive_shell_black.h
test/unit/parser/parser_black.h
test/unit/parser/parser_builder_black.h