1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #ifndef _XORFINDER_H_
24 #define _XORFINDER_H_
25
26 #include <vector>
27 #include <set>
28 #include <iostream>
29 #include <algorithm>
30 #include <set>
31 #include <limits>
32 #include "constants.h"
33 #include "xor.h"
34 #include "cset.h"
35 #include "watcharray.h"
36
37 using std::vector;
38 using std::set;
39
40 namespace CMSat {
41
42 //#define VERBOSE_DEBUG_XOR_FINDER
43
44 class Solver;
45 class OccSimplifier;
46
47 class PossibleXor
48 {
49 public:
PossibleXor()50 PossibleXor()
51 {
52 }
53
setup(const vector<Lit> & cl,const ClOffset offset,cl_abst_type _abst,vector<uint32_t> & seen)54 void setup(
55 const vector<Lit>& cl
56 , const ClOffset offset
57 , cl_abst_type _abst
58 , vector<uint32_t>& seen
59 ) {
60 abst = _abst;
61 size = cl.size();
62 offsets.clear();
63 fully_used.clear();
64 #ifdef VERBOSE_DEBUG_XOR_FINDER
65 cout << "Trying to create XOR from clause: " << cl << endl;
66 #endif
67
68 assert(cl.size() <= sizeof(origCl)/sizeof(Lit)
69 && "The XOR being recovered is larger than MAX_XOR_RECOVER_SIZE");
70 for(size_t i = 0; i < size; i++) {
71 origCl[i] = cl[i];
72 if (i > 0)
73 assert(cl[i-1] < cl[i]);
74 }
75 setup_seen_rhs_foundcomb(seen);
76 if (offset != std::numeric_limits<ClOffset>::max()) {
77 //this is the XOR that starts it all
78 //so it's fully used
79 offsets.push_back(offset);
80 fully_used.push_back(true);
81 }
82 }
83
clear_seen(vector<uint32_t> & seen)84 void clear_seen(vector<uint32_t>& seen)
85 {
86 for (uint32_t i = 0; i < size; i++) {
87 seen[origCl[i].var()] = 0;
88 }
89 }
90
91 //GET-type functions
92 cl_abst_type getAbst() const;
93 uint32_t getSize() const;
94 bool getRHS() const;
95 bool foundAll() const;
96
97 //Add
98 template<class T>
99 void add(const T& cl, const ClOffset offset, vector<uint32_t>& varsMissing);
100
get_offsets()101 const vector<ClOffset>& get_offsets() const
102 {
103 return offsets;
104 }
105
get_fully_used()106 const vector<char>& get_fully_used() const
107 {
108 return fully_used;
109 }
110
111 private:
setup_seen_rhs_foundcomb(vector<uint32_t> & seen)112 void setup_seen_rhs_foundcomb(vector<uint32_t>& seen)
113 {
114 //Calculate parameters of base clause.
115 //Also set 'seen' for easy check in 'findXorMatch()'
116 rhs = true;
117 uint32_t whichOne = 0;
118 for (uint32_t i = 0; i < size; i++) {
119 rhs ^= origCl[i].sign();
120 whichOne += ((uint32_t)origCl[i].sign()) << i;
121 seen[origCl[i].var()] = 1;
122 }
123
124 foundComb.clear();
125 foundComb.resize(1ULL<<size, false);
126 foundComb[whichOne] = true;
127 }
128 uint32_t NumberOfSetBits(uint32_t i) const;
129 bool bit(const uint32_t a, const uint32_t b) const;
130
131 //bitfield to indicate which of the following is already set
132 //-1 -2 -3
133 //-1 2 3
134 // 1 -2 3
135 // 1 2 -3
136 //order the above according to sign: if sign:
137 //LSB ... MSB
138 // 1 1 1
139 // 1 0 0
140 // 0 1 0
141 // 0 0 1
142 vector<char> foundComb;
143 Lit origCl[MAX_XOR_RECOVER_SIZE];
144 cl_abst_type abst;
145 uint32_t size;
146 bool rhs;
147 vector<ClOffset> offsets;
148 vector<char> fully_used;
149 };
150
151 class XorFinder
152 {
153 public:
154 XorFinder(OccSimplifier* occsimplifier, Solver* solver);
155 void find_xors();
156
157 struct Stats
158 {
clearStats159 void clear()
160 {
161 Stats tmp;
162 *this = tmp;
163 }
164
165 Stats& operator+=(const Stats& other);
166 void print_short(const Solver* solver, const double time_remain) const;
167
168 //Time
169 uint32_t numCalls = 0;
170 double findTime = 0.0;
171 uint32_t time_outs = 0;
172
173 //XOR stats
174 uint64_t foundXors = 0;
175 uint64_t sumSizeXors = 0;
176 uint32_t minsize = std::numeric_limits<uint32_t>::max();
177 uint32_t maxsize = std::numeric_limits<uint32_t>::min();
178 };
179
180 const Stats& get_stats() const;
181 size_t mem_used() const;
182 void grab_mem();
183 vector<Xor> remove_xors_without_connecting_vars(const vector<Xor>& this_xors);
184 bool xor_together_xors(vector<Xor>& xors);
185 bool add_new_truths_from_xors(vector<Xor>& xors, vector<Lit>* out_changed_occur = NULL);
186 void clean_equivalent_xors(vector<Xor>& txors);
187
188 vector<Xor>& xors;
189 vector<Xor>& unused_xors;
190
191 private:
192 PossibleXor poss_xor;
193 void add_found_xor(const Xor& found_xor);
194 void find_xors_based_on_long_clauses();
195 void print_found_xors();
196 bool xor_has_interesting_var(const Xor& x);
197 void clean_xors_from_empty(vector<Xor>& thisxors);
198
199 ///xor two -- don't re-allocate memory all the time
200 ///use tmp_vars_xor_two instead
201 uint32_t xor_two(Xor const* x1, Xor const* x2, uint32_t& clash_var);
202 vector<uint32_t> tmp_vars_xor_two;
203
204 int64_t xor_find_time_limit;
205
206 //Find XORs
207 void findXor(vector<Lit>& lits, const ClOffset offset, cl_abst_type abst);
208
209 ///Normal finding of matching clause for XOR
210 void findXorMatch(watch_subarray_const occ, const Lit wlit);
211
212 OccSimplifier* occsimplifier;
213 Solver *solver;
214
215 //Stats
216 Stats runStats;
217 Stats globalStats;
218
219 //Temporary
220 vector<Lit> tmpClause;
221 vector<uint32_t> varsMissing;
222 vector<Lit> binvec;
223
224 //Other temporaries
225 vector<uint32_t> occcnt;
226 vector<Lit>& toClear;
227 vector<uint16_t>& seen;
228 vector<uint8_t>& seen2;
229 vector<uint32_t> interesting;
230 };
231
232
getAbst()233 inline cl_abst_type PossibleXor::getAbst() const
234 {
235 return abst;
236 }
237
getSize()238 inline uint32_t PossibleXor::getSize() const
239 {
240 return size;
241 }
242
getRHS()243 inline bool PossibleXor::getRHS() const
244 {
245 return rhs;
246 }
247
add(const T & cl,const ClOffset offset,vector<uint32_t> & varsMissing)248 template<class T> void PossibleXor::add(
249 const T& cl
250 , const ClOffset offset
251 , vector<uint32_t>& varsMissing
252 ) {
253 #ifdef VERBOSE_DEBUG_XOR_FINDER
254 cout << "Adding to XOR: " << cl << endl;
255
256 cout << "FoundComb before:" << endl;
257 for(size_t i = 0; i < foundComb.size(); i++) {
258 cout << "foundComb[" << i << "]: " << (int)foundComb[i] << endl;
259 }
260 cout << "----" << endl;
261 #endif
262
263 //It's the base clause, skip.
264 if (!offsets.empty() && offset == offsets[0])
265 return;
266
267 assert(cl.size() <= size);
268
269 //If clause covers more than one combination, this is used to calculate which ones
270 varsMissing.clear();
271
272 //Position of literal in the ORIGINAL clause.
273 //This may be larger than the position in the current clause (as some literals could be missing)
274 uint32_t origI = 0;
275
276 //Position in current clause
277 uint32_t i = 0;
278
279 //Used to calculate this clause covers which combination(s)
280 uint32_t whichOne = 0;
281
282 bool thisRhs = true;
283
284 for (typename T::const_iterator
285 l = cl.begin(), end = cl.end()
286 ; l != end
287 ; l++, i++, origI++
288 ) {
289 thisRhs ^= l->sign();
290
291 //some variables might be missing in the middle
292 while(cl[i].var() != origCl[origI].var()) {
293 varsMissing.push_back(origI);
294 origI++;
295 assert(origI < size && "cl must be sorted");
296 }
297 if (i > 0) {
298 assert(cl[i-1] < cl[i] && "Must be sorted");
299 }
300 whichOne |= ((uint32_t)l->sign()) << origI;
301 }
302
303 //if vars are missing from the end
304 while(origI < size) {
305 varsMissing.push_back(origI);
306 origI++;
307 }
308
309 assert(cl.size() < size || rhs == thisRhs);
310
311 //set to true every combination for the missing variables
312 for (uint32_t j = 0; j < 1UL<<(varsMissing.size()); j++) {
313 uint32_t thisWhichOne = whichOne;
314 for (uint32_t i2 = 0; i2 < varsMissing.size(); i2++) {
315 if (bit(j, i2)) thisWhichOne+= 1<<(varsMissing[i2]);
316 }
317 foundComb[thisWhichOne] = true;
318 }
319 if (offset != std::numeric_limits<ClOffset>::max()) {
320 offsets.push_back(offset);
321 fully_used.push_back(varsMissing.empty());
322 }
323
324 #ifdef VERBOSE_DEBUG_XOR_FINDER
325 cout << "whichOne was:" << whichOne << endl;
326 cout << "FoundComb after:" << endl;
327 for(size_t i = 0; i < foundComb.size(); i++) {
328 cout << "foundComb[" << i << "]: " << foundComb[i] << endl;
329 }
330 cout << "----" << endl;
331 #endif
332 }
333
foundAll()334 inline bool PossibleXor::foundAll() const
335 {
336 bool OK = true;
337 for (uint32_t i = 0; i < foundComb.size(); i++) {
338 //Only count combinations with the correct RHS
339 if ((NumberOfSetBits(i)%2) == (uint32_t)rhs) {
340 continue;
341 }
342
343 //If this combination hasn't been found yet, then the XOR is not complete
344 if (!foundComb[i]) {
345 OK = false;
346 break;
347 }
348 }
349
350 #ifdef VERBOSE_DEBUG_XOR_FINDER
351 if (OK) {
352 cout << "Found all for this clause" << endl;
353 }
354 #endif
355
356 return OK;
357 }
358
NumberOfSetBits(uint32_t i)359 inline uint32_t PossibleXor::NumberOfSetBits(uint32_t i) const
360 {
361 //Magic is coming! (copied from some book.... never trust code like this!)
362 i = i - ((i >> 1) & 0x55555555);
363 i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
364 return (((i + (i >> 4)) & 0xF0F0F0F) * 0x1010101) >> 24;
365 }
366
bit(const uint32_t a,const uint32_t b)367 inline bool PossibleXor::bit(const uint32_t a, const uint32_t b) const
368 {
369 return (((a)>>(b))&1);
370 }
371
get_stats()372 inline const XorFinder::Stats& XorFinder::get_stats() const
373 {
374 return globalStats;
375 }
376
377 } //end namespace
378
379 #endif //_XORFINDER_H_
380