From: Mathias Preiner Date: Wed, 29 Aug 2018 21:38:33 +0000 (-0700) Subject: Refactor MipLibTrick preprocessing pass. (#2359) X-Git-Tag: cvc5-1.0.0~4698 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3eac9d04c5d4bfba81142d4a5fe91b86590b32ae;p=cvc5.git Refactor MipLibTrick preprocessing pass. (#2359) --- diff --git a/src/Makefile.am b/src/Makefile.am index 883d81957..7231820f8 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -93,6 +93,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/nl_ext_purify.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ preprocessing/passes/pseudo_boolean_processor.h \ + preprocessing/passes/miplib_trick.cpp \ + preprocessing/passes/miplib_trick.h \ preprocessing/passes/quantifiers_preprocess.cpp \ preprocessing/passes/quantifiers_preprocess.h \ preprocessing/passes/quantifier_macros.cpp \ diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp new file mode 100644 index 000000000..81588d039 --- /dev/null +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -0,0 +1,664 @@ +/********************* */ +/*! \file miplib_trick.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** 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 The MIPLIB trick preprocessing pass + ** + **/ + +#include "preprocessing/passes/miplib_trick.h" + +#include + +#include "expr/node_self_iterator.h" +#include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" +#include "smt_util/boolean_simplification.h" +#include "theory/booleans/circuit_propagator.h" +#include "theory/theory_model.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +namespace { + +/** + * Remove conjuncts in toRemove from conjunction n. Return # of removed + * conjuncts. + */ +size_t removeFromConjunction(Node& n, + const std::unordered_set& toRemove) +{ + Assert(n.getKind() == kind::AND); + Node trueNode = NodeManager::currentNM()->mkConst(true); + size_t removals = 0; + for (Node::iterator j = n.begin(); j != n.end(); ++j) + { + size_t subremovals = 0; + Node sub = *j; + if (toRemove.find(sub.getId()) != toRemove.end() + || (sub.getKind() == kind::AND + && (subremovals = removeFromConjunction(sub, toRemove)) > 0)) + { + NodeBuilder<> b(kind::AND); + b.append(n.begin(), j); + if (subremovals > 0) + { + removals += subremovals; + b << sub; + } + else + { + ++removals; + } + for (++j; j != n.end(); ++j) + { + if (toRemove.find((*j).getId()) != toRemove.end()) + { + ++removals; + } + else if ((*j).getKind() == kind::AND) + { + sub = *j; + if ((subremovals = removeFromConjunction(sub, toRemove)) > 0) + { + removals += subremovals; + b << sub; + } + else + { + b << *j; + } + } + else + { + b << *j; + } + } + if (b.getNumChildren() == 0) + { + n = trueNode; + b.clear(); + } + else if (b.getNumChildren() == 1) + { + n = b[0]; + b.clear(); + } + else + { + n = b; + } + n = Rewriter::rewrite(n); + return removals; + } + } + + Assert(removals == 0); + return 0; +} + +/** + * Trace nodes back to their assertions using CircuitPropagator's + * BackEdgesMap. + */ +void traceBackToAssertions(booleans::CircuitPropagator* propagator, + const std::vector& nodes, + std::vector& assertions) +{ + const booleans::CircuitPropagator::BackEdgesMap& backEdges = + propagator->getBackEdges(); + for (vector::const_iterator i = nodes.begin(); i != nodes.end(); ++i) + { + booleans::CircuitPropagator::BackEdgesMap::const_iterator j = + backEdges.find(*i); + // term must appear in map, otherwise how did we get here?! + Assert(j != backEdges.end()); + // if term maps to empty, that means it's a top-level assertion + if (!(*j).second.empty()) + { + traceBackToAssertions(propagator, (*j).second, assertions); + } + else + { + assertions.push_back(*i); + } + } +} + +} // namespace + +MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "miplib-trick") +{ + if (!options::incrementalSolving()) + { + NodeManager::currentNM()->subscribeEvents(this); + } +} + +MipLibTrick::~MipLibTrick() +{ + if (!options::incrementalSolving()) + { + NodeManager::currentNM()->unsubscribeEvents(this); + } +} + +void MipLibTrick::nmNotifyNewVar(TNode n, uint32_t flags) +{ + if (n.getType().isBoolean()) + { + d_boolVars.push_back(n); + } +} + +void MipLibTrick::nmNotifyNewSkolem(TNode n, + const std::string& comment, + uint32_t flags) +{ + if (n.getType().isBoolean()) + { + d_boolVars.push_back(n); + } +} + +PreprocessingPassResult MipLibTrick::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + Assert(assertionsToPreprocess->getRealAssertionsEnd() + == assertionsToPreprocess->size()); + Assert(!options::incrementalSolving()); + + context::Context fakeContext; + TheoryEngine* te = d_preprocContext->getTheoryEngine(); + booleans::CircuitPropagator* propagator = + d_preprocContext->getCircuitPropagator(); + const booleans::CircuitPropagator::BackEdgesMap& backEdges = + propagator->getBackEdges(); + unordered_set removeAssertions; + SubstitutionMap& top_level_substs = + assertionsToPreprocess->getTopLevelSubstitutions(); + + NodeManager* nm = NodeManager::currentNM(); + Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); + Node trueNode = nm->mkConst(true); + + unordered_map intVars; + for (TNode v : d_boolVars) + { + if (propagator->isAssigned(v)) + { + Debug("miplib") << "ineligible: " << v << " because assigned " + << propagator->getAssignment(v) << endl; + continue; + } + + vector assertions; + booleans::CircuitPropagator::BackEdgesMap::const_iterator j = + backEdges.find(v); + // if not in back edges map, the bool var is unconstrained, showing up in no + // assertions. if maps to an empty vector, that means the bool var was + // asserted itself. + if (j != backEdges.end()) + { + if (!(*j).second.empty()) + { + traceBackToAssertions(propagator, (*j).second, assertions); + } + else + { + assertions.push_back(v); + } + } + Debug("miplib") << "for " << v << endl; + bool eligible = true; + map, uint64_t> marks; + map, vector > coef; + map, vector > checks; + map, vector > asserts; + for (vector::const_iterator j = assertions.begin(); + j != assertions.end(); + ++j) + { + Debug("miplib") << " found: " << *j << endl; + if ((*j).getKind() != kind::IMPLIES) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl; + break; + } + Node conj = BooleanSimplification::simplify((*j)[0]); + if (conj.getKind() == kind::AND && conj.getNumChildren() > 6) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl; + break; + } + if (conj.getKind() != kind::AND && !conj.isVar() + && !(conj.getKind() == kind::NOT && conj[0].isVar())) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl; + break; + } + if ((*j)[1].getKind() != kind::EQUAL + || !(((*j)[1][0].isVar() + && (*j)[1][1].getKind() == kind::CONST_RATIONAL) + || ((*j)[1][0].getKind() == kind::CONST_RATIONAL + && (*j)[1][1].isVar()))) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl; + break; + } + if (conj.getKind() == kind::AND) + { + vector posv; + bool found_x = false; + map neg; + for (Node::iterator ii = conj.begin(); ii != conj.end(); ++ii) + { + if ((*ii).isVar()) + { + posv.push_back(*ii); + neg[*ii] = false; + found_x = found_x || v == *ii; + } + else if ((*ii).getKind() == kind::NOT && (*ii)[0].isVar()) + { + posv.push_back((*ii)[0]); + neg[(*ii)[0]] = true; + found_x = found_x || v == (*ii)[0]; + } + else + { + eligible = false; + Debug("miplib") + << " -- INELIGIBLE -- (non-var: " << *ii << ")" << endl; + break; + } + if (propagator->isAssigned(posv.back())) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (" << posv.back() + << " asserted)" << endl; + break; + } + } + if (!eligible) + { + break; + } + if (!found_x) + { + eligible = false; + Debug("miplib") << " --INELIGIBLE -- (couldn't find " << v + << " in conjunction)" << endl; + break; + } + sort(posv.begin(), posv.end()); + const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); + const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j)[1][1] + : (*j)[1][0]; + const pair pos_var(pos, var); + const Rational& constant = + ((*j)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j)[1][0].getConst() + : (*j)[1][1].getConst(); + uint64_t mark = 0; + unsigned countneg = 0, thepos = 0; + for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii) + { + if (neg[pos[ii]]) + { + ++countneg; + } + else + { + thepos = ii; + mark |= (0x1 << ii); + } + } + if ((marks[pos_var] & (1lu << mark)) != 0) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; + break; + } + Debug("miplib") << "mark is " << mark << " -- " << (1lu << mark) + << endl; + marks[pos_var] |= (1lu << mark); + Debug("miplib") << "marks[" << pos << "," << var << "] now " + << marks[pos_var] << endl; + if (countneg == pos.getNumChildren()) + { + if (constant != 0) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl; + break; + } + } + else if (countneg == pos.getNumChildren() - 1) + { + Assert(coef[pos_var].size() <= 6 && thepos < 6); + if (coef[pos_var].size() <= thepos) + { + coef[pos_var].resize(thepos + 1); + } + coef[pos_var][thepos] = constant; + } + else + { + if (checks[pos_var].size() <= mark) + { + checks[pos_var].resize(mark + 1); + } + checks[pos_var][mark] = constant; + } + asserts[pos_var].push_back(*j); + } + else + { + TNode x = conj; + if (x != v && x != (v).notNode()) + { + eligible = false; + Debug("miplib") + << " -- INELIGIBLE -- (x not present where I expect it)" << endl; + break; + } + const bool xneg = (x.getKind() == kind::NOT); + x = xneg ? x[0] : x; + Debug("miplib") << " x:" << x << " " << xneg << endl; + const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j)[1][1] + : (*j)[1][0]; + const pair x_var(x, var); + const Rational& constant = + ((*j)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j)[1][0].getConst() + : (*j)[1][1].getConst(); + unsigned mark = (xneg ? 0 : 1); + if ((marks[x_var] & (1u << mark)) != 0) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; + break; + } + marks[x_var] |= (1u << mark); + if (xneg) + { + if (constant != 0) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl; + break; + } + } + else + { + Assert(coef[x_var].size() <= 6); + coef[x_var].resize(6); + coef[x_var][0] = constant; + } + asserts[x_var].push_back(*j); + } + } + if (eligible) + { + for (map, uint64_t>::const_iterator j = marks.begin(); + j != marks.end(); + ++j) + { + const TNode pos = (*j).first.first; + const TNode var = (*j).first.second; + const pair& pos_var = (*j).first; + const uint64_t mark = (*j).second; + const unsigned numVars = + pos.getKind() == kind::AND ? pos.getNumChildren() : 1; + uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1; + expected = (expected == 0) ? -1 : expected; // fix for overflow + Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " + << expected << dec << endl; + Assert(pos.getKind() == kind::AND || pos.isVar()); + if (mark != expected) + { + Debug("miplib") << " -- INELIGIBLE " << pos + << " -- (insufficiently marked, got " << mark + << " for " << numVars << " vars, expected " + << expected << endl; + } + else + { + if (mark != 3) + { // exclude single-var case; nothing to check there + uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1; + sz = (sz == 0) ? -1 : sz; // fix for overflow + Assert(sz == mark, "expected size %u == mark %u", sz, mark); + for (size_t k = 0; k < checks[pos_var].size(); ++k) + { + if ((k & (k - 1)) != 0) + { + Rational sum = 0; + Debug("miplib") << k << " => " << checks[pos_var][k] << endl; + for (size_t v = 1, kk = k; kk != 0; ++v, kk >>= 1) + { + if ((kk & 0x1) == 1) + { + Assert(pos.getKind() == kind::AND); + Debug("miplib") << "var " << v << " : " << pos[v - 1] + << " coef:" << coef[pos_var][v - 1] << endl; + sum += coef[pos_var][v - 1]; + } + } + Debug("miplib") << "checkSum is " << sum << " input says " + << checks[pos_var][k] << endl; + if (sum != checks[pos_var][k]) + { + eligible = false; + Debug("miplib") << " -- INELIGIBLE " << pos + << " -- (nonlinear combination)" << endl; + break; + } + } + else + { + Assert(checks[pos_var][k] == 0, + "checks[(%s,%s)][%u] should be 0, but it's %s", + pos.toString().c_str(), + var.toString().c_str(), + k, + checks[pos_var][k] + .toString() + .c_str()); // we never set for single-positive-var + } + } + } + if (!eligible) + { + eligible = true; // next is still eligible + continue; + } + + Debug("miplib") << " -- ELIGIBLE " << v << " , " << pos << " --" + << endl; + vector newVars; + expr::NodeSelfIterator ii, iiend; + if (pos.getKind() == kind::AND) + { + ii = pos.begin(); + iiend = pos.end(); + } + else + { + ii = expr::NodeSelfIterator::self(pos); + iiend = expr::NodeSelfIterator::selfEnd(pos); + } + for (; ii != iiend; ++ii) + { + Node& varRef = intVars[*ii]; + if (varRef.isNull()) + { + stringstream ss; + ss << "mipvar_" << *ii; + Node newVar = nm->mkSkolem( + ss.str(), + nm->integerType(), + "a variable introduced due to scrubbing a miplib encoding", + NodeManager::SKOLEM_EXACT_NAME); + Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); + Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); + + Node n = Rewriter::rewrite(geq.andNode(leq)); + assertionsToPreprocess->push_back(n); + PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); + + SubstitutionMap nullMap(&fakeContext); + Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions + status = te->solve(geq, nullMap); + Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED, + "unexpected solution from arith's ppAssert()"); + Assert(nullMap.empty(), + "unexpected substitution from arith's ppAssert()"); + status = te->solve(leq, nullMap); + Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED, + "unexpected solution from arith's ppAssert()"); + Assert(nullMap.empty(), + "unexpected substitution from arith's ppAssert()"); + te->getModel()->addSubstitution(*ii, newVar.eqNode(one)); + newVars.push_back(newVar); + varRef = newVar; + } + else + { + newVars.push_back(varRef); + } + d_preprocContext->enableIntegers(); + } + Node sum; + if (pos.getKind() == kind::AND) + { + NodeBuilder<> sumb(kind::PLUS); + for (size_t ii = 0; ii < pos.getNumChildren(); ++ii) + { + sumb << nm->mkNode( + kind::MULT, nm->mkConst(coef[pos_var][ii]), newVars[ii]); + } + sum = sumb; + } + else + { + sum = nm->mkNode( + kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); + } + Debug("miplib") << "vars[] " << var << endl + << " eq " << Rewriter::rewrite(sum) << endl; + Node newAssertion = var.eqNode(Rewriter::rewrite(sum)); + if (top_level_substs.hasSubstitution(newAssertion[0])) + { + // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; + // Warning() << "REPLACE " << newAssertion[1] << endl; + // Warning() << "ORIG " << + // top_level_substs.getSubstitution(newAssertion[0]) << endl; + Assert(top_level_substs.getSubstitution(newAssertion[0]) + == newAssertion[1]); + } + else if (pos.getNumChildren() <= options::arithMLTrickSubstitutions()) + { + top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]); + Debug("miplib") << "addSubs: " << newAssertion[0] << " to " + << newAssertion[1] << endl; + } + else + { + Debug("miplib") + << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] + << " (threshold is " << options::arithMLTrickSubstitutions() + << ")" << endl; + } + newAssertion = Rewriter::rewrite(newAssertion); + Debug("miplib") << " " << newAssertion << endl; + + assertionsToPreprocess->push_back(newAssertion); + PROOF(ProofManager::currentPM()->addDependence(newAssertion, + Node::null())); + + Debug("miplib") << " assertions to remove: " << endl; + for (vector::const_iterator k = asserts[pos_var].begin(), + k_end = asserts[pos_var].end(); + k != k_end; + ++k) + { + Debug("miplib") << " " << *k << endl; + removeAssertions.insert((*k).getId()); + } + } + } + } + } + if (!removeAssertions.empty()) + { + Debug("miplib") << " scrubbing miplib encoding..." << endl; + for (size_t i = 0, size = assertionsToPreprocess->getRealAssertionsEnd(); + i < size; + ++i) + { + Node assertion = (*assertionsToPreprocess)[i]; + if (removeAssertions.find(assertion.getId()) != removeAssertions.end()) + { + Debug("miplib") << " - removing " << assertion << endl; + assertionsToPreprocess->replace(i, trueNode); + ++d_statistics.d_numMiplibAssertionsRemoved; + } + else if (assertion.getKind() == kind::AND) + { + size_t removals = removeFromConjunction(assertion, removeAssertions); + if (removals > 0) + { + Debug("miplib") << " - reduced " << assertion << endl; + Debug("miplib") << " - by " << removals << " conjuncts" << endl; + d_statistics.d_numMiplibAssertionsRemoved += removals; + } + } + Debug("miplib") << "had: " << assertion[i] << endl; + assertionsToPreprocess->replace( + i, Rewriter::rewrite(top_level_substs.apply(assertion))); + Debug("miplib") << "now: " << assertion << endl; + } + } + else + { + Debug("miplib") << " miplib pass found nothing." << endl; + } + assertionsToPreprocess->updateRealAssertionsEnd(); + return PreprocessingPassResult::NO_CONFLICT; +} + +MipLibTrick::Statistics::Statistics() + : d_numMiplibAssertionsRemoved( + "preprocessing::passes::MipLibTrick::numMiplibAssertionsRemoved", 0) +{ + smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); +} + +MipLibTrick::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h new file mode 100644 index 000000000..7e75372a8 --- /dev/null +++ b/src/preprocessing/passes/miplib_trick.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file miplib_trick.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** 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 The MIPLIB trick preprocessing pass + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#define __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class MipLibTrick : public PreprocessingPass, public NodeManagerListener +{ + public: + MipLibTrick(PreprocessingPassContext* preprocContext); + ~MipLibTrick(); + + // NodeManagerListener callbacks to collect d_boolVars. + void nmNotifyNewVar(TNode n, uint32_t flags) override; + void nmNotifyNewSkolem(TNode n, + const std::string& comment, + uint32_t flags) override; + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + struct Statistics + { + /** number of assertions removed by miplib pass */ + IntStat d_numMiplibAssertionsRemoved; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + + std::vector d_boolVars; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 31987b00b..af66c2a2a 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -22,8 +22,12 @@ namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( SmtEngine* smt, ResourceManager* resourceManager, - RemoveTermFormulas* iteRemover) - : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover) + RemoveTermFormulas* iteRemover, + theory::booleans::CircuitPropagator* circuitPropagator) + : d_smt(smt), + d_resourceManager(resourceManager), + d_iteRemover(iteRemover), + d_circuitPropagator(circuitPropagator) { } @@ -33,5 +37,11 @@ void PreprocessingPassContext::widenLogic(theory::TheoryId id) req.widenLogic(id); } +void PreprocessingPassContext::enableIntegers() +{ + LogicRequest req(*d_smt); + req.enableIntegers(); +} + } // namespace preprocessing } // namespace CVC4 diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 96e554680..a2e83aa4c 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -26,6 +26,7 @@ #include "preprocessing/util/ite_utilities.h" #include "smt/smt_engine.h" #include "smt/term_formula_removal.h" +#include "theory/booleans/circuit_propagator.h" #include "theory/theory_engine.h" #include "util/resource_manager.h" @@ -35,9 +36,12 @@ namespace preprocessing { class PreprocessingPassContext { public: - PreprocessingPassContext(SmtEngine* smt, - ResourceManager* resourceManager, - RemoveTermFormulas* iteRemover); + PreprocessingPassContext( + SmtEngine* smt, + ResourceManager* resourceManager, + RemoveTermFormulas* iteRemover, + theory::booleans::CircuitPropagator* circuitPropagator); + SmtEngine* getSmt() { return d_smt; } TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; } DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } @@ -46,6 +50,11 @@ class PreprocessingPassContext context::Context* getDecisionContext() { return d_smt->d_context; } RemoveTermFormulas* getIteRemover() { return d_iteRemover; } + theory::booleans::CircuitPropagator* getCircuitPropagator() + { + return d_circuitPropagator; + } + void spendResource(unsigned amount) { d_resourceManager->spendResource(amount); @@ -56,6 +65,9 @@ class PreprocessingPassContext /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); + /* Enable Integers. */ + void enableIntegers(); + private: /* Pointer to the SmtEngine that this context was created in. */ SmtEngine* d_smt; @@ -63,6 +75,9 @@ class PreprocessingPassContext /** Instance of the ITE remover */ RemoveTermFormulas* d_iteRemover; + + /** Instance of the circuit propagator */ + theory::booleans::CircuitPropagator* d_circuitPropagator; }; // class PreprocessingPassContext } // namespace preprocessing diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp index 5c0c5758d..c9ddad176 100644 --- a/src/smt/logic_request.cpp +++ b/src/smt/logic_request.cpp @@ -31,4 +31,15 @@ void LogicRequest::widenLogic(theory::TheoryId id) { d_smt.d_logic.lock(); } +/** Enable Integers if not yet enabled. */ +void LogicRequest::enableIntegers() +{ + if (!d_smt.d_logic.areIntegersUsed()) + { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableIntegers(); + d_smt.d_logic.lock(); + } +} + }/* CVC4 namespace */ diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h index 149939eb9..23add1cf4 100644 --- a/src/smt/logic_request.h +++ b/src/smt/logic_request.h @@ -42,6 +42,9 @@ public: /** Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); + /** Enable Integers. */ + void enableIntegers(); + };/* class LogicRequest */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3bfde1839..2b388275a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -84,6 +84,7 @@ #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/ite_simp.h" #include "preprocessing/passes/nl_ext_purify.h" +#include "preprocessing/passes/miplib_trick.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/quantifier_macros.h" #include "preprocessing/passes/quantifier_macros.h" @@ -199,10 +200,6 @@ struct SmtEngineStatistics { TimerStat d_definitionExpansionTime; /** time spent in non-clausal simplification */ TimerStat d_nonclausalSimplificationTime; - /** time spent in miplib pass */ - TimerStat d_miplibPassTime; - /** number of assertions removed by miplib pass */ - IntStat d_numMiplibAssertionsRemoved; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; /** time spent in theory preprocessing */ @@ -234,8 +231,6 @@ struct SmtEngineStatistics { SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), - d_miplibPassTime("smt::SmtEngine::miplibPassTime"), - d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), @@ -252,8 +247,6 @@ struct SmtEngineStatistics { { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime); - smtStatisticsRegistry()->registerStat(&d_miplibPassTime); - smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); @@ -272,8 +265,6 @@ struct SmtEngineStatistics { ~SmtEngineStatistics() { smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime); - smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); - smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); @@ -498,7 +489,8 @@ class SmtEnginePrivate : public NodeManagerListener { /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; - std::vector d_boolVars; + + bool d_propagatorNeedsFinish; /** Assertions in the preprocessing pipeline */ AssertionPipeline d_assertions; @@ -575,23 +567,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - /** - * Trace nodes back to their assertions using CircuitPropagator's - * BackEdgesMap. - */ - void traceBackToAssertions(const std::vector& nodes, - std::vector& assertions); - - /** - * Remove conjuncts in toRemove from conjunction n. Return # of removed - * conjuncts. - */ - size_t removeFromConjunction( - Node& n, const std::unordered_set& toRemove); - - /** Scrub miplib encodings. */ - void doMiplibTrick(); - /** * Perform non-clausal simplification of a Node. This involves * Theory implementations, but does NOT involve the SAT solver in @@ -737,9 +712,6 @@ class SmtEnginePrivate : public NodeManagerListener { if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { d_smt.addToModelCommandAndDump(c, flags); } - if(n.getType().isBoolean() && !options::incrementalSolving()) { - d_boolVars.push_back(n); - } } void nmNotifyNewSkolem(TNode n, @@ -754,9 +726,6 @@ class SmtEnginePrivate : public NodeManagerListener { if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { d_smt.addToModelCommandAndDump(c, flags, false, "skolems"); } - if(n.getType().isBoolean() && !options::incrementalSolving()) { - d_boolVars.push_back(n); - } } void nmNotifyDeleteNode(TNode n) override {} @@ -2612,8 +2581,8 @@ bool SmtEngine::isDefinedFunction( Expr func ){ void SmtEnginePrivate::finishInit() { - d_preprocessingPassContext.reset( - new PreprocessingPassContext(&d_smt, d_resourceManager, &d_iteRemover)); + d_preprocessingPassContext.reset(new PreprocessingPassContext( + &d_smt, d_resourceManager, &d_iteRemover, &d_propagator)); // TODO: register passes here (this will likely change when we add support for // actually assembling preprocessing pipelines). std::unique_ptr applySubsts( @@ -2644,6 +2613,8 @@ void SmtEnginePrivate::finishInit() new ITESimp(d_preprocessingPassContext.get())); std::unique_ptr nlExtPurify( new NlExtPurify(d_preprocessingPassContext.get())); + std::unique_ptr mipLibTrick( + new MipLibTrick(d_preprocessingPassContext.get())); std::unique_ptr quantifiersPreprocess( new QuantifiersPreprocess(d_preprocessingPassContext.get())); std::unique_ptr pbProc( @@ -2693,6 +2664,8 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp)); d_preprocessingPassRegistry.registerPass("nl-ext-purify", std::move(nlExtPurify)); + d_preprocessingPassRegistry.registerPass("miplib-trick", + std::move(mipLibTrick)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", @@ -3251,395 +3224,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -void SmtEnginePrivate::traceBackToAssertions(const std::vector& nodes, std::vector& assertions) { - const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); - for(vector::const_iterator i = nodes.begin(); i != nodes.end(); ++i) { - booleans::CircuitPropagator::BackEdgesMap::const_iterator j = backEdges.find(*i); - // term must appear in map, otherwise how did we get here?! - Assert(j != backEdges.end()); - // if term maps to empty, that means it's a top-level assertion - if(!(*j).second.empty()) { - traceBackToAssertions((*j).second, assertions); - } else { - assertions.push_back(*i); - } - } -} - -size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set& toRemove) { - Assert(n.getKind() == kind::AND); - size_t removals = 0; - for(Node::iterator j = n.begin(); j != n.end(); ++j) { - size_t subremovals = 0; - Node sub = *j; - if(toRemove.find(sub.getId()) != toRemove.end() || - (sub.getKind() == kind::AND && (subremovals = removeFromConjunction(sub, toRemove)) > 0)) { - NodeBuilder<> b(kind::AND); - b.append(n.begin(), j); - if(subremovals > 0) { - removals += subremovals; - b << sub; - } else { - ++removals; - } - for(++j; j != n.end(); ++j) { - if(toRemove.find((*j).getId()) != toRemove.end()) { - ++removals; - } else if((*j).getKind() == kind::AND) { - sub = *j; - if((subremovals = removeFromConjunction(sub, toRemove)) > 0) { - removals += subremovals; - b << sub; - } else { - b << *j; - } - } else { - b << *j; - } - } - if(b.getNumChildren() == 0) { - n = d_true; - b.clear(); - } else if(b.getNumChildren() == 1) { - n = b[0]; - b.clear(); - } else { - n = b; - } - n = Rewriter::rewrite(n); - return removals; - } - } - - Assert(removals == 0); - return 0; -} - -void SmtEnginePrivate::doMiplibTrick() { - Assert(d_assertions.getRealAssertionsEnd() == d_assertions.size()); - Assert(!options::incrementalSolving()); - - const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); - unordered_set removeAssertions; - - NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); - - SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions(); - unordered_map intVars; - for(vector::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) { - if(d_propagator.isAssigned(*i)) { - Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl; - continue; - } - - vector assertions; - booleans::CircuitPropagator::BackEdgesMap::const_iterator j = backEdges.find(*i); - // if not in back edges map, the bool var is unconstrained, showing up in no assertions. - // if maps to an empty vector, that means the bool var was asserted itself. - if(j != backEdges.end()) { - if(!(*j).second.empty()) { - traceBackToAssertions((*j).second, assertions); - } else { - assertions.push_back(*i); - } - } - Debug("miplib") << "for " << *i << endl; - bool eligible = true; - map, uint64_t> marks; - map, vector > coef; - map, vector > checks; - map, vector > asserts; - for(vector::const_iterator j = assertions.begin(); j != assertions.end(); ++j) { - Debug("miplib") << " found: " << *j << endl; - if((*j).getKind() != kind::IMPLIES) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl; - break; - } - Node conj = BooleanSimplification::simplify((*j)[0]); - if(conj.getKind() == kind::AND && conj.getNumChildren() > 6) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl; - break; - } - if(conj.getKind() != kind::AND && !conj.isVar() && !(conj.getKind() == kind::NOT && conj[0].isVar())) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl; - break; - } - if((*j)[1].getKind() != kind::EQUAL || - !( ( (*j)[1][0].isVar() && - (*j)[1][1].getKind() == kind::CONST_RATIONAL ) || - ( (*j)[1][0].getKind() == kind::CONST_RATIONAL && - (*j)[1][1].isVar() ) )) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl; - break; - } - if(conj.getKind() == kind::AND) { - vector posv; - bool found_x = false; - map neg; - for(Node::iterator ii = conj.begin(); ii != conj.end(); ++ii) { - if((*ii).isVar()) { - posv.push_back(*ii); - neg[*ii] = false; - found_x = found_x || *i == *ii; - } else if((*ii).getKind() == kind::NOT && (*ii)[0].isVar()) { - posv.push_back((*ii)[0]); - neg[(*ii)[0]] = true; - found_x = found_x || *i == (*ii)[0]; - } else { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (non-var: " << *ii << ")" << endl; - break; - } - if(d_propagator.isAssigned(posv.back())) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (" << posv.back() << " asserted)" << endl; - break; - } - } - if(!eligible) { - break; - } - if(!found_x) { - eligible = false; - Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i << " in conjunction)" << endl; - break; - } - sort(posv.begin(), posv.end()); - const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); - const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0]; - const pair pos_var(pos, var); - const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst() : (*j)[1][1].getConst(); - uint64_t mark = 0; - unsigned countneg = 0, thepos = 0; - for(unsigned ii = 0; ii < pos.getNumChildren(); ++ii) { - if(neg[pos[ii]]) { - ++countneg; - } else { - thepos = ii; - mark |= (0x1 << ii); - } - } - if((marks[pos_var] & (1lu << mark)) != 0) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; - break; - } - Debug("miplib") << "mark is " << mark << " -- " << (1lu << mark) << endl; - marks[pos_var] |= (1lu << mark); - Debug("miplib") << "marks[" << pos << "," << var << "] now " << marks[pos_var] << endl; - if(countneg == pos.getNumChildren()) { - if(constant != 0) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl; - break; - } - } else if(countneg == pos.getNumChildren() - 1) { - Assert(coef[pos_var].size() <= 6 && thepos < 6); - if(coef[pos_var].size() <= thepos) { - coef[pos_var].resize(thepos + 1); - } - coef[pos_var][thepos] = constant; - } else { - if(checks[pos_var].size() <= mark) { - checks[pos_var].resize(mark + 1); - } - checks[pos_var][mark] = constant; - } - asserts[pos_var].push_back(*j); - } else { - TNode x = conj; - if(x != *i && x != (*i).notNode()) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl; - break; - } - const bool xneg = (x.getKind() == kind::NOT); - x = xneg ? x[0] : x; - Debug("miplib") << " x:" << x << " " << xneg << endl; - const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0]; - const pair x_var(x, var); - const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst() : (*j)[1][1].getConst(); - unsigned mark = (xneg ? 0 : 1); - if((marks[x_var] & (1u << mark)) != 0) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; - break; - } - marks[x_var] |= (1u << mark); - if(xneg) { - if(constant != 0) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl; - break; - } - } else { - Assert(coef[x_var].size() <= 6); - coef[x_var].resize(6); - coef[x_var][0] = constant; - } - asserts[x_var].push_back(*j); - } - } - if(eligible) { - for(map, uint64_t>::const_iterator j = marks.begin(); j != marks.end(); ++j) { - const TNode pos = (*j).first.first; - const TNode var = (*j).first.second; - const pair& pos_var = (*j).first; - const uint64_t mark = (*j).second; - const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1; - uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1; - expected = (expected == 0) ? -1 : expected; // fix for overflow - Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl; - Assert(pos.getKind() == kind::AND || pos.isVar()); - if(mark != expected) { - Debug("miplib") << " -- INELIGIBLE " << pos << " -- (insufficiently marked, got " << mark << " for " << numVars << " vars, expected " << expected << endl; - } else { - if(mark != 3) { // exclude single-var case; nothing to check there - uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1; - sz = (sz == 0) ? -1 : sz; // fix for overflow - Assert(sz == mark, "expected size %u == mark %u", sz, mark); - for(size_t k = 0; k < checks[pos_var].size(); ++k) { - if((k & (k - 1)) != 0) { - Rational sum = 0; - Debug("miplib") << k << " => " << checks[pos_var][k] << endl; - for(size_t v = 1, kk = k; kk != 0; ++v, kk >>= 1) { - if((kk & 0x1) == 1) { - Assert(pos.getKind() == kind::AND); - Debug("miplib") << "var " << v << " : " << pos[v - 1] << " coef:" << coef[pos_var][v - 1] << endl; - sum += coef[pos_var][v - 1]; - } - } - Debug("miplib") << "checkSum is " << sum << " input says " << checks[pos_var][k] << endl; - if(sum != checks[pos_var][k]) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE " << pos << " -- (nonlinear combination)" << endl; - break; - } - } else { - Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var - } - } - } - if(!eligible) { - eligible = true; // next is still eligible - continue; - } - - Debug("miplib") << " -- ELIGIBLE " << *i << " , " << pos << " --" << endl; - vector newVars; - expr::NodeSelfIterator ii, iiend; - if(pos.getKind() == kind::AND) { - ii = pos.begin(); - iiend = pos.end(); - } else { - ii = expr::NodeSelfIterator::self(pos); - iiend = expr::NodeSelfIterator::selfEnd(pos); - } - for(; ii != iiend; ++ii) { - Node& varRef = intVars[*ii]; - if(varRef.isNull()) { - stringstream ss; - ss << "mipvar_" << *ii; - Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME); - Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); - Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); - addFormula(Rewriter::rewrite(geq.andNode(leq)), false, false); - SubstitutionMap nullMap(&d_fakeContext); - Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions - status = d_smt.d_theoryEngine->solve(geq, nullMap); - Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED, - "unexpected solution from arith's ppAssert()"); - Assert(nullMap.empty(), - "unexpected substitution from arith's ppAssert()"); - status = d_smt.d_theoryEngine->solve(leq, nullMap); - Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED, - "unexpected solution from arith's ppAssert()"); - Assert(nullMap.empty(), - "unexpected substitution from arith's ppAssert()"); - d_smt.d_theoryEngine->getModel()->addSubstitution(*ii, newVar.eqNode(one)); - newVars.push_back(newVar); - varRef = newVar; - } else { - newVars.push_back(varRef); - } - if(!d_smt.d_logic.areIntegersUsed()) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableIntegers(); - d_smt.d_logic.lock(); - } - } - Node sum; - if(pos.getKind() == kind::AND) { - NodeBuilder<> sumb(kind::PLUS); - for(size_t ii = 0; ii < pos.getNumChildren(); ++ii) { - sumb << nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][ii]), newVars[ii]); - } - sum = sumb; - } else { - sum = nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); - } - Debug("miplib") << "vars[] " << var << endl - << " eq " << Rewriter::rewrite(sum) << endl; - Node newAssertion = var.eqNode(Rewriter::rewrite(sum)); - if (top_level_substs.hasSubstitution(newAssertion[0])) - { - // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; - // Warning() << "REPLACE " << newAssertion[1] << endl; - // Warning() << "ORIG " << - // top_level_substs.getSubstitution(newAssertion[0]) << endl; - Assert(top_level_substs.getSubstitution(newAssertion[0]) - == newAssertion[1]); - } else if(pos.getNumChildren() <= options::arithMLTrickSubstitutions()) { - top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]); - Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl; - } else { - Debug("miplib") << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl; - } - newAssertion = Rewriter::rewrite(newAssertion); - Debug("miplib") << " " << newAssertion << endl; - addFormula(newAssertion, false, false); - Debug("miplib") << " assertions to remove: " << endl; - for(vector::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) { - Debug("miplib") << " " << *k << endl; - removeAssertions.insert((*k).getId()); - } - } - } - } - } - if(!removeAssertions.empty()) { - Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl; - for (size_t i = 0; i < d_assertions.getRealAssertionsEnd(); ++i) - { - if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) { - Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl; - d_assertions[i] = d_true; - ++d_smt.d_stats->d_numMiplibAssertionsRemoved; - } else if(d_assertions[i].getKind() == kind::AND) { - size_t removals = removeFromConjunction(d_assertions[i], removeAssertions); - if(removals > 0) { - Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl; - Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals << " conjuncts" << endl; - d_smt.d_stats->d_numMiplibAssertionsRemoved += removals; - } - } - Debug("miplib") << "had: " << d_assertions[i] << endl; - d_assertions[i] = - Rewriter::rewrite(top_level_substs.apply(d_assertions[i])); - Debug("miplib") << "now: " << d_assertions[i] << endl; - } - } else { - Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl; - } - d_assertions.updateRealAssertionsEnd(); -} - - // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() { @@ -3675,13 +3259,8 @@ bool SmtEnginePrivate::simplifyAssertions() // re-simplification, which we don't expect to be useful anyway) d_assertions.getRealAssertionsEnd() == d_assertions.size()) { - Chat() << "...fixing miplib encodings..." << endl; - Trace("simplify") << "SmtEnginePrivate::simplify(): " - << "looking for miplib pseudobooleans..." << endl; - - TimerStat::CodeTimer miplibTimer(d_smt.d_stats->d_miplibPassTime); - - doMiplibTrick(); + d_preprocessingPassRegistry.getPass("miplib-trick") + ->apply(&d_assertions); } else { Trace("simplify") << "SmtEnginePrivate::simplify(): " << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;