diff options
-rw-r--r-- | src/preproc/preprocessing_passes_core.cpp | 20 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.h | 12 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 14 |
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 |