diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-23 11:05:38 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-23 11:05:38 -0700 |
commit | f66f40912490226291d5af6c1f8b66e9ba6d7633 (patch) | |
tree | 5dc889390b7107cab051472e3bedd8ac151ab8f7 /src/preprocessing/passes/ite_simp.cpp | |
parent | f522d1e63e581cadeb987987ba3e3b0bd88f2e08 (diff) |
Refactor ITE simplification preprocessing pass. (#2360)
Diffstat (limited to 'src/preprocessing/passes/ite_simp.cpp')
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 263 |
1 files changed, 263 insertions, 0 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp new file mode 100644 index 000000000..137925f77 --- /dev/null +++ b/src/preprocessing/passes/ite_simp.cpp @@ -0,0 +1,263 @@ +/********************* */ +/*! \file ite_simp.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ITE simplification preprocessing pass. + **/ + +#include "preprocessing/passes/ite_simp.h" + +#include "options/proof_options.h" +#include "smt/smt_statistics_registry.h" +#include "smt_util/nary_builder.h" +#include "theory/arith/arith_ite_utils.h" + +#include <vector> + +using namespace CVC4; +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/* -------------------------------------------------------------------------- */ + +namespace { + +Node simpITE(util::ITEUtilities* ite_utils, TNode assertion) +{ + if (!ite_utils->containsTermITE(assertion)) + { + return assertion; + } + else + { + Node result = ite_utils->simpITE(assertion); + Node res_rewritten = Rewriter::rewrite(result); + + if (options::simplifyWithCareEnabled()) + { + Chat() << "starting simplifyWithCare()" << endl; + Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten); + Chat() << "ending simplifyWithCare()" + << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; + result = Rewriter::rewrite(postSimpWithCare); + } + else + { + result = res_rewritten; + } + return result; + } +} + +/** + * Ensures the assertions asserted after index 'before' now effectively come + * before 'real_assertions_end'. + */ +void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, + size_t before) +{ + size_t cur_size = assertionsToPreprocess->size(); + if (before >= cur_size || assertionsToPreprocess->getRealAssertionsEnd() <= 0 + || assertionsToPreprocess->getRealAssertionsEnd() >= cur_size) + { + return; + } + + // assertions + // original: [0 ... assertionsToPreprocess.getRealAssertionsEnd()) + // can be modified + // ites skolems [assertionsToPreprocess.getRealAssertionsEnd(), before) + // cannot be moved + // added [before, cur_size) + // can be modified + Assert(0 < assertionsToPreprocess->getRealAssertionsEnd()); + Assert(assertionsToPreprocess->getRealAssertionsEnd() <= before); + Assert(before < cur_size); + + std::vector<Node> intoConjunction; + for (size_t i = before; i < cur_size; ++i) + { + intoConjunction.push_back((*assertionsToPreprocess)[i]); + } + assertionsToPreprocess->resize(before); + size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1; + intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]); + Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + assertionsToPreprocess->replace(lastBeforeItes, newLast); + Assert(assertionsToPreprocess->size() == before); +} + +} // namespace + +/* -------------------------------------------------------------------------- */ + +ITESimp::Statistics::Statistics() + : d_arithSubstitutionsAdded( + "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0) +{ + smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); +} + +ITESimp::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); +} + +bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) +{ + // This pass does not support dependency tracking yet + // (learns substitutions from all assertions so just + // adding addDependence is not enough) + if (options::unsatCores() || options::fewerPreprocessingHoles()) + { + return true; + } + bool result = true; + bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); + if (simpDidALotOfWork) + { + if (options::compressItes()) + { + result = d_iteUtilities.compress(assertionsToPreprocess->ref()); + } + + if (result) + { + // if false, don't bother to reclaim memory here. + NodeManager* nm = NodeManager::currentNM(); + if (nm->poolSize() >= options::zombieHuntThreshold()) + { + Chat() << "..ite simplifier did quite a bit of work.. " + << nm->poolSize() << endl; + Chat() << "....node manager contains " << nm->poolSize() + << " nodes before cleanup" << endl; + d_iteUtilities.clear(); + Rewriter::clearCaches(); + nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + Chat() << "....node manager contains " << nm->poolSize() + << " nodes after cleanup" << endl; + } + } + } + + // Do theory specific preprocessing passes + TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine(); + if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH) + && !options::incrementalSolving()) + { + if (!simpDidALotOfWork) + { + util::ContainsTermITEVisitor& contains = + *(d_iteUtilities.getContainsVisitor()); + arith::ArithIteUtils aiteu(contains, + d_preprocContext->getUserContext(), + theory_engine->getModel()); + bool anyItes = false; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + if (contains.containsTermITE(curr)) + { + anyItes = true; + Node res = aiteu.reduceVariablesInItes(curr); + Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl + << " ->" << res << endl; + if (curr != res) + { + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + } + } + } + if (!anyItes) + { + unsigned prevSubCount = aiteu.getSubCount(); + aiteu.learnSubstitutions(assertionsToPreprocess->ref()); + if (prevSubCount < aiteu.getSubCount()) + { + d_statistics.d_arithSubstitutionsAdded += + aiteu.getSubCount() - prevSubCount; + bool anySuccess = false; + for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); + Node res = aiteu.reduceVariablesInItes(next); + Debug("arith::ite::red") << "@ " << i << " ... " << next << endl + << " ->" << res << endl; + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + if (more != next) + { + anySuccess = true; + break; + } + } + for (size_t i = 0, N = assertionsToPreprocess->size(); + anySuccess && i < N; + ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); + Node res = aiteu.reduceVariablesInItes(next); + Debug("arith::ite::red") << "@ " << i << " ... " << next << endl + << " ->" << res << endl; + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + } + } + } + } + } + return result; +} + +/* -------------------------------------------------------------------------- */ + +ITESimp::ITESimp(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ite-simp") +{ +} + +PreprocessingPassResult ITESimp::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + d_preprocContext->spendResource(options::preprocessStep()); + + size_t nasserts = assertionsToPreprocess->size(); + for (size_t i = 0; i < nasserts; ++i) + { + d_preprocContext->spendResource(options::preprocessStep()); + Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]); + assertionsToPreprocess->replace(i, simp); + if (simp.isConst() && !simp.getConst<bool>()) + { + return PreprocessingPassResult::CONFLICT; + } + } + bool done = doneSimpITE(assertionsToPreprocess); + if (nasserts < assertionsToPreprocess->size()) + { + compressBeforeRealAssertions(assertionsToPreprocess, nasserts); + } + return done ? PreprocessingPassResult::NO_CONFLICT + : PreprocessingPassResult::CONFLICT; +} + +/* -------------------------------------------------------------------------- */ + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 |