Move ownership of theory preprocessor to TheoryProxy (#5690)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 21 Dec 2020 17:48:22 +0000 (11:48 -0600)
committerGitHub <noreply@github.com>
Mon, 21 Dec 2020 17:48:22 +0000 (11:48 -0600)
commitccda071a9605baa42602d580affa296cbc674807
treeb45ff0d8259292895367c7f35754f54f402dd49d
parent0c2a43ab616c3670f3077758defcaa1f61cbe291
Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.
src/preprocessing/passes/ite_removal.cpp
src/preprocessing/passes/theory_preprocess.cpp
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/process_assertions.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_preprocessor.h