Move preprocessor to smt solver (#7321)

This breaks the circular dependency of preprocessing pass context of solver engine.

It also moves the preprocessor to be owned by SMT solver, instead of Solver engine.

It also changes the behavior of reset assertions: now, the preprocessing pass context is reset, whereas previously it was not. I believe this is the right behavior, as it eliminates stale data (e.g. learned literals, symbols in assertion cache).

1 files changed, 4 insertions, 1 deletions

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index aef461173..aca4239d5 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -46,7 +46,10 @@ class TestPPWhiteBVGauss : public TestSmt
     TestSmt::SetUp();
 
     d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
-        d_slvEngine.get(), d_slvEngine->getEnv(), nullptr));
+        d_slvEngine->getEnv(),
+        d_slvEngine->getTheoryEngine(),
+        d_slvEngine->getPropEngine(),
+        nullptr));
 
     d_bv_gauss.reset(new BVGauss(d_preprocContext.get()));