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

do not eliminate fresh variables when tightening

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-09-29 11:51:41 -07:00 committed by Lev Nachmanson
parent 52b0b8d5d5
commit a8e667c643
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/math/lp/dioph_eq.cpp
View file

@ -141,7 +141,7 @@ namespace lp {
std::list<unsigned> m_f; // F = {λ(t):t in m_f} std::list<unsigned> m_f; // F = {λ(t):t in m_f}
// set S // set S
std::list<unsigned> m_s; // S = {λ(t): t in m_s} std::list<unsigned> m_s; // S = {λ(t): t in m_s}
u_map<unsigned> m_k2s; // k is substituted by using equation in m_eprime[m_k2s[k]] vector<unsigned> m_k2s; // k is substituted by using equation in m_eprime[m_k2s[k]]
unsigned m_conflict_index = -1; // m_eprime[m_conflict_index] gives the conflict unsigned m_conflict_index = -1; // m_eprime[m_conflict_index] gives the conflict
@ -161,6 +161,8 @@ namespace lp {
void init() { void init() {
unsigned n_of_rows = lra.A_r().row_count(); unsigned n_of_rows = lra.A_r().row_count();
m_k2s.clear();
m_k2s.resize(lra.column_count(), -1);
m_conflict_index = -1; m_conflict_index = -1;
m_infeas_explanation.clear(); m_infeas_explanation.clear();
@ -292,12 +294,13 @@ namespace lp {
unsigned j = p.j(); unsigned j = p.j();
if (is_fresh_var(j)) { if (is_fresh_var(j)) {
j = lra.add_var(p.j(), true); j = lra.add_var(p.j(), true);
m_k2s.push_back(null_lpvar);
} }
t.add_monomial(coeff*p.coeff(), j); t.add_monomial(coeff*p.coeff(), j);
} }
t.c() += coeff*e.m_e.c(); t.c() += coeff*e.m_e.c();
for (const auto& p: t) { for (const auto& p: t) {
if (m_k2s.contains(p.j())) if (m_k2s[p.j()] != null_lpvar)
q.push(p.j()); q.push(p.j());
} }
@ -354,7 +357,7 @@ namespace lp {
term_o t; term_o t;
std::queue<unsigned> q; std::queue<unsigned> q;
for (const auto& p: lar_t) { for (const auto& p: lar_t) {
if (m_k2s.contains(p.j())) if (m_k2s[p.j()] != null_lpvar)
q.push(p.j()); q.push(p.j());
t.add_monomial(p.coeff(), p.j()); t.add_monomial(p.coeff(), p.j());
} }
@ -609,7 +612,8 @@ namespace lp {
// k is the index of the index of the variable with the coefficient +-1 that is being substituted // k is the index of the index of the variable with the coefficient +-1 that is being substituted
void move_from_f_to_s(unsigned k, std::list<unsigned>::iterator it) { void move_from_f_to_s(unsigned k, std::list<unsigned>::iterator it) {
m_s.push_back(*it); m_s.push_back(*it);
m_k2s.insert(k, *it); if (!is_fresh_var(k))
m_k2s[k] = *it;
m_f.erase(it); m_f.erase(it);
} }
@ -632,7 +636,7 @@ namespace lp {
} }
void explain(explanation& ex) { void explain(explanation& ex) {
if (m_conflict_index == static_cast<unsigned>(-1)) { if (m_conflict_index == UINT_MAX) {
SASSERT(!(lra.get_status() == lp_status::FEASIBLE || lra.get_status() == lp_status::OPTIMAL)); SASSERT(!(lra.get_status() == lp_status::FEASIBLE || lra.get_status() == lp_status::OPTIMAL));
for (auto ci: m_infeas_explanation) { for (auto ci: m_infeas_explanation) {
ex.push_back(ci.ci()); ex.push_back(ci.ci());