mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

do not register equality terms created in lar_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-09 12:12:51 -07:00
parent 285ff9540d
commit a0251ac745
3 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/lar_solver.cpp
View file

@ -1705,16 +1705,16 @@ bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>>
return true; return true;
} }
// do not register this term if ext_i == -1
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i) { var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i) {
TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";);
if (ext_i + 1)
m_term_register.add_var(ext_i, term_is_int(coeffs)); m_term_register.add_var(ext_i, term_is_int(coeffs));
lp_assert(all_vars_are_registered(coeffs)); lp_assert(all_vars_are_registered(coeffs));
if (strategy_is_undecided()) if (strategy_is_undecided())
return add_term_undecided(coeffs); return add_term_undecided(coeffs);
lar_term * t = new lar_term(coeffs); lar_term * t = new lar_term(coeffs);
push_term(t); push_term(t);
SASSERT(m_term_register.size() == m_terms.size());
unsigned adjusted_term_index = m_terms.size() - 1; unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = m_terms_start_index + adjusted_term_index; var_index ret = m_terms_start_index + adjusted_term_index;
if (use_tableau() && !coeffs.empty()) { if (use_tableau() && !coeffs.empty()) {
@ -2370,10 +2370,7 @@ std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j,
vector<std::pair<mpq, var_index>> coeffs; vector<std::pair<mpq, var_index>> coeffs;
coeffs.push_back(std::make_pair(mpq(1),j)); coeffs.push_back(std::make_pair(mpq(1),j));
coeffs.push_back(std::make_pair(mpq(-1),k)); coeffs.push_back(std::make_pair(mpq(-1),k));
unsigned ext_term_index = m_terms.size(); unsigned term_index = add_term(coeffs, -1); // -1 to not register the term: only external terms are registered
while (m_term_register.external_is_used(ext_term_index))
ext_term_index *= 2;
unsigned term_index = add_term(coeffs, ext_term_index);
return std::pair<constraint_index, constraint_index>( return std::pair<constraint_index, constraint_index>(
add_var_bound(term_index, lconstraint_kind::LE, mpq(0)), add_var_bound(term_index, lconstraint_kind::LE, mpq(0)),
add_var_bound(term_index, lconstraint_kind::GE, mpq(0))); add_var_bound(term_index, lconstraint_kind::GE, mpq(0)));

13
src/math/lp/var_register.h
View file

@ -66,10 +66,17 @@ public:
} }
return ret; return ret;
} }
// returns -1 if
unsigned local_to_external(unsigned local_var) const { unsigned local_to_external(unsigned local_var) const {
SASSERT(local_var >= m_local_offset); if (local_var + 1 == 0) // local_var == -1
return m_local_to_external[local_var - m_local_offset].external_j(); return -1;
if (local_var < m_local_offset)
return -1;
unsigned k = local_var - m_local_offset;
if (k >= m_local_to_external.size())
return -1;
return m_local_to_external[k].external_j();
} }
unsigned size() const { unsigned size() const {
return m_local_to_external.size(); return m_local_to_external.size();

2
src/smt/theory_lra.cpp
View file

@ -2364,7 +2364,7 @@ public:
if (v == null_theory_var) { if (v == null_theory_var) {
return false; return false;
} }
if (m_unassigned_bounds[v] == 0 || m_bounds.size() <= static_cast<unsigned>(v)) { if (m_bounds.size() <= static_cast<unsigned>(v) || m_unassigned_bounds[v] == 0) {
return false; return false;
} }
for (lp_api::bound* b : m_bounds[v]) { for (lp_api::bound* b : m_bounds[v]) {