From a376a8d3432be226127af80c71877a13246412fd Mon Sep 17 00:00:00 2001 From: Kirill Bobyrev Date: Tue, 2 Oct 2018 16:14:01 +0300 Subject: [PATCH] [NFC] Cleanup arith_eq_solver.(cpp|h) Use for-range loops instead of for-index loops where possible, remove trailing whitespaces. This patch does not affect functionality. --- src/smt/arith_eq_solver.cpp | 135 ++++++++++++++++++------------------ src/smt/arith_eq_solver.h | 24 +++---- 2 files changed, 78 insertions(+), 81 deletions(-) diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 128b35dd1..883255b8a 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -12,14 +12,11 @@ Abstract: Author: Nikolaj Bjorner (nbjorner) 2012-02-25 - + --*/ #include "smt/arith_eq_solver.h" -arith_eq_solver::~arith_eq_solver() { -} - arith_eq_solver::arith_eq_solver(ast_manager & m, params_ref const& p): m(m), m_params(p), @@ -93,9 +90,9 @@ void arith_eq_solver::gcd_normalize(vector& values) { if (g.is_zero() || g.is_one()) { return; } - for (unsigned i = 0; i < values.size(); ++i) { - values[i] = values[i] / g; - SASSERT(values[i].is_int()); + for (auto &value : values) { + value /= g; + SASSERT(value.is_int()); } } @@ -116,9 +113,9 @@ unsigned arith_eq_solver::find_abs_min(vector& values) { #ifdef _TRACE static void print_row(std::ostream& out, vector const& row) { - for(unsigned i = 0; i < row.size(); ++i) { - out << row[i] << " "; - } + for(unsigned i = 0; i < row.size(); ++i) { + out << row[i] << " "; + } out << "\n"; } @@ -165,7 +162,7 @@ bool arith_eq_solver::solve_integer_equation( bool& is_fresh ) { - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "solving: "; print_row(tout, values); ); @@ -174,31 +171,31 @@ bool arith_eq_solver::solve_integer_equation( // // Given: // a1*x1 + a2*x2 + .. + a_n*x_n + a_{n+1} = 0 - // + // // Assume gcd(a1,..,a_n,a_{n+1}) = 1 // Assume gcd(a1,...,a_n) divides a_{n+1} (eg. gcd(a1,..,an) = 1) - // + // // post-condition: values[index] = -1. - // + // // Let a_index be index of least absolute value. // // If |a_index| = 1, then return row and index. // Otherwise: // Let m = |a_index| + 1 // Set - // - // m*x_index' - // = + // + // m*x_index' + // = // ((a1 mod_hat m)*x1 + (a2 mod_hat m)*x2 + .. + (a_n mod_hat m)*x_n + (k mod_hat m)) - // = + // = // (a1'*x1 + a2'*x2 + .. (-)1*x_index + ...) - // + // // <=> Normalize signs so that sign to x_index is -1. // (-)a1'*x1 + (-)a2'*x2 + .. -1*x_index + ... + m*x_index' = 0 - // + // // Return row, where the coefficient to x_index is implicit. // Instead used the coefficient 'm' at position 'index'. - // + // gcd_normalize(values); if (!gcd_test(values)) { @@ -216,8 +213,8 @@ bool arith_eq_solver::solve_integer_equation( return true; } if (a.is_one()) { - for (unsigned i = 0; i < values.size(); ++i) { - values[i].neg(); + for (auto &value : values) { + value.neg(); } } is_fresh = !abs_a.is_one(); @@ -225,19 +222,19 @@ bool arith_eq_solver::solve_integer_equation( if (is_fresh) { numeral m = abs_a + numeral(1); - for (unsigned i = 0; i < values.size(); ++i) { - values[i] = mod_hat(values[i], m); + for (auto &value : values) { + value = mod_hat(value, m); } if (values[index].is_one()) { - for (unsigned i = 0; i < values.size(); ++i) { - values[i].neg(); + for (auto &value : values) { + value.neg(); } } SASSERT(values[index].is_minus_one()); values[index] = m; } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "solved at index " << index << ": "; print_row(tout, values); ); @@ -253,7 +250,7 @@ void arith_eq_solver::substitute( ) { SASSERT(1 <= index && index < s.size()); - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "substitute " << index << ":\n"; print_row(tout, r); print_row(tout, s); @@ -272,21 +269,21 @@ void arith_eq_solver::substitute( // s encodes an equation that contains a variable // with a unit coefficient. // - // Let + // Let // c = r[index] // s = s[index]*x + s'*y = 0 // r = c*x + r'*y = 0 - // - // => + // + // => // // 0 - // = - // -sign(s[index])*c*s + r - // = + // = + // -sign(s[index])*c*s + r + // = // -s[index]*sign(s[index])*c*x - sign(s[index])*c*s'*y + c*x + r'*y - // = + // = // -c*x - sign(s[index])*c*s'*y + c*x + r'*y - // = + // = // -sign(s[index])*c*s'*y + r'*y // numeral sign_s = s[index].is_pos()?numeral(1):numeral(-1); @@ -301,36 +298,36 @@ void arith_eq_solver::substitute( // // s encodes a substitution using an auxiliary variable. // the auxiliary variable is at position 'index'. - // - // Let + // + // Let // c = r[index] // s = s[index]*x + s'*y = 0 // r = c*x + r'*y = 0 // // s encodes : x |-> s[index]*x' + s'*y // - // Set: + // Set: // // r := c*s + r'*y - // + // r[index] = numeral(0); for (unsigned i = 0; i < r.size(); ++i) { r[i] += c*s[i]; - } + } for (unsigned i = r.size(); i < s.size(); ++i) { r.push_back(c*s[i]); } - } + } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "result: "; print_row(tout, r); ); } bool arith_eq_solver::solve_integer_equations( - vector& rows, + vector& rows, row& unsat_row ) { @@ -340,10 +337,10 @@ bool arith_eq_solver::solve_integer_equations( // // Naive integer equation solver where only units are eliminated. -// +// bool arith_eq_solver::solve_integer_equations_units( - vector& rows, + vector& rows, row& unsat_row ) { @@ -351,7 +348,7 @@ bool arith_eq_solver::solve_integer_equations_units( TRACE("arith_eq_solver", print_rows(tout << "solving:\n", rows);); unsigned_vector todo, done; - + for (unsigned i = 0; i < rows.size(); ++i) { todo.push_back(i); row& r = rows[i]; @@ -360,9 +357,9 @@ bool arith_eq_solver::solve_integer_equations_units( unsat_row = r; TRACE("arith_eq_solver", print_row(tout << "input is unsat: ", unsat_row); ); return false; - } + } } - for (unsigned i = 0; i < todo.size(); ++i) { + for (unsigned i = 0; i < todo.size(); ++i) { row& r = rows[todo[i]]; gcd_normalize(r); if (!gcd_test(r)) { @@ -388,7 +385,7 @@ bool arith_eq_solver::solve_integer_equations_units( todo.push_back(done[j]); done.erase(done.begin()+j); --j; - } + } } } else { @@ -396,7 +393,7 @@ bool arith_eq_solver::solve_integer_equations_units( } } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << ((done.size()<=1)?"solved ":"incomplete check ") << done.size() << "\n"; for (unsigned i = 0; i < done.size(); ++i) { print_row(tout, rows[done[i]]); @@ -411,12 +408,12 @@ bool arith_eq_solver::solve_integer_equations_units( // // Partial solver based on the omega test equalities. -// unsatisfiability is not preserved when eliminating +// unsatisfiability is not preserved when eliminating // auxiliary variables. // bool arith_eq_solver::solve_integer_equations_omega( - vector & rows, + vector & rows, row& unsat_row ) { @@ -460,16 +457,16 @@ bool arith_eq_solver::solve_integer_equations_omega( // // solved_row: -x_index + m*sigma + r1 = 0 // unsat_row: k*sigma + r2 = 0 - // - // <=> - // + // + // <=> + // // solved_row: -k*x_index + k*m*sigma + k*r1 = 0 // unsat_row: m*k*sigma + m*r2 = 0 // // => // // m*k*sigma + m*r2 + k*x_index - k*m*sigma - k*r1 = 0 - // + // for (unsigned l = 0; l < unsat_row.size(); ++l) { unsat_row[l] *= m; unsat_row[l] -= k*solved_row[l]; @@ -479,7 +476,7 @@ bool arith_eq_solver::solve_integer_equations_omega( } gcd_normalize(unsat_row); - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "gcd: "; print_row(tout, solved_row); print_row(tout, unsat_row); @@ -525,18 +522,18 @@ bool arith_eq_solver::solve_integer_equations_omega( // // Eliminate variables by searching for combination of rows where -// the coefficients have gcd = 1. -// +// the coefficients have gcd = 1. +// bool arith_eq_solver::solve_integer_equations_gcd( - vector & rows, + vector & rows, row& unsat_row ) -{ +{ unsigned_vector live, useful, gcd_pos; vector gcds; rational u, v; - + if (rows.empty()) { return true; } @@ -548,7 +545,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( unsat_row = r; TRACE("arith_eq_solver", print_row(tout << "input is unsat: ", unsat_row); ); return false; - } + } } unsigned max_column = rows[0].size(); bool change = true; @@ -579,7 +576,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( if (j == live.size()) { continue; } - + change = true; // found gcd, now identify reduced set of rows with GCD = 1. g = abs(rows[live[j]][i]); @@ -592,7 +589,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( useful.push_back(gcd_pos[j]); g = gcd(g, gcds[j]); SASSERT(j == 0 || gcd(g,gcds[j-1]).is_one()); - } + } } // // we now have a set "useful" of rows whose combined GCD = 1. @@ -600,7 +597,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( // row& r0 = rows[useful[0]]; for (j = 1; j < useful.size(); ++j) { - row& r1 = rows[useful[j]]; + row& r1 = rows[useful[j]]; g = gcd(r0[i], r1[i], u, v); for (unsigned k = 0; k < max_column; ++k) { r0[k] = u*r0[k] + v*r1[k]; @@ -626,7 +623,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( } } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << ((live.size()<=1)?"solved ":"incomplete check ") << live.size() << "\n"; for (unsigned i = 0; i < live.size(); ++i) { print_row(tout, rows[live[i]]); diff --git a/src/smt/arith_eq_solver.h b/src/smt/arith_eq_solver.h index b2db35ee1..68e58334d 100644 --- a/src/smt/arith_eq_solver.h +++ b/src/smt/arith_eq_solver.h @@ -12,7 +12,7 @@ Abstract: Author: Nikolaj Bjorner (nbjorner) 2012-02-25 - + --*/ #ifndef ARITH_EQ_SOLVER_H_ #define ARITH_EQ_SOLVER_H_ @@ -35,45 +35,45 @@ class arith_eq_solver { void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result); - bool gcd_test(vector& value); + bool gcd_test(vector& values); unsigned find_abs_min(vector& values); void gcd_normalize(vector& values); void substitute(vector& r, vector const& s, unsigned index); bool solve_integer_equations_units( - vector > & rows, + vector > & rows, vector& unsat_row ); - + bool solve_integer_equations_omega( - vector > & rows, + vector > & rows, vector& unsat_row ); void compute_hnf(vector >& A); bool solve_integer_equations_hermite( - vector > & rows, + vector > & rows, vector& unsat_row ); bool solve_integer_equations_gcd( - vector > & rows, + vector > & rows, vector& unsat_row ); public: arith_eq_solver(ast_manager & m, params_ref const& p = params_ref()); - ~arith_eq_solver(); + ~arith_eq_solver() = default; // Integer linear solver for a single equation. // The array values contains integer coefficients - // + // // Determine integer solutions to: // // a+k = 0 // // where a = sum_i a_i*k_i - // + // typedef vector row; typedef vector matrix; @@ -90,14 +90,14 @@ public: // a+k = 0 // // where a = sum_i a_i*k_i - // + // // Solution, if there is any, is returned as a substitution. // The return value is "true". // If there is no solution, then return "false". // together with equality "eq_unsat", such that // // eq_unsat = 0 - // + // // is implied and is unsatisfiable over the integers. //