mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

work on Grobner: remove unused m_scopes from the legacy version

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-08 10:45:47 -07:00
parent 86357de6fe
commit 70b57fbd02
2 changed files with 0 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/math/grobner/grobner.cpp
View file

@ -90,22 +90,6 @@ void grobner::unfreeze_equations(unsigned old_size) {
m_equations_to_unfreeze.shrink(old_size); m_equations_to_unfreeze.shrink(old_size);
} }
void grobner::push_scope() {
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_equations_to_unfreeze_lim = m_equations_to_unfreeze.size();
s.m_equations_to_delete_lim = m_equations_to_delete.size();
}
void grobner::pop_scope(unsigned num_scopes) {
SASSERT(num_scopes >= get_scope_level());
unsigned new_lvl = get_scope_level() - num_scopes;
scope & s = m_scopes[new_lvl];
unfreeze_equations(s.m_equations_to_unfreeze_lim);
del_equations(s.m_equations_to_delete_lim);
m_scopes.shrink(new_lvl);
}
void grobner::reset() { void grobner::reset() {
flush(); flush();
m_processed.reset(); m_processed.reset();
@ -312,7 +296,6 @@ grobner::monomial * grobner::mk_monomial(rational const & coeff, expr * m) {
} }
void grobner::init_equation(equation * eq, v_dependency * d) { void grobner::init_equation(equation * eq, v_dependency * d) {
eq->m_scope_lvl = get_scope_level();
unsigned bidx = m_equations_to_delete.size(); unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx; eq->m_bidx = bidx;
eq->m_dep = d; eq->m_dep = d;
@ -626,10 +609,6 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
if (is_subset(LT, curr, rest)) { if (is_subset(LT, curr, rest)) {
if (i == 0) if (i == 0)
m_changed_leading_term = true; m_changed_leading_term = true;
if (source->m_scope_lvl > target->m_scope_lvl) {
target = copy_equation(target);
SASSERT(target->m_scope_lvl >= source->m_scope_lvl);
}
if (!result) { if (!result) {
// first time that source is being applied. // first time that source is being applied.
target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep); target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);

8
src/math/grobner/grobner.h
View file

@ -58,7 +58,6 @@ public:
}; };
class equation { class equation {
unsigned m_scope_lvl; //!< scope level when this equation was created.
unsigned m_bidx:31; //!< position at m_equations_to_delete unsigned m_bidx:31; //!< position at m_equations_to_delete
unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. unsigned m_lc:1; //!< true if equation if a linear combination of the input equations.
ptr_vector<monomial> m_monomials; //!< sorted monomials ptr_vector<monomial> m_monomials; //!< sorted monomials
@ -108,7 +107,6 @@ protected:
unsigned m_equations_to_unfreeze_lim; unsigned m_equations_to_unfreeze_lim;
unsigned m_equations_to_delete_lim; unsigned m_equations_to_delete_lim;
}; };
svector<scope> m_scopes;
ptr_vector<monomial> m_tmp_monomials; ptr_vector<monomial> m_tmp_monomials;
ptr_vector<monomial> m_del_monomials; ptr_vector<monomial> m_del_monomials;
ptr_vector<expr> m_tmp_vars1; ptr_vector<expr> m_tmp_vars1;
@ -192,8 +190,6 @@ public:
~grobner(); ~grobner();
unsigned get_scope_level() const { return m_scopes.size(); }
/** /**
\brief Set the weight of a term that is viewed as a variable by this module. \brief Set the weight of a term that is viewed as a variable by this module.
The weight is used to order monomials. If the weight is not set for a term t, then the The weight is used to order monomials. If the weight is not set for a term t, then the
@ -278,10 +274,6 @@ public:
void get_equations(ptr_vector<equation> & result) const; void get_equations(ptr_vector<equation> & result) const;
void push_scope();
void pop_scope(unsigned num_scopes);
void display_equation(std::ostream & out, equation const & eq) const; void display_equation(std::ostream & out, equation const & eq) const;
void display_monomial(std::ostream & out, monomial const & m) const; void display_monomial(std::ostream & out, monomial const & m) const;