diff options
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/apply_substs.cpp | 13 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 5 |
3 files changed, 9 insertions, 11 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 6fb4b7793..f5c3520d0 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -44,8 +44,9 @@ PreprocessingPassResult ApplySubsts::applyInternal( // When solving incrementally, all substitutions are piled into the // assertion at d_substitutionsIndex: we don't want to apply substitutions // to this assertion or information will be lost. - context::CDO<unsigned>& substs_index = - assertionsToPreprocess->getSubstitutionsIndex(); + unsigned substs_index = d_preprocContext->getSubstitutionsIndex(); + theory::SubstitutionMap& substMap = + d_preprocContext->getTopLevelSubstitutions(); unsigned size = assertionsToPreprocess->size(); unsigned substitutionAssertion = substs_index > 0 ? substs_index : size; for (unsigned i = 0; i < size; ++i) @@ -57,11 +58,9 @@ PreprocessingPassResult ApplySubsts::applyInternal( Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] << std::endl; d_preprocContext->spendResource(options::preprocessStep()); - assertionsToPreprocess->replace( - i, - theory::Rewriter::rewrite( - assertionsToPreprocess->getTopLevelSubstitutions().apply( - (*assertionsToPreprocess)[i]))); + assertionsToPreprocess->replace(i, + theory::Rewriter::rewrite(substMap.apply( + (*assertionsToPreprocess)[i]))); Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] << std::endl; } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 81588d039..616ecd969 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( propagator->getBackEdges(); unordered_set<unsigned long> removeAssertions; SubstitutionMap& top_level_substs = - assertionsToPreprocess->getTopLevelSubstitutions(); + d_preprocContext->getTopLevelSubstitutions(); NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index e2ce1c301..653aed8ad 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -76,8 +76,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // Assert all the assertions to the propagator Trace("non-clausal-simplify") << "asserting to propagator" << std::endl; - context::CDO<unsigned>& substs_index = - assertionsToPreprocess->getSubstitutionsIndex(); + unsigned substs_index = d_preprocContext->getSubstitutionsIndex(); for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) @@ -114,7 +113,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << " learned literals." << std::endl; // No conflict, go through the literals and solve them SubstitutionMap& top_level_substs = - assertionsToPreprocess->getTopLevelSubstitutions(); + d_preprocContext->getTopLevelSubstitutions(); SubstitutionMap constantPropagations(d_preprocContext->getUserContext()); SubstitutionMap newSubstitutions(d_preprocContext->getUserContext()); SubstitutionMap::iterator pos; |