rebased

3 files changed, 17 insertions, 29 deletions

diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index 304a93f76..5f39c27e1 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -27,7 +27,7 @@ namespace preproc {
 ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, SmtEngine* smt, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_smt(smt), d_definitionExpansionTime(definitionExpansionTime){
 }
 
-Node ExpandingDefinitionsPass::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
+Node ExpandingDefinitionsPass::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
   stack< triple<Node, Node, bool> > worklist;
   stack<Node> result;
@@ -194,7 +194,7 @@ PreprocessingPassResult ExpandingDefinitionsPass::apply(AssertionPipeline* asser
   Chat() << "expanding definitions..." << std::endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_definitionExpansionTime);
-    hash_map<Node, Node, NodeHashFunction> cache;
+    unordered_map<Node, Node, NodeHashFunction> cache;
     for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
       assertionsToPreprocess->replace(i, expandDefinitions((*assertionsToPreprocess)[i], cache));
     }
@@ -205,7 +205,7 @@ NlExtPurifyPass::NlExtPurifyPass(ResourceManager* resourceManager) :
     PreprocessingPass(resourceManager){
 }
 
-void NlExtPurifyPass::apply(AssertionPipeline* assertionsToPreprocess) {
+PreprocessingPassResult NlExtPurifyPass::apply(AssertionPipeline* assertionsToPreprocess) {
   std::unordered_map<Node, Node, NodeHashFunction> cache;
   std::unordered_map<Node, Node, NodeHashFunction> bcache;
   std::vector<Node> var_eq;
@@ -670,7 +670,7 @@ PreprocessingPassResult BVAbstractionPass::apply(AssertionPipeline* assertionsTo
  return PreprocessingPassResult(true);
 } 
 
-ConstrainSubtypesPass::ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt) : PreprocessingPass(resourceManager), d_smt(smt) {
+/*ConstrainSubtypesPass::ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt) : PreprocessingPass(resourceManager), d_smt(smt) {
 }
 
 void ConstrainSubtypesPass::constrainSubtypes(TNode top, AssertionPipeline& assertions)
@@ -740,7 +740,7 @@ PreprocessingPassResult ConstrainSubtypesPass::apply(AssertionPipeline* assertio
       constrainSubtypes((*assertionsToPreprocess)[i], *assertionsToPreprocess);
     }
   return PreprocessingPassResult(true);
-}
+}*/
 
 UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager,
       TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine) :
@@ -1129,9 +1129,9 @@ RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager,
     d_realAssertionsEnd(realAssertionsEnd){
 }
 
-bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache)
+bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = cache.find(n);
   if (it != cache.end()) {
     return (*it).second;
@@ -1162,9 +1162,9 @@ bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bo
   return false;
 }
 
-void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache)
+void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = cache.find(n);
   if (it != cache.end()) {
     return;
@@ -1199,7 +1199,7 @@ PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPre
       // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
 
       // cache for expression traversal
-      std::hash_map<Node, bool, NodeHashFunction> cache;
+      std::unordered_map<Node, bool, NodeHashFunction> cache;
 
       // First, find all skolems that appear in the substitution map - their associated iteExpr will need
       // to be moved to the main assertion set
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index 9f8e91c3d..18004dd3b 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -14,8 +14,8 @@
 namespace CVC4 {
 namespace preproc {
 
-typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-typedef std::hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
 typedef context::CDList<Node> NodeList;
 
 class ExpandingDefinitionsPass : public PreprocessingPass {
@@ -86,7 +86,7 @@ class BVAbstractionPass : public PreprocessingPass {
   void bvAbstraction(AssertionPipeline* assertionsToPreprocess);  
 };
 
-class ConstrainSubtypesPass : public PreprocessingPass {
+/*class ConstrainSubtypesPass : public PreprocessingPass {
  public:
   virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
   ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt);
@@ -94,7 +94,7 @@ class ConstrainSubtypesPass : public PreprocessingPass {
   SmtEngine* d_smt;
   void constrainSubtypes(TNode n, AssertionPipeline& assertions)
     throw();
-};
+};*/
 
 class UnconstrainedSimpPass : public PreprocessingPass {
  public:
@@ -251,8 +251,8 @@ class RepeatSimpPass : public PreprocessingPass {
      RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, unsigned simplifyAssertionsDepth, bool* noConflict, IteSkolemMap iteSkolemMap, unsigned realAssertionsEnd);
   private: 
      theory::SubstitutionMap* d_topLevelSubstitutions;
-     void collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache);
-     bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache);
+     void collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache);
+     bool checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache);
      bool simplifyAssertions();
      unsigned d_simplifyAssertionsDepth;
      bool* noConflict;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2a7015046..29ac71d3d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3562,19 +3562,7 @@ void SmtEnginePrivate::processAssertions() {
  }
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-<<<<<<< e79fa19f8eacdeab55089cdfec717574b9b7af34
-=======
-  dumpAssertions("pre-constrain-subtypes", d_assertions);
-  {
-    preproc::ConstrainSubtypesPass pass(d_resourceManager, &d_smt);
-    pass.apply(&d_assertions);
- }
-  dumpAssertions("post-constrain-subtypes", d_assertions);
-
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
->>>>>>> ContrainSubtypes and ExpandingDefinitions classes
+ 
   bool noConflict = true;
 
   // Unconstrained simplification