mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

work on order lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-14 11:55:35 -08:00 • committed by Lev Nachmanson
parent f926ec7f4a
commit d63c051d20
2 changed files with 32 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -756,6 +756,9 @@ struct solver::imp {
m_vars_equivalence.clear();
collect_equivs();
m_vars_equivalence.create_tree();
for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
m_vars_equivalence.register_var(j, vvr(j));
}
}
void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i) {
@ -873,7 +876,9 @@ struct solver::imp {
bool order_lemma_on_factor(unsigned i_mon, const factorization& f, unsigned k, int sign) {
lpvar j = f[k];
for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j)) {
TRACE("nla_solver", tout << "k = " << k << ", j = " << j; );
for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j, [this](unsigned h) {return vvr(h);})) {
TRACE("nla_solver", tout << "p.var() = " << p.var() << ", p.sign() = " << p.sign(); );
if (order_lemma_on_factor_and_equiv(p.m_i, i_mon, f, k, sign * p.m_sign)) {
return true;
}
@ -888,7 +893,7 @@ struct solver::imp {
if (v.is_zero())
continue;
int sign = ((v.is_pos() && f.sign().is_pos()) || (v.is_neg() && f.sign().is_neg()))? 1 : -1;
int sign = (v.is_pos() == f.sign().is_pos())? 1 : -1;
if (order_lemma_on_factor(i_mon, f, k, sign)) {
return true;

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

@ -72,35 +72,32 @@ struct vars_equivalence {
};
//fields
// The map from the variables to m_equivs indices
// 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, unsigned> 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), that k is the parent of v
vector<equiv> m_equivs; // all equivalences extracted from constraints
vector<equiv> m_equivs; // all equivalences extracted from constraints
std::unordered_map<rational,unsigned_vector> m_vars_by_abs_values;
void clear() {
m_equivs.clear();
m_tree.clear();
}
// it also returns (j, 1)
vector<index_with_sign> get_equivalent_vars(lpvar j) const {
// it is just a place holder, see if we need something more substantial
vector<index_with_sign> get_equivalent_vars(lpvar j, std::function<rational(lpvar)> vvr) const {
vector<index_with_sign> ret;
ret.push_back(index_with_sign(j, rational(1)));
rational val = vvr(j);
for (lpvar j : m_vars_by_abs_values.find(abs(val))->second) {
if (val.is_pos())
ret.push_back(index_with_sign(j, rational(1)));
else
ret.push_back(index_with_sign(j, rational(-1)));
}
return ret;
/*
vector<index_with_sign> ret;
std::unordered_set<unsigned> returned;
std::unordered_set<unsigned> processed;
ret.push_back(std::make_pair(j, 1));
returned.insert(j);
processed.insert(j);
std::queue<unsigned> q;
q.enqueue(j);
*/
}
unsigned size() const { return static_cast<unsigned>(m_tree.size()); }
@ -194,5 +191,16 @@ struct vars_equivalence {
add_equiv_exp(j, exp);
}
void register_var(unsigned j, const rational& val) {
rational v = abs(val);
auto it = m_vars_by_abs_values.find(v);
if (it == m_vars_by_abs_values.end()) {
unsigned_vector uv;
uv.push_back(j);
m_vars_by_abs_values[val] = uv;
} else {
it->second.push_back(j);
}
}
}; // end of vars_equivalence
}