1 /*++ 2 Copyright (c) 2017 Microsoft Corporation 3 4 Module Name: 5 6 <name> 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Lev Nachmanson (levnach) 15 16 Revision History: 17 18 19 --*/ 20 21 #pragma once 22 #include "util/vector.h" 23 #include "util/debug.h" 24 #include <string> 25 #include <iomanip> 26 #include "math/lp/lp_utils.h" 27 #include "math/lp/lp_settings.h" 28 #include <unordered_set> 29 namespace lp { 30 31 template <typename T> void print_sparse_vector(const vector<T> & t, std::ostream & out); 32 33 void print_vector_as_doubles(const vector<mpq> & t, std::ostream & out); 34 template <typename T> 35 class indexed_vector { 36 public: 37 // m_index points to non-zero elements of m_data 38 vector<T> m_data; 39 vector<unsigned> m_index; indexed_vector(unsigned data_size)40 indexed_vector(unsigned data_size) { 41 m_data.resize(data_size, numeric_traits<T>::zero()); 42 } 43 44 indexed_vector& operator=(const indexed_vector<T>& y) { 45 for (unsigned i: m_index) 46 m_data[i] = zero_of_type<T>(); 47 48 m_index = y.m_index; 49 50 m_data.resize(y.data_size()); 51 for (unsigned i : m_index) 52 m_data[i] = y[i]; 53 return *this; 54 } 55 56 bool operator==(const indexed_vector<T>& y) const { 57 std::unordered_set<unsigned> y_index; 58 for (unsigned i : y.m_index) 59 y_index.insert(i); 60 61 std::unordered_set<unsigned> this_index; 62 for (unsigned i : m_index) 63 this_index.insert(i); 64 65 for (unsigned i : y.m_index) { 66 if (this_index.find(i) == this_index.end()) 67 return false; 68 } 69 70 for (unsigned i : m_index) { 71 if (y_index.find(i) == y_index.end()) 72 return false; 73 } 74 75 return vectors_are_equal(m_data, m_data); 76 77 } 78 indexed_vector()79 indexed_vector() {} 80 81 void resize(unsigned data_size); data_size()82 unsigned data_size() const { 83 return m_data.size(); 84 } 85 size()86 unsigned size() const { 87 return m_index.size(); 88 } 89 90 void set_value(const T& value, unsigned index); 91 92 void clear(); 93 void clear_all(); 94 const T& operator[] (unsigned i) const { 95 return m_data[i]; 96 } 97 98 T& operator[] (unsigned i) { 99 return m_data[i]; 100 } 101 clean_up()102 void clean_up() { 103 #if 0==1 104 for (unsigned k = 0; k < m_index.size(); k++) { 105 unsigned i = m_index[k]; 106 T & v = m_data[i]; 107 if (lp_settings::is_eps_small_general(v, 1e-14)) { 108 v = zero_of_type<T>(); 109 m_index.erase(m_index.begin() + k--); 110 } 111 } 112 #endif 113 vector<unsigned> index_copy; 114 for (unsigned i : m_index) { 115 T & v = m_data[i]; 116 if (!lp_settings::is_eps_small_general(v, 1e-14)) { 117 index_copy.push_back(i); 118 } else if (!numeric_traits<T>::is_zero(v)) { 119 v = zero_of_type<T>(); 120 } 121 } 122 m_index = index_copy; 123 } 124 125 126 void erase_from_index(unsigned j); 127 add_value_at_index_with_drop_tolerance(unsigned j,const T & val_to_add)128 void add_value_at_index_with_drop_tolerance(unsigned j, const T& val_to_add) { 129 T & v = m_data[j]; 130 bool was_zero = is_zero(v); 131 v += val_to_add; 132 if (lp_settings::is_eps_small_general(v, 1e-14)) { 133 v = zero_of_type<T>(); 134 if (!was_zero) { 135 erase_from_index(j); 136 } 137 } else { 138 if (was_zero) 139 m_index.push_back(j); 140 } 141 } 142 add_value_at_index(unsigned j,const T & val_to_add)143 void add_value_at_index(unsigned j, const T& val_to_add) { 144 T & v = m_data[j]; 145 bool was_zero = is_zero(v); 146 v += val_to_add; 147 if (is_zero(v)) { 148 if (!was_zero) 149 erase_from_index(j); 150 } else { 151 if (was_zero) 152 m_index.push_back(j); 153 } 154 } 155 restore_index_and_clean_from_data()156 void restore_index_and_clean_from_data() { 157 m_index.resize(0); 158 for (unsigned i = 0; i < m_data.size(); i++) { 159 T & v = m_data[i]; 160 if (lp_settings::is_eps_small_general(v, 1e-14)) { 161 v = zero_of_type<T>(); 162 } else { 163 m_index.push_back(i); 164 } 165 } 166 } 167 168 struct ival { 169 unsigned m_var; 170 const T & m_coeff; ivalival171 ival(unsigned var, const T & val) : m_var(var), m_coeff(val) { 172 } varival173 unsigned var() const { return m_var;} coeffival174 const T & coeff() const { return m_coeff; } deadival175 bool dead() const { return false; } 176 }; 177 178 struct const_iterator { 179 // fields 180 const unsigned *m_i; 181 const indexed_vector& m_v; 182 183 //typedefs 184 185 186 typedef const_iterator self_type; 187 typedef ival value_type; 188 typedef const ival reference; 189 // typedef const column_cell* pointer; 190 typedef int difference_type; 191 typedef std::forward_iterator_tag iterator_category; 192 193 reference operator*() const { 194 return ival(*m_i, m_v[*m_i]); 195 } 196 self_type operator++() { self_type i = *this; m_i++; return i; } 197 self_type operator++(int) { m_i++; return *this; } 198 const_iteratorconst_iterator199 const_iterator(const unsigned* it, const indexed_vector& v) : 200 m_i(it), 201 m_v(v) 202 {} 203 bool operator==(const self_type &other) const { 204 return m_i == other.m_i; 205 } 206 bool operator!=(const self_type &other) const { return !(*this == other); } 207 }; 208 begin()209 const_iterator begin() const { 210 return const_iterator(m_index.begin(), *this); 211 } 212 end()213 const_iterator end() const { 214 return const_iterator(m_index.end(), *this); 215 } 216 217 218 #ifdef Z3DEBUG 219 bool is_OK() const; 220 #endif 221 void print(std::ostream & out); 222 }; 223 } 224