mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

[NFC] Cleanup arith_eq_solver.(cpp|h)

Browse source 
Use for-range loops instead of for-index loops where possible, remove
trailing whitespaces.

This patch does not affect functionality.
This commit is contained in:
Kirill Bobyrev 2018-10-02 16:14:01 +03:00
parent 620c5d1d81
commit a376a8d343
2 changed files with 78 additions and 81 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/arith_eq_solver.h
View file

@ -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<numeral>& value);
bool gcd_test(vector<numeral>& values);
unsigned find_abs_min(vector<numeral>& values);
void gcd_normalize(vector<numeral>& values);
void substitute(vector<numeral>& r, vector<numeral> const& s, unsigned index);
bool solve_integer_equations_units(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
bool solve_integer_equations_omega(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
void compute_hnf(vector<vector<numeral> >& A);
bool solve_integer_equations_hermite(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
bool solve_integer_equations_gcd(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& 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<numeral> row;
typedef vector<row> 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.
//