mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

cheap eqs

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-10 15:02:40 -07:00
parent 50b9915c57
commit 94263167ec
3 changed files with 17 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/math/lp/lp_bound_propagator.h
View file

@ -319,8 +319,7 @@ public:
void cheap_eq_table(unsigned rid) { void cheap_eq_table(unsigned rid) {
TRACE("cheap_eqs", tout << "checking if row " << rid << " can propagate equality.\n"; display_row_info(rid, tout);); TRACE("cheap_eqs", tout << "checking if row " << rid << " can propagate equality.\n"; display_row_info(rid, tout););
unsigned x; unsigned x, y;
unsigned y;
mpq k; mpq k;
if (is_offset_row(rid, x, y, k)) { if (is_offset_row(rid, x, y, k)) {
if (y == null_lpvar) { if (y == null_lpvar) {
@ -358,41 +357,28 @@ public:
unsigned row_id; unsigned row_id;
var_offset key(y, k); var_offset key(y, k);
if (m_var_offset2row_id.find(key, row_id)) { if (m_var_offset2row_id.find(key, row_id)) {
if (row_id == rid) { if (row_id == rid) { // it is the same row.
// it is the same row.
return; return;
} }
unsigned x2; unsigned x2, y2;
unsigned y2;
mpq k2; mpq k2;
if (is_offset_row(row_id, x2, y2, k2)) { if (is_offset_row(row_id, x2, y2, k2)) {
bool new_eq = false; bool new_eq = false;
#ifdef _TRACE
bool swapped = false;
#endif
if (y == y2 && k == k2) { if (y == y2 && k == k2) {
new_eq = true; new_eq = true;
} }
else if (y2 != null_lpvar) { else if (y2 != null_lpvar && x2 == y && k == - k2) {
#ifdef _TRACE
swapped = true;
#endif
std::swap(x2, y2); std::swap(x2, y2);
k2.neg();
if (y == y2 && k == k2) {
new_eq = true; new_eq = true;
} }
}
if (new_eq) { if (new_eq) {
if (!is_equal(x, x2) && is_int(x) == is_int(x2)) { if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
SASSERT(y == y2 && k == k2); // SASSERT(y == y2 && k == k2 );
explanation ex; explanation ex;
explain_fixed_in_row(rid, ex); explain_fixed_in_row(rid, ex);
explain_fixed_in_row(row_id, ex); explain_fixed_in_row(row_id, ex);
TRACE("arith_eq", tout << "propagate eq two rows:\n"; TRACE("arith_eq", tout << "propagate eq two rows:\n";
tout << "swapped: " << swapped << "\n";
tout << "x : v" << x << "\n"; tout << "x : v" << x << "\n";
tout << "x2 : v" << x2 << "\n"; tout << "x2 : v" << x2 << "\n";
display_row_info(rid, tout); display_row_info(rid, tout);
@ -403,7 +389,6 @@ public:
} }
} }
// the original row was deleted or it is not offset row anymore ===> remove it from table // the original row was deleted or it is not offset row anymore ===> remove it from table
m_var_offset2row_id.erase(key);
} }
// add new entry // add new entry
m_var_offset2row_id.insert(key, rid); m_var_offset2row_id.insert(key, rid);

4
src/smt/smt_setup.cpp
View file

@ -755,7 +755,9 @@ namespace smt {
} }
void setup::setup_lra_arith() { void setup::setup_lra_arith() {
// m_context.register_plugin(alloc(smt::theory_mi_arith, m_context)); if (m_params.m_arith_mode == AS_OLD_ARITH)
m_context.register_plugin(alloc(smt::theory_mi_arith, m_context));
else
m_context.register_plugin(alloc(smt::theory_lra, m_context)); m_context.register_plugin(alloc(smt::theory_lra, m_context));
} }

12
src/smt/theory_arith_eq.h
View file

@ -253,6 +253,7 @@ namespace smt {
m_stats.m_fixed_eqs++; m_stats.m_fixed_eqs++;
propagate_eq_to_core(x, x2, ante); propagate_eq_to_core(x, x2, ante);
} }
//return;
} }
if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) { if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) {
@ -277,16 +278,10 @@ namespace smt {
numeral k2; numeral k2;
if (r2.get_base_var() != null_theory_var && is_offset_row(r2, x2, y2, k2)) { if (r2.get_base_var() != null_theory_var && is_offset_row(r2, x2, y2, k2)) {
bool new_eq = false; bool new_eq = false;
#ifdef _TRACE
bool swapped = false;
#endif
if (y == y2 && k == k2) { if (y == y2 && k == k2) {
new_eq = true; new_eq = true;
} }
else if (y2 != null_theory_var) { else if (y2 != null_theory_var) {
#ifdef _TRACE
swapped = true;
#endif
std::swap(x2, y2); std::swap(x2, y2);
k2.neg(); k2.neg();
if (y == y2 && k == k2) { if (y == y2 && k == k2) {
@ -301,7 +296,6 @@ namespace smt {
collect_fixed_var_justifications(r, ante); collect_fixed_var_justifications(r, ante);
collect_fixed_var_justifications(r2, ante); collect_fixed_var_justifications(r2, ante);
TRACE("arith_eq", tout << "propagate eq two rows:\n"; TRACE("arith_eq", tout << "propagate eq two rows:\n";
tout << "swapped: " << swapped << "\n";
tout << "x : v" << x << "\n"; tout << "x : v" << x << "\n";
tout << "x2 : v" << x2 << "\n"; tout << "x2 : v" << x2 << "\n";
display_row_info(tout, r); display_row_info(tout, r);
@ -312,9 +306,11 @@ namespace smt {
return; return;
} }
} }
// the original row was delete or it is not offset row anymore ===> remove it from table // the original row was delete or it is not offset row anymore ===> remove it from table
m_var_offset2row_id.erase(key);
} }
if (y == -1)
std::cout << "h";
// add new entry // add new entry
m_var_offset2row_id.insert(key, rid); m_var_offset2row_id.insert(key, rid);
} }