diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-29 14:38:33 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-29 16:38:33 -0500 |
commit | 3eac9d04c5d4bfba81142d4a5fe91b86590b32ae (patch) | |
tree | e3ed07e7268d57ce27c2f748524bd9ff45859579 /src/smt | |
parent | 1ae13e7e30aaaa088de057496c649649067867dc (diff) |
Refactor MipLibTrick preprocessing pass. (#2359)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/logic_request.cpp | 11 | ||||
-rw-r--r-- | src/smt/logic_request.h | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 443 |
3 files changed, 25 insertions, 432 deletions
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<Node> d_boolVars; + + bool d_propagatorNeedsFinish; /** Assertions in the preprocessing pipeline */ AssertionPipeline d_assertions; @@ -576,23 +568,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<Node>& nodes, - std::vector<TNode>& assertions); - - /** - * Remove conjuncts in toRemove from conjunction n. Return # of removed - * conjuncts. - */ - size_t removeFromConjunction( - Node& n, const std::unordered_set<unsigned long>& 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 * any way. @@ -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> applySubsts( @@ -2644,6 +2613,8 @@ void SmtEnginePrivate::finishInit() new ITESimp(d_preprocessingPassContext.get())); std::unique_ptr<NlExtPurify> nlExtPurify( new NlExtPurify(d_preprocessingPassContext.get())); + std::unique_ptr<MipLibTrick> mipLibTrick( + new MipLibTrick(d_preprocessingPassContext.get())); std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess( new QuantifiersPreprocess(d_preprocessingPassContext.get())); std::unique_ptr<PseudoBooleanProcessor> 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<Node>& nodes, std::vector<TNode>& assertions) { - const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); - for(vector<Node>::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<unsigned long>& 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<unsigned long> 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<TNode, Node, TNodeHashFunction> intVars; - for(vector<Node>::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<TNode> 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<pair<Node, Node>, uint64_t> marks; - map<pair<Node, Node>, vector<Rational> > coef; - map<pair<Node, Node>, vector<Rational> > checks; - map<pair<Node, Node>, vector<TNode> > asserts; - for(vector<TNode>::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<Node> posv; - bool found_x = false; - map<TNode, bool> 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<Node, Node> pos_var(pos, var); - const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst<Rational>() : (*j)[1][1].getConst<Rational>(); - 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<Node, Node> x_var(x, var); - const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst<Rational>() : (*j)[1][1].getConst<Rational>(); - 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<pair<Node, Node>, 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<Node, Node>& 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<Node> 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<TNode>::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; |