Fixed bugs for tests up to isQuantified flag

4 files changed, 221 insertions, 102 deletions

diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h
index 78afd629e..ee719e2c4 100644
--- a/src/preproc/preprocessing_pass.h
+++ b/src/preproc/preprocessing_pass.h
@@ -12,12 +12,38 @@
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
+
+namespace smt {
+class AssertionPipeline {
+  std::vector<Node> d_nodes;
+
+public:
+
+  size_t size() const { return d_nodes.size(); }
+
+  void resize(size_t n) { d_nodes.resize(n); }
+  void clear() { d_nodes.clear(); }
+
+  Node& operator[](size_t i) { return d_nodes[i]; }
+  const Node& operator[](size_t i) const { return d_nodes[i]; }
+  void push_back(Node n) { d_nodes.push_back(n); }
+
+  std::vector<Node>& ref() { return d_nodes; }
+  const std::vector<Node>& ref() const { return d_nodes; }
+
+  void replace(size_t i, Node n) {
+    PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
+    d_nodes[i] = n;
+  }
+};// class AssertionPipeline 
+} //namespace smt
+
 namespace preproc {
 
 class PreprocessingPass {
  public:
-  virtual void apply(std::vector<Node>* assertionsToPreprocess) = 0;
-  void dumpAssertions(const char* key, const std::vector<Node>& assertionList) {
+  virtual void apply(smt::AssertionPipeline* assertionsToPreprocess) = 0;
+  void dumpAssertions(const char* key, const smt::AssertionPipeline& assertionList) {
   if( Dump.isOn("assertions") &&
       Dump.isOn(std::string("assertions:") + key) ) {
     // Push the simplified assertions to the dump output stream
diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index b389fa142..d364f17ce 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -17,28 +17,26 @@
 namespace CVC4 {
 namespace preproc {
 
-NlExtPurifyPass::NlExtPurifyPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
+NlExtPurifyPass::NlExtPurifyPass(ResourceManager* resourceManager) :
+    PreprocessingPass(resourceManager){
 }
 
-void NlExtPurifyPass::apply(std::vector<Node>* assertionsToPreprocess) {
+void NlExtPurifyPass::apply(smt::AssertionPipeline* assertionsToPreprocess) {
   std::unordered_map<Node, Node, NodeHashFunction> cache;
   std::unordered_map<Node, Node, NodeHashFunction> bcache;
   std::vector<Node> var_eq;
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) {
-    (*assertionsToPreprocess)[i] =
-        purifyNlTerms((*assertionsToPreprocess)[i], cache, bcache, var_eq);
+    assertionsToPreprocess->replace(i, purifyNlTerms((*assertionsToPreprocess)[i], cache, bcache, var_eq));
   }
   if (!var_eq.empty()) {
     unsigned lastIndex = assertionsToPreprocess->size() - 1;
     var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]);
-    (*assertionsToPreprocess)[lastIndex] =
-        NodeManager::currentNM()->mkNode(kind::AND, var_eq);
+    assertionsToPreprocess->replace(lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq) );
   }
 }
 
-Node NlExtPurifyPass::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache,
-                                    std::vector<Node>& var_eq,
-                                    bool beneathMult) {
+Node NlExtPurifyPass::purifyNlTerms(TNode n, NodeMap& cache,
+   NodeMap& bcache, std::vector<Node>& var_eq, bool beneathMult) {
   if (beneathMult) {
     NodeMap::iterator find = bcache.find(n);
     if (find != bcache.end()) {
@@ -81,25 +79,27 @@ Node NlExtPurifyPass::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache,
   return ret;
 }
 
-CEGuidedInstPass::CEGuidedInstPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine){
+CEGuidedInstPass::CEGuidedInstPass(ResourceManager* resourceManager,
+    TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), 
+    d_theoryEngine(theoryEngine){
 }
 
-void CEGuidedInstPass::apply(std::vector<Node>* assertionsToPreprocess){
+void CEGuidedInstPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
     for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
       d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( (*assertionsToPreprocess)[i] );
     }
 }
 
-SolveRealAsIntPass::SolveRealAsIntPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
+SolveRealAsIntPass::SolveRealAsIntPass(ResourceManager* resourceManager) :
+     PreprocessingPass(resourceManager){
 }
 
-void SolveRealAsIntPass::apply(std::vector<Node>* assertionsToPreprocess) {
+void SolveRealAsIntPass::apply(smt::AssertionPipeline* assertionsToPreprocess) {
  Chat() << "converting reals to ints..." << std::endl;
  std::unordered_map<Node, Node, NodeHashFunction> cache;
  std::vector<Node> var_eq;
  for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
- (*assertionsToPreprocess)[i] = 
-  realToInt((*assertionsToPreprocess)[i], cache, var_eq);
+ assertionsToPreprocess->replace(i, realToInt((*assertionsToPreprocess)[i], cache, var_eq) );
  }
    /* these comments were here before
     if( !var_eq.empty() ){
@@ -198,16 +198,16 @@ Node SolveRealAsIntPass::realToInt(TNode n, NodeMap& cache, std::vector< Node >&
   }
 }
 
-SolveIntAsBVPass::SolveIntAsBVPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
+SolveIntAsBVPass::SolveIntAsBVPass(ResourceManager* resourceManager) :
+    PreprocessingPass(resourceManager){
 }
 
-void SolveIntAsBVPass::apply(std::vector<Node>* assertionsToPreprocess)
+void SolveIntAsBVPass::apply(smt::AssertionPipeline* assertionsToPreprocess)
 {
   Chat() << "converting ints to bit-vectors..." << std::endl;
   std::unordered_map<Node, Node, NodeHashFunction> cache;
   for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
-  (*assertionsToPreprocess)[i] =
-    intToBV((*assertionsToPreprocess)[i], cache);
+  assertionsToPreprocess->replace(i, intToBV((*assertionsToPreprocess)[i], cache) );
   }
 }
 
@@ -442,24 +442,29 @@ Node SolveIntAsBVPass::intToBV(TNode n, NodeMap& cache) {
   return cache[n_binary];
 }
 
-BitBlastModePass::BitBlastModePass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager) , d_theoryEngine(theoryEngine){
+BitBlastModePass::BitBlastModePass(ResourceManager* resourceManager,
+     TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager),
+     d_theoryEngine(theoryEngine){
 }
 
-void BitBlastModePass::apply(std::vector<Node>* assertionsToPreprocess){
-  d_theoryEngine->mkAckermanizationAsssertions(*assertionsToPreprocess);
+void BitBlastModePass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+  d_theoryEngine->mkAckermanizationAsssertions(assertionsToPreprocess->ref());
 }
 
-BVAbstractionPass::BVAbstractionPass(ResourceManager* resourceManager, SmtEngine* smt, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_smt(smt), d_theoryEngine(theoryEngine){
+BVAbstractionPass::BVAbstractionPass(ResourceManager* resourceManager,
+     SmtEngine* smt, TheoryEngine* theoryEngine) : 
+     PreprocessingPass(resourceManager), d_smt(smt), 
+     d_theoryEngine(theoryEngine){
 }
 
-void BVAbstractionPass::bvAbstraction(std::vector<Node>* assertionsToPreprocess){
+void BVAbstractionPass::bvAbstraction(smt::AssertionPipeline* assertionsToPreprocess){
   Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << std::endl;
   std::vector<Node> new_assertions;
-  bool changed = d_theoryEngine->ppBvAbstraction(*assertionsToPreprocess, new_assertions);
+  bool changed = d_theoryEngine->ppBvAbstraction(assertionsToPreprocess->ref(), 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);
+ assertionsToPreprocess->ref().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 &&
@@ -469,51 +474,60 @@ void BVAbstractionPass::bvAbstraction(std::vector<Node>* assertionsToPreprocess)
   }
 }
  
-void BVAbstractionPass::apply(std::vector<Node>* assertionsToPreprocess){
+void BVAbstractionPass::apply(smt::AssertionPipeline* 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){
+UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager,
+      TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine) :
+      PreprocessingPass(resourceManager), 
+      d_unconstrainedSimpTime(unconstrainedSimpTime), 
+      d_theoryEngine(theoryEngine){
 }
 
-void UnconstrainedSimpPass::apply(std::vector<Node>* assertionsToPreprocess){
+void UnconstrainedSimpPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
   TimerStat::CodeTimer unconstrainedSimpTimer(d_unconstrainedSimpTime);
   spendResource(options::preprocessStep());
   Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << std::endl;
+  d_theoryEngine->ppUnconstrainedSimp(assertionsToPreprocess->ref());
 }
 
-RewritePass::RewritePass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
+RewritePass::RewritePass(ResourceManager* resourceManager) : 
+    PreprocessingPass(resourceManager){
 }
 
-void RewritePass::apply(std::vector<Node>* assertionsToPreprocess){
+void RewritePass::apply(smt::AssertionPipeline* assertionsToPreprocess){
    for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
-      (*assertionsToPreprocess)[i] = 
-      theory::Rewriter::rewrite((*assertionsToPreprocess)[i]);
+    assertionsToPreprocess->replace(i, theory::Rewriter::rewrite((*assertionsToPreprocess)[i]));
     }
 }
 
-NotUnsatCoresPass::NotUnsatCoresPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions) : PreprocessingPass(resourceManager), d_topLevelSubstitutions(topLevelSubstitutions){
+NotUnsatCoresPass::NotUnsatCoresPass(ResourceManager* resourceManager, 
+     theory::SubstitutionMap* topLevelSubstitutions) : 
+     PreprocessingPass(resourceManager), 
+     d_topLevelSubstitutions(topLevelSubstitutions){
 }
 
-void NotUnsatCoresPass::apply(std::vector<Node>* assertionsToPreprocess){
+void NotUnsatCoresPass::apply(smt::AssertionPipeline* 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]));
+        assertionsToPreprocess->replace(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){
+BVToBoolPass::BVToBoolPass(ResourceManager* resourceManager,
+      TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager),
+      d_theoryEngine(theoryEngine){
 }
 
-void BVToBoolPass::apply(std::vector<Node>* assertionsToPreprocess){
+void BVToBoolPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
   dumpAssertions("pre-bv-to-bool", *assertionsToPreprocess);
   Chat() << "...doing bvToBool..." << std::endl;
   bvToBool(assertionsToPreprocess);
@@ -522,32 +536,34 @@ void BVToBoolPass::apply(std::vector<Node>* assertionsToPreprocess){
   Trace("smt") << "POST bvToBool" << std::endl;
 }
 
-void BVToBoolPass::bvToBool(std::vector<Node>* assertionsToPreprocess) {
+void BVToBoolPass::bvToBool(smt::AssertionPipeline* assertionsToPreprocess) {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << std::endl;
   spendResource(options::preprocessStep());
   std::vector<Node> new_assertions;
-  d_theoryEngine->ppBvToBool((*assertionsToPreprocess), new_assertions);
+  d_theoryEngine->ppBvToBool(assertionsToPreprocess->ref(), new_assertions);
   //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);
+  assertionsToPreprocess->ref().swap(new_assertions);
 }
 
-BoolToBVPass::BoolToBVPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager) , d_theoryEngine(theoryEngine){
+BoolToBVPass::BoolToBVPass(ResourceManager* resourceManager,
+     TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager),
+     d_theoryEngine(theoryEngine){
 }
   
-void BoolToBVPass::boolToBv(std::vector<Node>* assertionsToPreprocess) {
+void BoolToBVPass::boolToBv(smt::AssertionPipeline* assertionsToPreprocess) {
   Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << std::endl;
   spendResource(options::preprocessStep());
   std::vector<Node> new_assertions;
-  d_theoryEngine->ppBoolToBv((*assertionsToPreprocess), new_assertions);
+  d_theoryEngine->ppBoolToBv(assertionsToPreprocess->ref(), new_assertions);
   //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);
+  assertionsToPreprocess->ref().swap(new_assertions);
 }
 
-void BoolToBVPass::apply(std::vector<Node>* assertionsToPreprocess){
+void BoolToBVPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
     dumpAssertions("pre-bool-to-bv", *assertionsToPreprocess);
     Chat() << "...doing boolToBv..." << std::endl;
     boolToBv(assertionsToPreprocess);
@@ -558,22 +574,29 @@ void BoolToBVPass::apply(std::vector<Node>* assertionsToPreprocess){
 SepPreSkolemEmpPass::SepPreSkolemEmpPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
 }
 
-void SepPreSkolemEmpPass::apply(std::vector<Node>* assertionsToPreprocess){
+void SepPreSkolemEmpPass::apply(smt::AssertionPipeline* 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 );
+        assertionsToPreprocess->replace(i, theory::Rewriter::rewrite( next ));
         Trace("sep-preprocess") << "*** Preprocess sep " << prev << std::endl;
         Trace("sep-preprocess") << "   ...got " << (*assertionsToPreprocess)[i] << std::endl;
        }
   }
 }
 
-QuantifiedPass::QuantifiedPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined, std::map<Node,TypeNode> fmfRecFunctionsAbs, std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_fmfRecFunctionsDefined(fmfRecFunctionsDefined), d_fmfRecFunctionsAbs(fmfRecFunctionsAbs), d_fmfRecFunctionsConcrete(fmfRecFunctionsConcrete){
+QuantifiedPass::QuantifiedPass(ResourceManager* resourceManager, 
+   TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined, 
+   std::map<Node,TypeNode> fmfRecFunctionsAbs, 
+   std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete) : 
+   PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), 
+   d_fmfRecFunctionsDefined(fmfRecFunctionsDefined), 
+   d_fmfRecFunctionsAbs(fmfRecFunctionsAbs), 
+   d_fmfRecFunctionsConcrete(fmfRecFunctionsConcrete){
 }
 
-void QuantifiedPass::apply(std::vector<Node>* assertionsToPreprocess){
+void QuantifiedPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl;
 
     dumpAssertions("pre-skolem-quant", *assertionsToPreprocess);
@@ -582,7 +605,7 @@ void QuantifiedPass::apply(std::vector<Node>* assertionsToPreprocess){
       Node prev = (*assertionsToPreprocess)[i];
       Node next = theory::quantifiers::QuantifiersRewriter::preprocess( prev );
       if( next!=prev ){
-        (*assertionsToPreprocess)[i] = theory::Rewriter::rewrite( next );
+        assertionsToPreprocess->replace(i, theory::Rewriter::rewrite( next ) );
         Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev <<std::endl;
         Trace("quantifiers-preprocess") << "   ...got " << (*assertionsToPreprocess)[i] << std::endl;
       }
@@ -593,7 +616,7 @@ void QuantifiedPass::apply(std::vector<Node>* assertionsToPreprocess){
       theory::quantifiers::QuantifierMacros qm( d_theoryEngine->getQuantifiersEngine() );
       bool success;
       do{
-        success = qm.simplify( *assertionsToPreprocess, true );
+        success = qm.simplify( assertionsToPreprocess->ref(), true );
       }while( success );
       //finalize the definitions
       qm.finalizeDefinitions();
@@ -616,7 +639,7 @@ void QuantifiedPass::apply(std::vector<Node>* assertionsToPreprocess){
           fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
         }
       }
-      fdf.simplify(*assertionsToPreprocess);
+      fdf.simplify(assertionsToPreprocess->ref());
       //must store new definitions (for incremental)
       for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
         Node f = fdf.d_funcs[i];
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index d445e2e14..8470feefb 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -5,6 +5,7 @@
 
 #include "preproc/preprocessing_pass.h"
 #include "theory/substitutions.h"
+#include "smt/smt_engine.h"
 
 namespace CVC4 {
 namespace preproc {
@@ -15,7 +16,7 @@ typedef context::CDList<Node> NodeList;
   
 class NlExtPurifyPass : public PreprocessingPass {
  public:
-  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
   NlExtPurifyPass(ResourceManager* resourceManager);
  private:
   Node purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache,
@@ -24,16 +25,15 @@ class NlExtPurifyPass : public PreprocessingPass {
 
 class CEGuidedInstPass : public PreprocessingPass {
  public:
-  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
   CEGuidedInstPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine);
  private:
   TheoryEngine* d_theoryEngine;
 };
  
-// TODO: add classes for other preprocessing steps here
 class SolveRealAsIntPass : public PreprocessingPass {
  public:
-  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
   SolveRealAsIntPass(ResourceManager* resourceManager);
  private:
   Node realToInt(TNode n, NodeMap& cache, std::vector<Node>& var_eq);
@@ -41,7 +41,7 @@ class SolveRealAsIntPass : public PreprocessingPass {
 
 class SolveIntAsBVPass : public PreprocessingPass {
  public:
-  virtual void apply(std::vector<Node>* assertionsToPreprocess);
+  virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
   SolveIntAsBVPass(ResourceManager* resourceManager);
  private:
   Node intToBV(TNode n, NodeToNodeHashMap& cache);
@@ -50,28 +50,31 @@ class SolveIntAsBVPass : public PreprocessingPass {
 
 class BitBlastModePass : public PreprocessingPass {
  public:
-   virtual void apply(std::vector<Node>* assertionsToPreprocess);
-   BitBlastModePass(ResourceManager* resourceManager, TheoryEngine* theoryEngine); 
+   virtual void apply(smt::AssertionPipeline* 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);
+  virtual void apply(smt::AssertionPipeline* 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);  
+  void bvAbstraction(smt::AssertionPipeline* assertionsToPreprocess);  
 };
 
 class UnconstrainedSimpPass : public PreprocessingPass {
  public:
-  virtual void apply(std::vector<Node>* assertionsToPreprocess);
-  UnconstrainedSimpPass(ResourceManager* resourceManager, TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine);
+  virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+  UnconstrainedSimpPass(ResourceManager* resourceManager, 
+      TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine);
  private:
   TimerStat d_unconstrainedSimpTime;
   TheoryEngine* d_theoryEngine;
@@ -80,48 +83,54 @@ class UnconstrainedSimpPass : public PreprocessingPass {
 
 class RewritePass : public PreprocessingPass {
  public:
-    virtual void apply(std::vector<Node>* assertionsToPreprocess);
+    virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
     RewritePass(ResourceManager* resourceManager);
 };
  
 class NotUnsatCoresPass : public PreprocessingPass {
  public:
-    virtual void apply(std::vector<Node>* assertionsToPreprocess);
-    NotUnsatCoresPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions);
+    virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+    NotUnsatCoresPass(ResourceManager* resourceManager,
+       theory::SubstitutionMap* topLevelSubstitutions);
  private:
     theory::SubstitutionMap* d_topLevelSubstitutions;
 };
  
 class BVToBoolPass : public PreprocessingPass {
  public:
-   virtual void apply(std::vector<Node>* assertionsToPreprocess);
-   BVToBoolPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine);
+   virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+   BVToBoolPass(ResourceManager* resourceManager, 
+      TheoryEngine* theoryEngine);
  private:
   // Lift bit-vectors of size 1 to booleans
   TheoryEngine* d_theoryEngine;
-  void bvToBool(std::vector<Node>* assertionsToPreprocess);
+  void bvToBool(smt::AssertionPipeline* assertionsToPreprocess);
 };
 
 class BoolToBVPass : public PreprocessingPass {
  public:
-   virtual void apply(std::vector<Node>* assertionsTopreprocess);
-   BoolToBVPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine);
+   virtual void apply(smt::AssertionPipeline* assertionsTopreprocess);
+   BoolToBVPass(ResourceManager* resourceManager,
+     TheoryEngine* theoryEngine);
  private:
    // Convert booleans to bit-vectors of size 1
   TheoryEngine* d_theoryEngine;
-  void boolToBv(std::vector<Node>* assertionsToPreprocess);
+  void boolToBv(smt::AssertionPipeline* assertionsToPreprocess);
 };
 
 class SepPreSkolemEmpPass : public PreprocessingPass {
   public:
-   virtual void apply(std::vector<Node>* assertionsToPreprocess);
+   virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
    SepPreSkolemEmpPass(ResourceManager* resourceManager);
 };
 
 class QuantifiedPass : public PreprocessingPass {
   public:
-    virtual void apply(std::vector<Node>* assertionsToPreprocess);
-    QuantifiedPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined, std::map<Node,TypeNode> fmfRecFunctionsAbs, std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete); 
+    virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+    QuantifiedPass(ResourceManager* resourceManager, 
+      TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined, 
+      std::map<Node,TypeNode> fmfRecFunctionsAbs, 
+      std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete); 
   private:
     TheoryEngine* d_theoryEngine;
     NodeList* d_fmfRecFunctionsDefined;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2553fc57e..7881449dd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -102,6 +102,8 @@
 #include "util/proof.h"
 #include "util/resource_manager.h"
 
+#include "preproc/preprocessing_pass.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
@@ -157,7 +159,7 @@ public:
   Node getFormula() const { return d_formula; }
 };/* class DefinedFunction */
 
-class AssertionPipeline {
+/*class AssertionPipeline {
   vector<Node> d_nodes;
 
 public:
@@ -178,7 +180,8 @@ public:
     PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
     d_nodes[i] = n;
   }
-};/* class AssertionPipeline */
+}; //class AssertionPipeline 
+*/
 
 struct SmtEngineStatistics {
   /** time spent in definition-expansion */
@@ -596,6 +599,7 @@ private:
    * ite removal.
    */
   bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
+ 
  // Simplify ITE structure
   bool simpITE();
 
@@ -3304,7 +3308,7 @@ bool SmtEnginePrivate::simplifyAssertions()
     if(options::unconstrainedSimp()) {
       Chat() << "...doing unconstrained simplification..." << endl;
       preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine);
-      pass.apply(&d_assertions.ref());
+      pass.apply(&d_assertions);
    }
 
     dumpAssertions("post-unconstrained", d_assertions);
@@ -3517,23 +3521,23 @@ void SmtEnginePrivate::processAssertions() {
 
   if( options::nlExtPurify() ){
     preproc::NlExtPurifyPass pass(d_resourceManager);
-    pass.apply(&d_assertions.ref());
+    pass.apply(&d_assertions);
   }
 
   if( options::ceGuidedInst() ){
     //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
     preproc::CEGuidedInstPass pass(d_resourceManager, d_smt.d_theoryEngine);
-    pass.apply(&d_assertions.ref());
+    pass.apply(&d_assertions);
  }
 
   if (options::solveRealAsInt()) {
    preproc::SolveRealAsIntPass pass(d_resourceManager);
-   pass.apply(&d_assertions.ref());   
+   pass.apply(&d_assertions);   
   } 
 
   if (options::solveIntAsBV() > 0) {
    preproc::SolveIntAsBVPass pass(d_resourceManager);
-   pass.apply(&d_assertions.ref());   
+   pass.apply(&d_assertions);   
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
@@ -3547,16 +3551,16 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     preproc::BitBlastModePass pass(d_resourceManager, d_smt.d_theoryEngine);
-    pass.apply(&d_assertions.ref());   
+    pass.apply(&d_assertions);
   }
 
   if ( options::bvAbstraction() &&
       !options::incrementalSolving()) {
     preproc::BVAbstractionPass pass(d_resourceManager, &d_smt, d_smt.d_theoryEngine);
-    pass.apply(&d_assertions.ref());
+    pass.apply(&d_assertions);
 
     preproc::RewritePass pass1(d_resourceManager);
-    pass1.apply(&d_assertions.ref());
+    pass1.apply(&d_assertions);
  }
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
@@ -3568,12 +3572,12 @@ void SmtEnginePrivate::processAssertions() {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << std::endl;
     dumpAssertions("pre-unconstrained-simp", d_assertions);
     Chat() << "...doing unconstrained simplification..." << std::endl;
-    
+   
     preproc::RewritePass pass(d_resourceManager);
-    pass.apply(&d_assertions.ref());    
+    pass.apply(&d_assertions);    
 
     preproc::UnconstrainedSimpPass pass1(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine);
-    pass1.apply(&d_assertions.ref());
+    pass1.apply(&d_assertions);
  
    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << std::endl;
     dumpAssertions("post-unconstrained-simp", d_assertions);
@@ -3589,12 +3593,12 @@ void SmtEnginePrivate::processAssertions() {
   if(options::unsatCores()) {
     // special rewriting pass for unsat cores, since many of the passes below are skipped
     preproc::RewritePass pass(d_resourceManager);
-    pass.apply(&d_assertions.ref());
+    pass.apply(&d_assertions);
   } else {
     // Apply the substitutions we already have, and normalize
     //unsatCore check removed for redundancy
     preproc::NotUnsatCoresPass pass1(d_resourceManager, &d_topLevelSubstitutions);
-    pass1.apply(&d_assertions.ref()); 
+    pass1.apply(&d_assertions); 
   }
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl;
@@ -3605,29 +3609,86 @@ void SmtEnginePrivate::processAssertions() {
   // Lift bit-vectors of size 1 to bool
   if(options::bitvectorToBool()) {
     preproc::BVToBoolPass pass(d_resourceManager, d_smt.d_theoryEngine);
-    pass.apply(&d_assertions.ref());
+    pass.apply(&d_assertions);
 
     preproc::RewritePass pass1(d_resourceManager);
-    pass1.apply(&d_assertions.ref());
+    pass1.apply(&d_assertions);
   }
 
   // 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());
+    pass.apply(&d_assertions);
 
     preproc::RewritePass pass1(d_resourceManager);
-    pass1.apply(&d_assertions.ref());
+    pass1.apply(&d_assertions);
   }
 
   if(options::sepPreSkolemEmp()) {
     preproc::SepPreSkolemEmpPass pass(d_resourceManager);
-    pass.apply(&d_assertions.ref());
+    pass.apply(&d_assertions);
  }
 
   if( d_smt.d_logic.isQuantified() ){
-    preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine, d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs, d_smt.d_fmfRecFunctionsConcrete);
-    pass.apply(&d_assertions.ref());
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl;
+
+    dumpAssertions("pre-skolem-quant", d_assertions);
+    //remove rewrite rules, apply pre-skolemization to existential quantifiers
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      Node prev = (d_assertions)[i];
+      Node next = quantifiers::QuantifiersRewriter::preprocess( prev );
+      if( next!=prev ){
+        d_assertions.replace(i, Rewriter::rewrite( next ));
+        Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev <<std::endl;
+        Trace("quantifiers-preprocess") << "   ...got " << (d_assertions)[i] << std::endl;
+      }
+    }
+    dumpAssertions("post-skolem-quant", d_assertions);
+    if( options::macrosQuant() ){
+      //quantifiers macro expansion
+      quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() );
+      bool success;
+      do{
+        success = qm.simplify( d_assertions.ref(), true );
+      }while( success );
+      //finalize the definitions
+      qm.finalizeDefinitions();
+    }
+
+    //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
+    if( options::fmfFunWellDefined() ){
+      quantifiers::FunDefFmf fdf;
+      Assert( d_smt.d_fmfRecFunctionsDefined!=NULL );
+      //must carry over current definitions (for incremental)
+      for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
+           fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
+        Node f = (*fit);
+        Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!= d_fmfRecFunctionsAbs.end() );
+        TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
+        fdf.d_sorts[f] = ft;
+        std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
+        Assert( fcit!= d_smt.d_fmfRecFunctionsConcrete.end() );
+        for( unsigned j=0; j<fcit->second.size(); j++ ){
+          fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
+        }
+      }
+      fdf.simplify(d_assertions.ref());
+      //must store new definitions (for incremental)
+      for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
+        Node f = fdf.d_funcs[i];
+        d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
+        d_smt.d_fmfRecFunctionsConcrete[f].clear();
+        for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
+          d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
+        }
+        d_smt.d_fmfRecFunctionsDefined->push_back( f );
+      }
+    }
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl;
+  /*  preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine,
+     d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs,
+     d_smt.d_fmfRecFunctionsConcrete);
+    pass.apply(&d_assertions);*/
  }
 
   if( options::sortInference() || options::ufssFairnessMonotone() ){