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

remove m_conflict from nla_grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-11 20:07:12 -10:00
parent d0f682b239
commit 3f442ecef9
2 changed files with 4 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -583,7 +583,6 @@ void grobner::superpose(equation * eq1, equation * eq2) {
void grobner::register_report() {
m_reported++;
m_conflict = true;
}
// Let a be the greatest common divider of ab and bc,
// then ab/a is stored in b, and ac/a is stored in c
@ -724,20 +723,17 @@ bool grobner::done() const {
||
canceled()
||
m_reported > 100000
||
m_conflict) {
m_reported > 0
) {
TRACE("grobner",
tout << "done() is true because of ";
if (num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()) {
tout << "m_num_of_equations = " << num_of_equations() << "\n";
} else if (canceled()) {
tout << "canceled\n";
} else if (m_reported > 100000) {
} else if (m_reported > 0) {
tout << "m_reported = " << m_reported;
} else {
tout << "m_conflict = " << m_conflict;
}
}
tout << "\n";);
return true;
}

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

@ -90,7 +90,6 @@ class grobner : common {
nex_lt m_lt;
bool m_changed_leading_term;
unsigned m_reported;
bool m_conflict;
bool m_look_for_fixed_vars_in_rows;
public:
grobner(core *, intervals *);