added CEguided, BitBlast, BVAbstraction, UnconstrainedSimp, Rewrite, NotUnsatCores, SepPreSkolemPass classes

4 files changed, 212 insertions, 94 deletions

diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index 6be67362e..26679c771 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -2,10 +2,14 @@
 
 #include <unordered_map>
 #include <string>
+#include "theory/theory.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/sep/theory_sep_rewriter.h"
 #include "options/smt_options.h"
-#include "theory/theory.h"
-
+#include "options/bv_bitblast_mode.h"
+#include "options/bv_options.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+ 
 namespace CVC4 {
 namespace preproc {
 
@@ -73,6 +77,15 @@ Node NlExtPurifyPass::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache,
   return ret;
 }
 
+CEGuidedInstPass::CEGuidedInstPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine){
+}
+
+void CEGuidedInstPass::apply(std::vector<Node>* assertionsToPreprocess){
+    for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
+      d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( (*assertionsToPreprocess)[i] );
+    }
+}
+
 SolveRealAsIntPass::SolveRealAsIntPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
 }
 
@@ -425,26 +438,95 @@ Node SolveIntAsBVPass::intToBV(TNode n, NodeMap& cache) {
   return cache[n_binary];
 }
 
+BitBlastModePass::BitBlastModePass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager) , d_theoryEngine(theoryEngine){
+}
+
+void BitBlastModePass::apply(std::vector<Node>* assertionsToPreprocess){
+  d_theoryEngine->mkAckermanizationAsssertions(*assertionsToPreprocess);
+}
+
+BVAbstractionPass::BVAbstractionPass(ResourceManager* resourceManager, SmtEngine* smt, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_smt(smt), d_theoryEngine(theoryEngine){
+}
+
+void BVAbstractionPass::bvAbstraction(std::vector<Node>* assertionsToPreprocess){
+  Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << std::endl;
+  std::vector<Node> new_assertions;
+  bool changed = d_theoryEngine->ppBvAbstraction(*assertionsToPreprocess, new_assertions);
+  //This method just changes the assertionToPreprocess, so the new_assertions variable is not necessary.
+  //TODO: change how ppBvAbstraction works
+  //order of rewrite also changed around 
+  assertionsToPreprocess->swap(new_assertions);
+ // if we are using the lazy solver and the abstraction
+  // applies, then UF symbols were introduced
+  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
+      changed) {
+    LogicRequest req(*d_smt);
+    req.widenLogic(theory::THEORY_UF);
+  }
+}
+ 
+void BVAbstractionPass::apply(std::vector<Node>* assertionsToPreprocess){
+    dumpAssertions("pre-bv-abstraction", *assertionsToPreprocess);
+    bvAbstraction(assertionsToPreprocess);
+    dumpAssertions("post-bv-abstraction", *assertionsToPreprocess);
+} 
+
+UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager, TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_unconstrainedSimpTime(unconstrainedSimpTime), d_theoryEngine(theoryEngine){
+}
+
+void UnconstrainedSimpPass::apply(std::vector<Node>* assertionsToPreprocess){
+  TimerStat::CodeTimer unconstrainedSimpTimer(d_unconstrainedSimpTime);
+  spendResource(options::preprocessStep());
+  Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << std::endl;
+}
+
+RewritePass::RewritePass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
+}
+
+void RewritePass::apply(std::vector<Node>* assertionsToPreprocess){
+   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
+      (*assertionsToPreprocess)[i] = 
+      theory::Rewriter::rewrite((*assertionsToPreprocess)[i]);
+    }
+}
+
+NotUnsatCoresPass::NotUnsatCoresPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions) : PreprocessingPass(resourceManager), d_topLevelSubstitutions(topLevelSubstitutions){
+}
+
+void NotUnsatCoresPass::apply(std::vector<Node>* assertionsToPreprocess){
+  Chat() << "applying substitutions..." << std::endl;
+      Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                        << "applying substitutions" << std::endl;
+      for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
+        Trace("simplify") << "applying to " << (*assertionsToPreprocess)[i] << std::endl;
+        spendResource(options::preprocessStep());
+        (*assertionsToPreprocess)[i] =
+          theory::Rewriter::rewrite(d_topLevelSubstitutions->apply((*assertionsToPreprocess)[i]));
+        Trace("simplify") << "  got " << (*assertionsToPreprocess)[i] << std::endl;
+       }
+}
+     
+BVToBoolPass::BVToBoolPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager) , d_theoryEngine(theoryEngine){
+}
+
 void BVToBoolPass::apply(std::vector<Node>* assertionsToPreprocess){
   dumpAssertions("pre-bv-to-bool", *assertionsToPreprocess);
   Chat() << "...doing bvToBool..." << std::endl;
   bvToBool(assertionsToPreprocess);
+  //A rewrite pass was formerly here that has been moved to after the dump
   dumpAssertions("post-bv-to-bool", *assertionsToPreprocess);
   Trace("smt") << "POST bvToBool" << std::endl;
 }
 
-BVToBoolPass::BVToBoolPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager) , d_theoryEngine(theoryEngine){
-}
-
 void BVToBoolPass::bvToBool(std::vector<Node>* assertionsToPreprocess) {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << std::endl;
   spendResource(options::preprocessStep());
   std::vector<Node> new_assertions;
   d_theoryEngine->ppBvToBool((*assertionsToPreprocess), new_assertions);
-  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
-    (*assertionsToPreprocess)[i] =
-      theory::Rewriter::rewrite(new_assertions[i]);
-  }
+  //This method just changes the assertionToPreprocess, so the new_assertions variable is not necessary.
+  //TODO: change how ppBvToBool works
+  //order of rewrite also changed around 
+  assertionsToPreprocess->swap(new_assertions);
 }
 
 BoolToBVPass::BoolToBVPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager) , d_theoryEngine(theoryEngine){
@@ -455,10 +537,10 @@ void BoolToBVPass::boolToBv(std::vector<Node>* assertionsToPreprocess) {
   spendResource(options::preprocessStep());
   std::vector<Node> new_assertions;
   d_theoryEngine->ppBoolToBv((*assertionsToPreprocess), new_assertions);
-  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
-    (*assertionsToPreprocess)[i] = 
-      theory::Rewriter::rewrite(new_assertions[i]);
-   }
+  //This method just changes the assertionToPreprocess, so the new_assertions variable is not necessary.
+  // TODO: change how ppBooltoBv works
+  //Order of rewrite also changed around  
+  assertionsToPreprocess->swap(new_assertions);
 }
 
 void BoolToBVPass::apply(std::vector<Node>* assertionsToPreprocess){
@@ -469,5 +551,20 @@ void BoolToBVPass::apply(std::vector<Node>* assertionsToPreprocess){
     Trace("smt") << "POST boolToBv" << std::endl;
 }
 
+SepPreSkolemEmpPass::SepPreSkolemEmpPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
+}
+
+void SepPreSkolemEmpPass::apply(std::vector<Node>* assertionsToPreprocess){
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
+      Node prev = (*assertionsToPreprocess)[i];
+      Node next = theory::sep::TheorySepRewriter::preprocess( prev );
+      if( next!=prev ){
+        (*assertionsToPreprocess)[i] = theory::Rewriter::rewrite( next );
+        Trace("sep-preprocess") << "*** Preprocess sep " << prev << std::endl;
+        Trace("sep-preprocess") << "   ...got " << (*assertionsToPreprocess)[i] << std::endl;
+       }
+  }
+}
+
 }  // namespace preproc
 }  // namespace CVC4
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index 60d1030d7..383735cbe 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -4,6 +4,7 @@
 #define __CVC4__PREPROC__PREPROCESSING_PASSES_CORE_H
 
 #include "preproc/preprocessing_pass.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace preproc {
@@ -20,6 +21,14 @@ class NlExtPurifyPass : public PreprocessingPass {
                      std::vector<Node>& var_eq, bool beneathMult = false);
 };
 
+class CEGuidedInstPass : public PreprocessingPass {
+ public:
+  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  CEGuidedInstPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine);
+ private:
+  TheoryEngine* d_theoryEngine;
+};
+ 
 // TODO: add classes for other preprocessing steps here
 class SolveRealAsIntPass : public PreprocessingPass {
  public:
@@ -38,6 +47,50 @@ class SolveIntAsBVPass : public PreprocessingPass {
   Node intToBVMakeBinary(TNode n, NodeMap& cache); 
 };
 
+class BitBlastModePass : public PreprocessingPass {
+ public:
+   virtual void apply(std::vector<Node>* assertionsToPreprocess);
+   BitBlastModePass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); 
+ private:
+   TheoryEngine* d_theoryEngine;
+};
+
+class BVAbstractionPass : public PreprocessingPass {
+ public: 
+  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  BVAbstractionPass(ResourceManager* resourceManager, SmtEngine* smt, TheoryEngine* theoryEngine);
+ private:
+  SmtEngine* d_smt;
+  TheoryEngine* d_theoryEngine;
+  // Abstract common structure over small domains to UF
+  // return true if changes were made.
+  void bvAbstraction(std::vector<Node>* assertionsToPreprocess);  
+};
+
+class UnconstrainedSimpPass : public PreprocessingPass {
+ public:
+  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  UnconstrainedSimpPass(ResourceManager* resourceManager, TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine);
+ private:
+  TimerStat d_unconstrainedSimpTime;
+  TheoryEngine* d_theoryEngine;
+  // Simplify based on unconstrained values
+};
+
+class RewritePass : public PreprocessingPass {
+ public:
+    virtual void apply(std::vector<Node>* assertionsToPreprocess);
+    RewritePass(ResourceManager* resourceManager);
+};
+ 
+class NotUnsatCoresPass : public PreprocessingPass {
+ public:
+    virtual void apply(std::vector<Node>* assertionsToPreprocess);
+    NotUnsatCoresPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions);
+ private:
+    theory::SubstitutionMap* d_topLevelSubstitutions;
+};
+ 
 class BVToBoolPass : public PreprocessingPass {
  public:
    virtual void apply(std::vector<Node>* assertionsToPreprocess);
@@ -58,6 +111,12 @@ class BoolToBVPass : public PreprocessingPass {
   void boolToBv(std::vector<Node>* assertionsToPreprocess);
 };
 
+class SepPreSkolemEmpPass : public PreprocessingPass {
+  public:
+   virtual void apply(std::vector<Node>* assertionsToPreprocess);
+   SepPreSkolemEmpPass(ResourceManager* resourceManager);
+};
+
 }  // namespace preproc
 }  // namespace CVC4
 
diff --git a/src/smt/.smt_engine.cpp.swo b/src/smt/.smt_engine.cpp.swo
new file mode 100644
index 000000000..72c40172c
--- /dev/null
+++ b/src/smt/.smt_engine.cpp.swo
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f87a866c1..8d519e0ef 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -596,17 +596,9 @@ private:
    * ite removal.
    */
   bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
-
-  // Abstract common structure over small domains to UF
-  // return true if changes were made.
-  void bvAbstraction();
-
-  // Simplify ITE structure
+ // Simplify ITE structure
   bool simpITE();
 
-  // Simplify based on unconstrained values
-  void unconstrainedSimp();
-
   /**
    * Ensures the assertions asserted after before now effectively come before
    * d_realAssertionsEnd.
@@ -2783,22 +2775,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   return true;
 }
 
-void SmtEnginePrivate::bvAbstraction() {
-  Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl;
-  std::vector<Node> new_assertions;
-  bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions);
-  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-    d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
-  }
-  // if we are using the lazy solver and the abstraction
-  // applies, then UF symbols were introduced
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
-      changed) {
-    LogicRequest req(d_smt);
-    req.widenLogic(THEORY_UF);
-  }
-}
-
 bool SmtEnginePrivate::simpITE() {
   TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
 
@@ -2853,13 +2829,6 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
   Assert(d_assertions.size() == before);
 }
 
-void SmtEnginePrivate::unconstrainedSimp() {
-  TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
-  spendResource(options::preprocessStep());
-  Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
-  d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
-}
-
 void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
   for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
@@ -3334,8 +3303,9 @@ bool SmtEnginePrivate::simplifyAssertions()
     // Unconstrained simplification
     if(options::unconstrainedSimp()) {
       Chat() << "...doing unconstrained simplification..." << endl;
-      unconstrainedSimp();
-    }
+      preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine);
+      pass.apply(&d_assertions.ref());
+   }
 
     dumpAssertions("post-unconstrained", d_assertions);
     Trace("smt") << "POST unconstrainedSimp" << endl;
@@ -3552,10 +3522,9 @@ void SmtEnginePrivate::processAssertions() {
 
   if( options::ceGuidedInst() ){
     //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] );
-    }
-  }
+    preproc::CEGuidedInstPass pass(d_resourceManager, d_smt.d_theoryEngine);
+    pass.apply(&d_assertions.ref());
+ }
 
   if (options::solveRealAsInt()) {
    preproc::SolveRealAsIntPass pass(d_resourceManager);
@@ -3577,15 +3546,18 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref());
+    preproc::BitBlastModePass pass(d_resourceManager, d_smt.d_theoryEngine);
+    pass.apply(&d_assertions.ref());   
   }
 
   if ( options::bvAbstraction() &&
       !options::incrementalSolving()) {
-    dumpAssertions("pre-bv-abstraction", d_assertions);
-    bvAbstraction();
-    dumpAssertions("post-bv-abstraction", d_assertions);
-  }
+    preproc::BVAbstractionPass pass(d_resourceManager, &d_smt, d_smt.d_theoryEngine);
+    pass.apply(&d_assertions.ref());
+
+    preproc::RewritePass pass1(d_resourceManager);
+    pass1.apply(&d_assertions.ref());
+ }
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
@@ -3593,16 +3565,19 @@ void SmtEnginePrivate::processAssertions() {
 
   // Unconstrained simplification
   if(options::unconstrainedSimp()) {
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << std::endl;
     dumpAssertions("pre-unconstrained-simp", d_assertions);
-    Chat() << "...doing unconstrained simplification..." << endl;
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
-    }
-    unconstrainedSimp();
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
+    Chat() << "...doing unconstrained simplification..." << std::endl;
+    
+    preproc::RewritePass pass(d_resourceManager);
+    pass.apply(&d_assertions.ref());    
+
+    preproc::UnconstrainedSimpPass pass1(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine);
+    pass1.apply(&d_assertions.ref());
+ 
+   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << std::endl;
     dumpAssertions("post-unconstrained-simp", d_assertions);
-  }
+ }
 
   if(options::bvIntroducePow2()){
     theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
@@ -3613,23 +3588,15 @@ void SmtEnginePrivate::processAssertions() {
 
   if(options::unsatCores()) {
     // special rewriting pass for unsat cores, since many of the passes below are skipped
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
-    }
+    preproc::RewritePass pass(d_resourceManager);
+    pass.apply(&d_assertions.ref());
   } else {
     // Apply the substitutions we already have, and normalize
-    if(!options::unsatCores()) {
-      Chat() << "applying substitutions..." << endl;
-      Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
-                        << "applying substitutions" << endl;
-      for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-        Trace("simplify") << "applying to " << d_assertions[i] << endl;
-        spendResource(options::preprocessStep());
-        d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
-        Trace("simplify") << "  got " << d_assertions[i] << endl;
-      }
-    }
+    //unsatCore check removed for redundancy
+    preproc::NotUnsatCoresPass pass1(d_resourceManager, &d_topLevelSubstitutions);
+    pass1.apply(&d_assertions.ref()); 
   }
+
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl;
   dumpAssertions("post-substitution", d_assertions);
 
@@ -3639,29 +3606,24 @@ void SmtEnginePrivate::processAssertions() {
   if(options::bitvectorToBool()) {
     preproc::BVToBoolPass pass(d_resourceManager, d_smt.d_theoryEngine);
     pass.apply(&d_assertions.ref());
- }
+
+    preproc::RewritePass pass1(d_resourceManager);
+    pass1.apply(&d_assertions.ref());
+  }
+
   // Convert non-top-level Booleans to bit-vectors of size 1
   if(options::boolToBitvector()) {
     preproc::BoolToBVPass pass(d_resourceManager, d_smt.d_theoryEngine);
     pass.apply(&d_assertions.ref());
 
-   /* dumpAssertions("pre-bool-to-bv", d_assertions);
-    Chat() << "...doing boolToBv..." << endl;
-    boolToBv();
-    dumpAssertions("post-bool-to-bv", d_assertions);
-    Trace("smt") << "POST boolToBv" << endl;*/
+    preproc::RewritePass pass1(d_resourceManager);
+    pass1.apply(&d_assertions.ref());
   }
+
   if(options::sepPreSkolemEmp()) {
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Node prev = d_assertions[i];
-      Node next = sep::TheorySepRewriter::preprocess( prev );
-      if( next!=prev ){
-        d_assertions.replace( i, Rewriter::rewrite( next ) );
-        Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
-        Trace("sep-preprocess") << "   ...got " << d_assertions[i] << endl;
-      }
-    }
-  }
+    preproc::SepPreSkolemEmpPass pass(d_resourceManager);
+    pass.apply(&d_assertions.ref());
+ }
 
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;