mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

switch to constraint based sign lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2019-01-25 17:50:04 -08:00 • committed by Lev Nachmanson
parent 3441f565b2
commit 403743cb30
3 changed files with 102 additions and 85 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/util/lp/equiv_monomials.h
View file

@ -20,22 +20,22 @@
namespace nla {
struct const_iterator_equiv_mon {
// fields
const vector<const unsigned_vector*>& m_same_abs_vals;
const vector<unsigned_vector>& m_eq_vars;
vector<unsigned_vector::const_iterator> m_its;
bool m_done;
std::function<unsigned (const unsigned_vector&)> m_find_monomial;
// constructor for begin()
const_iterator_equiv_mon(const vector<const unsigned_vector*>& abs_vals,
const_iterator_equiv_mon(const vector<unsigned_vector>& abs_vals,
std::function<unsigned (const unsigned_vector&)> 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<const unsigned_vector*>& abs_vals) : m_same_abs_vals(abs_vals), m_done(true) {}
const_iterator_equiv_mon(const vector<unsigned_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<const unsigned_vector*(lpvar)> m_abs_eq_vars;
std::function<unsigned_vector (lpvar)> m_eq_vars;
std::function<unsigned (const unsigned_vector&)> m_find_monomial;
vector<const unsigned_vector*> m_vars_eqs;
vector<unsigned_vector> m_vars_eqs;
equiv_monomials(const monomial & m,
std::function<const unsigned_vector*(lpvar)> abs_eq_vars,
std::function<unsigned_vector (lpvar)> eq_vars,
std::function<unsigned (const unsigned_vector&)> 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<const unsigned_vector*> vars_eqs() const {
vector<const unsigned_vector*> r;
vector<unsigned_vector> vars_eqs() const {
vector<unsigned_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;
}

62
src/util/lp/nla_solver.cpp
View file

@ -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<rational>& 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<rational, vector<index_with_sign>> map;
for (const rational& v : abs_vals) {
map[v] = vector<index_with_sign>();
}
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<rational> abs_vals(const monomial& m) const {
vector<rational> 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<unsigned>(-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());

97
src/util/lp/vars_equivalence.h
View file

@ -50,12 +50,17 @@ struct vars_equivalence {
}
};
struct node {
unsigned m_parent; // points to m_equivs
svector<unsigned> 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<unsigned, unsigned> m_tree;
std::unordered_map<unsigned, node> 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<equiv> m_equivs; // all equivalences extracted from constraints
@ -79,6 +84,52 @@ struct vars_equivalence {
return it->second;
}
// j itself is also included
svector<lpvar> eq_vars(lpvar j) const {
svector<lpvar> r = path_to_root(j);
svector<lpvar> ch = children(j);
for (lpvar k : ch) {
r.push_back(k);
}
r.push_back(j);
return r;
}
svector<lpvar> children(lpvar j) const {
svector<lpvar> 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<lpvar> path_to_root(lpvar j) const {
svector<lpvar> r;
while (true) {
auto it = m_tree.find(j);
if (it == m_tree.end() || it->second.m_parent == static_cast<unsigned>(-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<unsigned>(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<unsigned>(-1);
return it->second.m_parent == static_cast<unsigned>(-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<unsigned>(-1)) {
if (it->second.m_parent == static_cast<unsigned>(-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<unsigned>(-1))
if (it->second.m_parent == static_cast<unsigned>(-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<unsigned>(-1))
if (it->second.m_parent == static_cast<unsigned>(-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);