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

register inner terms with null var

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-09 13:07:05 -07:00
parent a0251ac745
commit 719603f185
2 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1708,13 +1708,13 @@ bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>>
// do not register this term if ext_i == -1 // 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_terms.size() == m_term_register.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,7 +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 term_index = add_term(coeffs, -1); // -1 to not register the term: only external terms are registered unsigned term_index = add_term(coeffs, -1); // -1 is the external null var
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)));

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

@ -50,10 +50,12 @@ public:
} }
unsigned add_var(unsigned user_var, bool is_int) { unsigned add_var(unsigned user_var, bool is_int) {
if (user_var + 1) { // user_var != -1
auto t = m_external_to_local.find(user_var); auto t = m_external_to_local.find(user_var);
if (t != m_external_to_local.end()) { if (t != m_external_to_local.end()) {
return t->second; return t->second;
} }
}
m_local_to_external.push_back(ext_var_info(user_var, is_int)); m_local_to_external.push_back(ext_var_info(user_var, is_int));
return m_external_to_local[user_var] = size() - 1 + m_local_offset; return m_external_to_local[user_var] = size() - 1 + m_local_offset;