Branch data Line data Source code
1 : : /***********************************************************************************[SimpSolver.cc]
2 : : Copyright (c) 2006, Niklas Een, Niklas Sorensson
3 : : Copyright (c) 2007-2010, Niklas Sorensson
4 : :
5 : : Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 : : associated documentation files (the "Software"), to deal in the Software without restriction,
7 : : including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 : : sublicense, and/or sell 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 all copies or
12 : : substantial portions of the Software.
13 : :
14 : : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 : : NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 : : NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 : : DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 : : OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 : : **************************************************************************************************/
20 : :
21 : : #include "prop/minisat/simp/SimpSolver.h"
22 : :
23 : : #include "base/check.h"
24 : : #include "options/prop_options.h"
25 : : #include "options/smt_options.h"
26 : : #include "proof/clause_id.h"
27 : : #include "prop/minisat/mtl/Sort.h"
28 : : #include "prop/minisat/utils/System.h"
29 : :
30 : : using namespace cvc5::internal;
31 : : using namespace cvc5::internal::Minisat;
32 : :
33 : : //=================================================================================================
34 : : // Options:
35 : :
36 : :
37 : : static const char* _cat = "SIMP";
38 : :
39 : : static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
40 : : static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
41 : : static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
42 : : static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
43 : : static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
44 : : static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
45 : :
46 : :
47 : : //=================================================================================================
48 : : // Constructor/Destructor:
49 : :
50 : 50267 : SimpSolver::SimpSolver(Env& env,
51 : : prop::TheoryProxy* proxy,
52 : : context::Context* context,
53 : : context::UserContext* userContext,
54 : : prop::PropPfManager* ppm,
55 : 50267 : bool enableIncremental)
56 : : : Solver(env, proxy, context, userContext, ppm, enableIncremental),
57 : : grow(opt_grow),
58 : : clause_lim(opt_clause_lim),
59 : : subsumption_lim(opt_subsumption_lim),
60 : : simp_garbage_frac(opt_simp_garbage_frac),
61 : : use_asymm(opt_use_asymm),
62 : : // make sure this is not enabled if unsat cores or proofs are on
63 : 50267 : use_rcheck(opt_use_rcheck && !options().smt.produceUnsatCores && !ppm),
64 : : merges(0),
65 : : asymm_lits(0),
66 : : eliminated_vars(0),
67 : : elimorder(1),
68 : : use_simplification(
69 : 100534 : options().prop.minisatSimpMode != options::MinisatSimpMode::NONE
70 [ + - ][ + + ]: 50267 : && !enableIncremental && !options().smt.produceUnsatCores && !ppm),
[ + + ][ + - ]
71 : 0 : occurs(ClauseDeleted(ca)),
72 : 100534 : elim_heap(ElimLt(n_occ)),
73 : : bwdsub_assigns(0),
74 : 150801 : n_touched(0)
75 : : {
76 : 100534 : vec<Lit> dummy(1,lit_Undef);
77 : 50267 : ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
78 : 50267 : bwdsub_tmpunit = ca.alloc(0, dummy);
79 : 50267 : remove_satisfied = false;
80 : :
81 : : // add the initialization for all the internal variables
82 [ + + ]: 150801 : for (int i = frozen.size(); i < vardata.size(); ++ i) {
83 : 100534 : frozen .push(1);
84 : 100534 : eliminated.push(0);
85 [ + + ]: 100534 : if (use_simplification){
86 : 10524 : n_occ .push(0);
87 : 10524 : n_occ .push(0);
88 : 10524 : occurs .init(i);
89 : 10524 : touched .push(0);
90 : 10524 : elim_heap .insert(i);
91 : : }
92 : : }
93 : 50267 : }
94 : :
95 : :
96 : 100022 : SimpSolver::~SimpSolver()
97 : : {
98 : 100022 : }
99 : :
100 : 2212700 : Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool canErase)
101 : : {
102 : 2212700 : Var v = Solver::newVar(sign, dvar, isTheoryAtom, canErase);
103 : :
104 [ + + ]: 2212700 : if (use_simplification)
105 : : {
106 : 173616 : frozen.push((char)(!canErase));
107 : 173616 : eliminated.push((char)false);
108 : 173616 : n_occ.push(0);
109 : 173616 : n_occ.push(0);
110 : 173616 : occurs.init(v);
111 : 173616 : touched.push(0);
112 : 173616 : elim_heap.insert(v);
113 : : }
114 : 2212700 : return v;
115 : : }
116 : :
117 : 49677 : lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
118 : : {
119 [ - + ]: 49677 : if (options().prop.minisatDumpDimacs)
120 : : {
121 : 0 : toDimacs();
122 : 0 : return l_Undef;
123 : : }
124 [ - + ][ - + ]: 49677 : Assert(decisionLevel() == 0);
[ - - ]
125 : :
126 : 49690 : vec<Var> extra_frozen;
127 : 49677 : lbool result = l_True;
128 : :
129 : 49677 : do_simp &= use_simplification;
130 : :
131 [ + + ]: 49677 : if (do_simp){
132 : : // Assumptions must be temporarily frozen to run variable elimination:
133 [ - + ]: 4406 : for (int i = 0; i < assumptions.size(); i++){
134 : 0 : Var v = var(assumptions[i]);
135 : :
136 : : // If an assumption has been eliminated, remember it.
137 : 0 : Assert(!isEliminated(v));
138 : :
139 [ - - ]: 0 : if (!frozen[v]){
140 : : // Freeze and store.
141 : 0 : setFrozen(v, true);
142 : 0 : extra_frozen.push(v);
143 : : } }
144 : :
145 : 4406 : result = lbool(eliminate(turn_off_simp));
146 : : }
147 : :
148 [ + + ]: 49677 : if (result == l_True)
149 : 48572 : result = Solver::solve_();
150 [ + + ]: 1105 : else if (verbosity >= 1)
151 : 1 : printf("===============================================================================\n");
152 : :
153 [ + + ]: 49664 : if (result == l_True)
154 : 24145 : extendModel();
155 : :
156 [ + + ]: 49664 : if (do_simp)
157 : : // Unfreeze the assumptions that were frozen:
158 [ - + ]: 4400 : for (int i = 0; i < extra_frozen.size(); i++)
159 : 0 : setFrozen(extra_frozen[i], false);
160 : :
161 : 49664 : return result;
162 : : }
163 : :
164 : :
165 : :
166 : 6278210 : bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
167 : : {
168 : : #ifdef CVC5_ASSERTIONS
169 [ + + ]: 6278210 : if (use_simplification)
170 : : {
171 [ + + ][ - + ]: 2238270 : for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
[ - + ][ - - ]
172 : : }
173 : : #endif
174 : :
175 : 6278210 : int nclauses = clauses_persistent.size();
176 : :
177 [ - + ][ - - ]: 6278210 : if (use_rcheck && implied(ps))
[ - + ]
178 : 0 : return true;
179 : :
180 [ + + ]: 6278210 : if (!Solver::addClause_(ps, removable, id))
181 : 8505 : return false;
182 : :
183 [ + + ][ + + ]: 6269710 : if (use_simplification && clauses_persistent.size() == nclauses + 1){
[ + + ]
184 : 167948 : CRef cr = clauses_persistent.last();
185 : 167948 : const Clause& c = ca[cr];
186 : :
187 : : // NOTE: the clause is added to the queue immediately and then
188 : : // again during 'gatherTouchedClauses()'. If nothing happens
189 : : // in between, it will only be checked once. Otherwise, it may
190 : : // be checked twice unnecessarily. This is an unfortunate
191 : : // consequence of how backward subsumption is used to mimic
192 : : // forward subsumption.
193 : 167948 : subsumption_queue.insert(cr);
194 [ + + ]: 645534 : for (int i = 0; i < c.size(); i++){
195 : 477586 : occurs[var(c[i])].push(cr);
196 : 477586 : n_occ[toInt(c[i])]++;
197 : 477586 : touched[var(c[i])] = 1;
198 : 477586 : n_touched++;
199 [ + + ]: 477586 : if (elim_heap.inHeap(var(c[i])))
200 : 459884 : elim_heap.increase(var(c[i]));
201 : : }
202 : : }
203 : :
204 : 6269710 : return true;
205 : : }
206 : :
207 : :
208 : 58909 : void SimpSolver::removeClause(CRef cr)
209 : : {
210 : 58909 : const Clause& c = ca[cr];
211 [ + - ]: 58909 : Trace("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl;
212 : :
213 [ + - ]: 58909 : if (use_simplification)
214 [ + + ]: 220639 : for (int i = 0; i < c.size(); i++){
215 : 161730 : n_occ[toInt(c[i])]--;
216 : 161730 : updateElimHeap(var(c[i]));
217 : 161730 : occurs.smudge(var(c[i]));
218 : : }
219 : :
220 : 58909 : Solver::removeClause(cr);
221 : 58909 : }
222 : :
223 : :
224 : 18672 : bool SimpSolver::strengthenClause(CRef cr, Lit l)
225 : : {
226 : 18672 : Clause& c = ca[cr];
227 [ - + ][ - + ]: 18672 : Assert(decisionLevel() == 0);
[ - - ]
228 [ - + ][ - + ]: 18672 : Assert(use_simplification);
[ - - ]
229 : :
230 : : // FIX: this is too inefficient but would be nice to have (properly implemented)
231 : : // if (!find(subsumption_queue, &c))
232 : 18672 : subsumption_queue.insert(cr);
233 : :
234 [ + + ]: 18672 : if (c.size() == 2){
235 : 3047 : removeClause(cr);
236 : 3047 : c.strengthen(l);
237 : : }else{
238 : 15625 : detachClause(cr, true);
239 : 15625 : c.strengthen(l);
240 : 15625 : attachClause(cr);
241 : 15625 : remove(occurs[var(l)], cr);
242 : 15625 : n_occ[toInt(l)]--;
243 : 15625 : updateElimHeap(var(l));
244 : : }
245 : :
246 [ + + ][ + - ]: 18672 : return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUT_THEORY) == CRef_Undef : true;
[ + + ]
247 : : }
248 : :
249 : :
250 : : // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
251 : 50010 : bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
252 : : {
253 : 50010 : merges++;
254 : 50010 : out_clause.clear();
255 : :
256 : 50010 : bool ps_smallest = _ps.size() < _qs.size();
257 [ + + ]: 50010 : const Clause& ps = ps_smallest ? _qs : _ps;
258 [ + + ]: 50010 : const Clause& qs = ps_smallest ? _ps : _qs;
259 : :
260 [ + + ]: 114517 : for (int i = 0; i < qs.size(); i++)
261 : : {
262 [ + + ]: 93032 : if (var(qs[i]) != v)
263 : : {
264 [ + + ]: 250610 : for (int j = 0; j < ps.size(); j++)
265 : : {
266 [ + + ]: 220031 : if (var(ps[j]) == var(qs[i]))
267 : : {
268 [ + + ]: 33510 : if (ps[j] == ~qs[i])
269 : 28525 : return false;
270 : : else
271 : 4985 : goto next;
272 : : }
273 : : }
274 : 30579 : out_clause.push(qs[i]);
275 : : }
276 : 64507 : next:;
277 : : }
278 : :
279 [ + + ]: 104834 : for (int i = 0; i < ps.size(); i++)
280 [ + + ]: 83349 : if (var(ps[i]) != v)
281 : 61864 : out_clause.push(ps[i]);
282 : :
283 : 21485 : return true;
284 : : }
285 : :
286 : :
287 : : // Returns FALSE if clause is always satisfied.
288 : 285027 : bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
289 : : {
290 : 285027 : merges++;
291 : :
292 : 285027 : bool ps_smallest = _ps.size() < _qs.size();
293 [ + + ]: 285027 : const Clause& ps = ps_smallest ? _qs : _ps;
294 [ + + ]: 285027 : const Clause& qs = ps_smallest ? _ps : _qs;
295 : 285027 : const Lit* __ps = (const Lit*)ps;
296 : 285027 : const Lit* __qs = (const Lit*)qs;
297 : :
298 : 285027 : size = ps.size()-1;
299 : :
300 [ + + ]: 780725 : for (int i = 0; i < qs.size(); i++)
301 : : {
302 [ + + ]: 610409 : if (var(__qs[i]) != v)
303 : : {
304 [ + + ]: 2252650 : for (int j = 0; j < ps.size(); j++)
305 : : {
306 [ + + ]: 1986400 : if (var(__ps[j]) == var(__qs[i]))
307 : : {
308 [ + + ]: 142886 : if (__ps[j] == ~__qs[i])
309 : 114711 : return false;
310 : : else
311 : 28175 : goto next;
312 : : }
313 : : }
314 : 266254 : size++;
315 : : }
316 : 495698 : next:;
317 : : }
318 : :
319 : 170316 : return true;
320 : : }
321 : :
322 : :
323 : 3386 : void SimpSolver::gatherTouchedClauses()
324 : : {
325 [ + + ]: 3386 : if (n_touched == 0) return;
326 : :
327 : : int i,j;
328 [ + + ]: 148483 : for (i = j = 0; i < subsumption_queue.size(); i++)
329 [ + - ]: 146248 : if (ca[subsumption_queue[i]].mark() == 0)
330 : 146248 : ca[subsumption_queue[i]].mark(2);
331 : :
332 [ + + ]: 129286 : for (i = 0; i < touched.size(); i++)
333 [ + + ]: 127051 : if (touched[i]){
334 : 73054 : const vec<CRef>& cs = occurs.lookup(i);
335 [ + + ]: 565736 : for (j = 0; j < cs.size(); j++)
336 [ + + ]: 492682 : if (ca[cs[j]].mark() == 0){
337 : 37952 : subsumption_queue.insert(cs[j]);
338 : 37952 : ca[cs[j]].mark(2);
339 : : }
340 : 73054 : touched[i] = 0;
341 : : }
342 : :
343 [ + + ]: 186435 : for (i = 0; i < subsumption_queue.size(); i++)
344 [ + - ]: 184200 : if (ca[subsumption_queue[i]].mark() == 2)
345 : 184200 : ca[subsumption_queue[i]].mark(0);
346 : :
347 : 2235 : n_touched = 0;
348 : : }
349 : :
350 : :
351 : 0 : bool SimpSolver::implied(const vec<Lit>& c)
352 : : {
353 : 0 : Assert(decisionLevel() == 0);
354 : :
355 : 0 : trail_lim.push(trail.size());
356 [ - - ]: 0 : for (int i = 0; i < c.size(); i++)
357 : : {
358 [ - - ]: 0 : if (value(c[i]) == l_True)
359 : : {
360 : 0 : cancelUntil(0);
361 : 0 : return false;
362 : : }
363 [ - - ]: 0 : else if (value(c[i]) != l_False)
364 : : {
365 : 0 : Assert(value(c[i]) == l_Undef);
366 : 0 : uncheckedEnqueue(~c[i]);
367 : : }
368 : : }
369 : :
370 : 0 : bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
371 : 0 : cancelUntil(0);
372 : 0 : return result;
373 : : }
374 : :
375 : :
376 : : // Backward subsumption + backward subsumption resolution
377 : 9809 : bool SimpSolver::backwardSubsumptionCheck(bool verbose)
378 : : {
379 : 9809 : int cnt = 0;
380 : 9809 : int subsumed = 0;
381 : 9809 : int deleted_literals = 0;
382 [ - + ][ - + ]: 9809 : Assert(decisionLevel() == 0);
[ - - ]
383 : :
384 [ + + ][ + + ]: 265389 : while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
[ + + ]
385 : :
386 : : // Empty subsumption queue and return immediately on user-interrupt:
387 [ - + ]: 255582 : if (asynch_interrupt){
388 : 0 : subsumption_queue.clear();
389 : 0 : bwdsub_assigns = trail.size();
390 : 0 : break; }
391 : :
392 : : // Check top-level assignments by creating a dummy clause and placing it in the queue:
393 [ + + ][ + - ]: 255582 : if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
[ + + ]
394 : 31233 : Lit l = trail[bwdsub_assigns++];
395 : 31233 : ca[bwdsub_tmpunit][0] = l;
396 : 31233 : ca[bwdsub_tmpunit].calcAbstraction();
397 : 31233 : subsumption_queue.insert(bwdsub_tmpunit); }
398 : :
399 : 255582 : CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
400 : 255582 : Clause& c = ca[cr];
401 : :
402 [ + + ]: 255582 : if (c.mark()) continue;
403 : :
404 [ + + ][ - + ]: 250136 : if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
[ - - ][ - + ]
405 : 0 : printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
406 : :
407 [ + + ][ - + ]: 250136 : Assert(c.size() > 1
[ - + ][ - - ]
408 : : || value(c[0]) == l_True); // Unit-clauses should have been
409 : : // propagated before this point.
410 : :
411 : : // Find best variable to scan:
412 : 250136 : Var best = var(c[0]);
413 [ + + ]: 1705660 : for (int i = 1; i < c.size(); i++)
414 [ + + ]: 1455520 : if (occurs[var(c[i])].size() < occurs[best].size())
415 : 167474 : best = var(c[i]);
416 : :
417 : : // Search all candidates:
418 : 250136 : vec<CRef>& _cs = occurs.lookup(best);
419 : 250136 : CRef* cs = (CRef*)_cs;
420 : :
421 [ + + ]: 2402620 : for (int j = 0; j < _cs.size(); j++)
422 [ - + ]: 2152480 : if (c.mark())
423 : 0 : break;
424 [ + + ][ + + ]: 2152480 : else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
[ + - ][ + - ]
[ + + ]
425 : 1930730 : Lit l = c.subsumes(ca[cs[j]]);
426 : :
427 [ + + ]: 1930730 : if (l == lit_Undef)
428 : 21249 : subsumed++, removeClause(cs[j]);
429 [ + + ]: 1909480 : else if (l != lit_Error){
430 : 18672 : deleted_literals++;
431 : :
432 [ + + ]: 18672 : if (!strengthenClause(cs[j], ~l))
433 : 2 : return false;
434 : :
435 : : // Did current candidate get deleted from cs? Then check candidate at index j again:
436 [ + + ]: 18670 : if (var(l) == best)
437 : 15497 : j--;
438 : : }
439 : : }
440 : : }
441 : :
442 : 9807 : return true;
443 : : }
444 : :
445 : :
446 : 0 : bool SimpSolver::asymm(Var v, CRef cr)
447 : : {
448 : 0 : Clause& c = ca[cr];
449 : 0 : Assert(decisionLevel() == 0);
450 : :
451 : 0 : if (c.mark() || satisfied(c)) return true;
452 : :
453 : 0 : trail_lim.push(trail.size());
454 : 0 : Lit l = lit_Undef;
455 [ - - ]: 0 : for (int i = 0; i < c.size(); i++)
456 : 0 : if (var(c[i]) != v && value(c[i]) != l_False)
457 : 0 : uncheckedEnqueue(~c[i]);
458 : : else
459 : 0 : l = c[i];
460 : :
461 [ - - ]: 0 : if (propagate(CHECK_WITHOUT_THEORY) != CRef_Undef){
462 : 0 : cancelUntil(0);
463 : 0 : asymm_lits++;
464 [ - - ]: 0 : if (!strengthenClause(cr, l))
465 : 0 : return false;
466 : : }else
467 : 0 : cancelUntil(0);
468 : :
469 : 0 : return true;
470 : : }
471 : :
472 : :
473 : 0 : bool SimpSolver::asymmVar(Var v)
474 : : {
475 : 0 : Assert(use_simplification);
476 : :
477 : 0 : const vec<CRef>& cls = occurs.lookup(v);
478 : :
479 : 0 : if (value(v) != l_Undef || cls.size() == 0) return true;
480 : :
481 [ - - ]: 0 : for (int i = 0; i < cls.size(); i++)
482 [ - - ]: 0 : if (!asymm(v, cls[i])) return false;
483 : :
484 : 0 : return backwardSubsumptionCheck();
485 : : }
486 : :
487 : :
488 : 6425 : static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
489 : : {
490 : 6425 : elimclauses.push(toInt(x));
491 : 6425 : elimclauses.push(1);
492 : 6425 : }
493 : :
494 : :
495 : 13182 : static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
496 : : {
497 : 13182 : int first = elimclauses.size();
498 : 13182 : int v_pos = -1;
499 : :
500 : : // Copy clause to elimclauses-vector. Remember position where the
501 : : // variable 'v' occurs:
502 [ + + ]: 58292 : for (int i = 0; i < c.size(); i++){
503 : 45110 : elimclauses.push(toInt(c[i]));
504 [ + + ]: 45110 : if (var(c[i]) == v)
505 : 13182 : v_pos = i + first;
506 : : }
507 [ - + ][ - + ]: 13182 : Assert(v_pos != -1);
[ - - ]
508 : :
509 : : // Swap the first literal with the 'v' literal, so that the literal
510 : : // containing 'v' will occur first in the clause:
511 : 13182 : uint32_t tmp = elimclauses[v_pos];
512 : 13182 : elimclauses[v_pos] = elimclauses[first];
513 : 13182 : elimclauses[first] = tmp;
514 : :
515 : : // Store the length of the clause last:
516 : 13182 : elimclauses.push(c.size());
517 : 13182 : }
518 : :
519 : :
520 : :
521 : 16044 : bool SimpSolver::eliminateVar(Var v)
522 : : {
523 [ - + ][ - + ]: 16044 : Assert(!frozen[v]);
[ - - ]
524 [ - + ][ - + ]: 16044 : Assert(!isEliminated(v));
[ - - ]
525 [ - + ][ - + ]: 16044 : Assert(value(v) == l_Undef);
[ - - ]
526 : :
527 : : // Split the occurrences into positive and negative:
528 : : //
529 : 16044 : const vec<CRef>& cls = occurs.lookup(v);
530 : 32088 : vec<CRef> pos, neg;
531 [ + + ]: 212622 : for (int i = 0; i < cls.size(); i++)
532 [ + + ]: 196578 : (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
533 : :
534 : : // Check whether the increase in number of clauses stays within the allowed
535 : : // ('grow'). Moreover, no clause must exceed the limit on the maximal clause
536 : : // size (if it is set):
537 : : //
538 : 16044 : int cnt = 0;
539 : 16044 : int clause_size = 0;
540 : :
541 [ + + ]: 57575 : for (int i = 0; i < pos.size(); i++)
542 [ + + ]: 326558 : for (int j = 0; j < neg.size(); j++)
543 : 285027 : if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
544 [ + + ][ + + ]: 447491 : && (++cnt > cls.size() + grow
[ + + ]
545 [ + - ][ + + ]: 162464 : || (clause_lim != -1 && clause_size > clause_lim)))
546 : 9619 : return true;
547 : :
548 : : // Delete and store old clauses:
549 : 6425 : eliminated[v] = true;
550 : 6425 : setDecisionVar(v, false);
551 : 6425 : eliminated_vars++;
552 : :
553 [ + + ]: 6425 : if (pos.size() > neg.size())
554 : : {
555 [ + + ]: 4555 : for (int i = 0; i < neg.size(); i++)
556 : 2890 : mkElimClause(elimclauses, v, ca[neg[i]]);
557 : 1665 : mkElimClause(elimclauses, mkLit(v));
558 : : }
559 : : else
560 : : {
561 [ + + ]: 15052 : for (int i = 0; i < pos.size(); i++)
562 : 10292 : mkElimClause(elimclauses, v, ca[pos[i]]);
563 : 4760 : mkElimClause(elimclauses, ~mkLit(v));
564 : : }
565 : :
566 [ + + ]: 41038 : for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
567 : :
568 : 6425 : ClauseId id = ClauseIdUndef;
569 : : // Produce clauses in cross product:
570 : 6425 : vec<Lit>& resolvent = add_tmp;
571 [ + + ]: 22811 : for (int i = 0; i < pos.size(); i++)
572 [ + + ]: 66396 : for (int j = 0; j < neg.size(); j++) {
573 [ - + ][ - - ]: 50010 : bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
574 [ + + ][ - + ]: 71495 : if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
575 [ - + ]: 21485 : !addClause_(resolvent, removable, id)) {
576 : 0 : return false;
577 : : }
578 : : }
579 : :
580 : : // Free occurs list for this variable:
581 : 6425 : occurs[v].clear(true);
582 : :
583 : : // Free watchers lists for this variable, if possible:
584 [ + + ]: 6425 : if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
585 [ + + ]: 6425 : if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
586 : :
587 : 6425 : return backwardSubsumptionCheck();
588 : : }
589 : :
590 : :
591 : 0 : bool SimpSolver::substitute(Var v, Lit x)
592 : : {
593 : 0 : Assert(!frozen[v]);
594 : 0 : Assert(!isEliminated(v));
595 : 0 : Assert(value(v) == l_Undef);
596 : :
597 [ - - ]: 0 : if (!ok) return false;
598 : :
599 : 0 : eliminated[v] = true;
600 : 0 : setDecisionVar(v, false);
601 : 0 : const vec<CRef>& cls = occurs.lookup(v);
602 : :
603 : 0 : vec<Lit>& subst_clause = add_tmp;
604 [ - - ]: 0 : for (int i = 0; i < cls.size(); i++)
605 : : {
606 : 0 : Clause& c = ca[cls[i]];
607 : :
608 : 0 : subst_clause.clear();
609 [ - - ]: 0 : for (int j = 0; j < c.size(); j++)
610 : : {
611 : 0 : Lit p = c[j];
612 [ - - ]: 0 : subst_clause.push(var(p) == v ? x ^ sign(p) : p);
613 : : }
614 : :
615 : 0 : removeClause(cls[i]);
616 : 0 : ClauseId id = ClauseIdUndef;
617 [ - - ]: 0 : if (!addClause_(subst_clause, c.removable(), id))
618 : : {
619 : 0 : return ok = false;
620 : : }
621 : : }
622 : :
623 : 0 : return true;
624 : : }
625 : :
626 : :
627 : 24145 : void SimpSolver::extendModel()
628 : : {
629 : : int i, j;
630 : : Lit x;
631 : :
632 [ + + ]: 33507 : for (i = elimclauses.size()-1; i > 0; i -= j){
633 [ + + ]: 14156 : for (j = elimclauses[i--]; j > 1; j--, i--)
634 [ + + ]: 9247 : if (modelValue(toLit(elimclauses[i])) != l_False)
635 : 4453 : goto next;
636 : :
637 : 4909 : x = toLit(elimclauses[i]);
638 : 4909 : model[var(x)] = lbool(!sign(x));
639 : 9362 : next:;
640 : : }
641 : 24145 : }
642 : :
643 : :
644 : 4406 : bool SimpSolver::eliminate(bool turn_off_elim)
645 : : {
646 [ + + ]: 4406 : if (!simplify())
647 : 1103 : return false;
648 [ - + ]: 3303 : else if (!use_simplification)
649 : 0 : return true;
650 : :
651 : : // Main simplification loop:
652 : : //
653 [ + + ][ + + ]: 6687 : while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
[ - + ][ + + ]
654 : :
655 : 3386 : gatherTouchedClauses();
656 : : // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
657 [ + + ]: 4539 : if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
658 [ + + ][ + + ]: 4539 : && !backwardSubsumptionCheck(true))
[ + + ]
659 : : {
660 : 1 : ok = false;
661 : 1 : goto cleanup;
662 : : }
663 : :
664 : : // Empty elim_heap and return immediately on user-interrupt:
665 [ - + ]: 3385 : if (asynch_interrupt){
666 : 0 : Assert(bwdsub_assigns == trail.size());
667 : 0 : Assert(subsumption_queue.size() == 0);
668 : 0 : Assert(n_touched == 0);
669 : 0 : elim_heap.clear();
670 : 0 : goto cleanup;
671 : : }
672 : :
673 : : // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
674 [ + + ]: 92795 : for (int cnt = 0; !elim_heap.empty(); cnt++){
675 : 89411 : Var elim = elim_heap.removeMin();
676 : :
677 [ - + ]: 89411 : if (asynch_interrupt) break;
678 : :
679 [ + - ][ + + ]: 89411 : if (isEliminated(elim) || value(elim) != l_Undef) continue;
[ + + ]
680 : :
681 [ - + ][ - - ]: 58243 : if (verbosity >= 2 && cnt % 100 == 0)
682 : 0 : printf("elimination left: %10d\r", elim_heap.size());
683 : :
684 [ - + ]: 58243 : if (use_asymm){
685 : : // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
686 : 0 : bool was_frozen = frozen[elim];
687 : 0 : frozen[elim] = true;
688 [ - - ]: 0 : if (!asymmVar(elim)){
689 : 0 : ok = false; goto cleanup; }
690 : 0 : frozen[elim] = was_frozen; }
691 : :
692 : : // At this point, the variable may have been set by assymetric branching, so check it
693 : : // again. Also, don't eliminate frozen variables:
694 : 58243 : if (options().prop.minisatSimpMode
695 : : != options::MinisatSimpMode::CLAUSE_ELIM
696 [ + - ][ + + ]: 29998 : && value(elim) == l_Undef && !frozen[elim]
697 [ + + ][ + + ]: 88241 : && !eliminateVar(elim))
[ + + ]
698 : : {
699 : 1 : ok = false;
700 : 1 : goto cleanup;
701 : : }
702 : :
703 : 58242 : checkGarbage(simp_garbage_frac);
704 : : }
705 : :
706 [ - + ][ - + ]: 3384 : Assert(subsumption_queue.size() == 0);
[ - - ]
707 : : }
708 : 3301 : cleanup:
709 : :
710 : : // If no more simplification is needed, free all simplification-related data structures:
711 [ - + ]: 3303 : if (turn_off_elim){
712 : 0 : touched .clear(true);
713 : 0 : occurs .clear(true);
714 : 0 : n_occ .clear(true);
715 : 0 : elim_heap.clear(true);
716 : 0 : subsumption_queue.clear(true);
717 : :
718 : 0 : use_simplification = false;
719 : 0 : remove_satisfied = true;
720 : 0 : ca.extra_clause_field = false;
721 : :
722 : : // Force full cleanup (this is safe and desirable since it only happens once):
723 : 0 : rebuildOrderHeap();
724 : 0 : garbageCollect();
725 : : }else{
726 : : // Cheaper cleanup:
727 : 3303 : cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
728 : 3303 : checkGarbage();
729 : : }
730 : :
731 [ + + ][ - + ]: 3303 : if (verbosity >= 1 && elimclauses.size() > 0)
[ - + ]
732 : 0 : printf(
733 : : "| Eliminated clauses: %10.2f Mb "
734 : : " |\n",
735 : 0 : double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
736 : :
737 : 3303 : return ok;
738 : : }
739 : :
740 : :
741 : 6591 : void SimpSolver::cleanUpClauses()
742 : : {
743 : 6591 : occurs.cleanAll();
744 : : int i,j;
745 [ + + ]: 885953 : for (i = j = 0; i < clauses_persistent.size(); i++)
746 [ + + ]: 879362 : if (ca[clauses_persistent[i]].mark() == 0)
747 : 820453 : clauses_persistent[j++] = clauses_persistent[i];
748 : 6591 : clauses_persistent.shrink(i - j);
749 : 6591 : }
750 : :
751 : : //=================================================================================================
752 : : // Garbage Collection methods:
753 : :
754 : :
755 : 3288 : void SimpSolver::relocAll(ClauseAllocator& to)
756 : : {
757 [ + + ]: 3288 : if (!use_simplification) return;
758 : :
759 : : // All occurs lists:
760 : : //
761 [ + + ]: 295148 : for (int i = 0; i < nVars(); i++){
762 : 293839 : vec<CRef>& cs = occurs[i];
763 [ + + ]: 690051 : for (int j = 0; j < cs.size(); j++)
764 : 396212 : ca.reloc(cs[j], to);
765 : : }
766 : :
767 : : // Subsumption queue:
768 : : //
769 [ + + ]: 1317 : for (int i = 0; i < subsumption_queue.size(); i++)
770 : 8 : ca.reloc(subsumption_queue[i], to);
771 : : // TODO reloc now takes the proof form the core solver
772 : : // Temporary clause:
773 : : //
774 : 1309 : ca.reloc(bwdsub_tmpunit, to);
775 : : // TODO reloc now takes the proof form the core solver
776 : : }
777 : :
778 : :
779 : 3288 : void SimpSolver::garbageCollect()
780 : : {
781 : : // Initialize the next region to a size corresponding to the estimated utilization degree. This
782 : : // is not precise but should avoid some unnecessary reallocations for the new region:
783 : 6576 : ClauseAllocator to(ca.size() - ca.wasted());
784 : :
785 : 3288 : cleanUpClauses();
786 : 3288 : to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
787 : 3288 : relocAll(to);
788 : 3288 : Solver::relocAll(to);
789 [ - + ]: 3288 : if (verbosity >= 2)
790 : 0 : printf(
791 : : "| Garbage collection: %12d bytes => %12d bytes |\n",
792 : 0 : ca.size() * ClauseAllocator::Unit_Size,
793 : 0 : to.size() * ClauseAllocator::Unit_Size);
794 : 3288 : to.moveTo(ca);
795 : : // TODO: proof.finalizeUpdateId();
796 : 3288 : }
|
