Cleanup some includes (#5847)

[cvc5.git] / src / preprocessing / passes / theory_preprocess.cpp

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index a5d054c8b620e9351c6ae12c0be51066d96ee994..50831f585c3a4222bea42d8c06495b72f8c397f9 100644 (file)
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bv_abstraction.cpp
+/*! \file theory_preprocess.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner
+ **   Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -16,7 +16,7 @@
 
 #include "preprocessing/passes/theory_preprocess.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -30,22 +30,41 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "theory-preprocess"){};
 
 PreprocessingPassResult TheoryPreprocess::applyInternal(
-    AssertionPipeline* assertionsToPreprocess)
+    AssertionPipeline* assertions)
 {
-  TheoryEngine* te = d_preprocContext->getTheoryEngine();
-  te->preprocessStart();
-  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+
+  IteSkolemMap& imap = assertions->getIteSkolemMap();
+  PropEngine* propEngine = d_preprocContext->getPropEngine();
+  // Remove all of the ITE occurrences and normalize
+  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
-    TNode a = (*assertionsToPreprocess)[i];
-    Assert(Rewriter::rewrite(a) == a);
-    assertionsToPreprocess->replace(i, te->preprocess(a));
-    a = (*assertionsToPreprocess)[i];
-    Assert(Rewriter::rewrite(a) == a);
+    Node assertion = (*assertions)[i];
+    std::vector<theory::TrustNode> newAsserts;
+    std::vector<Node> newSkolems;
+    TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
+    if (!trn.isNull())
+    {
+      // process
+      assertions->replaceTrusted(i, trn);
+    }
+    Assert(newSkolems.size() == newAsserts.size());
+    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    {
+      imap[newSkolems[j]] = assertions->size();
+      assertions->pushBackTrusted(newAsserts[j]);
+      // new assertions have a dependence on the node (old pf architecture)
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
+                                                 assertion);
+      }
+    }
   }
+
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<TheoryPreprocess> X("theory-preprocess");
 
 }  // namespace passes
 }  // namespace preprocessing