From 785b3aec09a5ff9bb4e918e6d8215ba166d34e7d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 5 Feb 2013 16:00:02 -0500 Subject: [PATCH] Fix to miplib trick to make it less "cautious" and apply in more cases --- src/smt/smt_engine.cpp | 127 ++++++++++-------------- test/regress/regress0/arith/Makefile.am | 2 + test/regress/regress0/arith/miplib3.cvc | 34 +++++++ test/regress/regress0/arith/miplib4.cvc | 13 +++ 4 files changed, 104 insertions(+), 72 deletions(-) create mode 100644 test/regress/regress0/arith/miplib3.cvc create mode 100644 test/regress/regress0/arith/miplib4.cvc diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7ee660a85..0f0012971 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2029,11 +2029,10 @@ void SmtEnginePrivate::doMiplibTrick() { } Debug("miplib") << "for " << *i << endl; bool eligible = true; - map vars; - map marks; - map > coef; - map > checks; - map > asserts; + 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) { @@ -2093,24 +2092,11 @@ void SmtEnginePrivate::doMiplibTrick() { Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i << " in conjunction)" << endl; break; } - /* - if(x > y) { - // symmetric - continue; - } - */ sort(posv.begin(), posv.end()); - Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); - TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0]; + 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(); - Node& v = vars[pos]; - if(v.isNull()) { - v = var; - } else if(v != var) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (wrong var " << v << " != " << var << ")" << endl; - break; - } uint64_t mark = 0; unsigned countneg = 0, thepos = 0; for(unsigned ii = 0; ii < pos.getNumChildren(); ++ii) { @@ -2121,14 +2107,14 @@ void SmtEnginePrivate::doMiplibTrick() { mark |= (0x1 << ii); } } - if((marks[pos] & (1lu << mark)) != 0) { + 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] |= (1lu << mark); - Debug("miplib") << "marks[" << pos << "] now " << marks[pos] << 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; @@ -2136,16 +2122,16 @@ void SmtEnginePrivate::doMiplibTrick() { break; } } else if(countneg == pos.getNumChildren() - 1) { - Assert(coef[pos].size() <= 6 && thepos < 6); - coef[pos].resize(6); - coef[pos][thepos] = constant; + Assert(coef[pos_var].size() <= 6 && thepos < 6); + coef[pos_var].resize(6); + coef[pos_var][thepos] = constant; } else { - if(checks[pos].size() <= mark) { - checks[pos].resize(mark + 1); + if(checks[pos_var].size() <= mark) { + checks[pos_var].resize(mark + 1); } - checks[pos][mark] = constant; + checks[pos_var][mark] = constant; } - asserts[pos].push_back(*j); + asserts[pos_var].push_back(*j); } else { TNode x = conj; if(x != *i && x != (*i).notNode()) { @@ -2153,26 +2139,19 @@ void SmtEnginePrivate::doMiplibTrick() { Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl; break; } - bool xneg = (x.getKind() == kind::NOT); + const bool xneg = (x.getKind() == kind::NOT); x = xneg ? x[0] : x; Debug("miplib") << " x:" << x << " " << xneg << endl; - TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0]; + 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(); - Node& v = vars[x]; - if(v.isNull()) { - v = var; - } else if(v != var) { - eligible = false; - Debug("miplib") << " -- INELIGIBLE -- (wrong var " << v << " != " << var << ")" << endl; - break; - } unsigned mark = (xneg ? 0 : 1); - if((marks[x] & (1u << mark)) != 0) { + if((marks[x_var] & (1u << mark)) != 0) { eligible = false; Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; break; } - marks[x] |= (1u << mark); + marks[x_var] |= (1u << mark); if(xneg) { if(constant != 0) { eligible = false; @@ -2180,39 +2159,43 @@ void SmtEnginePrivate::doMiplibTrick() { break; } } else { - Assert(coef[x].size() <= 6); - coef[x].resize(6); - coef[x][0] = constant; - if(checks[x].size() <= mark) { - checks[x].resize(mark + 1); + Assert(coef[x_var].size() <= 6); + coef[x_var].resize(6); + coef[x_var][0] = constant; + if(checks[x_var].size() <= mark) { + checks[x_var].resize(mark + 1); } - checks[x][mark] = constant; + checks[x_var][mark] = constant; } - asserts[x].push_back(*j); + asserts[x_var].push_back(*j); } } if(eligible) { - for(map::const_iterator j = marks.begin(); j != marks.end(); ++j) { - unsigned numVars = (*j).first.getKind() == kind::AND ? (*j).first.getNumChildren() : 1; + 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") << "[" << (*j).first << "] => " << hex << (*j).second << " expect " << expected << dec << endl; - Assert((*j).first.getKind() == kind::AND || (*j).first.isVar()); - if((*j).second != expected) { - Debug("miplib") << " -- INELIGIBLE " << (*j).first << " -- (insufficiently marked, got " << (*j).second << " for " << numVars << " vars, expected " << expected << endl; + 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(false) { //checks[(*j).first] != coef[(*j).first][0] + coef[(*j).first][1]) { - Debug("miplib") << " -- INELIGIBLE " << (*j).first << " -- (not linear combination)" << endl; + if(false) { //checks[pos] != coef[pos][0] + coef[pos][1]) { + Debug("miplib") << " -- INELIGIBLE " << pos << " -- (not linear combination)" << endl; } else { - Debug("miplib") << " -- ELIGIBLE " << *i << " , " << (*j).first << " --" << endl; + Debug("miplib") << " -- ELIGIBLE " << *i << " , " << pos << " --" << endl; vector newVars; expr::NodeSelfIterator ii, iiend; - if((*j).first.getKind() == kind::AND) { - ii = (*j).first.begin(); - iiend = (*j).first.end(); + if(pos.getKind() == kind::AND) { + ii = pos.begin(); + iiend = pos.end(); } else { - ii = expr::NodeSelfIterator::self((*j).first); - iiend = expr::NodeSelfIterator::selfEnd((*j).first); + ii = expr::NodeSelfIterator::self(pos); + iiend = expr::NodeSelfIterator::selfEnd(pos); } for(; ii != iiend; ++ii) { Node& varRef = intVars[*ii]; @@ -2248,24 +2231,24 @@ void SmtEnginePrivate::doMiplibTrick() { } } Node sum; - if((*j).first.getKind() == kind::AND) { + if(pos.getKind() == kind::AND) { NodeBuilder<> sumb(kind::PLUS); - for(size_t ii = 0; ii < (*j).first.getNumChildren(); ++ii) { - sumb << nm->mkNode(kind::MULT, nm->mkConst(coef[(*j).first][ii]), newVars[ii]); + 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[(*j).first][0]), newVars[0]); + sum = nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); } - Debug("miplib") << "vars[] " << vars[(*j).first] << endl + Debug("miplib") << "vars[] " << var << endl << " eq " << Rewriter::rewrite(sum) << endl; - Node newAssertion = vars[(*j).first].eqNode(Rewriter::rewrite(sum)); + Node newAssertion = var.eqNode(Rewriter::rewrite(sum)); if(d_topLevelSubstitutions.hasSubstitution(newAssertion[0])) { //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; //Warning() << "REPLACE " << newAssertion[1] << endl; //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl; Assert(d_topLevelSubstitutions.getSubstitution(newAssertion[0]) == newAssertion[1]); - } else if((*j).first.getNumChildren() <= options::arithMLTrickSubstitutions()) { + } else if(pos.getNumChildren() <= options::arithMLTrickSubstitutions()) { d_topLevelSubstitutions.addSubstitution(newAssertion[0], newAssertion[1]); Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl; } else { @@ -2275,7 +2258,7 @@ void SmtEnginePrivate::doMiplibTrick() { Debug("miplib") << " " << newAssertion << endl; d_assertionsToCheck.push_back(newAssertion); Debug("miplib") << " assertions to remove: " << endl; - for(vector::const_iterator k = asserts[(*j).first].begin(); k != asserts[(*j).first].end(); ++k) { + 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()); } diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index b0cdc5b91..40f04b239 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -41,6 +41,8 @@ TESTS = \ bug443.delta01.smt \ miplib.cvc \ miplib2.cvc \ + miplib3.cvc \ + miplib4.cvc \ miplibtrick.smt # problem__003.smt2 diff --git a/test/regress/regress0/arith/miplib3.cvc b/test/regress/regress0/arith/miplib3.cvc new file mode 100644 index 000000000..009effb74 --- /dev/null +++ b/test/regress/regress0/arith/miplib3.cvc @@ -0,0 +1,34 @@ +% COMMAND-LINE: --enable-miplib-trick +% EXPECT: sat +% EXIT: 10 + +tmp1, tmp2, tmp3, tmp4 : INT; +x, y, z : BOOLEAN; + +% x = {0, 1}, (NOT x) = 1 - x +% i*Nx + j*Ny + k = 0 +% i*x + j*Ny + k = 4 +% i*Nx + j*y + k = 6 +% i*x + j*y + k = 10 + +ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; +ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; +ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; +ASSERT x AND ( y AND TRUE) => tmp1 = 10; + +ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0; +ASSERT x AND (NOT z AND TRUE) => tmp2 = 2; +ASSERT NOT x AND ( z AND TRUE) => tmp2 = 9; +ASSERT x AND ( z AND TRUE) => tmp2 = 11; + +ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0; +ASSERT y AND (NOT z AND TRUE) => tmp3 = 5; +ASSERT NOT y AND ( z AND TRUE) => tmp3 = 16; +ASSERT y AND ( z AND TRUE) => tmp3 = 21; + +ASSERT NOT x AND (NOT y AND TRUE) => tmp4 = 0; +ASSERT x AND (NOT y AND TRUE) => tmp4 = 4; +ASSERT NOT x AND ( y AND TRUE) => tmp4 = 6; +ASSERT x AND ( y AND TRUE) => tmp4 = 10; + +CHECKSAT; diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc new file mode 100644 index 000000000..d56015222 --- /dev/null +++ b/test/regress/regress0/arith/miplib4.cvc @@ -0,0 +1,13 @@ +% COMMAND-LINE: --enable-miplib-trick +% EXPECT: sat +% EXIT: 10 + +tmp1 : INT; +x, y : BOOLEAN; + +ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; +ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; +ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; +ASSERT x AND ( y AND TRUE) => tmp1 = 12; + +CHECKSAT; -- 2.30.2