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.

5 files changed, 6 insertions, 6 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 835dc1dba..07d798901 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -172,7 +172,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
             if (val.isNull())
             {
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
-              val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
+              val = rrChecker->getValue(refv);
             }
             Trace("rr-check") << "  " << v << " -> " << val << std::endl;
             pt.push_back(val);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index a7f32155c..9126aad94 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -597,7 +597,7 @@ void CegisCoreConnective::getModel(SmtEngine& smt,
 {
   for (const Node& v : d_vars)
   {
-    Node mv = Node::fromExpr(smt.getValue(v.toExpr()));
+    Node mv = smt.getValue(v);
     Trace("sygus-ccore-model") << v << " -> " << mv << " ";
     vals.push_back(mv);
   }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 2514b05e2..5ceac24b6 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -250,7 +250,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   {
     Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
     Node fov = d_sk_to_fo[v];
-    Node fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
+    Node fov_m = repcChecker->getValue(fov);
     Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
     // convert to sygus
     Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
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;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 70f46d6e5..4c7600da2 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -174,7 +174,7 @@ bool TheoryModel::isModelCoreSymbol(Expr sym) const
 Expr TheoryModel::getValue( Expr expr ) const{
   Node n = Node::fromExpr( expr );
   Node ret = getValue( n );
-  return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
+  return ret.toExpr();
 }
 
 /** get cardinality for sort */