mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

port Grobner: renaming and handle deps in simplifying

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-28 12:46:10 -07:00
parent 8744d987a3
commit 738165f0e7
2 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -301,6 +301,7 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
}
target->exp() = m_nex_creator.simplify(targ_sum);
target->dep = m_dep_manager.mk_join(source->dep, target->dep);
TRACE("grobner", tout << "target = "; display_equation(tout, *target););
return true;
}
@ -428,7 +429,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
}
}
bool nla_grobner::simplify_processed_with_eq(equation* eq) {
bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
@ -454,7 +455,7 @@ bool nla_grobner::simplify_processed_with_eq(equation* eq) {
return !canceled();
}
void nla_grobner::simplify_to_process(equation* eq) {
void nla_grobner::simplify_to_superpose(equation* eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
@ -622,11 +623,11 @@ bool nla_grobner::compute_basis_step() {
eq = new_eq;
}
if (canceled()) return false;
if (!simplify_processed_with_eq(eq)) return false;
if (!simplify_to_superpose_with_eq(eq)) return false;
TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
superpose(eq);
insert_to_superpose(eq);
simplify_to_process(eq);
simplify_to_superpose(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false;
}

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

@ -115,9 +115,9 @@ private:
equation * simplify_source_target(equation * source, equation * target);
equation* simplify_using_processed(equation*);
bool simplify_target_monomials(equation * source, equation * target);
void process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove);
bool simplify_processed_with_eq(equation*);
void simplify_to_process(equation*);
void process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove);
bool simplify_to_superpose_with_eq(equation*);
void simplify_to_superpose(equation*);
equation* pick_next();
void set_gb_exhausted();
bool canceled() const;