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