1 /******************************************
2 Copyright (c) 2018  Mate Soos
3 Copyright (c) 2012  Cheng-Shen Han
4 Copyright (c) 2012  Jie-Hong Roland Jiang
5 
6 For more information, see " When Boolean Satisfiability Meets Gaussian
7 Elimination in a Simplex Way." by Cheng-Shen Han and Jie-Hong Roland Jiang
8 in CAV (Computer Aided Verification), 2012: 410-426
9 
10 
11 Permission is hereby granted, free of charge, to any person obtaining a copy
12 of this software and associated documentation files (the "Software"), to deal
13 in the Software without restriction, including without limitation the rights
14 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
15 copies of the Software, and to permit persons to whom the Software is
16 furnished to do so, subject to the following conditions:
17 
18 The above copyright notice and this permission notice shall be included in
19 all copies or substantial portions of the Software.
20 
21 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
22 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
25 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
26 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
27 THE SOFTWARE.
28 ***********************************************/
29 
30 #ifndef PACKEDMATRIX_H
31 #define PACKEDMATRIX_H
32 
33 #include <algorithm>
34 #include <cstdint>
35 #include "packedrow.h"
36 
37 //#define DEBUG_MATRIX
38 
39 namespace CMSat {
40 
41 class PackedMatrix
42 {
43 public:
PackedMatrix()44     PackedMatrix() :
45         mp(NULL)
46         , numRows(0)
47         , numCols(0)
48     {
49     }
50 
~PackedMatrix()51     ~PackedMatrix()
52     {
53         #ifdef _MSC_VER
54         _aligned_free((void*)mp);
55         #else
56         free(mp);
57         #endif
58     }
59 
resize(const uint32_t num_rows,uint32_t num_cols)60     void resize(const uint32_t num_rows, uint32_t num_cols)
61     {
62         num_cols = num_cols / 64 + (bool)(num_cols % 64);
63         if (numRows*(numCols+1) < (int)num_rows*((int)num_cols+1)) {
64             size_t size = sizeof(int64_t) * num_rows*(num_cols+1);
65             #ifdef _MSC_VER
66             _aligned_free((void*)mp);
67             mp =  (int64_t*)_aligned_malloc(size, 16);
68             #else
69             free(mp);
70             posix_memalign((void**)&mp, 16,  size);
71             #endif
72         }
73 
74         numRows = num_rows;
75         numCols = num_cols;
76     }
77 
resizeNumRows(const uint32_t num_rows)78     void resizeNumRows(const uint32_t num_rows)
79     {
80         assert((int)num_rows <= numRows);
81         numRows = num_rows;
82     }
83 
84     PackedMatrix& operator=(const PackedMatrix& b)
85     {
86         if (numRows*(numCols+1) < b.numRows*(b.numCols+1)) {
87             size_t size = sizeof(int64_t) * b.numRows*(b.numCols+1);
88             #ifdef _MSC_VER
89             _aligned_free((void*)mp);
90             mp =  (int64_t*)_aligned_malloc(size, 16);
91             #else
92             free(mp);
93             posix_memalign((void**)&mp, 16,  size);
94             #endif
95         }
96         numRows = b.numRows;
97         numCols = b.numCols;
98         memcpy(mp, b.mp, sizeof(int)*numRows*(numCols+1));
99 
100         return *this;
101     }
102 
103     inline PackedRow operator[](const uint32_t i)
104     {
105         #ifdef DEBUG_MATRIX
106         assert(i <= numRows);
107         #endif
108 
109         return PackedRow(numCols, mp+i*(numCols+1));
110 
111     }
112 
113     inline PackedRow operator[](const uint32_t i) const
114     {
115         #ifdef DEBUG_MATRIX
116         assert(i <= numRows);
117         #endif
118 
119         return PackedRow(numCols, mp+i*(numCols+1));
120     }
121 
122     class iterator
123     {
124     public:
125         friend class PackedMatrix;
126 
127         PackedRow operator*()
128         {
129             return PackedRow(numCols, mp);
130         }
131 
132         iterator& operator++()
133         {
134             mp += (numCols+1);
135             return *this;
136         }
137 
138         iterator operator+(const uint32_t num) const
139         {
140             iterator ret(*this);
141             ret.mp += (numCols+1)*num;
142             return ret;
143         }
144 
145         uint32_t operator-(const iterator& b) const
146         {
147             return (mp - b.mp)/((numCols+1));
148         }
149 
150         void operator+=(const uint32_t num)
151         {
152             mp += (numCols+1)*num;  // add by f4
153         }
154 
155         bool operator!=(const iterator& it) const
156         {
157             return mp != it.mp;
158         }
159 
160         bool operator==(const iterator& it) const
161         {
162             return mp == it.mp;
163         }
164 
165     private:
iterator(int64_t * _mp,const uint32_t _numCols)166         iterator(int64_t* _mp, const uint32_t _numCols) :
167             mp(_mp)
168             , numCols(_numCols)
169         {}
170 
171         int64_t *mp;
172         const uint32_t numCols;
173     };
174 
begin()175     inline iterator begin()
176     {
177         return iterator(mp, numCols);
178     }
179 
end()180     inline iterator end()
181     {
182         return iterator(mp+numRows*(numCols+1), numCols);
183     }
184 
getSize()185     inline uint32_t getSize() const
186     {
187         return numRows;
188     }
189 
190 private:
191 
192     int64_t *mp;
193     int numRows;
194     int numCols;
195 };
196 
197 }
198 
199 #endif //PACKEDMATRIX_H
200