diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-20 14:03:04 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-20 14:03:04 -0500 |
commit | 03a11423f2c14c7806d1390094dbd6b47a99cefc (patch) | |
tree | 0a9b4783d72b35128064fae6d08633b4be868204 /src/theory/arith | |
parent | 252cd598a389adbb309019883e9a48d091452612 (diff) |
Internally remove redundant assertions and infer equalities in NonLinearExtension (#1633)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 158 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 18 |
2 files changed, 151 insertions, 25 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 5694ce451..07cf43a35 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1112,6 +1112,124 @@ int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) { return sum; } +void NonlinearExtension::getAssertions(std::vector<Node>& assertions) +{ + Trace("nl-ext") << "Getting assertions..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); + // get the assertions + std::map<Node, Rational> init_bounds[2]; + std::map<Node, Node> init_bounds_lit[2]; + unsigned nassertions = 0; + std::unordered_set<Node, NodeHashFunction> init_assertions; + for (Theory::assertions_iterator it = d_containing.facts_begin(); + it != d_containing.facts_end(); + ++it) + { + nassertions++; + const Assertion& assertion = *it; + Node lit = assertion.assertion; + init_assertions.insert(lit); + // check for concrete bounds + bool pol = lit.getKind() != NOT; + Node atom_orig = lit.getKind() == NOT ? lit[0] : lit; + + std::vector<Node> atoms; + if (atom_orig.getKind() == EQUAL) + { + if (pol) + { + // t = s is ( t >= s ^ t <= s ) + for (unsigned i = 0; i < 2; i++) + { + Node atom_new = nm->mkNode(GEQ, atom_orig[i], atom_orig[1 - i]); + atom_new = Rewriter::rewrite(atom_new); + atoms.push_back(atom_new); + } + } + } + else + { + atoms.push_back(atom_orig); + } + + for (const Node& atom : atoms) + { + // non-strict bounds only + if (atom.getKind() == GEQ || (!pol && atom.getKind() == GT)) + { + Node p = atom[0]; + Assert(atom[1].isConst()); + Rational bound = atom[1].getConst<Rational>(); + if (!pol) + { + if (atom[0].getType().isInteger()) + { + // ~( p >= c ) ---> ( p <= c-1 ) + bound = bound - Rational(1); + } + } + unsigned bindex = pol ? 0 : 1; + bool setBound = true; + std::map<Node, Rational>::iterator itb = init_bounds[bindex].find(p); + if (itb != init_bounds[bindex].end()) + { + if (itb->second == bound) + { + setBound = atom_orig.getKind() == EQUAL; + } + else + { + setBound = pol ? itb->second < bound : itb->second > bound; + } + if (setBound) + { + // the bound is subsumed + init_assertions.erase(init_bounds_lit[bindex][p]); + } + } + if (setBound) + { + Trace("nl-ext-init") << (pol ? "Lower" : "Upper") << " bound for " + << p << " : " << bound << std::endl; + init_bounds[bindex][p] = bound; + init_bounds_lit[bindex][p] = lit; + } + } + } + } + // for each bound that is the same, ensure we've inferred the equality + for (std::pair<const Node, Rational>& ib : init_bounds[0]) + { + Node p = ib.first; + Node lit1 = init_bounds_lit[0][p]; + if (lit1.getKind() != EQUAL) + { + std::map<Node, Rational>::iterator itb = init_bounds[1].find(p); + if (itb != init_bounds[1].end()) + { + if (ib.second == itb->second) + { + Node eq = p.eqNode(nm->mkConst(ib.second)); + eq = Rewriter::rewrite(eq); + Node lit2 = init_bounds_lit[1][p]; + Assert(lit2.getKind() != EQUAL); + // use the equality instead, thus these are redundant + init_assertions.erase(lit1); + init_assertions.erase(lit2); + init_assertions.insert(eq); + } + } + } + } + + for (const Node& a : init_assertions) + { + assertions.push_back(a); + } + Trace("nl-ext") << "...keep " << assertions.size() << " / " << nassertions + << " assertions." << std::endl; +} + std::vector<Node> NonlinearExtension::checkModel( const std::vector<Node>& assertions) { @@ -1551,7 +1669,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, //-----------------------------------inferred bounds lemmas // e.g. x >= t => y*x >= y*t std::vector< Node > nt_lemmas; - lemmas = checkMonomialInferBounds( nt_lemmas, false_asserts ); + lemmas = checkMonomialInferBounds(nt_lemmas, assertions, false_asserts); // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << // nt_lemmas.size() << std::endl; prioritize lemmas that do not // introduce new monomials @@ -1573,7 +1691,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, //------------------------------------factoring lemmas // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t if( options::nlExtFactor() ){ - lemmas = checkFactoring( false_asserts ); + lemmas = checkFactoring(assertions, false_asserts); lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; @@ -1634,26 +1752,22 @@ void NonlinearExtension::check(Theory::Effort e) { } } } else { + // get the assertions + std::vector<Node> assertions; + getAssertions(assertions); + bool needsRecheck; do { needsRecheck = false; Assert(e == Theory::EFFORT_LAST_CALL); - Trace("nl-ext-mv") << "Getting model values... check for [model-false]" - << std::endl; + // reset cached information d_mv[0].clear(); d_mv[1].clear(); - // get the assertions - std::vector<Node> assertions; - for (Theory::assertions_iterator it = d_containing.facts_begin(); - it != d_containing.facts_end(); - ++it) - { - const Assertion& assertion = *it; - assertions.push_back(assertion.assertion); - } + Trace("nl-ext-mv") << "Getting model values... check for [model-false]" + << std::endl; // get the assertions that are false in the model const std::vector<Node> false_asserts = checkModel(assertions); @@ -2499,15 +2613,15 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { } std::vector<Node> NonlinearExtension::checkMonomialInferBounds( - std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts) + std::vector<Node>& nt_lemmas, + const std::vector<Node>& asserts, + const std::vector<Node>& false_asserts) { std::vector< Node > lemmas; // register constraints Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; - for (context::CDList<Assertion>::const_iterator it = - d_containing.facts_begin(); - it != d_containing.facts_end(); ++it) { - Node lit = (*it).assertion; + for (const Node& lit : asserts) + { bool polarity = lit.getKind() != NOT; Node atom = lit.getKind() == NOT ? lit[0] : lit; registerConstraint(atom); @@ -2764,14 +2878,12 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( } std::vector<Node> NonlinearExtension::checkFactoring( - const std::vector<Node>& false_asserts) + const std::vector<Node>& asserts, const std::vector<Node>& false_asserts) { std::vector< Node > lemmas; Trace("nl-ext") << "Get factoring lemmas..." << std::endl; - for (context::CDList<Assertion>::const_iterator it = - d_containing.facts_begin(); - it != d_containing.facts_end(); ++it) { - Node lit = (*it).assertion; + for (const Node& lit : asserts) + { bool polarity = lit.getKind() != NOT; Node atom = lit.getKind() == NOT ? lit[0] : lit; if (std::find(false_asserts.begin(), false_asserts.end(), lit) diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index a37ef97f8..96d37cbc2 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -245,6 +245,17 @@ class NonlinearExtension { void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order, unsigned orderType); + /** get assertions + * + * Let M be the set of assertions known by THEORY_ARITH. This function adds a + * set of literals M' to assertions such that M' and M are equivalent. + * + * Examples of how M' differs with M: + * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where + * c and c' are constants, + * (2) M' may contain t = c if both t >= c and t <= c are in M. + */ + void getAssertions(std::vector<Node>& assertions); /** check model * * Returns the subset of assertions whose concrete values we cannot show are @@ -700,7 +711,9 @@ private: * that occur in the current context. */ std::vector<Node> checkMonomialInferBounds( - std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts); + std::vector<Node>& nt_lemmas, + const std::vector<Node>& asserts, + const std::vector<Node>& false_asserts); /** check factoring * @@ -714,7 +727,8 @@ private: * ...where k is fresh and x*z + y*z > t is a * constraint that occurs in the current context. */ - std::vector<Node> checkFactoring(const std::vector<Node>& false_asserts); + std::vector<Node> checkFactoring(const std::vector<Node>& asserts, + const std::vector<Node>& false_asserts); /** check monomial infer resolution bounds * |