mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

access by indeq from regular monomials to rooted

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2019-01-29 11:29:24 -08:00 committed by Lev Nachmanson
parent 5599dc984c
commit 7c074dc65c
2 changed files with 16 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -652,22 +652,6 @@ struct solver::imp {
return false;
}
const rooted_mon& mon_to_rooted_mon(const svector<lpvar>& vars) const {
auto rit = m_rm_table.map().find(vars);
SASSERT(rit != m_rm_table.map().end());
unsigned rm_i = rit->second;
return m_rm_table.vec()[rm_i];
}
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););
return mon_to_rooted_mon(mc.vars());
}
/**
* \brief <generate lemma by using the fact that -ab = (-a)b) and
-ab = a(-b)
@ -1457,13 +1441,8 @@ struct solver::imp {
const monomial& m = m_monomials[it->second];
SASSERT(m.var() == i);
SASSERT(abs(vvr(m)) == abs(vvr(c)));
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 it = m_rm_table.map().find(mc.vars());
SASSERT(it != m_rm_table.map().end());
i = it->second;
const index_with_sign & i_s = m_rm_table.get_rooted_mon(it->second);
i = i_s.index();
// SASSERT(abs(vvr(m_rm_table.vec()[i])) == abs(vvr(c)));
if (!contains(found_rm, i)) {
found_rm.insert(i);
@ -2436,7 +2415,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
s.set_column_value(lp_a, rational(1));
s.set_column_value(lp_b, rational(1));
s.set_column_value(lp_c, rational(1));
s.set_column_value(lp_e, rational(1));
s.set_column_value(lp_d, rational(1));
s.set_column_value(lp_e, rational(1));
s.set_column_value(lp_abcde, rational(1));
s.set_column_value(lp_ac, rational(1));

14
src/util/lp/rooted_mons.h
View file

@ -70,7 +70,10 @@ struct rooted_mon_table {
// such that for every i and every h in m_proper_factors[i] we have m_vector[i] as a proper factor of m_vector[h]
std::unordered_map<unsigned, std::unordered_set<unsigned>> m_proper_factors;
// points to m_vector
svector<unsigned> m_to_refine;
svector<unsigned> m_to_refine;
// maps the indices of the regular monomials to the rooted monomial indices
std::unordered_map<unsigned, index_with_sign> m_reg_to_rm;
const svector<unsigned>& to_refine() { return m_to_refine; }
@ -105,6 +108,7 @@ struct rooted_mon_table {
m_mons_containing_var.clear();
m_proper_factors.clear();
m_to_refine.clear();
m_reg_to_rm.clear();
}
const vector<rooted_mon>& vec() const { return m_vector; }
@ -200,16 +204,24 @@ struct rooted_mon_table {
void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i_mon) {
index_with_sign ms(i_mon, mc.coeff());
SASSERT(abs(mc.coeff()) == rational(1));
auto it = map().find(mc.vars());
if (it == map().end()) {
TRACE("nla_solver", tout << "size = " << vec().size(););
map().emplace(mc.vars(), vec().size());
m_reg_to_rm.emplace(i_mon, index_with_sign(vec().size(), mc.coeff()));
vec().push_back(rooted_mon(mc.vars(), i_mon, mc.coeff()));
}
else {
vec()[it->second].push_back(ms);
TRACE("nla_solver", tout << "add ms.m_i = " << ms.m_i;);
m_reg_to_rm.emplace(i_mon, index_with_sign(it->second, mc.coeff()));
}
}
const index_with_sign& get_rooted_mon(unsigned i_mon) const {
return m_reg_to_rm.find(i_mon)->second;
}
};
}