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 #include "clausecleaner.h"
24 #include "clauseallocator.h"
25 #include "solver.h"
26 #include "cryptominisat5/solvertypesmini.h"
27
28 using namespace CMSat;
29
30 //#define DEBUG_CLEAN
31 //#define VERBOSE_DEBUG
32
ClauseCleaner(Solver * _solver)33 ClauseCleaner::ClauseCleaner(Solver* _solver) :
34 solver(_solver)
35 {
36 }
37
satisfied(const Watched & watched,Lit lit)38 bool ClauseCleaner::satisfied(const Watched& watched, Lit lit)
39 {
40 assert(watched.isBin());
41 if (solver->value(lit) == l_True) return true;
42 if (solver->value(watched.lit2()) == l_True) return true;
43 return false;
44 }
45
clean_binary_implicit(Watched & ws,Watched * & j,const Lit lit)46 void ClauseCleaner::clean_binary_implicit(
47 Watched& ws
48 , Watched*& j
49 , const Lit lit
50 ) {
51 if (satisfied(ws, lit)) {
52 //Only delete once
53 if (lit < ws.lit2()) {
54 (*solver->drat) << del << lit << ws.lit2() << fin;
55 }
56
57 if (ws.red()) {
58 impl_data.remLBin++;
59 } else {
60 impl_data.remNonLBin++;
61 }
62 } else {
63 #ifdef SLOW_DEBUG
64 if (solver->value(ws.lit2()) != l_Undef
65 || solver->value(lit) != l_Undef
66 ) {
67 cout << "ERROR binary during cleaning has non-l-Undef "
68 << " Bin clause: " << lit << " " << ws.lit2() << endl
69 << " values: " << solver->value(lit)
70 << " " << solver->value(ws.lit2())
71 << endl;
72 }
73 #endif
74
75 assert(solver->value(ws.lit2()) == l_Undef);
76 assert(solver->value(lit) == l_Undef);
77 *j++ = ws;
78 }
79 }
80
clean_implicit_watchlist(watch_subarray & watch_list,const Lit lit)81 void ClauseCleaner::clean_implicit_watchlist(
82 watch_subarray& watch_list
83 , const Lit lit
84 ) {
85 Watched* i = watch_list.begin();
86 Watched* j = i;
87 for (Watched* end2 = watch_list.end(); i != end2; i++) {
88 if (i->isClause()) {
89 *j++ = *i;
90 continue;
91 }
92
93 if (i->isBin()) {
94 clean_binary_implicit(*i, j, lit);
95 continue;
96 }
97 }
98 watch_list.shrink_(i - j);
99 }
100
clean_implicit_clauses()101 void ClauseCleaner::clean_implicit_clauses()
102 {
103 if (solver->conf.verbosity > 15) {
104 cout << "c cleaning implicit clauses" << endl;
105 }
106
107 assert(solver->decisionLevel() == 0);
108 impl_data = ImplicitData();
109 size_t wsLit = 0;
110 size_t wsLit2 = 2;
111 for (size_t end = solver->watches.size()
112 ; wsLit != end
113 ; wsLit++, wsLit2++
114 ) {
115 if (wsLit2 < end
116 && !solver->watches[Lit::toLit(wsLit2)].empty()
117 ) {
118 solver->watches.prefetch(Lit::toLit(wsLit2).toInt());
119 }
120
121 const Lit lit = Lit::toLit(wsLit);
122 watch_subarray ws = solver->watches[lit];
123 if (ws.empty())
124 continue;
125
126 clean_implicit_watchlist(ws, lit);
127 }
128 impl_data.update_solver_stats(solver);
129
130 #ifdef DEBUG_IMPLICIT_STATS
131 solver->check_implicit_stats();
132 #endif
133 }
134
clean_clauses_inter(vector<ClOffset> & cs)135 void ClauseCleaner::clean_clauses_inter(vector<ClOffset>& cs)
136 {
137 assert(solver->decisionLevel() == 0);
138 assert(solver->prop_at_head());
139
140 if (solver->conf.verbosity > 15) {
141 cout << "Cleaning clauses in vector<>" << endl;
142 }
143
144 vector<ClOffset>::iterator s, ss, end;
145 size_t at = 0;
146 for (s = ss = cs.begin(), end = cs.end(); s != end; ++s, ++at) {
147 if (at + 1 < cs.size()) {
148 Clause* pre_cl = solver->cl_alloc.ptr(cs[at+1]);
149 __builtin_prefetch(pre_cl);
150 }
151
152 const ClOffset off = *s;
153 Clause& cl = *solver->cl_alloc.ptr(off);
154
155 const Lit origLit1 = cl[0];
156 const Lit origLit2 = cl[1];
157 const auto origSize = cl.size();
158 const bool red = cl.red();
159
160 if (clean_clause(cl)) {
161 solver->watches.smudge(origLit1);
162 solver->watches.smudge(origLit2);
163 cl.setRemoved();
164 if (red) {
165 solver->litStats.redLits -= origSize;
166 } else {
167 solver->litStats.irredLits -= origSize;
168 }
169 delayed_free.push_back(off);
170 } else {
171 *ss++ = *s;
172 }
173 }
174 cs.resize(cs.size() - (s-ss));
175 }
176
clean_clause(Clause & cl)177 bool ClauseCleaner::clean_clause(Clause& cl)
178 {
179 //Don't clean if detached. We'll deal with it during re-attach.
180 if (cl._xor_is_detached) {
181 return false;
182 }
183
184 assert(cl.size() > 2);
185 (*solver->drat) << deldelay << cl << fin;
186
187 #ifdef SLOW_DEBUG
188 uint32_t num_false_begin = 0;
189 Lit l1 = cl[0];
190 Lit l2 = cl[1];
191 num_false_begin += solver->value(cl[0]) == l_False;
192 num_false_begin += solver->value(cl[1]) == l_False;
193 #endif
194
195 Lit *i, *j, *end;
196 uint32_t num = 0;
197 for (i = j = cl.begin(), end = i + cl.size(); i != end; i++, num++) {
198 lbool val = solver->value(*i);
199 if (val == l_Undef) {
200 *j++ = *i;
201 continue;
202 }
203
204 if (val == l_True) {
205 (*solver->drat) << findelay;
206 return true;
207 }
208 }
209 if (i != j) {
210 cl.shrink(i-j);
211 (*solver->drat) << add << cl
212 #ifdef STATS_NEEDED
213 << solver->sumConflicts
214 #endif
215 << fin << findelay;
216 } else {
217 solver->drat->forget_delay();
218 }
219
220 assert(cl.size() != 0);
221 assert(cl.size() != 1);
222 assert(cl.size() > 1);
223 assert(solver->value(cl[0]) == l_Undef);
224 assert(solver->value(cl[1]) == l_Undef);
225
226 #ifdef SLOW_DEBUG
227 //no l_True, so first 2 of orig must have been l_Undef
228 if (num_false_begin != 0) {
229 cout << "val " << l1 << ":" << solver->value(l1) << endl;
230 cout << "val " << l2 << ":" << solver->value(l2) << endl;
231 }
232 assert(num_false_begin == 0 && "Propagation wasn't full? Watch lit was l_False and clause wasn't satisfied");
233 #endif
234
235 if (i != j) {
236 if (cl.size() == 2) {
237 solver->attach_bin_clause(cl[0], cl[1], cl.red());
238 return true;
239 } else {
240 if (cl.red()) {
241 solver->litStats.redLits -= i-j;
242 } else {
243 solver->litStats.irredLits -= i-j;
244 }
245 }
246 }
247
248 return false;
249 }
250
update_solver_stats(Solver * solver)251 void ClauseCleaner::ImplicitData::update_solver_stats(Solver* solver)
252 {
253 for(const BinaryClause& bincl: toAttach) {
254 assert(solver->value(bincl.getLit1()) == l_Undef);
255 assert(solver->value(bincl.getLit2()) == l_Undef);
256 solver->attach_bin_clause(bincl.getLit1(), bincl.getLit2(), bincl.isRed());
257 }
258
259 assert(remNonLBin % 2 == 0);
260 assert(remLBin % 2 == 0);
261 solver->binTri.irredBins -= remNonLBin/2;
262 solver->binTri.redBins -= remLBin/2;
263 }
264
clean_clauses_pre()265 void ClauseCleaner::clean_clauses_pre()
266 {
267 assert(solver->watches.get_smudged_list().empty());
268 assert(delayed_free.empty());
269 }
270
clean_clauses_post()271 void ClauseCleaner::clean_clauses_post()
272 {
273 solver->clean_occur_from_removed_clauses_only_smudged();
274 for(ClOffset off: delayed_free) {
275 solver->free_cl(off);
276 }
277 delayed_free.clear();
278 }
279
remove_and_clean_all()280 void ClauseCleaner::remove_and_clean_all()
281 {
282 double myTime = cpuTime();
283 assert(solver->okay());
284 assert(solver->prop_at_head());
285 assert(solver->decisionLevel() == 0);
286
287 clean_implicit_clauses();
288
289 clean_clauses_pre();
290 clean_clauses_inter(solver->longIrredCls);
291 for(auto& lredcls: solver->longRedCls) {
292 clean_clauses_inter(lredcls);
293 }
294 clean_clauses_post();
295
296
297 #ifndef NDEBUG
298 //Once we have cleaned the watchlists
299 //no watchlist whose lit is set may be non-empty
300 size_t wsLit = 0;
301 for(watch_array::const_iterator
302 it = solver->watches.begin(), end = solver->watches.end()
303 ; it != end
304 ; ++it, wsLit++
305 ) {
306 const Lit lit = Lit::toLit(wsLit);
307 if (solver->value(lit) != l_Undef) {
308 if (!it->empty()) {
309 cout << "ERROR watches size: " << it->size() << endl;
310 for(const auto& w: *it) {
311 cout << "ERROR w: " << w << endl;
312 }
313 }
314 assert(it->empty());
315 }
316 }
317 #endif
318
319 if (solver->conf.verbosity >= 2) {
320 cout
321 << "c [clean]"
322 << solver->conf.print_times(cpuTime() - myTime)
323 << endl;
324 }
325 }
326
327
clean_one_xor(Xor & x)328 bool ClauseCleaner::clean_one_xor(Xor& x)
329 {
330 bool rhs = x.rhs;
331 size_t i = 0;
332 size_t j = 0;
333 for(size_t size = x.size(); i < size; i++) {
334 uint32_t var = x[i];
335 if (solver->value(var) != l_Undef) {
336 rhs ^= solver->value(var) == l_True;
337 } else {
338 x[j++] = var;
339 }
340 }
341 x.resize(j);
342 x.rhs = rhs;
343
344 switch(x.size()) {
345 case 0:
346 solver->ok &= !x.rhs;
347 return false;
348
349 case 1: {
350 solver->fully_enqueue_this(Lit(x[0], !x.rhs));
351 return false;
352 }
353 case 2: {
354 solver->add_xor_clause_inter(vars_to_lits(x), x.rhs, true);
355 return false;
356 }
357 default: {
358 return true;
359 }
360 }
361 }
362
clean_xor_clauses(vector<Xor> & xors)363 bool ClauseCleaner::clean_xor_clauses(vector<Xor>& xors)
364 {
365 assert(solver->ok);
366 #ifdef VERBOSE_DEBUG
367 for(Xor& x : xors) {
368 cout << "orig XOR: " << x << endl;
369 }
370 #endif
371
372 size_t last_trail = std::numeric_limits<size_t>::max();
373 while(last_trail != solver->trail_size()) {
374 last_trail = solver->trail_size();
375 size_t i = 0;
376 size_t j = 0;
377 for(size_t size = xors.size(); i < size; i++) {
378 Xor& x = xors[i];
379 //cout << "Checking to keep xor: " << x << endl;
380 const bool keep = clean_one_xor(x);
381 if (!solver->ok) {
382 return false;
383 }
384
385 if (keep) {
386 xors[j++] = x;
387 } else {
388 solver->removed_xorclauses_clash_vars.insert(
389 solver->removed_xorclauses_clash_vars.end()
390 , x.clash_vars.begin()
391 , x.clash_vars.end()
392 );
393 //cout << "NOT keeping XOR" << endl;
394 }
395 }
396 xors.resize(j);
397
398 #ifdef VERBOSE_DEBUG
399 for(Xor& x : xors) {
400 cout << "cleaned XOR: " << x << endl;
401 }
402 #endif
403 }
404 return solver->okay();
405 }
406
407 //returns TRUE if removed or solver is UNSAT
full_clean(Clause & cl)408 bool ClauseCleaner::full_clean(Clause& cl)
409 {
410 Lit *i = cl.begin();
411 Lit *j = i;
412 for (Lit *end = cl.end(); i != end; i++) {
413 if (solver->value(*i) == l_True) {
414 return true;
415 }
416
417 if (solver->value(*i) == l_Undef) {
418 *j++ = *i;
419 }
420 }
421 cl.shrink(i-j);
422
423 if (cl.size() == 0) {
424 solver->ok = false;
425 return true;
426 }
427
428 if (cl.size() == 1) {
429 solver->enqueue(cl[0]);
430 return true;
431 }
432
433 if (cl.size() == 2) {
434 solver->attach_bin_clause(cl[0], cl[1], cl.red());
435 return true;
436 }
437
438 return false;
439 }
440