Move ownership of term formula removal to theory preprocessor (#5670)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Dec 2020 15:03:45 +0000 (09:03 -0600)
committerGitHub <noreply@github.com>
Wed, 16 Dec 2020 15:03:45 +0000 (09:03 -0600)
commit3a3735d58ddac7ecfac80dad35da963901f15f55
tree1aa213359a6637f571f22f3db7434bb75a8fc93e
parent5b90fdad09209da667cc281f5425300a4b2bb9c9
Move ownership of term formula removal to theory preprocessor (#5670)

This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.

This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.

The next step will move the TheoryPreprocessor inside prop::TheoryProxy.

There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.
13 files changed:
src/preprocessing/passes/ite_removal.cpp
src/preprocessing/preprocessing_pass_context.cpp
src/preprocessing/preprocessing_pass_context.h
src/smt/check_models.cpp
src/smt/preprocessor.cpp
src/smt/preprocessor.h
src/smt/smt_solver.cpp
src/smt/term_formula_removal.cpp
src/smt/term_formula_removal.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_preprocessor.cpp
src/theory/theory_preprocessor.h