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

introduce mon_to_rooted_mon

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-12-28 13:14:15 +05:30
parent 14a8612779
commit abbf8c587b
1 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -587,22 +587,23 @@ struct solver::imp {
return false;
}
const rooted_mon& mon_to_rooted_mon(const monomial& m) const {
monomial_coeff mc = canonize_monomial(m);
TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout);
tout << "mc = "; print_product_with_vars(mc.vars(), tout););
auto rit = m_rm_table.map().find(mc.vars());
SASSERT(rit != m_rm_table.map().end());
unsigned rm_i = rit->second.m_i;
return m_rm_table.vec()[rm_i];
}
bool basic_sign_lemma_on_a_var_bucket_of_abs_vals(const rational& v, const unsigned_vector& vars ) {
for(unsigned j : vars) {
auto it = m_var_to_its_monomial.find(j);
if (it == m_var_to_its_monomial.end()) {
continue;
}
unsigned i = it->second;
const monomial& m = m_monomials[i];
monomial_coeff mc = canonize_monomial(m);
TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout);
tout << "mc = "; print_product_with_vars(mc.vars(), tout););
auto rit = m_rm_table.map().find(mc.vars());
SASSERT(rit != m_rm_table.map().end());
unsigned rm_i = rit->second.m_i;
const rooted_mon& rm = m_rm_table.vec()[rm_i];
if (it == m_var_to_its_monomial.end()) continue;
const monomial& m = m_monomials[it->second];
const rooted_mon& rm = mon_to_rooted_mon(m);
unsigned rm_j = var(rm);
if (rm_j == j) continue;
if (abs(vvr(rm_j)) != v) {