mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 06:39:02 +00:00
Code Activity

toward order_lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-12 10:45:24 -08:00 committed by Lev Nachmanson
parent 23a7e5e302
commit 9dbb56fdfc
2 changed files with 58 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -30,15 +30,7 @@ struct solver::imp {
typedef lp::lar_base_constraint lpcon;
struct index_with_sign {
unsigned m_i; // the monomial index
rational m_sign; // the monomial sign: -1 or 1
index_with_sign(unsigned i, rational sign) : m_i(i), m_sign(sign) {}
index_with_sign() {}
bool operator==(const index_with_sign& b) {
return m_i == b.m_i && m_sign == b.m_sign;
}
};
//fields
vars_equivalence m_vars_equivalence;
@ -839,8 +831,30 @@ struct solver::imp {
m_expl->clear();
m_lemma->clear();
}
bool order_lemma_on_factor_equiv_and_other_mon(unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
NOT_IMPLEMENTED_YET();
return false;
}
// here e_j is equivalent to f[k],
// f is a factorization of m_monomials[i_mon]
bool order_lemma_on_factor_and_equiv(unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
lpvar j = f[k];
for (unsigned i : m_monomials_containing_var[j]) {
if (order_lemma_on_factor_equiv_and_other_mon(i, e_j, i_mon, f, k, sign)) {
return true;
}
}
return false;
}
bool order_lemma_on_factor(const factorization& f, unsigned k, int sign) {
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)) {
if (order_lemma_on_factor_and_equiv(p.m_i, i_mon, f, k, sign * p.m_sign)) {
return true;
}
}
return false;
}
@ -852,12 +866,13 @@ struct solver::imp {
int sign = ((v.is_pos() && f.sign().is_pos()) || (v.is_neg() && f.sign().is_neg()))? 1 : -1;
if (order_lemma_on_factor(f, k, sign)) {
if (order_lemma_on_factor(i_mon, f, k, sign)) {
return true;
}
}
return false;
}
bool order_lemma_on_monomial(unsigned i_mon) {
for (auto factorization : factorization_factory_imp(i_mon, *this)) {
if (factorization.is_empty())
@ -910,8 +925,8 @@ struct solver::imp {
m_expl = &exp;
m_lemma = &l;
if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL) {
TRACE("nla_solver", tout << "unknown\n";);
if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << lp_status_to_string(m_lar_solver.get_status()) << "\n";);
return l_undef;
}

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

@ -28,6 +28,15 @@ struct hash_svector {
}
};
struct index_with_sign {
unsigned m_i; // the index
rational m_sign; // the sign: -1 or 1
index_with_sign(unsigned i, rational sign) : m_i(i), m_sign(sign) {}
index_with_sign() {}
bool operator==(const index_with_sign& b) {
return m_i == b.m_i && m_sign == b.m_sign;
}
};
struct rat_hash {
typedef rational data;
@ -60,6 +69,8 @@ struct vars_equivalence {
}
};
// 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;
@ -70,6 +81,25 @@ struct vars_equivalence {
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> ret;
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()); }