From 403743cb30a07a99ef035f647993229b2960d9d6 Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 25 Jan 2019 17:50:04 -0800 Subject: [PATCH] switch to constraint based sign lemma Signed-off-by: Lev --- src/util/lp/equiv_monomials.h | 28 +++++----- src/util/lp/nla_solver.cpp | 62 ++++------------------ src/util/lp/vars_equivalence.h | 97 +++++++++++++++++++++++++++------- 3 files changed, 102 insertions(+), 85 deletions(-) diff --git a/src/util/lp/equiv_monomials.h b/src/util/lp/equiv_monomials.h index 5016222d7..24eb280d0 100644 --- a/src/util/lp/equiv_monomials.h +++ b/src/util/lp/equiv_monomials.h @@ -20,22 +20,22 @@ namespace nla { struct const_iterator_equiv_mon { // fields - const vector& m_same_abs_vals; + const vector& m_eq_vars; vector m_its; bool m_done; std::function m_find_monomial; // constructor for begin() - const_iterator_equiv_mon(const vector& abs_vals, + const_iterator_equiv_mon(const vector& abs_vals, std::function find_monomial) - : m_same_abs_vals(abs_vals), + : m_eq_vars(abs_vals), m_done(false), m_find_monomial(find_monomial) { - for (auto it: abs_vals){ - m_its.push_back(it->begin()); + for (auto& vars: abs_vals){ + m_its.push_back(vars.begin()); } } // constructor for end() - const_iterator_equiv_mon(const vector& abs_vals) : m_same_abs_vals(abs_vals), m_done(true) {} + const_iterator_equiv_mon(const vector& does_not_matter) : m_eq_vars(does_not_matter), m_done(true) {} //typedefs typedef const_iterator_equiv_mon self_type; @@ -51,7 +51,7 @@ struct const_iterator_equiv_mon { for (; k < m_its.size(); k++) { auto & it = m_its[k]; it++; - const auto & evars = *(m_same_abs_vals[k]); + const auto & evars = m_eq_vars[k]; if (it == evars.end()) { it = evars.begin(); } else { @@ -85,22 +85,22 @@ struct const_iterator_equiv_mon { struct equiv_monomials { const monomial & m_mon; - std::function m_abs_eq_vars; + std::function m_eq_vars; std::function m_find_monomial; - vector m_vars_eqs; + vector m_vars_eqs; equiv_monomials(const monomial & m, - std::function abs_eq_vars, + std::function eq_vars, std::function find_monomial) : m_mon(m), - m_abs_eq_vars(abs_eq_vars), + m_eq_vars(eq_vars), m_find_monomial(find_monomial), m_vars_eqs(vars_eqs()) {} - vector vars_eqs() const { - vector r; + vector vars_eqs() const { + vector r; for(lpvar j : m_mon.vars()) { - r.push_back(m_abs_eq_vars(j)); + r.push_back(m_eq_vars(j)); } return r; } diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 8e78e0c3e..784897bbf 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -546,54 +546,15 @@ struct solver::imp { // the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign // but it is not the case in the model - void generate_sign_lemma(const vector& abs_vals, const monomial& m, const monomial& n, const rational& sign) { + void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) { add_empty_lemma_and_explanation(); TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); tout << "n = "; print_monomial_with_vars(n, tout); - tout << "abs_vals="; print_vector(abs_vals, tout); ); - std::unordered_map> map; - for (const rational& v : abs_vals) { - map[v] = vector(); - } - - for (unsigned j : m) { - rational v = vvr(j); - int s; - if (v.is_pos()) { - s = 1; - } else { - s = -1; - v = -v; - }; - // v = abs(vvr(j)) - auto it = map.find(v); - SASSERT(it != map.end()); - it->second.push_back(index_with_sign(j, rational(s))); - } - - for (unsigned j : n) { - rational v = vvr(j); - rational s; - if (v.is_pos()) { - s = rational(1); - } else { - s = -rational(1); - v = -v; - }; - // v = abs(vvr(j)) - auto it = map.find(v); - SASSERT(it != map.end()); - index_with_sign & ins = it->second.back(); - if (j != ins.m_i) { - s *= ins.m_sign; - mk_ineq(j, -s, ins.m_i, llc::NE, m_lemma_vec->back()); - } - it->second.pop_back(); - } - - mk_ineq(m.var(), -sign, n.var(), llc::EQ, current_lemma()); + mk_ineq(m.var(), -sign, n.var(), llc::EQ, current_lemma()); + explain(m, current_expl()); + explain(n, current_expl()); TRACE("nla_solver", print_lemma(current_lemma(), tout);); } @@ -661,21 +622,15 @@ struct solver::imp { return vvr(m) != sign * vvr(n) ; } - vector abs_vals(const monomial& m) const { - vector r; - for(unsigned j : m){ - r.push_back(abs(vvr(j))); - } - return r; + unsigned_vector eq_vars(lpvar j) const { + return m_vars_equivalence.eq_vars(j); } - - bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n) { TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); tout << "n= "; print_monomial_with_vars(n, tout); ); rational sign; if (sign_contradiction(m, n, sign)) { - generate_sign_lemma(abs_vals(m) ,m, n, sign); + generate_sign_lemma(m, n, sign); return true; } return false; @@ -685,7 +640,7 @@ struct solver::imp { TRACE("nla_solver", tout << "i = " << i << ", mon = "; print_monomial_with_vars(m_monomials[i], tout);); const monomial& m = m_monomials[i]; - for (unsigned n : equiv_monomials(m, [this](lpvar j) {return &abs_eq_vars(j);}, + for (unsigned n : equiv_monomials(m, [this](lpvar j) {return eq_vars(j);}, [this](const unsigned_vector& key) {return find_monomial(key);}) ) { if (n == static_cast(-1) || n == i) continue; @@ -1727,6 +1682,7 @@ struct solver::imp { // not a strict version void generate_monl(const rooted_mon& a, const rooted_mon& b) { + add_empty_lemma_and_explanation(); auto akey = get_sorted_key_with_vars(a); auto bkey = get_sorted_key_with_vars(b); SASSERT(akey.size() == bkey.size()); diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h index 250debf1e..c70cd0880 100644 --- a/src/util/lp/vars_equivalence.h +++ b/src/util/lp/vars_equivalence.h @@ -50,12 +50,17 @@ struct vars_equivalence { } }; + struct node { + unsigned m_parent; // points to m_equivs + svector m_children; // point to m_equivs + node() : m_parent(-1) {} + }; //fields - // The map from the variables to m_equivs indices + // The map from the variables to m_nodes // m_tree is a spanning tree of the graph of equivs represented by m_equivs - std::unordered_map m_tree; + std::unordered_map m_tree; // If m_tree[v] == -1 then the variable is a root. // if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v vector m_equivs; // all equivalences extracted from constraints @@ -79,6 +84,52 @@ struct vars_equivalence { return it->second; } + // j itself is also included + svector eq_vars(lpvar j) const { + svector r = path_to_root(j); + svector ch = children(j); + for (lpvar k : ch) { + r.push_back(k); + } + r.push_back(j); + return r; + } + + svector children(lpvar j) const { + svector r; + auto it = m_tree.find(j); + if (it == m_tree.end()) + return r; + + const node& n = it->second; + for (unsigned e_k: n.m_children) { + const equiv & e = m_equivs[e_k]; + lpvar oj = e.m_i == j? e.m_j : e.m_i; + r.push_back(oj); + for (lpvar k : children(oj)) { + r.push_back(k); + } + } + return r; + } + + + + svector path_to_root(lpvar j) const { + svector r; + while (true) { + auto it = m_tree.find(j); + if (it == m_tree.end() || it->second.m_parent == static_cast(-1)) + return r; + + const equiv & e = m_equivs[it->second.m_parent]; + j = get_parent_node(j, e); + r.push_back(j); + } + SASSERT(false); + } + + unsigned size() const { return static_cast(m_tree.size()); } // we create a spanning tree on all variables participating in an equivalence @@ -92,27 +143,37 @@ struct vars_equivalence { } void connect_equiv_to_tree(unsigned k) { - // m_tree is a spanning tree of the graph of m_equivs + // m_tree is the tree with the edges formed by m_equivs const equiv &e = m_equivs[k]; TRACE("nla_vars_eq", tout << "m_i = " << e.m_i << ", " << "m_j = " << e.m_j ;); - bool i_is_in = m_tree.find(e.m_i) != m_tree.end(); - bool j_is_in = m_tree.find(e.m_j) != m_tree.end(); + auto it_i = m_tree.find(e.m_i); + auto it_j = m_tree.find(e.m_j); + bool i_is_in = it_i != m_tree.end(); + bool j_is_in = it_j != m_tree.end(); if (!(i_is_in || j_is_in)) { // none of the edge vertices is in the tree // let m_i be the parent, and m_j be the child TRACE("nla_vars_eq", tout << "create nodes for " << e.m_i << " and " << e.m_j; ); - m_tree.emplace(e.m_i, -1); - m_tree.emplace(e.m_j, k); + node parent; + node child; + child.m_parent = k; + parent.m_children.push_back(k); + m_tree.emplace(e.m_i, parent); + m_tree.emplace(e.m_j, child); } else if (i_is_in && (!j_is_in)) { // create a node for m_j, with m_i is the parent + node child; + child.m_parent = k; TRACE("nla_vars_eq", tout << "create a node for " << e.m_j; ); - m_tree.emplace(e.m_j, k); - // if m_i is a root here we can set its parent m_j + m_tree.emplace(e.m_j, child); + it_i->second.m_children.push_back(k); } else if ((!i_is_in) && j_is_in) { TRACE("nla_vars_eq", tout << "create a node for " << e.m_i; ); - m_tree.emplace(e.m_i, k); - // if m_j is a root here we can set its parent to m_i + node child; + child.m_parent = k; + m_tree.emplace(e.m_i, child); + it_j->second.m_children.push_back(k); } else { TRACE("nla_vars_eq", tout << "both vertices are in the tree";); } @@ -127,7 +188,7 @@ struct vars_equivalence { if (it == m_tree.end()) return true; - return it->second == static_cast(-1); + return it->second.m_parent == static_cast(-1); } static unsigned get_parent_node(unsigned j, const equiv& e) { @@ -143,11 +204,11 @@ struct vars_equivalence { auto it = m_tree.find(j); if (it == m_tree.end()) return j; - if (it->second == static_cast(-1)) { + if (it->second.m_parent == static_cast(-1)) { TRACE("nla_vars_eq", tout << "mapped to " << j << "\n";); return j; } - const equiv & e = m_equivs[it->second]; + const equiv & e = m_equivs[it->second.m_parent]; sign *= e.m_sign; j = get_parent_node(j, e); } @@ -160,9 +221,9 @@ struct vars_equivalence { auto it = m_tree.find(j); if (it == m_tree.end()) return j; - if (it->second == static_cast(-1)) + if (it->second.m_parent == static_cast(-1)) return j; - const equiv & e = m_equivs[it->second]; + const equiv & e = m_equivs[it->second.m_parent]; j = get_parent_node(j, e); } } @@ -178,9 +239,9 @@ struct vars_equivalence { auto it = m_tree.find(j); if (it == m_tree.end()) return; - if (it->second == static_cast(-1)) + if (it->second.m_parent == static_cast(-1)) return; - const equiv & e = m_equivs[it->second]; + const equiv & e = m_equivs[it->second.m_parent]; exp.add(e.m_c0); exp.add(e.m_c1); j = get_parent_node(j, e);