mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix in m_cg_table.find()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-25 17:50:06 -07:00
parent 8303d8c9ae
commit bdabd52fb9
3 changed files with 17 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/util/lp/emonomials.cpp
View file

@ -134,26 +134,13 @@ namespace nla {
monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
SASSERT(m_ve.is_root(vars));
// find a unique key for dummy monomial
lpvar v = m_var2index.size();
for (unsigned i = 0; i < m_var2index.size(); ++i) {
if (m_var2index[i] == UINT_MAX) {
v = i;
break;
}
}
unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, vars, idx));
m_var2index.setx(v, idx, UINT_MAX);
do_canonize(m_monomials[idx]);
m_find_key = vars;
std::sort(m_find_key.begin(), m_find_key.end());
monomial const* result = nullptr;
lpvar w;
if (m_cg_table.find(v, w)) {
SASSERT(w != v);
lpvar w;
if (m_cg_table.find(UINT_MAX, w)) {
result = &m_monomials[m_var2index[w]];
}
m_var2index[v] = UINT_MAX;
m_monomials.pop_back();
return result;
}

8
src/util/lp/emonomials.h
View file

@ -28,7 +28,7 @@
namespace nla {
class emonomials : public var_eqs_merge_handler {
mutable svector<lpvar> m_find_key;
/**
\brief singly-lined cyclic list of monomial indices where variable occurs.
Each variable points to the head and tail of the cyclic list.
@ -52,7 +52,7 @@ class emonomials : public var_eqs_merge_handler {
hash_canonical(emonomials& em): em(em) {}
unsigned operator()(lpvar v) const {
auto const& vec = em.m_monomials[em.m_var2index[v]].rvars();
auto const& vec = v != UINT_MAX? em.m_monomials[em.m_var2index[v]].rvars() : em.m_find_key;
return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
}
};
@ -67,8 +67,8 @@ class emonomials : public var_eqs_merge_handler {
emonomials& em;
eq_canonical(emonomials& em): em(em) {}
bool operator()(lpvar u, lpvar v) const {
auto const& uvec = em.m_monomials[em.m_var2index[u]].rvars();
auto const& vvec = em.m_monomials[em.m_var2index[v]].rvars();
auto const& uvec = u != UINT_MAX? em.m_monomials[em.m_var2index[u]].rvars(): em.m_find_key;
auto const& vvec = v != UINT_MAX? em.m_monomials[em.m_var2index[v]].rvars(): em.m_find_key;
return uvec == vvec;
}
};

11
src/util/lp/nla_order_lemmas.cpp
View file

@ -96,9 +96,12 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
// We look for monomials e = m.rvars()[k]*d and see if we can create an order lemma for m and e
void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) {
SASSERT(m.size() == 2);
TRACE("nla_solver", tout << "m = " << pp_rmon(c(), m););
SASSERT(m.size() == 2);
lpvar c = m.vars()[k];
for (monomial const& m2 : _().m_emons.get_products_of(c)) {
TRACE("nla_solver", tout << "m2 = " << pp_rmon(_(), m2););
order_lemma_on_factor_binomial_rm(m, k, m2);
if (done()) {
break;
@ -109,7 +112,11 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) {
// ac is a binomial
// create order lemma on monomials bd where d is equivalent to ac[k]
void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) {
TRACE("nla_solver", tout << "bd=" << pp_rmon(_(), bd) << "\n";);
TRACE("nla_solver",
tout << "ac=" << pp_rmon(_(), ac) << "\n";
tout << "k=" << k << "\n";
tout << "bd=" << pp_rmon(_(), bd) << "\n";
);
factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
factor b;
if (c().divide(bd, d, b)) {