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)
{
//-----------------------------------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
//------------------------------------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;
}
}
} 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);
}
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);
}
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)
projects / cvc5.git / commitdiff