mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 05:00:51 +00:00
Code Activity

renaming the smon fields to distingush them from monomial fields

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-21 14:19:17 -07:00
parent 7eeba3a917
commit e73296fbe5
4 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -47,9 +47,9 @@ public:
unsigned& prev() { return m_prev; } unsigned& prev() { return m_prev; }
unsigned visited() const { return m_visited; } unsigned visited() const { return m_visited; }
unsigned& visited() { return m_visited; } unsigned& visited() { return m_visited; }
svector<lpvar> const& vars() const { return m_rvars; } svector<lpvar> const& rvars() const { return m_rvars; }
svector<lp::var_index>::const_iterator begin() const { return vars().begin(); } svector<lp::var_index>::const_iterator begin() const { return rvars().begin(); }
svector<lp::var_index>::const_iterator end() const { return vars().end(); } svector<lp::var_index>::const_iterator end() const { return rvars().end(); }
unsigned size() const { return m_rvars.size(); } unsigned size() const { return m_rvars.size(); }
lpvar operator[](unsigned i) const { return m_rvars[i]; } lpvar operator[](unsigned i) const { return m_rvars[i]; }
bool sign() const { return m_rsign; } bool sign() const { return m_rsign; }
@ -97,7 +97,7 @@ class emonomials : public var_eqs_merge_handler {
hash_canonical(emonomials& em): em(em) {} hash_canonical(emonomials& em): em(em) {}
unsigned operator()(lpvar v) const { unsigned operator()(lpvar v) const {
auto const& vec = em.m_canonized[em.m_var2index[v]].vars(); auto const& vec = em.m_canonized[em.m_var2index[v]].rvars();
return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10); return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
} }
}; };
@ -112,8 +112,8 @@ class emonomials : public var_eqs_merge_handler {
emonomials& em; emonomials& em;
eq_canonical(emonomials& em): em(em) {} eq_canonical(emonomials& em): em(em) {}
bool operator()(lpvar u, lpvar v) const { bool operator()(lpvar u, lpvar v) const {
auto const& uvec = em.m_canonized[em.m_var2index[u]].vars(); auto const& uvec = em.m_canonized[em.m_var2index[u]].rvars();
auto const& vvec = em.m_canonized[em.m_var2index[v]].vars(); auto const& vvec = em.m_canonized[em.m_var2index[v]].rvars();
return uvec == vvec; return uvec == vvec;
} }
}; };

2
src/util/lp/factorization_factory_imp.cpp
View file

@ -22,7 +22,7 @@
namespace nla { namespace nla {
factorization_factory_imp::factorization_factory_imp(const smon& rm, const core& s) : factorization_factory_imp::factorization_factory_imp(const smon& rm, const core& s) :
factorization_factory(rm.vars(), &s.m_emons[rm.var()]), factorization_factory(rm.rvars(), &s.m_emons[rm.var()]),
m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { } m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }
bool factorization_factory_imp::find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const { bool factorization_factory_imp::find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {

12
src/util/lp/nla_core.cpp
View file

@ -83,7 +83,7 @@ svector<lpvar> core::sorted_vars(const factor& f) const {
return r; return r;
} }
TRACE("nla_solver", tout << "nv";); TRACE("nla_solver", tout << "nv";);
return m_emons.canonical[f.var()].vars(); return m_emons.canonical[f.var()].rvars();
} }
// the value of the factor is equal to the value of the variable multiplied // the value of the factor is equal to the value of the variable multiplied
@ -170,7 +170,7 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
print_var(f.var(), out); print_var(f.var(), out);
} else { } else {
out << "PROD, "; out << "PROD, ";
print_product(m_emons.canonical[f.var()].vars(), out); print_product(m_emons.canonical[f.var()].rvars(), out);
} }
out << "\n"; out << "\n";
return out; return out;
@ -820,7 +820,7 @@ int core::get_derived_sign(const smon& rm, const factorization& f) const {
} }
void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const { void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const {
out << "rooted vars: "; out << "rooted vars: ";
print_product(rm.vars(), out); print_product(rm.rvars(), out);
out << "\n"; out << "\n";
out << "mon: " << pp_mon(*this, rm.var()) << "\n"; out << "mon: " << pp_mon(*this, rm.var()) << "\n";
@ -1468,11 +1468,11 @@ bool core::divide(const smon& bc, const factor& c, factor & b) const {
tout << "c_vars = "; tout << "c_vars = ";
print_product(c_vars, tout); print_product(c_vars, tout);
tout << "\nbc_vars = "; tout << "\nbc_vars = ";
print_product(bc.vars(), tout);); print_product(bc.rvars(), tout););
if (!lp::is_proper_factor(c_vars, bc.vars())) if (!lp::is_proper_factor(c_vars, bc.rvars()))
return false; return false;
auto b_vars = lp::vector_div(bc.vars(), c_vars); auto b_vars = lp::vector_div(bc.rvars(), c_vars);
TRACE("nla_solver_div", tout << "b_vars = "; print_product(b_vars, tout);); TRACE("nla_solver_div", tout << "b_vars = "; print_product(b_vars, tout););
SASSERT(b_vars.size() > 0); SASSERT(b_vars.size() > 0);
if (b_vars.size() == 1) { if (b_vars.size() == 1) {

4
src/util/lp/nla_monotone_lemmas.cpp
View file

@ -120,7 +120,7 @@ bool monotone::monotonicity_lemma_on_lex_sorted(const monotone_array_t& lex_sort
vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const smon& a) const { vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const smon& a) const {
vector<std::pair<rational, lpvar>> r; vector<std::pair<rational, lpvar>> r;
for (lpvar j : a.vars()) { for (lpvar j : a.rvars()) {
r.push_back(std::make_pair(abs(vvr(j)), j)); r.push_back(std::make_pair(abs(vvr(j)), j));
} }
std::sort(r.begin(), r.end(), [](const std::pair<rational, lpvar>& a, std::sort(r.begin(), r.end(), [](const std::pair<rational, lpvar>& a,
@ -220,7 +220,7 @@ void monotone::generate_monl(const smon& a,
std::vector<rational> monotone::get_sorted_key(const smon& rm) const { std::vector<rational> monotone::get_sorted_key(const smon& rm) const {
std::vector<rational> r; std::vector<rational> r;
for (unsigned j : rm.vars()) { for (unsigned j : rm.rvars()) {
r.push_back(abs(vvr(j))); r.push_back(abs(vvr(j)));
} }
std::sort(r.begin(), r.end()); std::sort(r.begin(), r.end());