mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
7387fc9dec
commit
180fb3abf6
1 changed files with 49 additions and 68 deletions
|
|
@ -30,10 +30,10 @@ inline void addmul(mpq& r, mpq const& a, mpq const& b) { r.addmul(a, b); }
|
|||
template <typename T, typename X>
|
||||
void static_matrix<T, X>::init_row_columns(unsigned m, unsigned n) {
|
||||
lp_assert(m_rows.size() == 0 && m_columns.size() == 0);
|
||||
for (unsigned i = 0; i < m; i++){
|
||||
for (unsigned i = 0; i < m; i++) {
|
||||
m_rows.push_back(row_strip<T>());
|
||||
}
|
||||
for (unsigned j = 0; j < n; j++){
|
||||
for (unsigned j = 0; j < n; j++) {
|
||||
m_columns.push_back(column_strip());
|
||||
}
|
||||
}
|
||||
|
|
@ -88,14 +88,12 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * /* basis *
|
|||
m_vector_of_row_offsets(A.column_count(), numeric_traits<T>::zero()) {
|
||||
unsigned m = A.row_count();
|
||||
init_row_columns(m, m);
|
||||
while (m--) {
|
||||
for (auto & col : A.m_columns[m]){
|
||||
for (; m-- > 0; )
|
||||
for (auto & col : A.m_columns[m])
|
||||
set(col.var(), m, A.get_value_of_column_cell(col));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::clear() {
|
||||
template <typename T, typename X> void static_matrix<T, X>::clear() {
|
||||
m_vector_of_row_offsets.clear();
|
||||
m_rows.clear();
|
||||
m_columns.clear();
|
||||
|
|
@ -106,12 +104,12 @@ template <typename T, typename X> void static_matrix<T, X>::init_vector_of_row_o
|
|||
m_vector_of_row_offsets.resize(column_count(), -1);
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::init_empty_matrix(unsigned m, unsigned n) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::init_empty_matrix(unsigned m, unsigned n) {
|
||||
init_vector_of_row_offsets();
|
||||
init_row_columns(m, n);
|
||||
}
|
||||
|
||||
template <typename T, typename X> unsigned static_matrix<T, X>::lowest_row_in_column(unsigned col) {
|
||||
template <typename T, typename X> unsigned static_matrix<T, X>::lowest_row_in_column(unsigned col) {
|
||||
lp_assert(col < column_count());
|
||||
column_strip & colstrip = m_columns[col];
|
||||
lp_assert(colstrip.size() > 0);
|
||||
|
|
@ -124,15 +122,15 @@ template <typename T, typename X> unsigned static_matrix<T, X>::lowest_row_in
|
|||
return ret;
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::add_columns_at_the_end(unsigned delta) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::add_columns_at_the_end(unsigned delta) {
|
||||
for (unsigned i = 0; i < delta; i++)
|
||||
add_column();
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::forget_last_columns(unsigned how_many_to_forget) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::forget_last_columns(unsigned how_many_to_forget) {
|
||||
lp_assert(m_columns.size() >= how_many_to_forget);
|
||||
unsigned j = column_count() - 1;
|
||||
for (; how_many_to_forget > 0; how_many_to_forget--) {
|
||||
for (; how_many_to_forget-- > 0; ) {
|
||||
remove_last_column(j --);
|
||||
}
|
||||
}
|
||||
|
|
@ -154,15 +152,12 @@ template <typename T, typename X> void static_matrix<T, X>::remove_last_column(u
|
|||
m_vector_of_row_offsets.pop_back();
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::set(unsigned row, unsigned col, T const & val) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::set(unsigned row, unsigned col, T const & val) {
|
||||
if (numeric_traits<T>::is_zero(val)) return;
|
||||
lp_assert(row < row_count() && col < column_count());
|
||||
auto & r = m_rows[row];
|
||||
unsigned offs_in_cols = static_cast<unsigned>(m_columns[col].size());
|
||||
m_columns[col].push_back(make_column_cell(row, static_cast<unsigned>(r.size())));
|
||||
unsigned offs_in_cols = m_columns[col].size();
|
||||
m_columns[col].push_back(make_column_cell(row, r.size()));
|
||||
r.push_back(make_row_cell(col, offs_in_cols, val));
|
||||
}
|
||||
|
||||
|
|
@ -170,15 +165,14 @@ template <typename T, typename X>
|
|||
std::set<std::pair<unsigned, unsigned>> static_matrix<T, X>::get_domain() {
|
||||
std::set<std::pair<unsigned, unsigned>> ret;
|
||||
for (unsigned i = 0; i < m_rows.size(); i++) {
|
||||
for (auto &it : m_rows[i]) {
|
||||
ret.insert(std::make_pair(i, it.var()));
|
||||
for (auto &cell : m_rows[i]) {
|
||||
ret.insert(std::make_pair(i, cell.var()));
|
||||
}
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::copy_column_to_indexed_vector (unsigned j, indexed_vector<T> & v) const {
|
||||
template <typename T, typename X> void static_matrix<T, X>::copy_column_to_indexed_vector (unsigned j, indexed_vector<T> & v) const {
|
||||
lp_assert(j < m_columns.size());
|
||||
for (auto & it : m_columns[j]) {
|
||||
const T& val = get_val(it);
|
||||
|
|
@ -187,20 +181,18 @@ template <typename T, typename X> void static_matrix<T, X>::copy_column_to_in
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_row(unsigned row) const {
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_row(unsigned row) const {
|
||||
T ret = numeric_traits<T>::zero();
|
||||
for (auto & t : m_rows[row]) {
|
||||
T a = abs(t.coeff());
|
||||
if (a > ret) {
|
||||
if (a > ret) {
|
||||
ret = a;
|
||||
}
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_row(unsigned row) const {
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_row(unsigned row) const {
|
||||
bool first_time = true;
|
||||
T ret = numeric_traits<T>::zero();
|
||||
for (auto & t : m_rows[row]) {
|
||||
|
|
@ -208,7 +200,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_row(u
|
|||
if (first_time) {
|
||||
ret = a;
|
||||
first_time = false;
|
||||
} else if (a < ret) {
|
||||
} else if (a < ret) {
|
||||
ret = a;
|
||||
}
|
||||
}
|
||||
|
|
@ -216,18 +208,18 @@ template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_row(u
|
|||
}
|
||||
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_column(unsigned column) const {
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_column(unsigned column) const {
|
||||
T ret = numeric_traits<T>::zero();
|
||||
for (const auto & t : m_columns[column]) {
|
||||
T a = abs(get_val(t));
|
||||
if (a > ret) {
|
||||
if (a > ret) {
|
||||
ret = a;
|
||||
}
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_column(unsigned column) const {
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_column(unsigned column) const {
|
||||
bool first_time = true;
|
||||
T ret = numeric_traits<T>::zero();
|
||||
for (auto & t : m_columns[column]) {
|
||||
|
|
@ -235,7 +227,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_colu
|
|||
if (first_time) {
|
||||
first_time = false;
|
||||
ret = a;
|
||||
} else if (a < ret) {
|
||||
} else if (a < ret) {
|
||||
ret = a;
|
||||
}
|
||||
}
|
||||
|
|
@ -243,9 +235,9 @@ template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_colu
|
|||
}
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
template <typename T, typename X> void static_matrix<T, X>::check_consistency() {
|
||||
template <typename T, typename X> void static_matrix<T, X>::check_consistency() {
|
||||
std::unordered_map<std::pair<unsigned, unsigned>, T> by_rows;
|
||||
for (int i = 0; i < m_rows.size(); i++){
|
||||
for (unsigned i = 0; i < m_rows.size(); i++) {
|
||||
for (auto & t : m_rows[i]) {
|
||||
std::pair<unsigned, unsigned> p(i, t.var());
|
||||
lp_assert(by_rows.find(p) == by_rows.end());
|
||||
|
|
@ -253,7 +245,7 @@ template <typename T, typename X> void static_matrix<T, X>::check_consistency
|
|||
}
|
||||
}
|
||||
std::unordered_map<std::pair<unsigned, unsigned>, T> by_cols;
|
||||
for (int i = 0; i < m_columns.size(); i++){
|
||||
for (unsigned i = 0; i < m_columns.size(); i++) {
|
||||
for (auto & t : m_columns[i]) {
|
||||
std::pair<unsigned, unsigned> p(t.var(), i);
|
||||
lp_assert(by_cols.find(p) == by_cols.end());
|
||||
|
|
@ -271,7 +263,7 @@ template <typename T, typename X> void static_matrix<T, X>::check_consistency
|
|||
#endif
|
||||
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::cross_out_row(unsigned k) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::cross_out_row(unsigned k) {
|
||||
#ifdef Z3DEBUG
|
||||
check_consistency();
|
||||
#endif
|
||||
|
|
@ -284,25 +276,20 @@ template <typename T, typename X> void static_matrix<T, X>::cross_out_row(uns
|
|||
#endif
|
||||
}
|
||||
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::fix_row_indices_in_each_column_for_crossed_row(unsigned k) {
|
||||
for (unsigned j = 0; j < m_columns.size(); j++) {
|
||||
auto & col = m_columns[j];
|
||||
for (int i = 0; i < col.size(); i++) {
|
||||
if (col[i].var() > k) {
|
||||
col[i].var()--;
|
||||
}
|
||||
}
|
||||
}
|
||||
template <typename T, typename X> void static_matrix<T, X>::fix_row_indices_in_each_column_for_crossed_row(unsigned k) {
|
||||
for (auto & column : m_columns)
|
||||
for (auto& cell : column)
|
||||
if (cell.var() > k)
|
||||
cell.var()--;
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::cross_out_row_from_columns(unsigned k, row_strip<T> & row) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::cross_out_row_from_columns(unsigned k, row_strip<T> & row) {
|
||||
for (auto & t : row) {
|
||||
cross_out_row_from_column(t.var(), k);
|
||||
}
|
||||
}
|
||||
|
||||
template <typename T, typename X> void static_matrix<T, X>::cross_out_row_from_column(unsigned col, unsigned k) {
|
||||
template <typename T, typename X> void static_matrix<T, X>::cross_out_row_from_column(unsigned col, unsigned k) {
|
||||
auto & s = m_columns[col];
|
||||
for (unsigned i = 0; i < s.size(); i++) {
|
||||
if (s[i].var() == k) {
|
||||
|
|
@ -312,7 +299,7 @@ template <typename T, typename X> void static_matrix<T, X>::cross_out_row_fro
|
|||
}
|
||||
}
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_elem(unsigned i, unsigned j) const { // should not be used in efficient code !!!!
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_elem(unsigned i, unsigned j) const { // should not be used in efficient code !!!!
|
||||
for (auto & t : m_rows[i]) {
|
||||
if (t.var() == j) {
|
||||
return t.coeff();
|
||||
|
|
@ -321,8 +308,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_elem(unsigned i,
|
|||
return numeric_traits<T>::zero();
|
||||
}
|
||||
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_balance() const {
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_balance() const {
|
||||
T ret = zero_of_type<T>();
|
||||
for (unsigned i = 0; i < row_count(); i++) {
|
||||
ret += get_row_balance(i);
|
||||
|
|
@ -330,7 +316,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_balance() const
|
|||
return ret;
|
||||
}
|
||||
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_row_balance(unsigned row) const {
|
||||
template <typename T, typename X> T static_matrix<T, X>::get_row_balance(unsigned row) const {
|
||||
T ret = zero_of_type<T>();
|
||||
for (auto & t : m_rows[row]) {
|
||||
if (numeric_traits<T>::is_zero(t.coeff())) continue;
|
||||
|
|
@ -342,13 +328,11 @@ template <typename T, typename X> T static_matrix<T, X>::get_row_balance(unsi
|
|||
}
|
||||
|
||||
template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
|
||||
for (unsigned i = 0; i < m_rows.size(); i++) {
|
||||
auto &r = m_rows[i];
|
||||
for (auto & row : m_rows) {
|
||||
std::unordered_set<unsigned> s;
|
||||
for (auto & rc : r) {
|
||||
if (s.find(rc.var()) != s.end()) {
|
||||
for (auto & rc : row) {
|
||||
if (s.find(rc.var()) != s.end())
|
||||
return false;
|
||||
}
|
||||
s.insert(rc.var());
|
||||
if (rc.var() >= m_columns.size())
|
||||
return false;
|
||||
|
|
@ -356,20 +340,16 @@ template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
|
|||
return false;
|
||||
if (rc.coeff() != get_val(m_columns[rc.var()][rc.offset()]))
|
||||
return false;
|
||||
if (is_zero(rc.coeff())) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if (is_zero(rc.coeff()))
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned j = 0; j < m_columns.size(); j++) {
|
||||
auto & c = m_columns[j];
|
||||
for (auto & column : m_columns) {
|
||||
std::unordered_set<unsigned> s;
|
||||
for (auto & cc : c) {
|
||||
if (s.find(cc.var()) != s.end()) {
|
||||
for (auto & cc : column) {
|
||||
if (s.find(cc.var()) != s.end())
|
||||
return false;
|
||||
}
|
||||
s.insert(cc.var());
|
||||
if (cc.var() >= m_rows.size())
|
||||
return false;
|
||||
|
|
@ -401,12 +381,13 @@ void static_matrix<T, X>::remove_element(vector<row_cell<T>> & row_vals, row_cel
|
|||
column_vals.pop_back();
|
||||
row_vals.pop_back();
|
||||
}
|
||||
|
||||
template <typename T, typename X>
|
||||
void static_matrix<T, X>::add_new_element(unsigned row, unsigned col, const T& val) {
|
||||
auto & row_vals = m_rows[row];
|
||||
auto & col_vals = m_columns[col];
|
||||
unsigned row_el_offs = static_cast<unsigned>(row_vals.size());
|
||||
unsigned col_el_offs = static_cast<unsigned>(col_vals.size());
|
||||
unsigned row_el_offs = row_vals.size();
|
||||
unsigned col_el_offs = col_vals.size();
|
||||
row_vals.push_back(row_cell<T>(col, col_el_offs, val));
|
||||
col_vals.push_back(column_cell(row, row_el_offs));
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue