diff options
Diffstat (limited to 'src/theory/arith/nl/nl_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/nl_solver.cpp | 1592 |
1 files changed, 0 insertions, 1592 deletions
diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp deleted file mode 100644 index 521539674..000000000 --- a/src/theory/arith/nl/nl_solver.cpp +++ /dev/null @@ -1,1592 +0,0 @@ -/********************* */ -/*! \file nl_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Ahmed Irfan - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Implementation of non-linear solver - **/ - -#include "theory/arith/nl/nl_solver.h" - -#include "options/arith_options.h" -#include "theory/arith/arith_msum.h" -#include "theory/arith/arith_utilities.h" -#include "theory/arith/theory_arith.h" -#include "theory/theory_model.h" - -using namespace CVC4::kind; - -namespace CVC4 { -namespace theory { -namespace arith { -namespace nl { - -void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) -{ - Node t = ArithMSum::mkCoeffTerm(coeff, x); - Trace(c) << t << " " << type << " " << rhs; -} - -bool hasNewMonomials(Node n, const std::vector<Node>& existing) -{ - std::set<Node> visited; - - std::vector<Node> worklist; - worklist.push_back(n); - while (!worklist.empty()) - { - Node current = worklist.back(); - worklist.pop_back(); - if (visited.find(current) == visited.end()) - { - visited.insert(current); - if (current.getKind() == NONLINEAR_MULT) - { - if (std::find(existing.begin(), existing.end(), current) - == existing.end()) - { - return true; - } - } - else - { - worklist.insert(worklist.end(), current.begin(), current.end()); - } - } - } - return false; -} - -NlSolver::NlSolver(TheoryArith& containing, NlModel& model) - : d_containing(containing), - d_model(model), - d_cdb(d_mdb), - d_zero_split(containing.getUserContext()) -{ - NodeManager* nm = NodeManager::currentNM(); - d_true = nm->mkConst(true); - d_false = nm->mkConst(false); - d_zero = nm->mkConst(Rational(0)); - d_one = nm->mkConst(Rational(1)); - d_neg_one = nm->mkConst(Rational(-1)); - d_order_points.push_back(d_neg_one); - d_order_points.push_back(d_zero); - d_order_points.push_back(d_one); -} - -NlSolver::~NlSolver() {} - -void NlSolver::initLastCall(const std::vector<Node>& assertions, - const std::vector<Node>& false_asserts, - const std::vector<Node>& xts) -{ - d_ms_vars.clear(); - d_ms_proc.clear(); - d_ms.clear(); - d_mterms.clear(); - d_m_nconst_factor.clear(); - d_tplane_refine.clear(); - d_ci.clear(); - d_ci_exp.clear(); - d_ci_max.clear(); - - Trace("nl-ext-mv") << "Extended terms : " << std::endl; - // for computing congruence - std::map<Kind, ArgTrie> argTrie; - for (unsigned i = 0, xsize = xts.size(); i < xsize; i++) - { - Node a = xts[i]; - d_model.computeConcreteModelValue(a); - d_model.computeAbstractModelValue(a); - d_model.printModelValue("nl-ext-mv", a); - Kind ak = a.getKind(); - if (ak == NONLINEAR_MULT) - { - d_ms.push_back(a); - - // context-independent registration - d_mdb.registerMonomial(a); - - const std::vector<Node>& varList = d_mdb.getVariableList(a); - for (const Node& v : varList) - { - if (std::find(d_ms_vars.begin(), d_ms_vars.end(), v) == d_ms_vars.end()) - { - d_ms_vars.push_back(v); - } - Node mvk = d_model.computeAbstractModelValue(v); - if (!mvk.isConst()) - { - d_m_nconst_factor[a] = true; - } - } - // mark processed if has a "one" factor (will look at reduced monomial)? - } - } - - // register constants - d_mdb.registerMonomial(d_one); - for (unsigned j = 0; j < d_order_points.size(); j++) - { - Node c = d_order_points[j]; - d_model.computeConcreteModelValue(c); - d_model.computeAbstractModelValue(c); - } - - // register variables - Trace("nl-ext-mv") << "Variables in monomials : " << std::endl; - for (unsigned i = 0; i < d_ms_vars.size(); i++) - { - Node v = d_ms_vars[i]; - d_mdb.registerMonomial(v); - d_model.computeConcreteModelValue(v); - d_model.computeAbstractModelValue(v); - d_model.printModelValue("nl-ext-mv", v); - } - - Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl; -} - -void NlSolver::setMonomialFactor(Node a, Node b, const NodeMultiset& common) -{ - // Could not tell if this was being inserted intentionally or not. - std::map<Node, Node>& mono_diff_a = d_mono_diff[a]; - if (mono_diff_a.find(b) == mono_diff_a.end()) - { - Trace("nl-ext-mono-factor") - << "Set monomial factor for " << a << "/" << b << std::endl; - mono_diff_a[b] = d_mdb.mkMonomialRemFactor(a, common); - } -} - -std::vector<NlLemma> NlSolver::checkSplitZero() -{ - std::vector<NlLemma> lemmas; - for (unsigned i = 0; i < d_ms_vars.size(); i++) - { - Node v = d_ms_vars[i]; - if (d_zero_split.insert(v)) - { - Node eq = v.eqNode(d_zero); - eq = Rewriter::rewrite(eq); - Node literal = d_containing.getValuation().ensureLiteral(eq); - d_containing.getOutputChannel().requirePhase(literal, true); - lemmas.emplace_back(literal.orNode(literal.negate()), - Inference::SPLIT_ZERO); - } - } - return lemmas; -} - -void NlSolver::assignOrderIds(std::vector<Node>& vars, - NodeMultiset& order, - bool isConcrete, - bool isAbsolute) -{ - SortNlModel smv; - smv.d_nlm = &d_model; - smv.d_isConcrete = isConcrete; - smv.d_isAbsolute = isAbsolute; - smv.d_reverse_order = false; - std::sort(vars.begin(), vars.end(), smv); - - order.clear(); - // assign ordering id's - unsigned counter = 0; - unsigned order_index = isConcrete ? 0 : 1; - Node prev; - for (unsigned j = 0; j < vars.size(); j++) - { - Node x = vars[j]; - Node v = d_model.computeModelValue(x, isConcrete); - if (!v.isConst()) - { - Trace("nl-ext-mvo") << "..do not assign order to " << x << " : " << v - << std::endl; - // don't assign for non-constant values (transcendental function apps) - break; - } - Trace("nl-ext-mvo") << " order " << x << " : " << v << std::endl; - if (v != prev) - { - // builtin points - bool success; - do - { - success = false; - if (order_index < d_order_points.size()) - { - Node vv = d_model.computeModelValue(d_order_points[order_index], - isConcrete); - if (d_model.compareValue(v, vv, isAbsolute) <= 0) - { - counter++; - Trace("nl-ext-mvo") << "O[" << d_order_points[order_index] - << "] = " << counter << std::endl; - order[d_order_points[order_index]] = counter; - prev = vv; - order_index++; - success = true; - } - } - } while (success); - } - if (prev.isNull() || d_model.compareValue(v, prev, isAbsolute) != 0) - { - counter++; - } - Trace("nl-ext-mvo") << "O[" << x << "] = " << counter << std::endl; - order[x] = counter; - prev = v; - } - while (order_index < d_order_points.size()) - { - counter++; - Trace("nl-ext-mvo") << "O[" << d_order_points[order_index] - << "] = " << counter << std::endl; - order[d_order_points[order_index]] = counter; - order_index++; - } -} - -// show a <> 0 by inequalities between variables in monomial a w.r.t 0 -int NlSolver::compareSign(Node oa, - Node a, - unsigned a_index, - int status, - std::vector<Node>& exp, - std::vector<NlLemma>& lem) -{ - Trace("nl-ext-debug") << "Process " << a << " at index " << a_index - << ", status is " << status << std::endl; - NodeManager* nm = NodeManager::currentNM(); - Node mvaoa = d_model.computeAbstractModelValue(oa); - const std::vector<Node>& vla = d_mdb.getVariableList(a); - if (a_index == vla.size()) - { - if (mvaoa.getConst<Rational>().sgn() != status) - { - Node lemma = - safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2)); - lem.emplace_back(lemma, Inference::SIGN); - } - return status; - } - Assert(a_index < vla.size()); - Node av = vla[a_index]; - unsigned aexp = d_mdb.getExponent(a, av); - // take current sign in model - Node mvaav = d_model.computeAbstractModelValue(av); - int sgn = mvaav.getConst<Rational>().sgn(); - Trace("nl-ext-debug") << "Process var " << av << "^" << aexp - << ", model sign = " << sgn << std::endl; - if (sgn == 0) - { - if (mvaoa.getConst<Rational>().sgn() != 0) - { - Node lemma = av.eqNode(d_zero).impNode(oa.eqNode(d_zero)); - lem.emplace_back(lemma, Inference::SIGN); - } - return 0; - } - if (aexp % 2 == 0) - { - exp.push_back(av.eqNode(d_zero).negate()); - return compareSign(oa, a, a_index + 1, status, exp, lem); - } - exp.push_back(nm->mkNode(sgn == 1 ? GT : LT, av, d_zero)); - return compareSign(oa, a, a_index + 1, status * sgn, exp, lem); -} - -bool NlSolver::compareMonomial( - Node oa, - Node a, - NodeMultiset& a_exp_proc, - Node ob, - Node b, - NodeMultiset& b_exp_proc, - std::vector<Node>& exp, - std::vector<NlLemma>& lem, - std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers) -{ - Trace("nl-ext-comp-debug") - << "Check |" << a << "| >= |" << b << "|" << std::endl; - unsigned pexp_size = exp.size(); - if (compareMonomial( - oa, a, 0, a_exp_proc, ob, b, 0, b_exp_proc, 0, exp, lem, cmp_infers)) - { - return true; - } - exp.resize(pexp_size); - Trace("nl-ext-comp-debug") - << "Check |" << b << "| >= |" << a << "|" << std::endl; - if (compareMonomial( - ob, b, 0, b_exp_proc, oa, a, 0, a_exp_proc, 0, exp, lem, cmp_infers)) - { - return true; - } - return false; -} - -Node NlSolver::mkLit(Node a, Node b, int status, bool isAbsolute) -{ - if (status == 0) - { - Node a_eq_b = a.eqNode(b); - if (!isAbsolute) - { - return a_eq_b; - } - Node negate_b = NodeManager::currentNM()->mkNode(UMINUS, b); - return a_eq_b.orNode(a.eqNode(negate_b)); - } - else if (status < 0) - { - return mkLit(b, a, -status); - } - Assert(status == 1 || status == 2); - NodeManager* nm = NodeManager::currentNM(); - Kind greater_op = status == 1 ? GEQ : GT; - if (!isAbsolute) - { - return nm->mkNode(greater_op, a, b); - } - // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) ); - Node zero = mkRationalNode(0); - Node a_is_nonnegative = nm->mkNode(GEQ, a, zero); - Node b_is_nonnegative = nm->mkNode(GEQ, b, zero); - Node negate_a = nm->mkNode(UMINUS, a); - Node negate_b = nm->mkNode(UMINUS, b); - return a_is_nonnegative.iteNode( - b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b), - nm->mkNode(greater_op, a, negate_b)), - b_is_nonnegative.iteNode(nm->mkNode(greater_op, negate_a, b), - nm->mkNode(greater_op, negate_a, negate_b))); -} - -bool NlSolver::cmp_holds(Node x, - Node y, - std::map<Node, std::map<Node, Node> >& cmp_infers, - std::vector<Node>& exp, - std::map<Node, bool>& visited) -{ - if (x == y) - { - return true; - } - else if (visited.find(x) != visited.end()) - { - return false; - } - visited[x] = true; - std::map<Node, std::map<Node, Node> >::iterator it = cmp_infers.find(x); - if (it != cmp_infers.end()) - { - for (std::map<Node, Node>::iterator itc = it->second.begin(); - itc != it->second.end(); - ++itc) - { - exp.push_back(itc->second); - if (cmp_holds(itc->first, y, cmp_infers, exp, visited)) - { - return true; - } - exp.pop_back(); - } - } - return false; -} - -// trying to show a ( >, = ) b by inequalities between variables in -// monomials a,b -bool NlSolver::compareMonomial( - Node oa, - Node a, - unsigned a_index, - NodeMultiset& a_exp_proc, - Node ob, - Node b, - unsigned b_index, - NodeMultiset& b_exp_proc, - int status, - std::vector<Node>& exp, - std::vector<NlLemma>& lem, - std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers) -{ - Trace("nl-ext-comp-debug") - << "compareMonomial " << oa << " and " << ob << ", indices = " << a_index - << " " << b_index << std::endl; - Assert(status == 0 || status == 2); - const std::vector<Node>& vla = d_mdb.getVariableList(a); - const std::vector<Node>& vlb = d_mdb.getVariableList(b); - if (a_index == vla.size() && b_index == vlb.size()) - { - // finished, compare absolute value of abstract model values - int modelStatus = d_model.compare(oa, ob, false, true) * -2; - Trace("nl-ext-comp") << "...finished comparison with " << oa << " <" - << status << "> " << ob - << ", model status = " << modelStatus << std::endl; - if (status != modelStatus) - { - Trace("nl-ext-comp-infer") - << "infer : " << oa << " <" << status << "> " << ob << std::endl; - if (status == 2) - { - // must state that all variables are non-zero - for (unsigned j = 0; j < vla.size(); j++) - { - exp.push_back(vla[j].eqNode(d_zero).negate()); - } - } - NodeManager* nm = NodeManager::currentNM(); - Node clem = nm->mkNode( - IMPLIES, safeConstructNary(AND, exp), mkLit(oa, ob, status, true)); - Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; - lem.emplace_back(clem, Inference::COMPARISON); - cmp_infers[status][oa][ob] = clem; - } - return true; - } - // get a/b variable information - Node av; - unsigned aexp = 0; - unsigned avo = 0; - if (a_index < vla.size()) - { - av = vla[a_index]; - unsigned aexpTotal = d_mdb.getExponent(a, av); - Assert(a_exp_proc[av] <= aexpTotal); - aexp = aexpTotal - a_exp_proc[av]; - if (aexp == 0) - { - return compareMonomial(oa, - a, - a_index + 1, - a_exp_proc, - ob, - b, - b_index, - b_exp_proc, - status, - exp, - lem, - cmp_infers); - } - Assert(d_order_vars.find(av) != d_order_vars.end()); - avo = d_order_vars[av]; - } - Node bv; - unsigned bexp = 0; - unsigned bvo = 0; - if (b_index < vlb.size()) - { - bv = vlb[b_index]; - unsigned bexpTotal = d_mdb.getExponent(b, bv); - Assert(b_exp_proc[bv] <= bexpTotal); - bexp = bexpTotal - b_exp_proc[bv]; - if (bexp == 0) - { - return compareMonomial(oa, - a, - a_index, - a_exp_proc, - ob, - b, - b_index + 1, - b_exp_proc, - status, - exp, - lem, - cmp_infers); - } - Assert(d_order_vars.find(bv) != d_order_vars.end()); - bvo = d_order_vars[bv]; - } - // get "one" information - Assert(d_order_vars.find(d_one) != d_order_vars.end()); - unsigned ovo = d_order_vars[d_one]; - Trace("nl-ext-comp-debug") << "....vars : " << av << "^" << aexp << " " << bv - << "^" << bexp << std::endl; - - //--- cases - if (av.isNull()) - { - if (bvo <= ovo) - { - Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl; - // can multiply b by <=1 - exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, true)); - return compareMonomial(oa, - a, - a_index, - a_exp_proc, - ob, - b, - b_index + 1, - b_exp_proc, - bvo == ovo ? status : 2, - exp, - lem, - cmp_infers); - } - Trace("nl-ext-comp-debug") - << "...failure, unmatched |b|>1 component." << std::endl; - return false; - } - else if (bv.isNull()) - { - if (avo >= ovo) - { - Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl; - // can multiply a by >=1 - exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, true)); - return compareMonomial(oa, - a, - a_index + 1, - a_exp_proc, - ob, - b, - b_index, - b_exp_proc, - avo == ovo ? status : 2, - exp, - lem, - cmp_infers); - } - Trace("nl-ext-comp-debug") - << "...failure, unmatched |a|<1 component." << std::endl; - return false; - } - Assert(!av.isNull() && !bv.isNull()); - if (avo >= bvo) - { - if (bvo < ovo && avo >= ovo) - { - Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl; - // do avo>=1 instead - exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, true)); - return compareMonomial(oa, - a, - a_index + 1, - a_exp_proc, - ob, - b, - b_index, - b_exp_proc, - avo == ovo ? status : 2, - exp, - lem, - cmp_infers); - } - unsigned min_exp = aexp > bexp ? bexp : aexp; - a_exp_proc[av] += min_exp; - b_exp_proc[bv] += min_exp; - Trace("nl-ext-comp-debug") << "...take leading " << min_exp << " from " - << av << " and " << bv << std::endl; - exp.push_back(mkLit(av, bv, avo == bvo ? 0 : 2, true)); - bool ret = compareMonomial(oa, - a, - a_index, - a_exp_proc, - ob, - b, - b_index, - b_exp_proc, - avo == bvo ? status : 2, - exp, - lem, - cmp_infers); - a_exp_proc[av] -= min_exp; - b_exp_proc[bv] -= min_exp; - return ret; - } - if (bvo <= ovo) - { - Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl; - // try multiply b <= 1 - exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, true)); - return compareMonomial(oa, - a, - a_index, - a_exp_proc, - ob, - b, - b_index + 1, - b_exp_proc, - bvo == ovo ? status : 2, - exp, - lem, - cmp_infers); - } - Trace("nl-ext-comp-debug") - << "...failure, leading |b|>|a|>1 component." << std::endl; - return false; -} - -std::vector<NlLemma> NlSolver::checkMonomialSign() -{ - std::vector<NlLemma> lemmas; - std::map<Node, int> signs; - Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl; - for (unsigned j = 0; j < d_ms.size(); j++) - { - Node a = d_ms[j]; - if (d_ms_proc.find(a) == d_ms_proc.end()) - { - std::vector<Node> exp; - if (Trace.isOn("nl-ext-debug")) - { - Node cmva = d_model.computeConcreteModelValue(a); - Trace("nl-ext-debug") - << " process " << a << ", mv=" << cmva << "..." << std::endl; - } - if (d_m_nconst_factor.find(a) == d_m_nconst_factor.end()) - { - signs[a] = compareSign(a, a, 0, 1, exp, lemmas); - if (signs[a] == 0) - { - d_ms_proc[a] = true; - Trace("nl-ext-debug") - << "...mark " << a << " reduced since its value is 0." - << std::endl; - } - } - else - { - Trace("nl-ext-debug") - << "...can't conclude sign lemma for " << a - << " since model value of a factor is non-constant." << std::endl; - } - } - } - return lemmas; -} - -std::vector<NlLemma> NlSolver::checkMonomialMagnitude(unsigned c) -{ - // ensure information is setup - if (c == 0) - { - // sort by absolute values of abstract model values - assignOrderIds(d_ms_vars, d_order_vars, false, true); - - // sort individual variable lists - Trace("nl-ext-proc") << "Assign order var lists..." << std::endl; - d_mdb.sortVariablesByModel(d_ms, d_model); - } - - unsigned r = 1; - std::vector<NlLemma> lemmas; - // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L - // in lemmas - std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers; - Trace("nl-ext") << "Get monomial comparison lemmas (order=" << r - << ", compare=" << c << ")..." << std::endl; - for (unsigned j = 0; j < d_ms.size(); j++) - { - Node a = d_ms[j]; - if (d_ms_proc.find(a) == d_ms_proc.end() - && d_m_nconst_factor.find(a) == d_m_nconst_factor.end()) - { - if (c == 0) - { - // compare magnitude against 1 - std::vector<Node> exp; - NodeMultiset a_exp_proc; - NodeMultiset b_exp_proc; - compareMonomial(a, - a, - a_exp_proc, - d_one, - d_one, - b_exp_proc, - exp, - lemmas, - cmp_infers); - } - else - { - const NodeMultiset& mea = d_mdb.getMonomialExponentMap(a); - if (c == 1) - { - // could compare not just against containing variables? - // compare magnitude against variables - for (unsigned k = 0; k < d_ms_vars.size(); k++) - { - Node v = d_ms_vars[k]; - Node mvcv = d_model.computeConcreteModelValue(v); - if (mvcv.isConst()) - { - std::vector<Node> exp; - NodeMultiset a_exp_proc; - NodeMultiset b_exp_proc; - if (mea.find(v) != mea.end()) - { - a_exp_proc[v] = 1; - b_exp_proc[v] = 1; - setMonomialFactor(a, v, a_exp_proc); - setMonomialFactor(v, a, b_exp_proc); - compareMonomial(a, - a, - a_exp_proc, - v, - v, - b_exp_proc, - exp, - lemmas, - cmp_infers); - } - } - } - } - else - { - // compare magnitude against other non-linear monomials - for (unsigned k = (j + 1); k < d_ms.size(); k++) - { - Node b = d_ms[k]; - //(signs[a]==signs[b])==(r==0) - if (d_ms_proc.find(b) == d_ms_proc.end() - && d_m_nconst_factor.find(b) == d_m_nconst_factor.end()) - { - const NodeMultiset& meb = d_mdb.getMonomialExponentMap(b); - - std::vector<Node> exp; - // take common factors of monomials, set minimum of - // common exponents as processed - NodeMultiset a_exp_proc; - NodeMultiset b_exp_proc; - for (NodeMultiset::const_iterator itmea2 = mea.begin(); - itmea2 != mea.end(); - ++itmea2) - { - NodeMultiset::const_iterator itmeb2 = meb.find(itmea2->first); - if (itmeb2 != meb.end()) - { - unsigned min_exp = itmea2->second > itmeb2->second - ? itmeb2->second - : itmea2->second; - a_exp_proc[itmea2->first] = min_exp; - b_exp_proc[itmea2->first] = min_exp; - Trace("nl-ext-comp") << "Common exponent : " << itmea2->first - << " : " << min_exp << std::endl; - } - } - if (!a_exp_proc.empty()) - { - setMonomialFactor(a, b, a_exp_proc); - setMonomialFactor(b, a, b_exp_proc); - } - /* - if( !a_exp_proc.empty() ){ - //reduction based on common exponents a > 0 => ( a * b - <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b - !<> c ) ? }else{ compareMonomial( a, a, a_exp_proc, b, - b, b_exp_proc, exp, lemmas ); - } - */ - compareMonomial( - a, a, a_exp_proc, b, b, b_exp_proc, exp, lemmas, cmp_infers); - } - } - } - } - } - } - // remove redundant lemmas, e.g. if a > b, b > c, a > c were - // inferred, discard lemma with conclusion a > c - Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size() - << " lemmas." << std::endl; - // naive - std::unordered_set<Node, NodeHashFunction> r_lemmas; - for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb = - cmp_infers.begin(); - itb != cmp_infers.end(); - ++itb) - { - for (std::map<Node, std::map<Node, Node> >::iterator itc = - itb->second.begin(); - itc != itb->second.end(); - ++itc) - { - for (std::map<Node, Node>::iterator itc2 = itc->second.begin(); - itc2 != itc->second.end(); - ++itc2) - { - std::map<Node, bool> visited; - for (std::map<Node, Node>::iterator itc3 = itc->second.begin(); - itc3 != itc->second.end(); - ++itc3) - { - if (itc3->first != itc2->first) - { - std::vector<Node> exp; - if (cmp_holds(itc3->first, itc2->first, itb->second, exp, visited)) - { - r_lemmas.insert(itc2->second); - Trace("nl-ext-comp") - << "...inference of " << itc->first << " > " << itc2->first - << " was redundant." << std::endl; - break; - } - } - } - } - } - } - std::vector<NlLemma> nr_lemmas; - for (unsigned i = 0; i < lemmas.size(); i++) - { - if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end()) - { - nr_lemmas.push_back(lemmas[i]); - } - } - // could only take maximal lower/minimial lower bounds? - - Trace("nl-ext-comp") << nr_lemmas.size() << " / " << lemmas.size() - << " were non-redundant." << std::endl; - return nr_lemmas; -} - -std::vector<NlLemma> NlSolver::checkTangentPlanes() -{ - std::vector<NlLemma> lemmas; - Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl; - NodeManager* nm = NodeManager::currentNM(); - const std::map<Node, std::vector<Node> >& ccMap = - d_mdb.getContainsChildrenMap(); - unsigned kstart = d_ms_vars.size(); - for (unsigned k = kstart; k < d_mterms.size(); k++) - { - Node t = d_mterms[k]; - // if this term requires a refinement - if (d_tplane_refine.find(t) == d_tplane_refine.end()) - { - continue; - } - Trace("nl-ext-tplanes") - << "Look at monomial requiring refinement : " << t << std::endl; - // get a decomposition - std::map<Node, std::vector<Node> >::const_iterator it = ccMap.find(t); - if (it == ccMap.end()) - { - continue; - } - std::map<Node, std::map<Node, bool> > dproc; - for (unsigned j = 0; j < it->second.size(); j++) - { - Node tc = it->second[j]; - if (tc != d_one) - { - Node tc_diff = d_mdb.getContainsDiffNl(tc, t); - Assert(!tc_diff.isNull()); - Node a = tc < tc_diff ? tc : tc_diff; - Node b = tc < tc_diff ? tc_diff : tc; - if (dproc[a].find(b) == dproc[a].end()) - { - dproc[a][b] = true; - Trace("nl-ext-tplanes") - << " decomposable into : " << a << " * " << b << std::endl; - Node a_v_c = d_model.computeAbstractModelValue(a); - Node b_v_c = d_model.computeAbstractModelValue(b); - // points we will add tangent planes for - std::vector<Node> pts[2]; - pts[0].push_back(a_v_c); - pts[1].push_back(b_v_c); - // if previously refined - bool prevRefine = d_tangent_val_bound[0][a].find(b) - != d_tangent_val_bound[0][a].end(); - // a_min, a_max, b_min, b_max - for (unsigned p = 0; p < 4; p++) - { - Node curr_v = p <= 1 ? a_v_c : b_v_c; - if (prevRefine) - { - Node pt_v = d_tangent_val_bound[p][a][b]; - Assert(!pt_v.isNull()); - if (curr_v != pt_v) - { - Node do_extend = - nm->mkNode((p == 1 || p == 3) ? GT : LT, curr_v, pt_v); - do_extend = Rewriter::rewrite(do_extend); - if (do_extend == d_true) - { - for (unsigned q = 0; q < 2; q++) - { - pts[p <= 1 ? 0 : 1].push_back(curr_v); - pts[p <= 1 ? 1 : 0].push_back( - d_tangent_val_bound[p <= 1 ? 2 + q : q][a][b]); - } - } - } - } - else - { - d_tangent_val_bound[p][a][b] = curr_v; - } - } - - for (unsigned p = 0; p < pts[0].size(); p++) - { - Node a_v = pts[0][p]; - Node b_v = pts[1][p]; - - // tangent plane - Node tplane = nm->mkNode( - MINUS, - nm->mkNode( - PLUS, nm->mkNode(MULT, b_v, a), nm->mkNode(MULT, a_v, b)), - nm->mkNode(MULT, a_v, b_v)); - // conjuncts of the tangent plane lemma - std::vector<Node> tplaneConj; - for (unsigned d = 0; d < 4; d++) - { - Node aa = nm->mkNode(d == 0 || d == 3 ? GEQ : LEQ, a, a_v); - Node ab = nm->mkNode(d == 1 || d == 3 ? GEQ : LEQ, b, b_v); - Node conc = nm->mkNode(d <= 1 ? LEQ : GEQ, t, tplane); - Node tlem = nm->mkNode(OR, aa.negate(), ab.negate(), conc); - Trace("nl-ext-tplanes") - << "Tangent plane lemma : " << tlem << std::endl; - tplaneConj.push_back(tlem); - } - - // tangent plane reverse implication - - // t <= tplane -> ( (a <= a_v ^ b >= b_v) v - // (a >= a_v ^ b <= b_v) ). - // in clause form, the above becomes - // t <= tplane -> a <= a_v v b <= b_v. - // t <= tplane -> b >= b_v v a >= a_v. - Node a_leq_av = nm->mkNode(LEQ, a, a_v); - Node b_leq_bv = nm->mkNode(LEQ, b, b_v); - Node a_geq_av = nm->mkNode(GEQ, a, a_v); - Node b_geq_bv = nm->mkNode(GEQ, b, b_v); - - Node t_leq_tplane = nm->mkNode(LEQ, t, tplane); - Node a_leq_av_or_b_leq_bv = nm->mkNode(OR, a_leq_av, b_leq_bv); - Node b_geq_bv_or_a_geq_av = nm->mkNode(OR, b_geq_bv, a_geq_av); - Node ub_reverse1 = - nm->mkNode(OR, t_leq_tplane.negate(), a_leq_av_or_b_leq_bv); - Trace("nl-ext-tplanes") - << "Tangent plane lemma (reverse) : " << ub_reverse1 - << std::endl; - tplaneConj.push_back(ub_reverse1); - Node ub_reverse2 = - nm->mkNode(OR, t_leq_tplane.negate(), b_geq_bv_or_a_geq_av); - Trace("nl-ext-tplanes") - << "Tangent plane lemma (reverse) : " << ub_reverse2 - << std::endl; - tplaneConj.push_back(ub_reverse2); - - // t >= tplane -> ( (a <= a_v ^ b <= b_v) v - // (a >= a_v ^ b >= b_v) ). - // in clause form, the above becomes - // t >= tplane -> a <= a_v v b >= b_v. - // t >= tplane -> b >= b_v v a <= a_v - Node t_geq_tplane = nm->mkNode(GEQ, t, tplane); - Node a_leq_av_or_b_geq_bv = nm->mkNode(OR, a_leq_av, b_geq_bv); - Node a_geq_av_or_b_leq_bv = nm->mkNode(OR, a_geq_av, b_leq_bv); - Node lb_reverse1 = - nm->mkNode(OR, t_geq_tplane.negate(), a_leq_av_or_b_geq_bv); - Trace("nl-ext-tplanes") - << "Tangent plane lemma (reverse) : " << lb_reverse1 - << std::endl; - tplaneConj.push_back(lb_reverse1); - Node lb_reverse2 = - nm->mkNode(OR, t_geq_tplane.negate(), a_geq_av_or_b_leq_bv); - Trace("nl-ext-tplanes") - << "Tangent plane lemma (reverse) : " << lb_reverse2 - << std::endl; - tplaneConj.push_back(lb_reverse2); - - Node tlem = nm->mkNode(AND, tplaneConj); - lemmas.emplace_back(tlem, Inference::TANGENT_PLANE); - } - } - } - } - } - Trace("nl-ext") << "...trying " << lemmas.size() << " tangent plane lemmas..." - << std::endl; - return lemmas; -} - -std::vector<NlLemma> NlSolver::checkMonomialInferBounds( - std::vector<NlLemma>& nt_lemmas, - const std::vector<Node>& asserts, - const std::vector<Node>& false_asserts) -{ - // sort monomials by degree - Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl; - d_mdb.sortByDegree(d_ms); - // all monomials - d_mterms.insert(d_mterms.end(), d_ms_vars.begin(), d_ms_vars.end()); - d_mterms.insert(d_mterms.end(), d_ms.begin(), d_ms.end()); - - const std::map<Node, std::map<Node, ConstraintInfo> >& cim = - d_cdb.getConstraints(); - - std::vector<NlLemma> lemmas; - NodeManager* nm = NodeManager::currentNM(); - // register constraints - Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; - for (const Node& lit : asserts) - { - bool polarity = lit.getKind() != NOT; - Node atom = lit.getKind() == NOT ? lit[0] : lit; - d_cdb.registerConstraint(atom); - bool is_false_lit = - std::find(false_asserts.begin(), false_asserts.end(), lit) - != false_asserts.end(); - // add information about bounds to variables - std::map<Node, std::map<Node, ConstraintInfo> >::const_iterator itc = - cim.find(atom); - if (itc == cim.end()) - { - continue; - } - for (const std::pair<const Node, ConstraintInfo>& itcc : itc->second) - { - Node x = itcc.first; - Node coeff = itcc.second.d_coeff; - Node rhs = itcc.second.d_rhs; - Kind type = itcc.second.d_type; - Node exp = lit; - if (!polarity) - { - // reverse - if (type == EQUAL) - { - // we will take the strict inequality in the direction of the - // model - Node lhs = ArithMSum::mkCoeffTerm(coeff, x); - Node query = nm->mkNode(GT, lhs, rhs); - Node query_mv = d_model.computeAbstractModelValue(query); - if (query_mv == d_true) - { - exp = query; - type = GT; - } - else - { - Assert(query_mv == d_false); - exp = nm->mkNode(LT, lhs, rhs); - type = LT; - } - } - else - { - type = negateKind(type); - } - } - // add to status if maximal degree - d_ci_max[x][coeff][rhs] = d_cdb.isMaximal(atom, x); - if (Trace.isOn("nl-ext-bound-debug2")) - { - Node t = ArithMSum::mkCoeffTerm(coeff, x); - Trace("nl-ext-bound-debug2") << "Add Bound: " << t << " " << type << " " - << rhs << " by " << exp << std::endl; - } - bool updated = true; - std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs); - if (its == d_ci[x][coeff].end()) - { - d_ci[x][coeff][rhs] = type; - d_ci_exp[x][coeff][rhs] = exp; - } - else if (type != its->second) - { - Trace("nl-ext-bound-debug2") - << "Joining kinds : " << type << " " << its->second << std::endl; - Kind jk = joinKinds(type, its->second); - if (jk == UNDEFINED_KIND) - { - updated = false; - } - else if (jk != its->second) - { - if (jk == type) - { - d_ci[x][coeff][rhs] = type; - d_ci_exp[x][coeff][rhs] = exp; - } - else - { - d_ci[x][coeff][rhs] = jk; - d_ci_exp[x][coeff][rhs] = - nm->mkNode(AND, d_ci_exp[x][coeff][rhs], exp); - } - } - else - { - updated = false; - } - } - if (Trace.isOn("nl-ext-bound")) - { - if (updated) - { - Trace("nl-ext-bound") << "Bound: "; - debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs); - Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs]; - if (d_ci_max[x][coeff][rhs]) - { - Trace("nl-ext-bound") << ", is max degree"; - } - Trace("nl-ext-bound") << std::endl; - } - } - // compute if bound is not satisfied, and store what is required - // for a possible refinement - if (options::nlExtTangentPlanes()) - { - if (is_false_lit) - { - d_tplane_refine.insert(x); - } - } - } - } - // reflexive constraints - Node null_coeff; - for (unsigned j = 0; j < d_mterms.size(); j++) - { - Node n = d_mterms[j]; - d_ci[n][null_coeff][n] = EQUAL; - d_ci_exp[n][null_coeff][n] = d_true; - d_ci_max[n][null_coeff][n] = false; - } - - Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl; - const std::map<Node, std::vector<Node> >& cpMap = - d_mdb.getContainsParentMap(); - for (unsigned k = 0; k < d_mterms.size(); k++) - { - Node x = d_mterms[k]; - Trace("nl-ext-bound-debug") - << "Process bounds for " << x << " : " << std::endl; - std::map<Node, std::vector<Node> >::const_iterator itm = cpMap.find(x); - if (itm == cpMap.end()) - { - Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl; - continue; - } - Trace("nl-ext-bound-debug") - << "...has " << itm->second.size() << " parent monomials." << std::endl; - // check derived bounds - std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc = - d_ci.find(x); - if (itc == d_ci.end()) - { - continue; - } - for (std::map<Node, std::map<Node, Kind> >::iterator itcc = - itc->second.begin(); - itcc != itc->second.end(); - ++itcc) - { - Node coeff = itcc->first; - Node t = ArithMSum::mkCoeffTerm(coeff, x); - for (std::map<Node, Kind>::iterator itcr = itcc->second.begin(); - itcr != itcc->second.end(); - ++itcr) - { - Node rhs = itcr->first; - // only consider this bound if maximal degree - if (!d_ci_max[x][coeff][rhs]) - { - continue; - } - Kind type = itcr->second; - for (unsigned j = 0; j < itm->second.size(); j++) - { - Node y = itm->second[j]; - Node mult = d_mdb.getContainsDiff(x, y); - // x <k> t => m*x <k'> t where y = m*x - // get the sign of mult - Node mmv = d_model.computeConcreteModelValue(mult); - Trace("nl-ext-bound-debug2") - << "Model value of " << mult << " is " << mmv << std::endl; - if (!mmv.isConst()) - { - Trace("nl-ext-bound-debug") - << " ...coefficient " << mult - << " is non-constant (probably transcendental)." << std::endl; - continue; - } - int mmv_sign = mmv.getConst<Rational>().sgn(); - Trace("nl-ext-bound-debug2") - << " sign of " << mmv << " is " << mmv_sign << std::endl; - if (mmv_sign == 0) - { - Trace("nl-ext-bound-debug") - << " ...coefficient " << mult << " is zero." << std::endl; - continue; - } - Trace("nl-ext-bound-debug") - << " from " << x << " * " << mult << " = " << y << " and " << t - << " " << type << " " << rhs << ", infer : " << std::endl; - Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type; - Node infer_lhs = nm->mkNode(MULT, mult, t); - Node infer_rhs = nm->mkNode(MULT, mult, rhs); - Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs); - Trace("nl-ext-bound-debug") << " " << infer << std::endl; - infer = Rewriter::rewrite(infer); - Trace("nl-ext-bound-debug2") - << " ...rewritten : " << infer << std::endl; - // check whether it is false in model for abstraction - Node infer_mv = d_model.computeAbstractModelValue(infer); - Trace("nl-ext-bound-debug") - << " ...infer model value is " << infer_mv << std::endl; - if (infer_mv == d_false) - { - Node exp = - nm->mkNode(AND, - nm->mkNode(mmv_sign == 1 ? GT : LT, mult, d_zero), - d_ci_exp[x][coeff][rhs]); - Node iblem = nm->mkNode(IMPLIES, exp, infer); - Node pr_iblem = iblem; - iblem = Rewriter::rewrite(iblem); - bool introNewTerms = hasNewMonomials(iblem, d_ms); - Trace("nl-ext-bound-lemma") - << "*** Bound inference lemma : " << iblem - << " (pre-rewrite : " << pr_iblem << ")" << std::endl; - // Trace("nl-ext-bound-lemma") << " intro new - // monomials = " << introNewTerms << std::endl; - if (!introNewTerms) - { - lemmas.emplace_back(iblem, Inference::INFER_BOUNDS); - } - else - { - nt_lemmas.emplace_back(iblem, Inference::INFER_BOUNDS_NT); - } - } - } - } - } - } - return lemmas; -} - -std::vector<NlLemma> NlSolver::checkFactoring( - const std::vector<Node>& asserts, const std::vector<Node>& false_asserts) -{ - std::vector<NlLemma> lemmas; - NodeManager* nm = NodeManager::currentNM(); - Trace("nl-ext") << "Get factoring lemmas..." << std::endl; - for (const Node& lit : asserts) - { - bool polarity = lit.getKind() != NOT; - Node atom = lit.getKind() == NOT ? lit[0] : lit; - Node litv = d_model.computeConcreteModelValue(lit); - bool considerLit = false; - // Only consider literals that are in false_asserts. - considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit) - != false_asserts.end(); - - if (considerLit) - { - std::map<Node, Node> msum; - if (ArithMSum::getMonomialSumLit(atom, msum)) - { - Trace("nl-ext-factor") << "Factoring for literal " << lit - << ", monomial sum is : " << std::endl; - if (Trace.isOn("nl-ext-factor")) - { - ArithMSum::debugPrintMonomialSum(msum, "nl-ext-factor"); - } - std::map<Node, std::vector<Node> > factor_to_mono; - std::map<Node, std::vector<Node> > factor_to_mono_orig; - for (std::map<Node, Node>::iterator itm = msum.begin(); - itm != msum.end(); - ++itm) - { - if (!itm->first.isNull()) - { - if (itm->first.getKind() == NONLINEAR_MULT) - { - std::vector<Node> children; - for (unsigned i = 0; i < itm->first.getNumChildren(); i++) - { - children.push_back(itm->first[i]); - } - std::map<Node, bool> processed; - for (unsigned i = 0; i < itm->first.getNumChildren(); i++) - { - if (processed.find(itm->first[i]) == processed.end()) - { - processed[itm->first[i]] = true; - children[i] = d_one; - if (!itm->second.isNull()) - { - children.push_back(itm->second); - } - Node val = nm->mkNode(MULT, children); - if (!itm->second.isNull()) - { - children.pop_back(); - } - children[i] = itm->first[i]; - val = Rewriter::rewrite(val); - factor_to_mono[itm->first[i]].push_back(val); - factor_to_mono_orig[itm->first[i]].push_back(itm->first); - } - } - } - } - } - for (std::map<Node, std::vector<Node> >::iterator itf = - factor_to_mono.begin(); - itf != factor_to_mono.end(); - ++itf) - { - Node x = itf->first; - if (itf->second.size() == 1) - { - std::map<Node, Node>::iterator itm = msum.find(x); - if (itm != msum.end()) - { - itf->second.push_back(itm->second.isNull() ? d_one : itm->second); - factor_to_mono_orig[x].push_back(x); - } - } - if (itf->second.size() <= 1) - { - continue; - } - Node sum = nm->mkNode(PLUS, itf->second); - sum = Rewriter::rewrite(sum); - Trace("nl-ext-factor") - << "* Factored sum for " << x << " : " << sum << std::endl; - Node kf = getFactorSkolem(sum, lemmas); - std::vector<Node> poly; - poly.push_back(nm->mkNode(MULT, x, kf)); - std::map<Node, std::vector<Node> >::iterator itfo = - factor_to_mono_orig.find(x); - Assert(itfo != factor_to_mono_orig.end()); - for (std::map<Node, Node>::iterator itm = msum.begin(); - itm != msum.end(); - ++itm) - { - if (std::find(itfo->second.begin(), itfo->second.end(), itm->first) - == itfo->second.end()) - { - poly.push_back(ArithMSum::mkCoeffTerm( - itm->second, itm->first.isNull() ? d_one : itm->first)); - } - } - Node polyn = poly.size() == 1 ? poly[0] : nm->mkNode(PLUS, poly); - Trace("nl-ext-factor") - << "...factored polynomial : " << polyn << std::endl; - Node conc_lit = nm->mkNode(atom.getKind(), polyn, d_zero); - conc_lit = Rewriter::rewrite(conc_lit); - if (!polarity) - { - conc_lit = conc_lit.negate(); - } - - std::vector<Node> lemma_disj; - lemma_disj.push_back(lit.negate()); - lemma_disj.push_back(conc_lit); - Node flem = nm->mkNode(OR, lemma_disj); - Trace("nl-ext-factor") << "...lemma is " << flem << std::endl; - lemmas.emplace_back(flem, Inference::FACTOR); - } - } - } - } - return lemmas; -} - -Node NlSolver::getFactorSkolem(Node n, std::vector<NlLemma>& lemmas) -{ - std::map<Node, Node>::iterator itf = d_factor_skolem.find(n); - if (itf == d_factor_skolem.end()) - { - NodeManager* nm = NodeManager::currentNM(); - Node k = nm->mkSkolem("kf", n.getType()); - Node k_eq = Rewriter::rewrite(k.eqNode(n)); - lemmas.push_back(k_eq); - d_factor_skolem[n] = k; - return k; - } - return itf->second; -} - -std::vector<NlLemma> NlSolver::checkMonomialInferResBounds() -{ - std::vector<NlLemma> lemmas; - NodeManager* nm = NodeManager::currentNM(); - Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." - << std::endl; - size_t nmterms = d_mterms.size(); - for (unsigned j = 0; j < nmterms; j++) - { - Node a = d_mterms[j]; - std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca = - d_ci.find(a); - if (itca == d_ci.end()) - { - continue; - } - for (unsigned k = (j + 1); k < nmterms; k++) - { - Node b = d_mterms[k]; - std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itcb = - d_ci.find(b); - if (itcb == d_ci.end()) - { - continue; - } - Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a - << " and " << b << std::endl; - // if they have common factors - std::map<Node, Node>::iterator ita = d_mono_diff[a].find(b); - if (ita == d_mono_diff[a].end()) - { - continue; - } - Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a - << " vs [b] " << b << std::endl; - std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a); - Assert(itb != d_mono_diff[b].end()); - Node mv_a = d_model.computeAbstractModelValue(ita->second); - Assert(mv_a.isConst()); - int mv_a_sgn = mv_a.getConst<Rational>().sgn(); - if (mv_a_sgn == 0) - { - // we don't compare monomials whose current model value is zero - continue; - } - Node mv_b = d_model.computeAbstractModelValue(itb->second); - Assert(mv_b.isConst()); - int mv_b_sgn = mv_b.getConst<Rational>().sgn(); - if (mv_b_sgn == 0) - { - // we don't compare monomials whose current model value is zero - continue; - } - Trace("nl-ext-rbound") << " [a] factor is " << ita->second - << ", sign in model = " << mv_a_sgn << std::endl; - Trace("nl-ext-rbound") << " [b] factor is " << itb->second - << ", sign in model = " << mv_b_sgn << std::endl; - - std::vector<Node> exp; - // bounds of a - for (std::map<Node, std::map<Node, Kind> >::iterator itcac = - itca->second.begin(); - itcac != itca->second.end(); - ++itcac) - { - Node coeff_a = itcac->first; - for (std::map<Node, Kind>::iterator itcar = itcac->second.begin(); - itcar != itcac->second.end(); - ++itcar) - { - Node rhs_a = itcar->first; - Node rhs_a_res_base = nm->mkNode(MULT, itb->second, rhs_a); - rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base); - if (hasNewMonomials(rhs_a_res_base, d_ms)) - { - continue; - } - Kind type_a = itcar->second; - exp.push_back(d_ci_exp[a][coeff_a][rhs_a]); - - // bounds of b - for (std::map<Node, std::map<Node, Kind> >::iterator itcbc = - itcb->second.begin(); - itcbc != itcb->second.end(); - ++itcbc) - { - Node coeff_b = itcbc->first; - Node rhs_a_res = ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base); - for (std::map<Node, Kind>::iterator itcbr = itcbc->second.begin(); - itcbr != itcbc->second.end(); - ++itcbr) - { - Node rhs_b = itcbr->first; - Node rhs_b_res = nm->mkNode(MULT, ita->second, rhs_b); - rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res); - rhs_b_res = Rewriter::rewrite(rhs_b_res); - if (hasNewMonomials(rhs_b_res, d_ms)) - { - continue; - } - Kind type_b = itcbr->second; - exp.push_back(d_ci_exp[b][coeff_b][rhs_b]); - if (Trace.isOn("nl-ext-rbound")) - { - Trace("nl-ext-rbound") << "* try bounds : "; - debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a); - Trace("nl-ext-rbound") << std::endl; - Trace("nl-ext-rbound") << " "; - debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b); - Trace("nl-ext-rbound") << std::endl; - } - Kind types[2]; - for (unsigned r = 0; r < 2; r++) - { - Node pivot_factor = r == 0 ? itb->second : ita->second; - int pivot_factor_sign = r == 0 ? mv_b_sgn : mv_a_sgn; - types[r] = r == 0 ? type_a : type_b; - if (pivot_factor_sign == (r == 0 ? 1 : -1)) - { - types[r] = reverseRelationKind(types[r]); - } - if (pivot_factor_sign == 1) - { - exp.push_back(nm->mkNode(GT, pivot_factor, d_zero)); - } - else - { - exp.push_back(nm->mkNode(LT, pivot_factor, d_zero)); - } - } - Kind jk = transKinds(types[0], types[1]); - Trace("nl-ext-rbound-debug") - << "trans kind : " << types[0] << " + " << types[1] << " = " - << jk << std::endl; - if (jk != UNDEFINED_KIND) - { - Node conc = nm->mkNode(jk, rhs_a_res, rhs_b_res); - Node conc_mv = d_model.computeAbstractModelValue(conc); - if (conc_mv == d_false) - { - Node rblem = nm->mkNode(IMPLIES, nm->mkNode(AND, exp), conc); - Trace("nl-ext-rbound-lemma-debug") - << "Resolution bound lemma " - "(pre-rewrite) " - ": " - << rblem << std::endl; - rblem = Rewriter::rewrite(rblem); - Trace("nl-ext-rbound-lemma") - << "Resolution bound lemma : " << rblem << std::endl; - lemmas.emplace_back(rblem, Inference::RES_INFER_BOUNDS); - } - } - exp.pop_back(); - exp.pop_back(); - exp.pop_back(); - } - } - exp.pop_back(); - } - } - } - } - return lemmas; -} - -} // namespace nl -} // namespace arith -} // namespace theory -} // namespace CVC4 |