mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +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-22 16:23:04 -07:00
parent 47bb9b2689
commit 3fd853752b
2 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/lp/nla_grobner.cpp
View file

@ -423,7 +423,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
m_equations_to_unfreeze.push_back(target); m_equations_to_unfreeze.push_back(target);
to_remove.push_back(target); to_remove.push_back(target);
if (m_changed_leading_term) { if (m_changed_leading_term) {
insert_to_process(new_target); insert_to_simplify(new_target);
to_remove.push_back(target); to_remove.push_back(target);
} }
else { else {
@ -433,7 +433,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
} }
else { else {
if (m_changed_leading_term) { if (m_changed_leading_term) {
insert_to_process(target); insert_to_simplify(target);
to_remove.push_back(target); to_remove.push_back(target);
} }
} }
@ -457,7 +457,7 @@ bool nla_grobner::simplify_processed_with_eq(equation* eq) {
to_delete.push_back(target); to_delete.push_back(target);
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
insert_processed(eq); insert_to_superpose(eq);
for (equation* eq : to_remove) for (equation* eq : to_remove)
m_to_superpose.erase(eq); m_to_superpose.erase(eq);
for (equation* eq : to_delete) for (equation* eq : to_delete)
@ -481,7 +481,7 @@ void nla_grobner::simplify_to_process(equation* eq) {
to_delete.push_back(target); to_delete.push_back(target);
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
insert_to_process(eq); insert_to_simplify(eq);
for (equation* eq : to_remove) for (equation* eq : to_remove)
m_to_simplify.erase(eq); m_to_simplify.erase(eq);
for (equation* eq : to_delete) for (equation* eq : to_delete)
@ -499,8 +499,8 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
if (!find_b_c(ab, ac, b, c)) { if (!find_b_c(ab, ac, b, c)) {
return; return;
} }
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
// insert_to_
} }
bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) { bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) {
@ -543,6 +543,7 @@ bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) {
bp++; bp++;
} }
TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";); TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";);
return true;
} }
bool nla_grobner::find_b_c_check(const nex_mul*ab, const nex_mul* ac) const { bool nla_grobner::find_b_c_check(const nex_mul*ab, const nex_mul* ac) const {
@ -589,7 +590,7 @@ bool nla_grobner::compute_basis_step() {
if (canceled()) return false; if (canceled()) return false;
if (!simplify_processed_with_eq(eq)) return false; if (!simplify_processed_with_eq(eq)) return false;
superpose(eq); superpose(eq);
insert_processed(eq); insert_to_superpose(eq);
simplify_to_process(eq); simplify_to_process(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout);); TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false; return false;
@ -727,7 +728,7 @@ void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
return; return;
equation * eq = new equation(); equation * eq = new equation();
init_equation(eq, e, dep); init_equation(eq, e, dep);
insert_to_process(eq); insert_to_simplify(eq);
} }
void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) { void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {

4
src/math/lp/nla_grobner.h
View file

@ -147,8 +147,8 @@ bool simplify_processed_with_eq(equation*);
void init_equation(equation* eq, nex*, ci_dependency* d); void init_equation(equation* eq, nex*, ci_dependency* d);
std::ostream& display_dependency(std::ostream& out, ci_dependency*); std::ostream& display_dependency(std::ostream& out, ci_dependency*);
void insert_to_process(equation *eq) { m_to_simplify.insert(eq); } void insert_to_simplify(equation *eq) { m_to_simplify.insert(eq); }
void insert_processed(equation *eq) { m_to_superpose.insert(eq); } void insert_to_superpose(equation *eq) { m_to_superpose.insert(eq); }
void simplify_equations_to_process(); void simplify_equations_to_process();
nex_mul * get_highest_monomial(nex * e) const; nex_mul * get_highest_monomial(nex * e) const;
ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints); ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints);