--- /dev/null
+/********************* */
+/*! \file nl_alg.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/nonlinear_extension.h"
+
+#include <set>
+
+#include "expr/node_builder.h"
+#include "options/arith_options.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/theory_model.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+namespace {
+
+// Return true if a collection c contains an elem k. Compatible with map and set
+// containers.
+template <class Container, class Key>
+bool Contains(const Container& c, const Key& k) {
+ return c.find(k) != c.end();
+}
+
+// Inserts value into the set/map c if the value was not present there. Returns
+// true if the value was inserted.
+template <class Container, class Value>
+bool InsertIfNotPresent(Container* c, const Value& value) {
+ return (c->insert(value)).second;
+}
+
+// Returns true if a vector c contains an elem t.
+template <class T>
+bool IsInVector(const std::vector<T>& c, const T& t) {
+ return std::find(c.begin(), c.end(), t) != c.end();
+}
+
+// Returns the a[key] and assertion fails in debug mode.
+inline unsigned getCount(const NodeMultiset& a, Node key) {
+ NodeMultiset::const_iterator it = a.find(key);
+ Assert(it != a.end());
+ return it->second;
+}
+
+// Returns a[key] if key is in a or value otherwise.
+unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value) {
+ NodeMultiset::const_iterator it = a.find(key);
+ return (it == a.end()) ? value : it->second;
+}
+
+// Returns map[key] if key is in map or Node::null() otherwise.
+Node getNodeOrNull(const std::map<Node, Node>& map, Node key) {
+ std::map<Node, Node>::const_iterator it = map.find(key);
+ return (it == map.end()) ? Node::null() : it->second;
+}
+
+// Returns true if for any key then a[key] <= b[key] where the value for any key
+// not present is interpreted as 0.
+bool isSubset(const NodeMultiset& a, const NodeMultiset& b) {
+ for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a) {
+ Node key = it_a->first;
+ const unsigned a_value = it_a->second;
+ const unsigned b_value = getCountWithDefault(b, key, 0);
+ if (a_value > b_value) {
+ return false;
+ }
+ }
+ return true;
+}
+
+// Given two multisets return the multiset difference a \ b.
+NodeMultiset diffMultiset(const NodeMultiset& a, const NodeMultiset& b) {
+ NodeMultiset difference;
+ for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a) {
+ Node key = it_a->first;
+ const unsigned a_value = it_a->second;
+ const unsigned b_value = getCountWithDefault(b, key, 0);
+ if (a_value > b_value) {
+ difference[key] = a_value - b_value;
+ }
+ }
+ return difference;
+}
+
+// Return a vector containing a[key] repetitions of key in a multiset a.
+std::vector<Node> ExpandMultiset(const NodeMultiset& a) {
+ std::vector<Node> expansion;
+ for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a) {
+ expansion.insert(expansion.end(), it_a->second, it_a->first);
+ }
+ return expansion;
+}
+
+void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) {
+ Node t = QuantArith::mkCoeffTerm(coeff, x);
+ Trace(c) << t << " " << type << " " << rhs;
+}
+
+struct SubstitutionConstResult {
+ // The resulting term of the substitution.
+ Node term;
+
+ // ?
+ std::vector<Node> const_exp;
+
+ // ??
+ // A term sum[i] for which for rep_sum[i] not in rep_to_const.
+ Node variable_term;
+}; /* struct SubstitutionConstResult */
+
+SubstitutionConstResult getSubstitutionConst(
+ Node n, const std::vector<Node>& sum, const std::vector<Node>& rep_sum,
+ const std::map<Node, Node>& rep_to_const,
+ const std::map<Node, Node>& rep_to_const_exp,
+ const std::map<Node, Node>& rep_to_const_base) {
+ Assert(sum.size() == rep_sum.size());
+
+ SubstitutionConstResult result;
+
+ std::vector<Node> vars;
+ std::vector<Node> subs;
+ std::set<Node> rep_exp_proc;
+ for (unsigned i = 0; i < rep_sum.size(); i++) {
+ Node cr = rep_sum[i];
+ Node const_of_cr = getNodeOrNull(rep_to_const, cr);
+ if (const_of_cr.isNull()) {
+ result.variable_term = sum[i];
+ continue;
+ }
+ Assert(!const_of_cr.isNull());
+ Node const_base_of_cr = getNodeOrNull(rep_to_const_base, cr);
+ Assert(!const_base_of_cr.isNull());
+ if (const_base_of_cr != sum[i]) {
+ result.const_exp.push_back(const_base_of_cr.eqNode(sum[i]));
+ }
+ if (rep_exp_proc.find(cr) == rep_exp_proc.end()) {
+ rep_exp_proc.insert(cr);
+ Node const_exp = getNodeOrNull(rep_to_const_exp, cr);
+ if (!const_exp.isNull()) {
+ result.const_exp.push_back(const_exp);
+ }
+ }
+ vars.push_back(sum[i]);
+ subs.push_back(const_of_cr);
+ }
+ Node substituted =
+ n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ result.term = Rewriter::rewrite(substituted);
+ return result;
+}
+
+struct SortNonlinearExtension {
+ SortNonlinearExtension()
+ : d_nla(NULL), d_order_type(0), d_reverse_order(false) {}
+ NonlinearExtension* d_nla;
+ unsigned d_order_type;
+ bool d_reverse_order;
+ bool operator()(Node i, Node j) {
+ int cv = d_nla->compare(i, j, d_order_type);
+ if (cv == 0) {
+ return i < j;
+ } else {
+ return d_reverse_order ? cv < 0 : cv > 0;
+ }
+ }
+};
+
+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 (!Contains(visited, current)) {
+ visited.insert(current);
+ if (current.getKind() == kind::NONLINEAR_MULT) {
+ if (!IsInVector(existing, current)) {
+ return true;
+ }
+ } else {
+ worklist.insert(worklist.end(), current.begin(), current.end());
+ }
+ }
+ }
+ return false;
+}
+
+} // namespace
+
+NonlinearExtension::NonlinearExtension(TheoryArith& containing,
+ eq::EqualityEngine* ee)
+ : d_lemmas(containing.getUserContext()),
+ d_zero_split(containing.getUserContext()),
+ d_containing(containing),
+ d_ee(ee),
+ d_needsLastCall(false) {
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+ d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(Rational(1));
+ d_neg_one = NodeManager::currentNM()->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);
+}
+
+NonlinearExtension::~NonlinearExtension() {}
+
+// Returns a reference to either map[key] if it exists in the map
+// or to a default value otherwise.
+//
+// Warning: special care must be taken if value is a temporary object.
+template <class MapType, class Key, class Value>
+const Value& FindWithDefault(const MapType& map, const Key& key,
+ const Value& value) {
+ typename MapType::const_iterator it = map.find(key);
+ if (it == map.end()) {
+ return value;
+ }
+ return it->second;
+}
+
+const NodeMultiset& NonlinearExtension::getMonomialExponentMap(
+ Node monomial) const {
+ MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
+ Assert(it != d_m_exp.end());
+ return it->second;
+}
+
+bool NonlinearExtension::isMonomialSubset(Node a, Node b) const {
+ const NodeMultiset& a_exponent_map = getMonomialExponentMap(a);
+ const NodeMultiset& b_exponent_map = getMonomialExponentMap(b);
+
+ return isSubset(a_exponent_map, b_exponent_map);
+}
+
+void NonlinearExtension::registerMonomialSubset(Node a, Node b) {
+ Assert(isMonomialSubset(a, b));
+
+ const NodeMultiset& a_exponent_map = getMonomialExponentMap(a);
+ const NodeMultiset& b_exponent_map = getMonomialExponentMap(b);
+
+ std::vector<Node> diff_children =
+ ExpandMultiset(diffMultiset(b_exponent_map, a_exponent_map));
+ Assert(!diff_children.empty());
+
+ d_m_contain_parent[a].push_back(b);
+ d_m_contain_children[b].push_back(a);
+
+ Node mult_term = safeConstructNary(kind::MULT, diff_children);
+ Node nlmult_term = safeConstructNary(kind::NONLINEAR_MULT, diff_children);
+ d_m_contain_mult[a][b] = mult_term;
+ d_m_contain_umult[a][b] = nlmult_term;
+ Trace("nl-alg-mindex") << "..." << a << " is a subset of " << b
+ << ", difference is " << mult_term << std::endl;
+}
+
+class NonLinearExtentionSubstitutionSolver {
+ public:
+ NonLinearExtentionSubstitutionSolver(const eq::EqualityEngine* ee)
+ : d_ee(ee) {}
+
+ bool solve(const std::vector<Node>& vars, std::vector<Node>* subs,
+ std::map<Node, std::vector<Node> >* exp,
+ std::map<Node, std::vector<int> >* rep_to_subs_index);
+
+ private:
+ bool setSubstitutionConst(
+ const std::vector<Node>& vars, Node r, Node r_c, Node r_cb,
+ const std::vector<Node>& r_c_exp, std::vector<Node>* subs,
+ std::map<Node, std::vector<Node> >* exp,
+ std::map<Node, std::vector<int> >* rep_to_subs_index);
+
+ const eq::EqualityEngine* d_ee;
+
+ std::map<Node, Node> d_rep_to_const;
+ std::map<Node, Node> d_rep_to_const_exp;
+ std::map<Node, Node> d_rep_to_const_base;
+
+ // key in term_to_sum iff key in term_to_rep_sum.
+ std::map<Node, std::vector<Node> > d_term_to_sum;
+ std::map<Node, std::vector<Node> > d_term_to_rep_sum;
+ std::map<Node, int> d_term_to_nconst_rep_count;
+
+ std::map<Node, std::vector<Node> > d_reps_to_parent_terms;
+ std::map<Node, std::vector<Node> > d_reps_to_terms;
+};
+
+bool NonLinearExtentionSubstitutionSolver::solve(
+ const std::vector<Node>& vars, std::vector<Node>* subs,
+ std::map<Node, std::vector<Node> >* exp,
+ std::map<Node, std::vector<int> >* rep_to_subs_index) {
+ // std::map<Node, Node> rep_to_const;
+ // std::map<Node, Node> rep_to_const_exp;
+ // std::map<Node, Node> rep_to_const_base;
+
+ // std::map<Node, std::vector<Node> > term_to_sum;
+ // std::map<Node, std::vector<Node> > term_to_rep_sum;
+ // std::map<Node, int> term_to_nconst_rep_count;
+ // std::map<Node, std::vector<Node> > reps_to_parent_terms;
+ // std::map<Node, std::vector<Node> > reps_to_terms;
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_ee);
+
+ bool retVal = false;
+ while (!eqcs_i.isFinished() && !rep_to_subs_index->empty()) {
+ Node r = (*eqcs_i);
+ if (r.getType().isReal()) {
+ Trace("nl-subs-debug")
+ << "Process equivalence class " << r << "..." << std::endl;
+ Node r_c;
+ Node r_cb;
+ std::vector<Node> r_c_exp;
+ if (r.isConst()) {
+ r_c = r;
+ r_cb = r;
+ }
+ // scan the class
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_ee);
+ while (!eqc_i.isFinished()) {
+ Node n = (*eqc_i);
+ if (!n.isConst()) {
+ Trace("nl-subs-debug") << "Look at term : " << n << std::endl;
+ std::map<Node, Node> msum;
+ if (QuantArith::getMonomialSum(n, msum)) {
+ int nconst_count = 0;
+ bool evaluatable = true;
+ for (std::map<Node, Node>::iterator itm = msum.begin();
+ itm != msum.end(); ++itm) {
+ if (!itm->first.isNull()) {
+ if (d_ee->hasTerm(itm->first)) {
+ Trace("nl-subs-debug")
+ << " ...monomial " << itm->first << std::endl;
+ Node cr = d_ee->getRepresentative(itm->first);
+ d_term_to_sum[n].push_back(itm->first);
+ d_term_to_rep_sum[n].push_back(cr);
+ if (!Contains(d_rep_to_const, cr)) {
+ if (!IsInVector(d_reps_to_parent_terms[cr], n)) {
+ d_reps_to_parent_terms[cr].push_back(n);
+ nconst_count++;
+ }
+ }
+ } else {
+ Trace("nl-subs-debug")
+ << "...is not evaluatable due to monomial " << itm->first
+ << std::endl;
+ evaluatable = false;
+ break;
+ }
+ }
+ }
+ if (evaluatable) {
+ Trace("nl-subs-debug")
+ << " ...term has " << nconst_count
+ << " unique non-constant represenative children."
+ << std::endl;
+ if (nconst_count == 0) {
+ if (r_c.isNull()) {
+ const SubstitutionConstResult result = getSubstitutionConst(
+ n, d_term_to_sum[n], d_term_to_rep_sum[n], d_rep_to_const,
+ d_rep_to_const_exp, d_rep_to_const_base);
+ r_c_exp.insert(r_c_exp.end(), result.const_exp.begin(),
+ result.const_exp.end());
+ r_c = result.term;
+ r_cb = n;
+ Assert(result.variable_term.isNull());
+ Assert(r_c.isConst());
+ }
+ } else {
+ d_reps_to_terms[r].push_back(n);
+ d_term_to_nconst_rep_count[n] = nconst_count;
+ }
+ }
+ } else {
+ Trace("nl-subs-debug")
+ << "...could not get monomial sum " << std::endl;
+ }
+ }
+ ++eqc_i;
+ }
+ if (!r_c.isNull()) {
+ setSubstitutionConst(vars, r, r_c, r_cb, r_c_exp, subs, exp,
+ rep_to_subs_index);
+ }
+ }
+ ++eqcs_i;
+ }
+ return retVal;
+}
+
+bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst(
+ const std::vector<Node>& vars, Node r, Node r_c, Node r_cb,
+ const std::vector<Node>& r_c_exp, std::vector<Node>* subs,
+ std::map<Node, std::vector<Node> >* exp,
+ std::map<Node, std::vector<int> >* rep_to_subs_index) {
+ Trace("nl-subs-debug") << "Set constant equivalence class : " << r << " -> "
+ << r_c << std::endl;
+ bool retVal = false;
+
+ d_rep_to_const[r] = r_c;
+ Node expn;
+ if (!r_c_exp.empty()) {
+ expn = r_c_exp.size() == 1
+ ? r_c_exp[0]
+ : NodeManager::currentNM()->mkNode(kind::AND, r_c_exp);
+ Trace("nl-subs-debug") << "...explanation is " << expn << std::endl;
+ d_rep_to_const_exp[r] = expn;
+ }
+ d_rep_to_const_base[r] = r_cb;
+
+ std::map<Node, std::vector<int> >::const_iterator iti =
+ rep_to_subs_index->find(r);
+ if (iti != rep_to_subs_index->end()) {
+ for (unsigned i = 0; i < iti->second.size(); i++) {
+ int ii = iti->second[i];
+ (*subs)[ii] = r_c;
+ std::vector<Node>& exp_var_ii = (*exp)[vars[ii]];
+ exp_var_ii.clear();
+ if (!expn.isNull()) {
+ exp_var_ii.push_back(expn);
+ }
+ if (vars[ii] != r_cb) {
+ exp_var_ii.push_back(vars[ii].eqNode(r_cb));
+ }
+ }
+ retVal = true;
+ rep_to_subs_index->erase(r);
+ if (rep_to_subs_index->empty()) {
+ return retVal;
+ }
+ }
+
+ // new inferred constants
+ std::map<Node, Node> new_const;
+ std::map<Node, std::vector<Node> > new_const_exp;
+
+ // parent terms now evaluate to constants
+ std::map<Node, std::vector<Node> >::const_iterator itrp =
+ d_reps_to_parent_terms.find(r);
+ if (itrp != d_reps_to_parent_terms.end()) {
+ // Trace("nl-subs-debug") << "Look at " << itrp->second.size() << " parent
+ // terms." << std::endl;
+ for (unsigned i = 0; i < itrp->second.size(); i++) {
+ Node m = itrp->second[i];
+ d_term_to_nconst_rep_count[m]--;
+ Node r = d_ee->getRepresentative(m);
+ if (d_term_to_nconst_rep_count[m] == 0) {
+ if (!Contains(d_rep_to_const, r)) {
+ Trace("nl-subs-debug") << "...parent term " << m
+ << " evaluates to constant." << std::endl;
+ if (!Contains(new_const, m)) {
+ const SubstitutionConstResult result = getSubstitutionConst(
+ m, d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const,
+ d_rep_to_const_exp, d_rep_to_const_base);
+ new_const_exp[m].insert(new_const_exp[m].end(),
+ result.const_exp.begin(),
+ result.const_exp.end());
+ Node m_c = result.term;
+ // count should be accurate
+ Assert(result.variable_term.isNull());
+ Assert(m_c.isConst());
+ new_const[m] = m_c;
+ }
+ }
+ } else if (d_term_to_nconst_rep_count[m] == 1) {
+ // check if it is now univariate solved
+ if (Contains(d_rep_to_const, r)) {
+ Trace("nl-subs-debug") << "...parent term " << m
+ << " is univariate solved." << std::endl;
+ const SubstitutionConstResult result = getSubstitutionConst(
+ m, d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const,
+ d_rep_to_const_exp, d_rep_to_const_base);
+ Node eq = (result.term).eqNode(d_rep_to_const[r]);
+ Node v_c = QuantArith::solveEqualityFor(eq, result.variable_term);
+ if (!v_c.isNull()) {
+ Assert(v_c.isConst());
+ if (Contains(new_const, result.variable_term)) {
+ new_const[result.variable_term] = v_c;
+ std::vector<Node>& explanation =
+ new_const_exp[result.variable_term];
+ explanation.insert(explanation.end(), result.const_exp.begin(),
+ result.const_exp.end());
+ if (m != d_rep_to_const_base[r]) {
+ explanation.push_back(m.eqNode(d_rep_to_const_base[r]));
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ // equal univariate terms now solved
+ std::map<Node, std::vector<Node> >::iterator itt = d_reps_to_terms.find(r);
+ if (itt != d_reps_to_terms.end()) {
+ for (unsigned i = 0; i < itt->second.size(); i++) {
+ Node m = itt->second[i];
+ if (d_term_to_nconst_rep_count[m] == 1) {
+ Trace("nl-subs-debug")
+ << "...term " << m << " is univariate solved." << std::endl;
+ const SubstitutionConstResult result = getSubstitutionConst(
+ m, d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const,
+ d_rep_to_const_exp, d_rep_to_const_base);
+ Node v = result.variable_term;
+ Node m_t = result.term;
+ Node eq = m_t.eqNode(r_c);
+ Node v_c = QuantArith::solveEqualityFor(eq, v);
+ if (!v_c.isNull()) {
+ Assert(v_c.isConst());
+ if (new_const.find(v) == new_const.end()) {
+ new_const[v] = v_c;
+ new_const_exp[v].insert(new_const_exp[v].end(),
+ result.const_exp.begin(),
+ result.const_exp.end());
+ if (m != r_cb) {
+ new_const_exp[v].push_back(m.eqNode(r_cb));
+ }
+ }
+ }
+ }
+ }
+ }
+
+ // now, process new inferred constants
+ for (std::map<Node, Node>::iterator itn = new_const.begin();
+ itn != new_const.end(); ++itn) {
+ Node m = itn->first;
+ Node r = d_ee->getRepresentative(m);
+ if (!Contains(d_rep_to_const, r)) {
+ if (setSubstitutionConst(vars, r, itn->second, m, new_const_exp[m], subs,
+ exp, rep_to_subs_index)) {
+ retVal = true;
+ }
+ }
+ }
+ return retVal;
+}
+
+bool NonlinearExtension::getCurrentSubstitution(
+ int effort, const std::vector<Node>& vars, std::vector<Node>& subs,
+ std::map<Node, std::vector<Node> >& exp) {
+ // get the constant equivalence classes
+ std::map<Node, std::vector<int> > rep_to_subs_index;
+
+ bool retVal = false;
+ for (unsigned i = 0; i < vars.size(); i++) {
+ Node n = vars[i];
+ if (d_ee->hasTerm(n)) {
+ Node nr = d_ee->getRepresentative(n);
+ if (nr.isConst()) {
+ subs.push_back(nr);
+ Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr
+ << std::endl;
+ exp[n].push_back(n.eqNode(nr));
+ retVal = true;
+ } else {
+ rep_to_subs_index[nr].push_back(i);
+ subs.push_back(n);
+ }
+ } else {
+ subs.push_back(n);
+ }
+ }
+
+ if (options::nlAlgSolveSubs()) {
+ NonLinearExtentionSubstitutionSolver substitution_solver(d_ee);
+ if (substitution_solver.solve(vars, &subs, &exp, &rep_to_subs_index)) {
+ retVal = true;
+ }
+ }
+
+ // return true if the substitution is non-trivial
+ return retVal;
+
+ // d_containing.getValuation().getModel()->getRepresentative( n );
+}
+
+std::pair<bool, Node> NonlinearExtension::isExtfReduced(
+ int effort, Node n, Node on, const std::vector<Node>& exp) const {
+ if (n != d_zero) {
+ return std::make_pair(n.getKind() != kind::NONLINEAR_MULT, Node::null());
+ }
+ Assert(n == d_zero);
+ Trace("nl-alg-zero-exp") << "Infer zero : " << on << " == " << n << std::endl;
+ // minimize explanation
+ const std::set<Node> vars(on.begin(), on.end());
+
+ for (unsigned i = 0; i < exp.size(); i++) {
+ Trace("nl-alg-zero-exp") << " exp[" << i << "] = " << exp[i] << std::endl;
+ std::vector<Node> eqs;
+ if (exp[i].getKind() == kind::EQUAL) {
+ eqs.push_back(exp[i]);
+ } else if (exp[i].getKind() == kind::AND) {
+ for (unsigned j = 0; j < exp[i].getNumChildren(); j++) {
+ if (exp[i][j].getKind() == kind::EQUAL) {
+ eqs.push_back(exp[i][j]);
+ }
+ }
+ }
+
+ for (unsigned j = 0; j < eqs.size(); j++) {
+ for (unsigned r = 0; r < 2; r++) {
+ if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) {
+ Trace("nl-alg-zero-exp") << "...single exp : " << eqs[j] << std::endl;
+ return std::make_pair(true, eqs[j]);
+ }
+ }
+ }
+ }
+ return std::make_pair(true, Node::null());
+}
+
+Node NonlinearExtension::computeModelValue(Node n, unsigned index) {
+ std::map<Node, Node>::iterator it = d_mv[index].find(n);
+ if (it != d_mv[index].end()) {
+ return it->second;
+ } else {
+ Trace("nl-alg-debug") << "computeModelValue " << n << std::endl;
+ Node ret;
+ if (n.isConst()) {
+ ret = n;
+ } else {
+ if (n.getNumChildren() == 0) {
+ ret = d_containing.getValuation().getModel()->getValue(n);
+ } else {
+ if (index == 1 && n.getKind() == kind::NONLINEAR_MULT) {
+ if (d_containing.getValuation().getModel()->hasTerm(n)) {
+ // use model value for abstraction
+ ret = d_containing.getValuation().getModel()->getRepresentative(n);
+ } else {
+ // abstraction does not exist, use concrete
+ ret = computeModelValue(n, 0);
+ }
+ } else {
+ // otherwise, compute true value
+ std::vector<Node> children;
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ children.push_back(n.getOperator());
+ }
+ for (unsigned i = 0; i < n.getNumChildren(); i++) {
+ Node mc = computeModelValue(n[i], index);
+ children.push_back(mc);
+ }
+ ret = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(n.getKind(), children));
+ if (!ret.isConst()) {
+ Trace("nl-alg-debug") << "...got non-constant : " << ret << " for "
+ << n << ", ask model directly." << std::endl;
+ ret = d_containing.getValuation().getModel()->getValue(ret);
+ }
+ }
+ }
+ if (ret.getType().isReal() && !isArithKind(n.getKind())) {
+ // Trace("nl-alg-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n
+ // << " ] -> " << ret << std::endl;
+ Assert(ret.isConst());
+ }
+ }
+ Trace("nl-alg-debug") << "computed " << (index == 0 ? "M" : "M_A") << "["
+ << n << "] = " << ret << std::endl;
+ d_mv[index][n] = ret;
+ return ret;
+ }
+}
+
+void NonlinearExtension::registerMonomial(Node n) {
+ if (!IsInVector(d_monomials, n)) {
+ d_monomials.push_back(n);
+ Trace("nl-alg-debug") << "Register monomial : " << n << std::endl;
+ if (n.getKind() == kind::NONLINEAR_MULT) {
+ // get exponent count
+ for (unsigned k = 0; k < n.getNumChildren(); k++) {
+ d_m_exp[n][n[k]]++;
+ if (k == 0 || n[k] != n[k - 1]) {
+ d_m_vlist[n].push_back(n[k]);
+ }
+ }
+ d_m_degree[n] = n.getNumChildren();
+ } else if (n == d_one) {
+ d_m_exp[n].clear();
+ d_m_vlist[n].clear();
+ d_m_degree[n] = 0;
+ } else {
+ Assert(!isArithKind(n.getKind()));
+ d_m_exp[n][n] = 1;
+ d_m_vlist[n].push_back(n);
+ d_m_degree[n] = 1;
+ }
+ // TODO: sort necessary here?
+ std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end());
+ Trace("nl-alg-mindex") << "Add monomial to index : " << n << std::endl;
+ d_m_index.addTerm(n, d_m_vlist[n], this);
+ }
+}
+
+void NonlinearExtension::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 (!Contains(mono_diff_a, b)) {
+ Trace("nl-alg-mono-factor")
+ << "Set monomial factor for " << a << "/" << b << std::endl;
+ mono_diff_a[b] = mkMonomialRemFactor(a, common);
+ }
+}
+
+void NonlinearExtension::registerConstraint(Node atom) {
+ if (!IsInVector(d_constraints, atom)) {
+ d_constraints.push_back(atom);
+ Trace("nl-alg-debug") << "Register constraint : " << atom << std::endl;
+ std::map<Node, Node> msum;
+ if (QuantArith::getMonomialSumLit(atom, msum)) {
+ Trace("nl-alg-debug") << "got monomial sum: " << std::endl;
+ if (Trace.isOn("nl-alg-debug")) {
+ QuantArith::debugPrintMonomialSum(msum, "nl-alg-debug");
+ }
+ unsigned max_degree = 0;
+ std::vector<Node> all_m;
+ std::vector<Node> max_deg_m;
+ for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
+ ++itm) {
+ if (!itm->first.isNull()) {
+ all_m.push_back(itm->first);
+ registerMonomial(itm->first);
+ Trace("nl-alg-debug2")
+ << "...process monomial " << itm->first << std::endl;
+ Assert(d_m_degree.find(itm->first) != d_m_degree.end());
+ unsigned d = d_m_degree[itm->first];
+ if (d > max_degree) {
+ max_degree = d;
+ max_deg_m.clear();
+ }
+ if (d >= max_degree) {
+ max_deg_m.push_back(itm->first);
+ }
+ }
+ }
+ // isolate for each maximal degree monomial
+ for (unsigned i = 0; i < all_m.size(); i++) {
+ Node m = all_m[i];
+ Node rhs, coeff;
+ int res = QuantArith::isolate(m, msum, coeff, rhs, atom.getKind());
+ if (res != 0) {
+ Kind type = atom.getKind();
+ if (res == -1) {
+ type = reverseRelationKind(type);
+ }
+ Trace("nl-alg-constraint") << "Constraint : " << atom << " <=> ";
+ if (!coeff.isNull()) {
+ Trace("nl-alg-constraint") << coeff << " * ";
+ }
+ Trace("nl-alg-constraint")
+ << m << " " << type << " " << rhs << std::endl;
+ d_c_info[atom][m].d_rhs = rhs;
+ d_c_info[atom][m].d_coeff = coeff;
+ d_c_info[atom][m].d_type = type;
+ }
+ }
+ for (unsigned i = 0; i < max_deg_m.size(); i++) {
+ Node m = max_deg_m[i];
+ d_c_info_maxm[atom][m] = true;
+ }
+ } else {
+ Trace("nl-alg-debug") << "...failed to get monomial sum." << std::endl;
+ }
+ }
+}
+
+bool NonlinearExtension::isArithKind(Kind k) {
+ return k == kind::PLUS || k == kind::MULT || k == kind::NONLINEAR_MULT;
+}
+
+Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) {
+ if (status == 0) {
+ Node a_eq_b = a.eqNode(b);
+ if (orderType == 0) {
+ return a_eq_b;
+ } else {
+ // return mkAbs( a ).eqNode( mkAbs( b ) );
+ Node negate_b = NodeManager::currentNM()->mkNode(kind::UMINUS, b);
+ return a_eq_b.orNode(a.eqNode(negate_b));
+ }
+ } else if (status < 0) {
+ return mkLit(b, a, -status);
+ } else {
+ Assert(status == 1 || status == 2);
+ NodeManager* nm = NodeManager::currentNM();
+ Kind greater_op = status == 1 ? kind::GEQ : kind::GT;
+ if (orderType == 0) {
+ return nm->mkNode(greater_op, a, b);
+ } else {
+ // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) );
+ Node zero = mkRationalNode(0);
+ Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, zero);
+ Node b_is_nonnegative = nm->mkNode(kind::GEQ, b, zero);
+ Node negate_a = nm->mkNode(kind::UMINUS, a);
+ Node negate_b = nm->mkNode(kind::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)));
+ }
+ }
+}
+
+Node NonlinearExtension::mkAbs(Node a) {
+ if (a.isConst()) {
+ return mkRationalNode(a.getConst<Rational>().abs());
+ } else {
+ NodeManager* nm = NodeManager::currentNM();
+ Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, mkRationalNode(0));
+ return a_is_nonnegative.iteNode(a, nm->mkNode(kind::UMINUS, a));
+ }
+}
+
+// by a <k1> b, a <k2> b, we know a <ret> b
+Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) {
+ if (k2 < k1) {
+ return joinKinds(k2, k1);
+ } else if (k1 == k2) {
+ return k1;
+ } else {
+ Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ ||
+ k1 == kind::GT || k1 == kind::GEQ);
+ Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ ||
+ k2 == kind::GT || k2 == kind::GEQ);
+ if (k1 == kind::EQUAL) {
+ if (k2 == kind::LEQ || k2 == kind::GEQ) {
+ return k1;
+ }
+ } else if (k1 == kind::LT) {
+ if (k2 == kind::LEQ) {
+ return k1;
+ }
+ } else if (k1 == kind::LEQ) {
+ if (k2 == kind::GEQ) {
+ return kind::EQUAL;
+ }
+ } else if (k1 == kind::GT) {
+ if (k2 == kind::GEQ) {
+ return k1;
+ }
+ }
+ return UNDEFINED_KIND;
+ }
+}
+
+// by a <k1> b, b <k2> c, we know a <ret> c
+Kind NonlinearExtension::transKinds(Kind k1, Kind k2) {
+ if (k2 < k1) {
+ return transKinds(k2, k1);
+ } else if (k1 == k2) {
+ return k1;
+ } else {
+ Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ ||
+ k1 == kind::GT || k1 == kind::GEQ);
+ Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ ||
+ k2 == kind::GT || k2 == kind::GEQ);
+ if (k1 == kind::EQUAL) {
+ return k2;
+ } else if (k1 == kind::LT) {
+ if (k2 == kind::LEQ) {
+ return k1;
+ }
+ } else if (k1 == kind::GT) {
+ if (k2 == kind::GEQ) {
+ return k1;
+ }
+ }
+ return UNDEFINED_KIND;
+ }
+}
+
+Node NonlinearExtension::mkMonomialRemFactor(
+ Node n, const NodeMultiset& n_exp_rem) const {
+ std::vector<Node> children;
+ const NodeMultiset& exponent_map = getMonomialExponentMap(n);
+ for (NodeMultiset::const_iterator itme2 = exponent_map.begin();
+ itme2 != exponent_map.end(); ++itme2) {
+ Node v = itme2->first;
+ unsigned inc = itme2->second;
+ Trace("nl-alg-mono-factor")
+ << "..." << inc << " factors of " << v << std::endl;
+ unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0);
+ Assert(count_in_n_exp_rem <= inc);
+ inc -= count_in_n_exp_rem;
+ Trace("nl-alg-mono-factor")
+ << "......rem, now " << inc << " factors of " << v << std::endl;
+ children.insert(children.end(), inc, v);
+ }
+ Node ret = safeConstructNary(kind::MULT, children);
+ ret = Rewriter::rewrite(ret);
+ Trace("nl-alg-mono-factor") << "...return : " << ret << std::endl;
+ return ret;
+}
+
+int NonlinearExtension::flushLemma(Node lem) {
+ Trace("nl-alg-lemma-debug")
+ << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl;
+ lem = Rewriter::rewrite(lem);
+ if (Contains(d_lemmas, lem)) {
+ Trace("nl-alg-lemma-debug")
+ << "NonlinearExtension::Lemma duplicate : " << lem << std::endl;
+ // should not generate duplicates
+ // Assert( false );
+ return 0;
+ }
+ d_lemmas.insert(lem);
+ Trace("nl-alg-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
+ d_containing.getOutputChannel().lemma(lem);
+ return 1;
+}
+
+int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) {
+ if (options::nlAlgEntailConflicts()) {
+ // check if any are entailed to be false
+ for (unsigned i = 0; i < lemmas.size(); i++) {
+ Node ch_lemma = lemmas[i].negate();
+ ch_lemma = Rewriter::rewrite(ch_lemma);
+ Trace("nl-alg-et-debug")
+ << "Check entailment of " << ch_lemma << "..." << std::endl;
+ std::pair<bool, Node> et = d_containing.getValuation().entailmentCheck(
+ THEORY_OF_TYPE_BASED, ch_lemma);
+ Trace("nl-alg-et-debug") << "entailment test result : " << et.first << " "
+ << et.second << std::endl;
+ if (et.first) {
+ Trace("nl-alg-et") << "*** Lemma entailed to be in conflict : "
+ << lemmas[i] << std::endl;
+ // return just this lemma
+ if (flushLemma(lemmas[i])) {
+ lemmas.clear();
+ return 1;
+ }
+ }
+ }
+ }
+
+ int sum = 0;
+ for (unsigned i = 0; i < lemmas.size(); i++) {
+ sum += flushLemma(lemmas[i]);
+ }
+ lemmas.clear();
+ return sum;
+}
+
+std::set<Node> NonlinearExtension::getFalseInModel(
+ const std::vector<Node>& assertions) {
+ std::set<Node> false_asserts;
+ for (size_t i = 0; i < assertions.size(); ++i) {
+ Node lit = assertions[i];
+ Node litv = computeModelValue(lit);
+ Trace("nl-alg-mv") << "M[[ " << lit << " ]] -> " << litv;
+ if (litv != d_true) {
+ Trace("nl-alg-mv") << " [model-false]" << std::endl;
+ Assert(litv == d_false);
+ false_asserts.insert(lit);
+ } else {
+ Trace("nl-alg-mv") << std::endl;
+ }
+ }
+ return false_asserts;
+}
+
+std::vector<Node> NonlinearExtension::splitOnZeros(
+ const std::vector<Node>& ms_vars) {
+ std::vector<Node> lemmas;
+ if (!options::nlAlgSplitZero()) {
+ return lemmas;
+ }
+ for (unsigned i = 0; i < ms_vars.size(); i++) {
+ Node v = ms_vars[i];
+ if (d_zero_split.insert(v)) {
+ Node lem = v.eqNode(d_zero);
+ lem = Rewriter::rewrite(lem);
+ d_containing.getValuation().ensureLiteral(lem);
+ d_containing.getOutputChannel().requirePhase(lem, true);
+ lem = NodeManager::currentNM()->mkNode(kind::OR, lem, lem.negate());
+ lemmas.push_back(lem);
+ }
+ }
+ return lemmas;
+}
+
+void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
+ const std::set<Node>& false_asserts) {
+ // processed monomials
+ std::map<Node, bool> ms_proc;
+
+ // list of monomials
+ std::vector<Node> ms;
+ d_containing.getExtTheory()->getTerms(ms);
+ // list of variables occurring in monomials
+ std::vector<Node> ms_vars;
+
+ // register monomials
+ Trace("nl-alg-mv") << "Monomials : " << std::endl;
+ for (unsigned j = 0; j < ms.size(); j++) {
+ Node a = ms[j];
+ registerMonomial(a);
+ computeModelValue(a, 0);
+ computeModelValue(a, 1);
+ Assert(d_mv[1][a].isConst());
+ Assert(d_mv[0][a].isConst());
+ Trace("nl-alg-mv") << " " << a << " -> " << d_mv[1][a] << " ["
+ << d_mv[0][a] << "]" << std::endl;
+
+ std::map<Node, std::vector<Node> >::iterator itvl = d_m_vlist.find(a);
+ Assert(itvl != d_m_vlist.end());
+ for (unsigned k = 0; k < itvl->second.size(); k++) {
+ if (!IsInVector(ms_vars, itvl->second[k])) {
+ ms_vars.push_back(itvl->second[k]);
+ }
+ }
+ /*
+ //mark processed if has a "one" factor (will look at reduced monomial)
+ std::map< Node, std::map< Node, unsigned > >::iterator itme =
+ d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node,
+ unsigned >::iterator itme2 = itme->second.begin(); itme2 !=
+ itme->second.end(); ++itme2 ){ Node v = itme->first; Assert(
+ d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if(
+ mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true;
+ Trace("nl-alg-mv")
+ << "...mark " << a << " reduced since has 1 factor." << std::endl;
+ break;
+ }
+ }
+ */
+ }
+
+ // register constants
+ registerMonomial(d_one);
+ for (unsigned j = 0; j < d_order_points.size(); j++) {
+ Node c = d_order_points[j];
+ computeModelValue(c, 0);
+ computeModelValue(c, 1);
+ }
+
+ int lemmas_proc;
+ std::vector<Node> lemmas;
+
+ // register variables
+ Trace("nl-alg-mv") << "Variables : " << std::endl;
+ Trace("nl-alg") << "Get zero split lemmas..." << std::endl;
+ for (unsigned i = 0; i < ms_vars.size(); i++) {
+ Node v = ms_vars[i];
+ registerMonomial(v);
+ computeModelValue(v, 0);
+ computeModelValue(v, 1);
+ Trace("nl-alg-mv") << " " << v << " -> " << d_mv[0][v] << std::endl;
+ }
+
+ // possibly split on zero?
+ lemmas = splitOnZeros(ms_vars);
+ lemmas_proc = flushLemmas(lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas."
+ << std::endl;
+ return;
+ }
+
+ //-----------------------------------lemmas based on sign (comparison to zero)
+ std::map<Node, int> signs;
+ Trace("nl-alg") << "Get sign lemmas..." << std::endl;
+ for (unsigned j = 0; j < ms.size(); j++) {
+ Node a = ms[j];
+ if (ms_proc.find(a) == ms_proc.end()) {
+ std::vector<Node> exp;
+ Trace("nl-alg-debug") << " process " << a << "..." << std::endl;
+ signs[a] = compareSign(a, a, 0, 1, exp, lemmas);
+ if (signs[a] == 0) {
+ ms_proc[a] = true;
+ Trace("nl-alg-mv") << "...mark " << a
+ << " reduced since its value is 0." << std::endl;
+ }
+ }
+ }
+ lemmas_proc = flushLemmas(lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas."
+ << std::endl;
+ return;
+ }
+
+ //-----------------------------lemmas based on magnitude of non-zero monomials
+ for (unsigned r = 1; r <= 1; r++) {
+ assignOrderIds(ms_vars, d_order_vars[r], r);
+
+ // sort individual variable lists
+ SortNonlinearExtension smv;
+ smv.d_nla = this;
+ smv.d_order_type = r;
+ smv.d_reverse_order = true;
+ for (unsigned j = 0; j < ms.size(); j++) {
+ std::sort(d_m_vlist[ms[j]].begin(), d_m_vlist[ms[j]].end(), smv);
+ }
+ for (unsigned c = 0; c < 3; c++) {
+ // 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-alg") << "Get comparison lemmas (order=" << r
+ << ", compare=" << c << ")..." << std::endl;
+ for (unsigned j = 0; j < ms.size(); j++) {
+ Node a = ms[j];
+ if (ms_proc.find(a) == ms_proc.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 {
+ std::map<Node, NodeMultiset>::iterator itmea = d_m_exp.find(a);
+ Assert(itmea != d_m_exp.end());
+ if (c == 1) {
+ // TODO : not just against containing variables?
+ // compare magnitude against variables
+ for (unsigned k = 0; k < ms_vars.size(); k++) {
+ Node v = ms_vars[k];
+ std::vector<Node> exp;
+ NodeMultiset a_exp_proc;
+ NodeMultiset b_exp_proc;
+ if (itmea->second.find(v) != itmea->second.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 < ms.size(); k++) {
+ Node b = ms[k];
+ //(signs[a]==signs[b])==(r==0)
+ if (ms_proc.find(b) == ms_proc.end()) {
+ std::map<Node, NodeMultiset>::iterator itmeb =
+ d_m_exp.find(b);
+ Assert(itmeb != d_m_exp.end());
+
+ 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::iterator itmea2 = itmea->second.begin();
+ itmea2 != itmea->second.end(); ++itmea2) {
+ NodeMultiset::iterator itmeb2 =
+ itmeb->second.find(itmea2->first);
+ if (itmeb2 != itmeb->second.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-alg-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-alg-comp") << "Compute redundancies for " << lemmas.size()
+ << " lemmas." << std::endl;
+ // naive
+ std::vector<Node> 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.push_back(itc2->second);
+ Trace("nl-alg-comp")
+ << "...inference of " << itc->first << " > "
+ << itc2->first << " was redundant." << std::endl;
+ break;
+ }
+ }
+ }
+ }
+ }
+ }
+ std::vector<Node> nr_lemmas;
+ for (unsigned i = 0; i < lemmas.size(); i++) {
+ if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) ==
+ r_lemmas.end()) {
+ nr_lemmas.push_back(lemmas[i]);
+ }
+ }
+ // TODO: only take maximal lower/minimial lower bounds?
+
+ Trace("nl-alg-comp") << nr_lemmas.size() << " / " << lemmas.size()
+ << " were non-redundant." << std::endl;
+ lemmas_proc = flushLemmas(nr_lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc
+ << " new lemmas (out of possible " << lemmas.size()
+ << ")." << std::endl;
+ return;
+ }
+ }
+ }
+
+ // sort monomials by degree
+ SortNonlinearExtension snlad;
+ snlad.d_nla = this;
+ snlad.d_order_type = 4;
+ snlad.d_reverse_order = false;
+ std::sort(ms.begin(), ms.end(), snlad);
+ // all monomials
+ std::vector<Node> terms;
+ terms.insert(terms.end(), ms_vars.begin(), ms_vars.end());
+ terms.insert(terms.end(), ms.begin(), ms.end());
+
+ // term -> coeff -> rhs -> ( status, exp, b ),
+ // where we have that : exp => ( coeff * term <status> rhs )
+ // b is true if degree( term ) >= degree( rhs )
+ std::map<Node, std::map<Node, std::map<Node, Kind> > > ci;
+ std::map<Node, std::map<Node, std::map<Node, Node> > > ci_exp;
+ std::map<Node, std::map<Node, std::map<Node, bool> > > ci_max;
+
+ // If ( m, p1, true ), then it would help satisfiability if m were ( >
+ // if p1=true, < if p1=false )
+ std::map<Node, std::map<bool, bool> > tplane_refine_dir;
+
+ // register constraints
+ Trace("nl-alg-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;
+ bool polarity = lit.getKind() != kind::NOT;
+ Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+ registerConstraint(atom);
+ bool is_false_lit = false_asserts.find(lit) != false_asserts.end();
+ // add information about bounds to variables
+ std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc =
+ d_c_info.find(atom);
+ std::map<Node, std::map<Node, bool> >::iterator itcm =
+ d_c_info_maxm.find(atom);
+ if (itc != d_c_info.end()) {
+ Assert(itcm != d_c_info_maxm.end());
+ for (std::map<Node, ConstraintInfo>::iterator itcc = itc->second.begin();
+ itcc != itc->second.end(); ++itcc) {
+ 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 == kind::EQUAL) {
+ // we will take the strict inequality in the direction of the
+ // model
+ Node lhs = QuantArith::mkCoeffTerm(coeff, x);
+ Node query = NodeManager::currentNM()->mkNode(kind::GT, lhs, rhs);
+ Node query_mv = computeModelValue(query, 1);
+ if (query_mv == d_true) {
+ exp = query;
+ type = kind::GT;
+ } else {
+ Assert(query_mv == d_false);
+ exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs);
+ type = kind::LT;
+ }
+ } else {
+ type = negateKind(type);
+ }
+ }
+ // add to status if maximal degree
+ ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end();
+ if (Trace.isOn("nl-alg-bound-debug2")) {
+ Node t = QuantArith::mkCoeffTerm(coeff, x);
+ Trace("nl-alg-bound-debug2")
+ << "Add Bound: " << t << " " << type << " " << rhs << " by "
+ << exp << std::endl;
+ }
+ bool updated = true;
+ std::map<Node, Kind>::iterator its = ci[x][coeff].find(rhs);
+ if (its == ci[x][coeff].end()) {
+ ci[x][coeff][rhs] = type;
+ ci_exp[x][coeff][rhs] = exp;
+ } else if (type != its->second) {
+ Trace("nl-alg-bound-debug2")
+ << "Joining kinds : " << type << " " << its->second << std::endl;
+ Kind jk = joinKinds(type, its->second);
+ if (jk == kind::UNDEFINED_KIND) {
+ updated = false;
+ } else if (jk != its->second) {
+ if (jk == type) {
+ ci[x][coeff][rhs] = type;
+ ci_exp[x][coeff][rhs] = exp;
+ } else {
+ ci[x][coeff][rhs] = jk;
+ ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode(
+ kind::AND, ci_exp[x][coeff][rhs], exp);
+ }
+ } else {
+ updated = false;
+ }
+ }
+ if (Trace.isOn("nl-alg-bound")) {
+ if (updated) {
+ Trace("nl-alg-bound") << "Bound: ";
+ debugPrintBound("nl-alg-bound", coeff, x, ci[x][coeff][rhs], rhs);
+ Trace("nl-alg-bound") << " by " << ci_exp[x][coeff][rhs];
+ if (ci_max[x][coeff][rhs]) {
+ Trace("nl-alg-bound") << ", is max degree";
+ }
+ Trace("nl-alg-bound") << std::endl;
+ }
+ }
+ // compute if bound is not satisfied, and store what is required
+ // for a possible refinement
+ if (options::nlAlgTangentPlanes()) {
+ if (is_false_lit) {
+ Node rhs_v = computeModelValue(rhs, 0);
+ Node x_v = computeModelValue(x, 0);
+ bool needsRefine = false;
+ bool refineDir;
+ if (rhs_v == x_v) {
+ if (type == kind::GT) {
+ needsRefine = true;
+ refineDir = true;
+ } else if (type == kind::LT) {
+ needsRefine = true;
+ refineDir = false;
+ }
+ } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) {
+ if (type != kind::GT && type != kind::GEQ) {
+ needsRefine = true;
+ refineDir = false;
+ }
+ } else {
+ if (type != kind::LT && type != kind::LEQ) {
+ needsRefine = true;
+ refineDir = true;
+ }
+ }
+ Trace("nl-alg-tplanes-cons-debug")
+ << "...compute if bound corresponds to a required "
+ "refinement"
+ << std::endl;
+ Trace("nl-alg-tplanes-cons-debug")
+ << "...M[" << x << "] = " << x_v << ", M[" << rhs
+ << "] = " << rhs_v << std::endl;
+ Trace("nl-alg-tplanes-cons-debug") << "...refine = " << needsRefine
+ << "/" << refineDir << std::endl;
+ if (needsRefine) {
+ Trace("nl-alg-tplanes-cons")
+ << "---> By " << lit << " and since M[" << x << "] = " << x_v
+ << ", M[" << rhs << "] = " << rhs_v << ", ";
+ Trace("nl-alg-tplanes-cons")
+ << "monomial " << x << " should be "
+ << (refineDir ? "larger" : "smaller") << std::endl;
+ tplane_refine_dir[x][refineDir] = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ // reflexive constraints
+ Node null_coeff;
+ for (unsigned j = 0; j < terms.size(); j++) {
+ Node n = terms[j];
+ ci[n][null_coeff][n] = kind::EQUAL;
+ ci_exp[n][null_coeff][n] = d_true;
+ ci_max[n][null_coeff][n] = false;
+ }
+
+ //-----------------------------------------------------------------------------------------inferred
+ // bounds lemmas, e.g. x >= t => y*x >= y*t
+ Trace("nl-alg") << "Get inferred bound lemmas..." << std::endl;
+
+ std::vector<Node> nt_lemmas;
+ for (unsigned k = 0; k < terms.size(); k++) {
+ Node x = terms[k];
+ Trace("nl-alg-bound-debug")
+ << "Process bounds for " << x << " : " << std::endl;
+ std::map<Node, std::vector<Node> >::iterator itm =
+ d_m_contain_parent.find(x);
+ if (itm != d_m_contain_parent.end()) {
+ Trace("nl-alg-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 =
+ ci.find(x);
+ if (itc != ci.end()) {
+ for (std::map<Node, std::map<Node, Kind> >::iterator itcc =
+ itc->second.begin();
+ itcc != itc->second.end(); ++itcc) {
+ Node coeff = itcc->first;
+ Node t = QuantArith::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 (ci_max[x][coeff][rhs]) {
+ Kind type = itcr->second;
+ for (unsigned j = 0; j < itm->second.size(); j++) {
+ Node y = itm->second[j];
+ Assert(d_m_contain_mult[x].find(y) !=
+ d_m_contain_mult[x].end());
+ Node mult = d_m_contain_mult[x][y];
+ // x <k> t => m*x <k'> t where y = m*x
+ // get the sign of mult
+ Node mmv = computeModelValue(mult);
+ Trace("nl-alg-bound-debug2")
+ << "Model value of " << mult << " is " << mmv << std::endl;
+ Assert(mmv.isConst());
+ int mmv_sign = mmv.getConst<Rational>().sgn();
+ Trace("nl-alg-bound-debug2")
+ << " sign of " << mmv << " is " << mmv_sign << std::endl;
+ if (mmv_sign != 0) {
+ Trace("nl-alg-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 =
+ NodeManager::currentNM()->mkNode(kind::MULT, mult, t);
+ Node infer_rhs =
+ NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs);
+ Node infer = NodeManager::currentNM()->mkNode(
+ infer_type, infer_lhs, infer_rhs);
+ Trace("nl-alg-bound-debug") << " " << infer << std::endl;
+ infer = Rewriter::rewrite(infer);
+ Trace("nl-alg-bound-debug2")
+ << " ...rewritten : " << infer << std::endl;
+ // check whether it is false in model for abstraction
+ Node infer_mv = computeModelValue(infer, 1);
+ Trace("nl-alg-bound-debug")
+ << " ...infer model value is " << infer_mv
+ << std::endl;
+ if (infer_mv == d_false) {
+ Node exp = NodeManager::currentNM()->mkNode(
+ kind::AND,
+ NodeManager::currentNM()->mkNode(
+ mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero),
+ ci_exp[x][coeff][rhs]);
+ Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
+ exp, infer);
+ Node pr_iblem = iblem;
+ iblem = Rewriter::rewrite(iblem);
+ bool introNewTerms = hasNewMonomials(iblem, ms);
+ Trace("nl-alg-bound-lemma")
+ << "*** Bound inference lemma : " << iblem
+ << " (pre-rewrite : " << pr_iblem << ")" << std::endl;
+ // Trace("nl-alg-bound-lemma") << " intro new
+ // monomials = " << introNewTerms << std::endl;
+ if (!introNewTerms) {
+ lemmas.push_back(iblem);
+ } else {
+ nt_lemmas.push_back(iblem);
+ }
+ }
+ } else {
+ Trace("nl-alg-bound-debug") << " ...coefficient " << mult
+ << " is zero." << std::endl;
+ }
+ }
+ }
+ }
+ }
+ }
+ } else {
+ Trace("nl-alg-bound-debug") << "...has no parent monomials." << std::endl;
+ }
+ }
+ // Trace("nl-alg") << "Bound lemmas : " << lemmas.size() << ", " <<
+ // nt_lemmas.size() << std::endl; prioritize lemmas that do not
+ // introduce new monomials
+ lemmas_proc = flushLemmas(lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas."
+ << std::endl;
+ return;
+ }
+
+ //------------------------------------resolution bound inferences, e.g.
+ //(
+ // y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
+ if (options::nlAlgResBound()) {
+ Trace("nl-alg") << "Get resolution inferred bound lemmas..." << std::endl;
+ for (unsigned j = 0; j < terms.size(); j++) {
+ Node a = terms[j];
+ std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca =
+ ci.find(a);
+ if (itca != ci.end()) {
+ for (unsigned k = (j + 1); k < terms.size(); k++) {
+ Node b = terms[k];
+ std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator
+ itcb = ci.find(b);
+ if (itcb != ci.end()) {
+ Trace("nl-alg-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()) {
+ std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a);
+ Assert(itb != d_mono_diff[b].end());
+ Node mv_a = computeModelValue(ita->second, 1);
+ Assert(mv_a.isConst());
+ int mv_a_sgn = mv_a.getConst<Rational>().sgn();
+ Assert(mv_a_sgn != 0);
+ Node mv_b = computeModelValue(itb->second, 1);
+ Assert(mv_b.isConst());
+ int mv_b_sgn = mv_b.getConst<Rational>().sgn();
+ Assert(mv_b_sgn != 0);
+ Trace("nl-alg-rbound") << "Get resolution inferences for [a] "
+ << a << " vs [b] " << b << std::endl;
+ Trace("nl-alg-rbound")
+ << " [a] factor is " << ita->second
+ << ", sign in model = " << mv_a_sgn << std::endl;
+ Trace("nl-alg-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 = NodeManager::currentNM()->mkNode(
+ kind::MULT, itb->second, rhs_a);
+ rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
+ if (!hasNewMonomials(rhs_a_res_base, ms)) {
+ Kind type_a = itcar->second;
+ exp.push_back(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 =
+ QuantArith::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 = NodeManager::currentNM()->mkNode(
+ kind::MULT, ita->second, rhs_b);
+ rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res);
+ rhs_b_res = Rewriter::rewrite(rhs_b_res);
+ if (!hasNewMonomials(rhs_b_res, ms)) {
+ Kind type_b = itcbr->second;
+ exp.push_back(ci_exp[b][coeff_b][rhs_b]);
+ if (Trace.isOn("nl-alg-rbound")) {
+ Trace("nl-alg-rbound") << "* try bounds : ";
+ debugPrintBound("nl-alg-rbound", coeff_a, a, type_a,
+ rhs_a);
+ Trace("nl-alg-rbound") << std::endl;
+ Trace("nl-alg-rbound") << " ";
+ debugPrintBound("nl-alg-rbound", coeff_b, b, type_b,
+ rhs_b);
+ Trace("nl-alg-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(NodeManager::currentNM()->mkNode(
+ kind::GT, pivot_factor, d_zero));
+ } else {
+ exp.push_back(NodeManager::currentNM()->mkNode(
+ kind::LT, pivot_factor, d_zero));
+ }
+ }
+ Kind jk = transKinds(types[0], types[1]);
+ Trace("nl-alg-rbound-debug")
+ << "trans kind : " << types[0] << " + "
+ << types[1] << " = " << jk << std::endl;
+ if (jk != kind::UNDEFINED_KIND) {
+ Node conc = NodeManager::currentNM()->mkNode(
+ jk, rhs_a_res, rhs_b_res);
+ Node conc_mv = computeModelValue(conc, 1);
+ if (conc_mv == d_false) {
+ Node rblem = NodeManager::currentNM()->mkNode(
+ kind::IMPLIES,
+ NodeManager::currentNM()->mkNode(kind::AND,
+ exp),
+ conc);
+ Trace("nl-alg-rbound-lemma-debug")
+ << "Resolution bound lemma "
+ "(pre-rewrite) "
+ ": "
+ << rblem << std::endl;
+ rblem = Rewriter::rewrite(rblem);
+ Trace("nl-alg-rbound-lemma")
+ << "Resolution bound lemma : " << rblem
+ << std::endl;
+ lemmas.push_back(rblem);
+ }
+ }
+ exp.pop_back();
+ exp.pop_back();
+ exp.pop_back();
+ }
+ }
+ }
+ exp.pop_back();
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ lemmas_proc = flushLemmas(lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas."
+ << std::endl;
+ return;
+ }
+ }
+
+ // from inferred bound inferences
+ lemmas_proc = flushLemmas(nt_lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc
+ << " new (monomial-introducing) lemmas." << std::endl;
+ return;
+ }
+
+ if (options::nlAlgTangentPlanes()) {
+ Trace("nl-alg") << "Get tangent plane lemmas..." << std::endl;
+ unsigned kstart = ms_vars.size();
+ for (unsigned k = kstart; k < terms.size(); k++) {
+ Node t = terms[k];
+ // if this term requires a refinement
+ if (tplane_refine_dir.find(t) != tplane_refine_dir.end()) {
+ Trace("nl-alg-tplanes")
+ << "Look at monomial requiring refinement : " << t << std::endl;
+ // get a decomposition
+ std::map<Node, std::vector<Node> >::iterator it =
+ d_m_contain_children.find(t);
+ if (it != d_m_contain_children.end()) {
+ 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_m_contain_umult[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-alg-tplanes")
+ << " decomposable into : " << a << " * " << b << std::endl;
+ Node a_v = computeModelValue(a, 1);
+ Node b_v = computeModelValue(b, 1);
+ // tangent plane
+ Node tplane = NodeManager::currentNM()->mkNode(
+ kind::MINUS,
+ NodeManager::currentNM()->mkNode(
+ kind::PLUS,
+ NodeManager::currentNM()->mkNode(kind::MULT, b_v, a),
+ NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)),
+ NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v));
+ for (unsigned d = 0; d < 4; d++) {
+ Node aa = NodeManager::currentNM()->mkNode(
+ d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v);
+ Node ab = NodeManager::currentNM()->mkNode(
+ d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v);
+ Node conc = NodeManager::currentNM()->mkNode(
+ d <= 1 ? kind::LEQ : kind::GEQ, t, tplane);
+ Node tlem = NodeManager::currentNM()->mkNode(
+ kind::OR, aa.negate(), ab.negate(), conc);
+ Trace("nl-alg-tplanes")
+ << "Tangent plane lemma : " << tlem << std::endl;
+ lemmas.push_back(tlem);
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ Trace("nl-alg") << "...trying " << lemmas.size()
+ << " tangent plane lemmas..." << std::endl;
+ lemmas_proc = flushLemmas(lemmas);
+ if (lemmas_proc > 0) {
+ Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas."
+ << std::endl;
+ return;
+ }
+ }
+
+ Trace("nl-alg") << "...set incomplete" << std::endl;
+ d_containing.getOutputChannel().setIncomplete();
+}
+
+void NonlinearExtension::check(Theory::Effort e) {
+ Trace("nl-alg") << std::endl;
+ Trace("nl-alg") << "NonlinearExtension::check, effort = " << e << std::endl;
+ if (e == Theory::EFFORT_FULL) {
+ d_containing.getExtTheory()->clearCache();
+ d_needsLastCall = true;
+ if (options::nlAlgRewrites()) {
+ std::vector<Node> nred;
+ if (!d_containing.getExtTheory()->doInferences(0, nred)) {
+ Trace("nl-alg") << "...sent no lemmas, # extf to reduce = "
+ << nred.size() << std::endl;
+ if (nred.empty()) {
+ d_needsLastCall = false;
+ }
+ } else {
+ Trace("nl-alg") << "...sent lemmas." << std::endl;
+ }
+ }
+ } else {
+ Assert(e == Theory::EFFORT_LAST_CALL);
+ Trace("nl-alg-mv") << "Getting model values... check for [model-false]"
+ << std::endl;
+ d_mv[0].clear();
+ d_mv[1].clear();
+ 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);
+ }
+ const std::set<Node> false_asserts = getFalseInModel(assertions);
+ if (!false_asserts.empty()) {
+ checkLastCall(assertions, false_asserts);
+ }
+ }
+}
+
+void NonlinearExtension::assignOrderIds(std::vector<Node>& vars,
+ NodeMultiset& order,
+ unsigned orderType) {
+ SortNonlinearExtension smv;
+ smv.d_nla = this;
+ smv.d_order_type = orderType;
+ smv.d_reverse_order = false;
+ std::sort(vars.begin(), vars.end(), smv);
+
+ order.clear();
+ // assign ordering id's
+ unsigned counter = 0;
+ unsigned order_index = (orderType == 0 || orderType == 2) ? 0 : 1;
+ Node prev;
+ for (unsigned j = 0; j < vars.size(); j++) {
+ Node x = vars[j];
+ Node v = get_compare_value(x, orderType);
+ Trace("nl-alg-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 = get_compare_value(d_order_points[order_index], orderType);
+ if (compare_value(v, vv, orderType) <= 0) {
+ counter++;
+ Trace("nl-alg-mvo")
+ << "O_" << orderType << "[" << 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() || compare_value(v, prev, orderType) != 0) {
+ counter++;
+ }
+ Trace("nl-alg-mvo") << "O_" << orderType << "[" << x << "] = " << counter
+ << std::endl;
+ order[x] = counter;
+ prev = v;
+ }
+ while (order_index < d_order_points.size()) {
+ counter++;
+ Trace("nl-alg-mvo") << "O_" << orderType << "["
+ << d_order_points[order_index] << "] = " << counter
+ << std::endl;
+ order[d_order_points[order_index]] = counter;
+ order_index++;
+ }
+}
+
+int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const {
+ Assert(orderType >= 0);
+ if (orderType <= 3) {
+ return compare_value(get_compare_value(i, orderType),
+ get_compare_value(j, orderType), orderType);
+ // minimal degree
+ } else if (orderType == 4) {
+ unsigned i_count = getCount(d_m_degree, i);
+ unsigned j_count = getCount(d_m_degree, j);
+ return i_count == j_count ? 0 : (i_count < j_count ? 1 : -1);
+ } else {
+ return 0;
+ }
+}
+
+int NonlinearExtension::compare_value(Node i, Node j,
+ unsigned orderType) const {
+ Assert(orderType >= 0 && orderType <= 3);
+ Trace("nl-alg-debug") << "compare_value " << i << " " << j
+ << ", o = " << orderType << std::endl;
+ int ret;
+ if (i == j) {
+ ret = 0;
+ } else if (orderType == 0 || orderType == 2) {
+ ret = i.getConst<Rational>() < j.getConst<Rational>() ? 1 : -1;
+ } else {
+ Trace("nl-alg-debug") << "vals : " << i.getConst<Rational>() << " "
+ << j.getConst<Rational>() << std::endl;
+ Trace("nl-alg-debug") << i.getConst<Rational>().abs() << " "
+ << j.getConst<Rational>().abs() << std::endl;
+ ret = (i.getConst<Rational>().abs() == j.getConst<Rational>().abs()
+ ? 0
+ : (i.getConst<Rational>().abs() < j.getConst<Rational>().abs()
+ ? 1
+ : -1));
+ }
+ Trace("nl-alg-debug") << "...return " << ret << std::endl;
+ return ret;
+}
+
+Node NonlinearExtension::get_compare_value(Node i, unsigned orderType) const {
+ Trace("nl-alg-debug") << "Compare variable " << i << " " << orderType
+ << std::endl;
+ Assert(orderType >= 0 && orderType <= 3);
+ unsigned mindex = orderType <= 1 ? 0 : 1;
+ std::map<Node, Node>::const_iterator iti = d_mv[mindex].find(i);
+ Assert(iti != d_mv[mindex].end());
+ return iti->second;
+}
+
+// trying to show a <> 0 by inequalities between variables in monomial a w.r.t
+// 0
+int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index,
+ int status, std::vector<Node>& exp,
+ std::vector<Node>& lem) {
+ Trace("nl-alg-debug") << "Process " << a << " at index " << a_index
+ << ", status is " << status << std::endl;
+ Assert(d_mv[1].find(oa) != d_mv[1].end());
+ if (a_index == d_m_vlist[a].size()) {
+ if (d_mv[1][oa].getConst<Rational>().sgn() != status) {
+ Node lemma = safeConstructNary(kind::AND, exp)
+ .impNode(mkLit(oa, d_zero, status * 2));
+ lem.push_back(lemma);
+ }
+ return status;
+ } else {
+ Assert(a_index < d_m_vlist[a].size());
+ Node av = d_m_vlist[a][a_index];
+ unsigned aexp = d_m_exp[a][av];
+ // take current sign in model
+ Assert(d_mv[0].find(av) != d_mv[0].end());
+ int sgn = d_mv[0][av].getConst<Rational>().sgn();
+ Trace("nl-alg-debug") << "Process var " << av << "^" << aexp
+ << ", model sign = " << sgn << std::endl;
+ if (sgn == 0) {
+ if (d_mv[1][oa].getConst<Rational>().sgn() != 0) {
+ Node lemma = av.eqNode(d_zero).impNode(oa.eqNode(d_zero));
+ lem.push_back(lemma);
+ }
+ return 0;
+ } else {
+ if (aexp % 2 == 0) {
+ exp.push_back(av.eqNode(d_zero).negate());
+ return compareSign(oa, a, a_index + 1, status, exp, lem);
+ } else {
+ exp.push_back(NodeManager::currentNM()->mkNode(
+ sgn == 1 ? kind::GT : kind::LT, av, d_zero));
+ return compareSign(oa, a, a_index + 1, status * sgn, exp, lem);
+ }
+ }
+ }
+}
+
+bool NonlinearExtension::compareMonomial(
+ Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b,
+ NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem,
+ std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers) {
+ Trace("nl-alg-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;
+ } else {
+ exp.resize(pexp_size);
+ Trace("nl-alg-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;
+ } else {
+ return false;
+ }
+ }
+}
+
+bool NonlinearExtension::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()) {
+ 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 NonlinearExtension::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<Node>& lem,
+ std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers) {
+ Trace("nl-alg-comp-debug")
+ << "compareMonomial " << oa << " and " << ob << ", indices = " << a_index
+ << " " << b_index << std::endl;
+ Assert(status == 0 || status == 2);
+ if (a_index == d_m_vlist[a].size() && b_index == d_m_vlist[b].size()) {
+ // finished, compare abstract values
+ int modelStatus = compare(oa, ob, 3) * -2;
+ Trace("nl-alg-comp") << "...finished comparison with " << oa << " <"
+ << status << "> " << ob
+ << ", model status = " << modelStatus << std::endl;
+ if (status != modelStatus) {
+ Trace("nl-alg-comp-infer")
+ << "infer : " << oa << " <" << status << "> " << ob << std::endl;
+ if (status == 2) {
+ // must state that all variables are non-zero
+ for (unsigned j = 0; j < d_m_vlist[a].size(); j++) {
+ exp.push_back(d_m_vlist[a][j].eqNode(d_zero).negate());
+ }
+ }
+ Node clem = NodeManager::currentNM()->mkNode(
+ kind::IMPLIES, safeConstructNary(kind::AND, exp),
+ mkLit(oa, ob, status, 1));
+ Trace("nl-alg-comp-lemma") << "comparison lemma : " << clem << std::endl;
+ lem.push_back(clem);
+ cmp_infers[status][oa][ob] = clem;
+ }
+ return true;
+ } else {
+ // get a/b variable information
+ Node av;
+ unsigned aexp = 0;
+ unsigned avo = 0;
+ if (a_index < d_m_vlist[a].size()) {
+ av = d_m_vlist[a][a_index];
+ Assert(a_exp_proc[av] <= d_m_exp[a][av]);
+ aexp = d_m_exp[a][av] - 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[1].find(av) != d_order_vars[1].end());
+ avo = d_order_vars[1][av];
+ }
+ Node bv;
+ unsigned bexp = 0;
+ unsigned bvo = 0;
+ if (b_index < d_m_vlist[b].size()) {
+ bv = d_m_vlist[b][b_index];
+ Assert(b_exp_proc[bv] <= d_m_exp[b][bv]);
+ bexp = d_m_exp[b][bv] - 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[1].find(bv) != d_order_vars[1].end());
+ bvo = d_order_vars[1][bv];
+ }
+ // get "one" information
+ Assert(d_order_vars[1].find(d_one) != d_order_vars[1].end());
+ unsigned ovo = d_order_vars[1][d_one];
+ Trace("nl-alg-comp-debug") << "....vars : " << av << "^" << aexp << " "
+ << bv << "^" << bexp << std::endl;
+
+ //--- cases
+ if (av.isNull()) {
+ if (bvo <= ovo) {
+ Trace("nl-alg-comp-debug") << "...take leading " << bv << std::endl;
+ // can multiply b by <=1
+ exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, 1));
+ 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);
+ } else {
+ Trace("nl-alg-comp-debug")
+ << "...failure, unmatched |b|>1 component." << std::endl;
+ return false;
+ }
+ } else if (bv.isNull()) {
+ if (avo >= ovo) {
+ Trace("nl-alg-comp-debug") << "...take leading " << av << std::endl;
+ // can multiply a by >=1
+ exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, 1));
+ 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);
+ } else {
+ Trace("nl-alg-comp-debug")
+ << "...failure, unmatched |a|<1 component." << std::endl;
+ return false;
+ }
+ } else {
+ Assert(!av.isNull() && !bv.isNull());
+ if (avo >= bvo) {
+ if (bvo < ovo && avo >= ovo) {
+ Trace("nl-alg-comp-debug") << "...take leading " << av << std::endl;
+ // do avo>=1 instead
+ exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, 1));
+ 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);
+ } else {
+ unsigned min_exp = aexp > bexp ? bexp : aexp;
+ a_exp_proc[av] += min_exp;
+ b_exp_proc[bv] += min_exp;
+ Trace("nl-alg-comp-debug")
+ << "...take leading " << min_exp << " from " << av << " and "
+ << bv << std::endl;
+ exp.push_back(mkLit(av, bv, avo == bvo ? 0 : 2, 1));
+ 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;
+ }
+ } else {
+ if (bvo <= ovo) {
+ Trace("nl-alg-comp-debug") << "...take leading " << bv << std::endl;
+ // try multiply b <= 1
+ exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, 1));
+ 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);
+ } else {
+ Trace("nl-alg-comp-debug")
+ << "...failure, leading |b|>|a|>1 component." << std::endl;
+ return false;
+ }
+ }
+ }
+ }
+}
+
+// status 0 : n equal, -1 : n superset, 1 : n subset
+void NonlinearExtension::MonomialIndex::addTerm(Node n,
+ const std::vector<Node>& reps,
+ NonlinearExtension* nla,
+ int status, unsigned argIndex) {
+ if (status == 0) {
+ if (argIndex == reps.size()) {
+ d_monos.push_back(n);
+ } else {
+ d_data[reps[argIndex]].addTerm(n, reps, nla, status, argIndex + 1);
+ }
+ }
+ for (std::map<Node, MonomialIndex>::iterator it = d_data.begin();
+ it != d_data.end(); ++it) {
+ if (status != 0 || argIndex == reps.size() || it->first != reps[argIndex]) {
+ // if we do not contain this variable, then if we were a superset,
+ // fail (-2), otherwise we are subset. if we do contain this
+ // variable, then if we were equal, we are superset since variables
+ // are ordered, otherwise we remain the same.
+ int new_status =
+ std::find(reps.begin(), reps.end(), it->first) == reps.end()
+ ? (status >= 0 ? 1 : -2)
+ : (status == 0 ? -1 : status);
+ if (new_status != -2) {
+ it->second.addTerm(n, reps, nla, new_status, argIndex);
+ }
+ }
+ }
+ // compare for subsets
+ for (unsigned i = 0; i < d_monos.size(); i++) {
+ Node m = d_monos[i];
+ if (m != n) {
+ // we are superset if we are equal and haven't traversed all variables
+ int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status;
+ Trace("nl-alg-mindex-debug") << " compare " << n << " and " << m
+ << ", status = " << cstatus << std::endl;
+ if (cstatus <= 0 && nla->isMonomialSubset(m, n)) {
+ nla->registerMonomialSubset(m, n);
+ Trace("nl-alg-mindex-debug") << "...success" << std::endl;
+ } else if (cstatus >= 0 && nla->isMonomialSubset(n, m)) {
+ nla->registerMonomialSubset(n, m);
+ Trace("nl-alg-mindex-debug") << "...success (rev)" << std::endl;
+ }
+ }
+ }
+}
+
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
#include "theory/arith/partial_model.h"
#include "theory/arith/simplex.h"
#include "theory/arith/theory_arith.h"
+#include "theory/arith/nonlinear_extension.h"
#include "theory/ite_utilities.h"
#include "theory/quantifiers/bounded_integers.h"
#include "theory/rewriter.h"
namespace theory {
namespace arith {
+namespace attr {
+ struct ToIntegerTag { };
+ struct LinearIntDivTag { };
+}/* CVC4::theory::arith::attr namespace */
+
+/**
+ * This attribute maps the child of a to_int / is_int to the
+ * corresponding integer skolem.
+ */
+typedef expr::CDAttribute<attr::ToIntegerTag, Node> ToIntegerAttr;
+
+/**
+ * This attribute maps division-by-constant-k terms to a variable
+ * used to eliminate them.
+ */
+typedef expr::CDAttribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
+
static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
static double fRand(double fMin, double fMax);
static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
d_learner(u),
- d_quantEngine(NULL),
d_assertionsThatDoNotMatchTheirLiterals(c),
d_nextIntegerCheckVar(0),
d_constantIntegerVariables(c),
d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
-
+ d_nonlinearExtension( NULL ),
d_pass1SDP(NULL),
d_otherSDP(NULL),
d_lastContextIntegerAttempted(c,-1),
d_statistics()
{
srand(79);
+
+ if( options::nlAlg() ){
+ d_nonlinearExtension = new NonlinearExtension(
+ containing, d_congruenceManager.getEqualityEngine());
+ }
}
TheoryArithPrivate::~TheoryArithPrivate(){
if(d_treeLog != NULL){ delete d_treeLog; }
if(d_approxStats != NULL) { delete d_approxStats; }
+ if(d_nonlinearExtension != NULL) { delete d_nonlinearExtension; }
}
static bool contains(const ConstraintCPVec& v, ConstraintP con){
// return safeConstructNary(nb);
}
-void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_congruenceManager.setMasterEqualityEngine(eq);
+// Returns a skolem variable that is constrained to equal
+// division_total(num, den) in the current context. May add lemmas to out.
+static Node getSkolemConstrainedToDivisionTotal(
+ Node num, Node den, OutputChannel* out) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node total_div_node = nm->mkNode(kind::DIVISION_TOTAL, num, den);
+ Node total_div_skolem;
+ if(total_div_node.getAttribute(LinearIntDivAttr(), total_div_skolem)) {
+ return total_div_skolem;
+ }
+ total_div_skolem = nm->mkSkolem("DivisionTotalSkolem", nm->integerType(),
+ "the result of an intdiv-by-k term");
+ total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem);
+ Node zero = mkRationalNode(0);
+ Node lemma = den.eqNode(zero).iteNode(
+ total_div_skolem.eqNode(zero), num.eqNode(mkMult(total_div_skolem, den)));
+ out->lemma(lemma);
+ return total_div_skolem;
+}
+
+// Returns a skolem variable that is constrained to equal division(num, den) in
+// the current context. May add lemmas to out.
+static Node getSkolemConstrainedToDivision(
+ Node num, Node den, Node div0Func, OutputChannel* out) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node div_node = nm->mkNode(kind::DIVISION, num, den);
+ Node div_skolem;
+ if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) {
+ return div_skolem;
+ }
+ div_skolem = nm->mkSkolem("DivisionSkolem", nm->integerType(),
+ "the result of an intdiv-by-k term");
+ div_node.setAttribute(LinearIntDivAttr(), div_skolem);
+ Node div0 = nm->mkNode(APPLY_UF, div0Func, num);
+ Node total_div = getSkolemConstrainedToDivisionTotal(num, den, out);
+ out->lemma(mkOnZeroIte(den, div_skolem, div0, total_div));
+ return div_skolem;
+}
+
+
+// Integer division axioms:
+// These concenrate the high level constructs needed to constrain the functions:
+// div, mod, div_total and mod_total.
+//
+// The high level constraint.
+// (for all ((m Int) (n Int))
+// (=> (distinct n 0)
+// (let ((q (div m n)) (r (mod m n)))
+// (and (= m (+ (* n q) r))
+// (<= 0 r (- (abs n) 1))))))
+//
+// We now add division by 0 functions.
+// (for all ((m Int) (n Int))
+// (let ((q (div m n)) (r (mod m n)))
+// (ite (= n 0)
+// (and (= q (div_0_func m)) (= r (mod_0_func m)))
+// (and (= m (+ (* n q) r))
+// (<= 0 r (- (abs n) 1)))))))
+//
+// We now express div and mod in terms of div_total and mod_total.
+// (for all ((m Int) (n Int))
+// (let ((q (div m n)) (r (mod m n)))
+// (ite (= n 0)
+// (and (= q (div_0_func m)) (= r (mod_0_func m)))
+// (and (= q (div_total m n)) (= r (mod_total m n))))))
+//
+// Alternative div_total and mod_total without the abs function:
+// (for all ((m Int) (n Int))
+// (let ((q (div_total m n)) (r (mod_total m n)))
+// (ite (= n 0)
+// (and (= q 0) (= r 0))
+// (and (r = m - n * q)
+// (ite (> n 0)
+// (n*q <= m < n*q + n)
+// (n*q <= m < n*q - n))))))
+
+
+// Returns a formula that entails that q equals the total integer division of m
+// by n.
+// (for all ((m Int) (n Int))
+// (let ((q (div_total m n)))
+// (ite (= n 0)
+// (= q 0)
+// (ite (> n 0)
+// (n*q <= m < n*q + n)
+// (n*q <= m < n*q - n)))))
+Node mkAxiomForTotalIntDivision(Node m, Node n, Node q) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node zero = mkRationalNode(0);
+ // (n*q <= m < n*q + n) is equivalent to (0 <= m - n*q < n).
+ Node diff = nm->mkNode(kind::MINUS, m, mkMult(n, q));
+ Node when_n_is_positive = mkInRange(diff, zero, n);
+ Node when_n_is_negative = mkInRange(diff, zero, nm->mkNode(kind::UMINUS, n));
+ return n.eqNode(zero).iteNode(
+ q.eqNode(zero), nm->mkNode(kind::GT, n, zero)
+ .iteNode(when_n_is_positive, when_n_is_negative));
+}
+
+// Returns a formula that entails that r equals the integer division total of m
+// by n assuming q is equal to (div_total m n).
+// (for all ((m Int) (n Int))
+// (let ((q (div_total m n)) (r (mod_total m n)))
+// (ite (= n 0)
+// (= r 0)
+// (= r (- m (n * q))))))
+Node mkAxiomForTotalIntMod(Node m, Node n, Node q, Node r) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node diff = nm->mkNode(kind::MINUS, m, mkMult(n, q));
+ return mkOnZeroIte(n, r, mkRationalNode(0), diff);
+}
+
+// Returns an expression that constrains a term to be the result of the
+// [total] integer division of num by den. Equivalently:
+// (and (=> (den > 0) (den*term <= num < den*term + den))
+// (=> (den < 0) (den*term <= num < den*term - den))
+// (=> (den = 0) (term = 0)))
+// static Node mkIntegerDivisionConstraint(Node term, Node num, Node den) {
+// // We actually encode:
+// // (and (=> (den > 0) (0 <= num - den*term < den))
+// // (=> (den < 0) (0 <= num - den*term < -den))
+// // (=> (den = 0) (term = 0)))
+// NodeManager* nm = NodeManager::currentNM();
+// Node zero = nm->mkConst(Rational(0));
+// Node den_is_positive = nm->mkNode(kind::GT, den, zero);
+// Node den_is_negative = nm->mkNode(kind::LT, den, zero);
+// Node diff = nm->mkNode(kind::MINUS, num, mkMult(den, term));
+// Node when_den_positive = den_positive.impNode(mkInRange(diff, zero, den));
+// Node when_den_negative = den_negative.impNode(
+// mkInRange(diff, zero, nm->mkNode(kind::UMINUS, den)));
+// Node when_den_is_zero = (den.eqNode(zero)).impNode(term.eqNode(zero));
+// return mk->mkNode(kind::AND, when_den_positive, when_den_negative,
+// when_den_is_zero);
+// }
+
+// Returns a skolem variable that is constrained to equal
+// integer_division_total(num, den) in the current context. May add lemmas to
+// out.
+static Node getSkolemConstrainedToIntegerDivisionTotal(
+ Node num, Node den, OutputChannel* out) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node total_div_node = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
+ Node total_div_skolem;
+ if(total_div_node.getAttribute(LinearIntDivAttr(), total_div_skolem)) {
+ return total_div_skolem;
+ }
+ total_div_skolem = nm->mkSkolem("linearIntDiv", nm->integerType(),
+ "the result of an intdiv-by-k term");
+ total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem);
+ out->lemma(mkAxiomForTotalIntDivision(num, den, total_div_skolem));
+ return total_div_skolem;
+}
+
+// Returns a skolem variable that is constrained to equal
+// integer_division(num, den) in the current context. May add lemmas to out.
+static Node getSkolemConstrainedToIntegerDivision(
+ Node num, Node den, Node div0Func, OutputChannel* out) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node div_node = nm->mkNode(kind::INTS_DIVISION, num, den);
+ Node div_skolem;
+ if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) {
+ return div_skolem;
+ }
+ div_skolem = nm->mkSkolem("IntDivSkolem", nm->integerType(),
+ "the result of an intdiv-by-k term");
+ div_node.setAttribute(LinearIntDivAttr(), div_skolem);
+ Node div0 = nm->mkNode(APPLY_UF, div0Func, num);
+ Node total_div = getSkolemConstrainedToIntegerDivisionTotal(num, den, out);
+ out->lemma(mkOnZeroIte(den, div_skolem, div0, total_div));
+ return div_skolem;
+}
+
+// Returns a skolem variable that is constrained to equal
+// integer_modulus_total(num, den) in the current context. May add lemmas to
+// out.
+static Node getSkolemConstrainedToIntegerModulusTotal(
+ Node num, Node den, OutputChannel* out) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node total_mod_node = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
+ Node total_mod_skolem;
+ if(total_mod_node.getAttribute(LinearIntDivAttr(), total_mod_skolem)) {
+ return total_mod_skolem;
+ }
+ total_mod_skolem = nm->mkSkolem("IntModTotalSkolem", nm->integerType(),
+ "the result of an intdiv-by-k term");
+ total_mod_node.setAttribute(LinearIntDivAttr(), total_mod_skolem);
+ Node total_div = getSkolemConstrainedToIntegerDivisionTotal(num, den, out);
+ out->lemma(mkAxiomForTotalIntMod(num, den, total_div, total_mod_skolem));
+ return total_mod_skolem;
+}
+
+// Returns a skolem variable that is constrained to equal
+// integer_modulus(num, den) in the current context. May add lemmas to out.
+static Node getSkolemConstrainedToIntegerModulus(
+ Node num, Node den, Node mod0Func, OutputChannel* out) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node mod_node = nm->mkNode(kind::INTS_MODULUS, num, den);
+ Node mod_skolem;
+ if(mod_node.getAttribute(LinearIntDivAttr(), mod_skolem)) {
+ return mod_skolem;
+ }
+ mod_skolem = nm->mkSkolem("IntModSkolem", nm->integerType(),
+ "the result of an intdiv-by-k term");
+ mod_node.setAttribute(LinearIntDivAttr(), mod_skolem);
+ Node mod0 = nm->mkNode(APPLY_UF, mod0Func, num);
+ Node total_mod = getSkolemConstrainedToIntegerModulusTotal(num, den, out);
+ out->lemma(mkOnZeroIte(den, mod_skolem, mod0, total_mod));
+ return mod_skolem;
}
-void TheoryArithPrivate::setQuantifiersEngine(QuantifiersEngine* qe) {
- d_quantEngine = qe;
+void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_congruenceManager.setMasterEqualityEngine(eq);
}
Node TheoryArithPrivate::getRealDivideBy0Func(){
}
}
-namespace attr {
- struct ToIntegerTag { };
- struct LinearIntDivTag { };
-}/* CVC4::theory::arith::attr namespace */
-
-/**
- * This attribute maps the child of a to_int / is_int to the
- * corresponding integer skolem.
- */
-typedef expr::CDAttribute<attr::ToIntegerTag, Node> ToIntegerAttr;
-
-/**
- * This attribute maps division-by-constant-k terms to a variable
- * used to eliminate them.
- */
-typedef expr::CDAttribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
-
Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
if(Theory::theoryOf(n) != THEORY_ARITH) {
return n;
case kind::TO_INTEGER:
case kind::IS_INTEGER: {
- Node intVar;
- if(!n[0].getAttribute(ToIntegerAttr(), intVar)) {
- intVar = nm->mkSkolem("toInt", nm->integerType(), "a conversion of a Real term to its Integer part");
- n[0].setAttribute(ToIntegerAttr(), intVar);
- d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LT, nm->mkNode(kind::MINUS, n[0], nm->mkConst(Rational(1))), intVar), nm->mkNode(kind::LEQ, intVar, n[0])));
- }
- if(n.getKind() == kind::TO_INTEGER) {
- Node node = intVar;
- return node;
- } else {
- Node node = nm->mkNode(kind::EQUAL, n[0], intVar);
- return node;
- }
- Unreachable();
+ Node toIntSkolem;
+ if(!n[0].getAttribute(ToIntegerAttr(), toIntSkolem)) {
+ toIntSkolem = nm->mkSkolem("toInt", nm->integerType(),
+ "a conversion of a Real term to its Integer part");
+ n[0].setAttribute(ToIntegerAttr(), toIntSkolem);
+ // n[0] - 1 < toIntSkolem <= n[0]
+ // -1 < toIntSkolem - n[0] <= 0
+ // 0 <= n[0] - toIntSkolem < 1
+ Node one = mkRationalNode(1);
+ Node lem = mkAxiomForTotalIntDivision(n[0], one, toIntSkolem);
+ d_containing.d_out->lemma(lem);
+ }
+ if(k == kind::IS_INTEGER) {
+ return nm->mkNode(kind::EQUAL, n[0], toIntSkolem);
+ }
+ Assert(k == kind::TO_INTEGER);
+ return toIntSkolem;
}
-
+ case kind::INTS_MODULUS:
+ case kind::INTS_MODULUS_TOTAL:
case kind::INTS_DIVISION:
case kind::INTS_DIVISION_TOTAL: {
- if(!options::rewriteDivk()) {
- return n;
- }
- Node num = Rewriter::rewrite(n[0]);
Node den = Rewriter::rewrite(n[1]);
- if(den.isConst()) {
- const Rational& rat = den.getConst<Rational>();
- Assert(!num.isConst());
- if(rat != 0) {
- Node intVar;
- Node rw = nm->mkNode(k, num, den);
- if(!rw.getAttribute(LinearIntDivAttr(), intVar)) {
- intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
- rw.setAttribute(LinearIntDivAttr(), intVar);
- if(rat > 0) {
- d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))));
- } else {
- d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))));
- }
- }
- return intVar;
- }
- }
- break;
- }
-
- case kind::INTS_MODULUS:
- case kind::INTS_MODULUS_TOTAL: {
- if(!options::rewriteDivk()) {
+ if (!options::rewriteDivk() && den.isConst()) {
return n;
}
+ Node num = Rewriter::rewrite(n[0]);
+ if (k == kind::INTS_MODULUS) {
+ return getSkolemConstrainedToIntegerModulus(
+ num, den, getIntModulusBy0Func(), d_containing.d_out);
+ } else if (k == kind::INTS_MODULUS_TOTAL) {
+ return getSkolemConstrainedToIntegerModulusTotal(num, den,
+ d_containing.d_out);
+ } else if (k == kind::INTS_DIVISION) {
+ return getSkolemConstrainedToIntegerDivision(
+ num, den, getIntDivideBy0Func(), d_containing.d_out);
+ }
+ Assert(k == kind::INTS_DIVISION_TOTAL);
+ return getSkolemConstrainedToIntegerDivisionTotal(num, den,
+ d_containing.d_out);
+ }
+ case kind::DIVISION:
+ case kind::DIVISION_TOTAL: {
Node num = Rewriter::rewrite(n[0]);
Node den = Rewriter::rewrite(n[1]);
- if(den.isConst()) {
- const Rational& rat = den.getConst<Rational>();
- Assert(!num.isConst());
- if(rat != 0) {
- Node intVar;
- Node rw = nm->mkNode(k, num, den);
- if(!rw.getAttribute(LinearIntDivAttr(), intVar)) {
- intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
- rw.setAttribute(LinearIntDivAttr(), intVar);
- if(rat > 0) {
- d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))));
- } else {
- d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))));
- }
- }
- Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar));
- return node;
- }
+ Assert(!den.isConst());
+ if (k == kind::DIVISION) {
+ return getSkolemConstrainedToDivision(num, den, getRealDivideBy0Func(),
+ d_containing.d_out);
}
- break;
+ Assert(k == kind::DIVISION_TOTAL);
+ return getSkolemConstrainedToDivisionTotal(num, den, d_containing.d_out);
}
default:
- ;
+ break;
}
for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) {
throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
}
- setIncomplete();
- d_nlIncomplete = true;
+ if( !options::nlAlg() ){
+ setIncomplete();
+ d_nlIncomplete = true;
+ }
++(d_statistics.d_statUserVariables);
requestArithVar(vlNode, false, false);
// (DIVISION n d)
// (ite (= d 0)
// (APPLY [div_0_skolem_function] n)
- // (DIVISION_TOTAL x y))))
+ // (DIVISION_TOTAL n d))))
Polynomial n = Polynomial::parsePolynomial(divLike[0]);
Polynomial d = Polynomial::parsePolynomial(divLike[1]);
Kind k = int_div_like.getKind();
Assert(k == INTS_DIVISION_TOTAL || k == INTS_MODULUS_TOTAL);
- // (for all ((m Int) (n Int))
- // (=> (distinct n 0)
- // (let ((q (div m n)) (r (mod m n)))
- // (and (= m (+ (* n q) r))
- // (<= 0 r (- (abs n) 1))))))
-
- // Updated for div 0 functions
- // (for all ((m Int) (n Int))
- // (let ((q (div m n)) (r (mod m n)))
- // (ite (= n 0)
- // (and (= q (div_0_func m)) (= r (mod_0_func m)))
- // (and (= m (+ (* n q) r))
- // (<= 0 r (- (abs n) 1)))))))
+ // See the discussion of integer division axioms above.
Polynomial n = Polynomial::parsePolynomial(int_div_like[0]);
Polynomial d = Polynomial::parsePolynomial(int_div_like[1]);
void TheoryArithPrivate::preRegisterTerm(TNode n) {
Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
+
+ if( options::nlAlg() ){
+ d_containing.getExtTheory()->registerTermRec( n );
+ }
try {
if(isRelationOperator(n.getKind())){
void TheoryArithPrivate::check(Theory::Effort effortLevel){
Assert(d_currentPropagationList.empty());
- if(done() && !Theory::fullEffort(effortLevel) && ( d_qflraStatus == Result::SAT) ){
+ if(done() && effortLevel < Theory::EFFORT_FULL && ( d_qflraStatus == Result::SAT) ){
+ return;
+ }
+
+ if(effortLevel == Theory::EFFORT_LAST_CALL){
+ if( options::nlAlg() ){
+ d_nonlinearExtension->check( effortLevel );
+ }
return;
}
}
}
}//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
+
+ if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){
+ if( options::nlAlg() ){
+ d_nonlinearExtension->check( effortLevel );
+ }
+ }
+
if(Theory::fullEffort(effortLevel) && d_nlIncomplete){
// TODO this is total paranoia
setIncomplete();
}
}
-
+bool TheoryArithPrivate::needsCheckLastEffort() {
+ if( options::nlAlg() ){
+ return d_nonlinearExtension->needsCheckLastEffort();
+ }else{
+ return false;
+ }
+}
Node TheoryArithPrivate::explain(TNode n) {
}
}
+bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
+ if( options::nlAlg() ){
+ return d_nonlinearExtension->getCurrentSubstitution( effort, vars, subs, exp );
+ }else{
+ return false;
+ }
+}
+
+bool TheoryArithPrivate::isExtfReduced(int effort, Node n, Node on,
+ std::vector<Node>& exp) {
+ if (options::nlAlg()) {
+ std::pair<bool, Node> reduced =
+ d_nonlinearExtension->isExtfReduced(effort, n, on, exp);
+ if (!reduced.second.isNull()) {
+ exp.clear();
+ exp.push_back(reduced.second);
+ }
+ return reduced.first;
+ } else {
+ return false; // d_containing.isExtfReduced( effort, n, on );
+ }
+}
void TheoryArithPrivate::propagate(Theory::Effort e) {
// This uses model values for safety. Disable for now.
return value;
}
- case kind::MULT: { // 2+ args
+ case kind::MULT:
+ case kind::NONLINEAR_MULT: { // 2+ args
DeltaRational value(1);
unsigned variableParts = 0;
for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
projects / cvc5.git / commitdiff