mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

remove m_lc field from equation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-11-03 11:34:22 -08:00
parent f5c8ead995
commit 4a87ca8b92
3 changed files with 5 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -27,21 +27,6 @@ nla_grobner::nla_grobner(core *c, intervals *s)
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(m_val_manager, m_alloc),
m_changed_leading_term(false) {} m_changed_leading_term(false) {}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue
bool nla_grobner::scan_for_linear(ptr_vector<equation>& eqs) {
bool result = false;
for (nla_grobner::equation* eq : eqs) {
if (!eq->is_linear_combination()) {
TRACE("non_linear", tout << "processing new equality:\n"; display_equation(tout, *eq););
TRACE("non_linear_bug", tout << "processing new equality:\n"; display_equation(tout, *eq););
if (internalize_gb_eq(eq))
result = true;
}
}
return result;
}
bool nla_grobner::internalize_gb_eq(equation* ) { bool nla_grobner::internalize_gb_eq(equation* ) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return false; return false;
@ -735,7 +720,7 @@ bool nla_grobner::done() const {
|| ||
canceled() canceled()
|| ||
m_reported > 0 // 10 m_reported > 10
|| ||
m_conflict) { m_conflict) {
TRACE("grobner", tout << "done()\n";); TRACE("grobner", tout << "done()\n";);
@ -766,9 +751,7 @@ void nla_grobner::update_statistics(){
bool nla_grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) { bool nla_grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) {
return scan_for_linear(eqs) return (!m_nl_gb_exhausted) &&
&&
(!m_nl_gb_exhausted) &&
try_to_modify_eqs(eqs, next_weight); try_to_modify_eqs(eqs, next_weight);
} }
@ -837,7 +820,6 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
unsigned bidx = m_equations_to_delete.size(); unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx; eq->m_bidx = bidx;
eq->dep() = dep; eq->dep() = dep;
eq->m_lc = true;
eq->exp() = e; eq->exp() = e;
m_equations_to_delete.push_back(eq); m_equations_to_delete.push_back(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);

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

@ -39,8 +39,8 @@ struct grobner_stats {
class nla_grobner : common { class nla_grobner : common {
class equation { class equation {
unsigned m_bidx:31; //!< position at m_equations_to_delete unsigned m_bidx; //!< position at m_equations_to_delete
unsigned m_lc:1; //!< true if equation if a linear combination of the input equations.
nex * m_expr; // simplified expressionted monomials nex * m_expr; // simplified expressionted monomials
ci_dependency * m_dep; //!< justification for the equality ci_dependency * m_dep; //!< justification for the equality
public: public:
@ -71,7 +71,6 @@ class nla_grobner : common {
ci_dependency * dep() const { return m_dep; } ci_dependency * dep() const { return m_dep; }
ci_dependency *& dep() { return m_dep; } ci_dependency *& dep() { return m_dep; }
unsigned hash() const { return m_bidx; } unsigned hash() const { return m_bidx; }
bool is_linear_combination() const { return m_lc; }
friend class nla_grobner; friend class nla_grobner;
}; };
@ -101,7 +100,6 @@ public:
void grobner_lemmas(); void grobner_lemmas();
~nla_grobner(); ~nla_grobner();
private: private:
bool scan_for_linear(ptr_vector<equation>& eqs);
void find_nl_cluster(); void find_nl_cluster();
void prepare_rows_and_active_vars(); void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar>& q); void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar>& q);

2
src/smt/theory_arith_nl.h
View file

@ -2292,7 +2292,7 @@ bool theory_arith<Ext>::try_to_modify_eqs(ptr_vector<grobner::equation>& eqs, gr
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::scan_for_linear(ptr_vector<grobner::equation>& eqs, grobner& gb) { bool theory_arith<Ext>::scan_for_linear(ptr_vector<grobner::equation>& eqs, grobner& gb) {
bool result = false; bool result = false;
if (m_params.m_nl_arith_gb_eqs) { if (m_params.m_nl_arith_gb_eqs) { // m_nl_arith_gb_eqs is false by default
for (grobner::equation* eq : eqs) { for (grobner::equation* eq : eqs) {
if (!eq->is_linear_combination()) { if (!eq->is_linear_combination()) {
TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq);); TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););