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

use for pattern

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-02 04:35:22 -07:00
parent 88dd9ac668
commit 61d887b36f
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_lra.cpp
View file

@ -1176,7 +1176,7 @@ public:
if (m_solver->is_term(wi)) { if (m_solver->is_term(wi)) {
const lp::lar_term& term = m_solver->get_term(wi); const lp::lar_term& term = m_solver->get_term(wi);
result += term.m_v * coeff; result += term.m_v * coeff;
for (const auto & i: term.m_coeffs) { for (const auto & i : term.m_coeffs) {
m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second)); m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
} }
} }
@ -2088,8 +2088,8 @@ public:
vi = m_todo_vars.back(); vi = m_todo_vars.back();
m_todo_vars.pop_back(); m_todo_vars.pop_back();
lp::lar_term const& term = m_solver->get_term(vi); lp::lar_term const& term = m_solver->get_term(vi);
for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) { for (auto const& coeff : term.m_coeffs) {
lp::var_index wi = i->first; lp::var_index wi = coeff.first;
if (m_solver->is_term(wi)) { if (m_solver->is_term(wi)) {
m_todo_vars.push_back(wi); m_todo_vars.push_back(wi);
} }
@ -2113,8 +2113,8 @@ public:
vi = m_todo_vars.back(); vi = m_todo_vars.back();
m_todo_vars.pop_back(); m_todo_vars.pop_back();
lp::lar_term const& term = m_solver->get_term(vi); lp::lar_term const& term = m_solver->get_term(vi);
for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) { for (auto const& coeff : term.m_coeffs) {
lp::var_index wi = i->first; lp::var_index wi = coeff.first;
if (m_solver->is_term(wi)) { if (m_solver->is_term(wi)) {
m_todo_vars.push_back(wi); m_todo_vars.push_back(wi);
} }
@ -2204,7 +2204,7 @@ public:
lp::var_index vi = m_theory_var2var_index[v]; lp::var_index vi = m_theory_var2var_index[v];
SASSERT(m_solver->is_term(vi)); SASSERT(m_solver->is_term(vi));
lp::lar_term const& term = m_solver->get_term(vi); lp::lar_term const& term = m_solver->get_term(vi);
for (auto const coeff : term.m_coeffs) { for (auto const & coeff : term.m_coeffs) {
lp::var_index wi = coeff.first; lp::var_index wi = coeff.first;
lp::constraint_index ci; lp::constraint_index ci;
rational value; rational value;