Split preprocessor from SmtEngine (#4854)

This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal).

It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 2419962aa..8810acbe8 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -112,8 +112,8 @@ Result checkWithSubsolver(Node query,
   {
     for (const Node& v : vars)
     {
-      Expr val = smte->getValue(v.toExpr());
-      modelVals.push_back(Node::fromExpr(val));
+      Node val = smte->getValue(v);
+      modelVals.push_back(val);
     }
   }
   return r;