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

port Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-09 17:11:30 -07:00
parent 005021f74e
commit 1e5ade1dc2
2 changed files with 41 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -709,42 +709,45 @@ grobner::equation * grobner::pick_next() {
return r; return r;
} }
void grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
if (new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_remove.push_back(target);
if (m_changed_leading_term) {
m_to_process.insert(new_target);
to_remove.push_back(target);
}
else {
to_insert.push_back(new_target);
}
target = new_target;
}
else {
if (m_changed_leading_term) {
m_to_process.insert(target);
to_remove.push_back(target);
}
}
}
/** /**
\brief Use the given equation to simplify processed terms. \brief Use the given equation to simplify processed terms.
*/ */
bool grobner::simplify_processed(equation * eq) { bool grobner::simplify_processed_with_eq(equation * eq) {
ptr_buffer<equation> to_insert; ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove; ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
equation_set::iterator it = m_processed.begin(); equation_set::iterator it = m_processed.begin();
equation_set::iterator end = m_processed.end(); equation_set::iterator end = m_processed.end();
for (; it != end && !m_manager.canceled(); ++it) { for (; it != end && !m_manager.canceled(); ++it) {
equation * curr = *it; equation * target = *it;
m_changed_leading_term = false; m_changed_leading_term = false;
// if the leading term is simplified, then the equation has to be moved to m_to_process // if the leading term is simplified, then the equation has to be moved to m_to_process
equation * new_curr = simplify_source_target(eq, curr); equation * new_target = simplify_source_target(eq, target);
if (new_curr != nullptr) { if (new_target != nullptr) {
if (new_curr != curr) { process_simplified_target(to_insert, new_target, target, to_remove);
m_equations_to_unfreeze.push_back(curr);
to_remove.push_back(curr);
if (m_changed_leading_term) {
m_to_process.insert(new_curr);
to_remove.push_back(curr);
} }
else { if (is_trivial(target))
to_insert.push_back(new_curr); to_delete.push_back(target);
}
curr = new_curr;
}
else {
if (m_changed_leading_term) {
m_to_process.insert(curr);
to_remove.push_back(curr);
}
}
}
if (is_trivial(curr))
to_delete.push_back(curr);
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
m_processed.insert(eq); m_processed.insert(eq);
@ -762,16 +765,16 @@ void grobner::simplify_to_process(equation * eq) {
ptr_buffer<equation> to_insert; ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove; ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
for (equation* curr : m_to_process) { for (equation* target : m_to_process) {
equation * new_curr = simplify_source_target(eq, curr); equation * new_target = simplify_source_target(eq, target);
if (new_curr != nullptr && new_curr != curr) { if (new_target != nullptr && new_target != target) {
m_equations_to_unfreeze.push_back(curr); m_equations_to_unfreeze.push_back(target);
to_insert.push_back(new_curr); to_insert.push_back(new_target);
to_remove.push_back(curr); to_remove.push_back(target);
curr = new_curr; target = new_target;
} }
if (is_trivial(curr)) if (is_trivial(target))
to_delete.push_back(curr); to_delete.push_back(target);
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
m_to_process.insert(eq); m_to_process.insert(eq);
@ -864,8 +867,8 @@ void grobner::superpose(equation * eq1, equation * eq2) {
\brief Superpose the given equations with the equations in m_processed. \brief Superpose the given equations with the equations in m_processed.
*/ */
void grobner::superpose(equation * eq) { void grobner::superpose(equation * eq) {
for (equation * curr : m_processed) { for (equation * target : m_processed) {
superpose(eq, curr); superpose(eq, target);
} }
} }
@ -891,7 +894,7 @@ bool grobner::compute_basis_step() {
eq = new_eq; eq = new_eq;
} }
if (m_manager.canceled()) return false; if (m_manager.canceled()) return false;
if (!simplify_processed(eq)) return false; if (!simplify_processed_with_eq(eq)) return false;
superpose(eq); superpose(eq);
m_processed.insert(eq); m_processed.insert(eq);
simplify_to_process(eq); simplify_to_process(eq);

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

@ -174,7 +174,7 @@ protected:
equation * pick_next(); equation * pick_next();
bool simplify_processed(equation * eq); bool simplify_processed_with_eq(equation * eq);
void simplify_to_process(equation * eq); void simplify_to_process(equation * eq);
@ -280,6 +280,7 @@ public:
void display_monomial(std::ostream & out, monomial const & m) const; void display_monomial(std::ostream & out, monomial const & m) const;
void display(std::ostream & out) const; void display(std::ostream & out) const;
void process_simplified_target(ptr_buffer<equation>& to_delete, equation* new_curr, equation*& curr, ptr_buffer<equation>& to_remove);
}; };
#endif /* GROBNER_H_ */ #endif /* GROBNER_H_ */