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 : 51874 : SimpSolver::SimpSolver(Env& env,
51 : : prop::TheoryProxy* proxy,
52 : : context::Context* context,
53 : 51874 : bool enableIncremental)
54 : : : Solver(env, proxy, context, enableIncremental),
55 : 103748 : grow(opt_grow),
56 : 51874 : clause_lim(opt_clause_lim),
57 : 51874 : subsumption_lim(opt_subsumption_lim),
58 : 51874 : simp_garbage_frac(opt_simp_garbage_frac),
59 : 51874 : use_asymm(opt_use_asymm),
60 : : // make sure this is not enabled if unsat cores or proofs are on
61 [ - - ]: 51874 : use_rcheck(opt_use_rcheck && !options().smt.produceUnsatCores
62 [ - + ][ - - ]: 51874 : && !options().smt.produceProofs),
63 : 51874 : merges(0),
64 : 51874 : asymm_lits(0),
65 : 51874 : eliminated_vars(0),
66 : 51874 : elimorder(1),
67 : 51874 : use_simplification(
68 : 51874 : options().prop.minisatSimpMode != options::MinisatSimpMode::NONE
69 [ + + ]: 51874 : && !enableIncremental
70 [ + + ]: 7711 : && !options().smt.produceUnsatCores
71 [ + - ][ + + ]: 103748 : && !options().smt.produceProofs),
72 : 51874 : occurs(ClauseDeleted(ca)),
73 : 51874 : elim_heap(ElimLt(n_occ)),
74 : 51874 : bwdsub_assigns(0),
75 : 207496 : n_touched(0)
76 : : {
77 : 51874 : vec<Lit> dummy(1,lit_Undef);
78 : 51874 : ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
79 : 51874 : bwdsub_tmpunit = ca.alloc(0, dummy);
80 : 51874 : remove_satisfied = false;
81 : :
82 : : // add the initialization for all the internal variables
83 [ + + ]: 155622 : for (int i = frozen.size(); i < vardata.size(); ++ i) {
84 : 103748 : frozen .push(1);
85 : 103748 : eliminated.push(0);
86 [ + + ]: 103748 : if (use_simplification){
87 : 10222 : n_occ .push(0);
88 : 10222 : n_occ .push(0);
89 : 10222 : occurs .init(i);
90 : 10222 : touched .push(0);
91 : 10222 : elim_heap .insert(i);
92 : : }
93 : : }
94 : 51874 : }
95 : :
96 : 20164 : void SimpSolver::attachProofManager(prop::PropPfManager* ppm)
97 : : {
98 [ + - ][ + - ]: 20164 : AlwaysAssert(!use_simplification && !use_rcheck);
[ - + ][ - + ]
[ - - ]
99 : 20164 : Solver::attachProofManager(ppm);
100 : 20164 : }
101 : :
102 : 2186205 : Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool canErase)
103 : : {
104 : 2186205 : Var v = Solver::newVar(sign, dvar, isTheoryAtom);
105 : :
106 [ + + ]: 2186205 : if (use_simplification)
107 : : {
108 : 178449 : frozen.push((char)(!canErase));
109 : 178449 : eliminated.push((char)false);
110 : 178449 : n_occ.push(0);
111 : 178449 : n_occ.push(0);
112 : 178449 : occurs.init(v);
113 : 178449 : touched.push(0);
114 : 178449 : elim_heap.insert(v);
115 : : }
116 : 2186205 : return v;
117 : : }
118 : :
119 : 50587 : lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
120 : : {
121 [ - + ]: 50587 : if (options().prop.minisatDumpDimacs)
122 : : {
123 : 0 : toDimacs();
124 : 0 : return l_Undef;
125 : : }
126 [ - + ][ - + ]: 50587 : Assert(decisionLevel() == 0);
[ - - ]
127 : :
128 : 50587 : vec<Var> extra_frozen;
129 : 50587 : lbool result = l_True;
130 : :
131 : 50587 : do_simp &= use_simplification;
132 : :
133 [ + + ]: 50587 : if (do_simp){
134 : : // Assumptions must be temporarily frozen to run variable elimination:
135 [ - + ]: 4211 : for (int i = 0; i < assumptions.size(); i++){
136 : 0 : Var v = var(assumptions[i]);
137 : :
138 : : // If an assumption has been eliminated, remember it.
139 : 0 : Assert(!isEliminated(v));
140 : :
141 [ - - ]: 0 : if (!frozen[v]){
142 : : // Freeze and store.
143 : 0 : setFrozen(v, true);
144 : 0 : extra_frozen.push(v);
145 : : } }
146 : :
147 : 4211 : result = lbool(eliminate(turn_off_simp));
148 : : }
149 : :
150 [ + + ]: 50587 : if (result == l_True)
151 : 49530 : result = Solver::solve_();
152 [ + + ]: 1057 : else if (verbosity >= 1)
153 : 1 : printf("===============================================================================\n");
154 : :
155 [ + + ]: 50571 : if (result == l_True)
156 : 24727 : extendModel();
157 : :
158 [ + + ]: 50571 : if (do_simp)
159 : : // Unfreeze the assumptions that were frozen:
160 [ - + ]: 4205 : for (int i = 0; i < extra_frozen.size(); i++)
161 : 0 : setFrozen(extra_frozen[i], false);
162 : :
163 : 50571 : return result;
164 : 50587 : }
165 : :
166 : :
167 : :
168 : 6025766 : bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
169 : : {
170 : : #ifdef CVC5_ASSERTIONS
171 [ + + ]: 6025766 : if (use_simplification)
172 : : {
173 [ - + ][ - + ]: 2054302 : for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
[ + + ][ - - ]
174 : : }
175 : : #endif
176 : :
177 : 6025766 : int nclauses = clauses_persistent.size();
178 : :
179 [ - + ][ - - ]: 6025766 : if (use_rcheck && implied(ps))
[ - + ]
180 : 0 : return true;
181 : :
182 [ + + ]: 6025766 : if (!Solver::addClause_(ps, removable, id))
183 : 9037 : return false;
184 : :
185 [ + + ][ + + ]: 6016729 : if (use_simplification && clauses_persistent.size() == nclauses + 1){
[ + + ]
186 : 165148 : CRef cr = clauses_persistent.last();
187 : 165148 : const Clause& c = ca[cr];
188 : :
189 : : // NOTE: the clause is added to the queue immediately and then
190 : : // again during 'gatherTouchedClauses()'. If nothing happens
191 : : // in between, it will only be checked once. Otherwise, it may
192 : : // be checked twice unnecessarily. This is an unfortunate
193 : : // consequence of how backward subsumption is used to mimic
194 : : // forward subsumption.
195 : 165148 : subsumption_queue.insert(cr);
196 [ + + ]: 633288 : for (int i = 0; i < c.size(); i++){
197 : 468140 : occurs[var(c[i])].push(cr);
198 : 468140 : n_occ[toInt(c[i])]++;
199 : 468140 : touched[var(c[i])] = 1;
200 : 468140 : n_touched++;
201 [ + + ]: 468140 : if (elim_heap.inHeap(var(c[i])))
202 : 450434 : elim_heap.increase(var(c[i]));
203 : : }
204 : : }
205 : :
206 : 6016729 : return true;
207 : : }
208 : :
209 : :
210 : 58304 : void SimpSolver::removeClause(CRef cr)
211 : : {
212 : 58304 : const Clause& c = ca[cr];
213 [ + - ]: 58304 : Trace("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl;
214 : :
215 [ + - ]: 58304 : if (use_simplification)
216 [ + + ]: 218454 : for (int i = 0; i < c.size(); i++){
217 : 160150 : n_occ[toInt(c[i])]--;
218 : 160150 : updateElimHeap(var(c[i]));
219 : 160150 : occurs.smudge(var(c[i]));
220 : : }
221 : :
222 : 58304 : Solver::removeClause(cr);
223 : 58304 : }
224 : :
225 : :
226 : 18080 : bool SimpSolver::strengthenClause(CRef cr, Lit l)
227 : : {
228 : 18080 : Clause& c = ca[cr];
229 [ - + ][ - + ]: 18080 : Assert(decisionLevel() == 0);
[ - - ]
230 [ - + ][ - + ]: 18080 : Assert(use_simplification);
[ - - ]
231 : :
232 : : // FIX: this is too inefficient but would be nice to have (properly implemented)
233 : : // if (!find(subsumption_queue, &c))
234 : 18080 : subsumption_queue.insert(cr);
235 : :
236 [ + + ]: 18080 : if (c.size() == 2){
237 : 2997 : removeClause(cr);
238 : 2997 : c.strengthen(l);
239 : : }else{
240 : 15083 : detachClause(cr, true);
241 : 15083 : c.strengthen(l);
242 : 15083 : attachClause(cr);
243 : 15083 : remove(occurs[var(l)], cr);
244 : 15083 : n_occ[toInt(l)]--;
245 : 15083 : updateElimHeap(var(l));
246 : : }
247 : :
248 [ + + ][ + - ]: 18080 : return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUT_THEORY) == CRef_Undef : true;
[ + + ]
249 : : }
250 : :
251 : :
252 : : // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
253 : 50014 : bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
254 : : {
255 : 50014 : merges++;
256 : 50014 : out_clause.clear();
257 : :
258 : 50014 : bool ps_smallest = _ps.size() < _qs.size();
259 [ + + ]: 50014 : const Clause& ps = ps_smallest ? _qs : _ps;
260 [ + + ]: 50014 : const Clause& qs = ps_smallest ? _ps : _qs;
261 : :
262 [ + + ]: 114525 : for (int i = 0; i < qs.size(); i++)
263 : : {
264 [ + + ]: 93038 : if (var(qs[i]) != v)
265 : : {
266 [ + + ]: 250621 : for (int j = 0; j < ps.size(); j++)
267 : : {
268 [ + + ]: 220040 : if (var(ps[j]) == var(qs[i]))
269 : : {
270 [ + + ]: 33512 : if (ps[j] == ~qs[i])
271 : 28527 : return false;
272 : : else
273 : 4985 : goto next;
274 : : }
275 : : }
276 : 30581 : out_clause.push(qs[i]);
277 : : }
278 : 64511 : next:;
279 : : }
280 : :
281 [ + + ]: 104842 : for (int i = 0; i < ps.size(); i++)
282 [ + + ]: 83355 : if (var(ps[i]) != v)
283 : 61868 : out_clause.push(ps[i]);
284 : :
285 : 21487 : return true;
286 : : }
287 : :
288 : :
289 : : // Returns FALSE if clause is always satisfied.
290 : 285031 : bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
291 : : {
292 : 285031 : merges++;
293 : :
294 : 285031 : bool ps_smallest = _ps.size() < _qs.size();
295 [ + + ]: 285031 : const Clause& ps = ps_smallest ? _qs : _ps;
296 [ + + ]: 285031 : const Clause& qs = ps_smallest ? _ps : _qs;
297 : 285031 : const Lit* __ps = (const Lit*)ps;
298 : 285031 : const Lit* __qs = (const Lit*)qs;
299 : :
300 : 285031 : size = ps.size()-1;
301 : :
302 [ + + ]: 780733 : for (int i = 0; i < qs.size(); i++)
303 : : {
304 [ + + ]: 610415 : if (var(__qs[i]) != v)
305 : : {
306 [ + + ]: 2252664 : for (int j = 0; j < ps.size(); j++)
307 : : {
308 [ + + ]: 1986408 : if (var(__ps[j]) == var(__qs[i]))
309 : : {
310 [ + + ]: 142888 : if (__ps[j] == ~__qs[i])
311 : 114713 : return false;
312 : : else
313 : 28175 : goto next;
314 : : }
315 : : }
316 : 266256 : size++;
317 : : }
318 : 495702 : next:;
319 : : }
320 : :
321 : 170318 : return true;
322 : : }
323 : :
324 : :
325 : 3240 : void SimpSolver::gatherTouchedClauses()
326 : : {
327 [ + + ]: 3240 : if (n_touched == 0) return;
328 : :
329 [ + + ]: 145277 : for (int i = 0; i < subsumption_queue.size(); i++)
330 [ + - ]: 143331 : if (ca[subsumption_queue[i]].mark() == 0)
331 : 143331 : ca[subsumption_queue[i]].mark(2);
332 : :
333 [ + + ]: 128737 : for (int i = 0; i < touched.size(); i++)
334 [ + + ]: 126791 : if (touched[i]){
335 : 73221 : const vec<CRef>& cs = occurs.lookup(i);
336 [ + + ]: 556208 : for (int j = 0; j < cs.size(); j++)
337 [ + + ]: 482987 : if (ca[cs[j]].mark() == 0){
338 : 37954 : subsumption_queue.insert(cs[j]);
339 : 37954 : ca[cs[j]].mark(2);
340 : : }
341 : 73221 : touched[i] = 0;
342 : : }
343 : :
344 [ + + ]: 183231 : for (int i = 0; i < subsumption_queue.size(); i++)
345 [ + - ]: 181285 : if (ca[subsumption_queue[i]].mark() == 2)
346 : 181285 : ca[subsumption_queue[i]].mark(0);
347 : :
348 : 1946 : n_touched = 0;
349 : : }
350 : :
351 : :
352 : 0 : bool SimpSolver::implied(const vec<Lit>& c)
353 : : {
354 : 0 : Assert(decisionLevel() == 0);
355 : :
356 : 0 : trail_lim.push(trail.size());
357 [ - - ]: 0 : for (int i = 0; i < c.size(); i++)
358 : : {
359 [ - - ]: 0 : if (value(c[i]) == l_True)
360 : : {
361 : 0 : cancelUntil(0);
362 : 0 : return false;
363 : : }
364 [ - - ]: 0 : else if (value(c[i]) != l_False)
365 : : {
366 : 0 : Assert(value(c[i]) == l_Undef);
367 : 0 : uncheckedEnqueue(~c[i]);
368 : : }
369 : : }
370 : :
371 : 0 : bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
372 : 0 : cancelUntil(0);
373 : 0 : return result;
374 : : }
375 : :
376 : :
377 : : // Backward subsumption + backward subsumption resolution
378 : 9666 : bool SimpSolver::backwardSubsumptionCheck(bool verbose)
379 : : {
380 : 9666 : int cnt = 0;
381 : 9666 : int subsumed = 0;
382 : 9666 : int deleted_literals = 0;
383 [ - + ][ - + ]: 9666 : Assert(decisionLevel() == 0);
[ - - ]
384 : :
385 [ + + ][ + + ]: 261572 : while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
[ + + ]
386 : :
387 : : // Empty subsumption queue and return immediately on user-interrupt:
388 [ - + ]: 251908 : if (asynch_interrupt){
389 : 0 : subsumption_queue.clear();
390 : 0 : bwdsub_assigns = trail.size();
391 : 0 : break; }
392 : :
393 : : // Check top-level assignments by creating a dummy clause and placing it in the queue:
394 [ + + ][ + - ]: 251908 : if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
[ + + ]
395 : 31064 : Lit l = trail[bwdsub_assigns++];
396 : 31064 : ca[bwdsub_tmpunit][0] = l;
397 : 31064 : ca[bwdsub_tmpunit].calcAbstraction();
398 : 31064 : subsumption_queue.insert(bwdsub_tmpunit); }
399 : :
400 : 251908 : CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
401 : 251908 : Clause& c = ca[cr];
402 : :
403 [ + + ]: 251908 : if (c.mark()) continue;
404 : :
405 [ + + ][ - + ]: 246650 : if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
[ - - ][ - + ]
406 : 0 : printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
407 : :
408 [ + + ][ + - ]: 246650 : Assert(c.size() > 1
[ - + ][ - + ]
[ - - ]
409 : : || value(c[0]) == l_True); // Unit-clauses should have been
410 : : // propagated before this point.
411 : :
412 : : // Find best variable to scan:
413 : 246650 : Var best = var(c[0]);
414 [ + + ]: 1695171 : for (int i = 1; i < c.size(); i++)
415 [ + + ]: 1448521 : if (occurs[var(c[i])].size() < occurs[best].size())
416 : 163627 : best = var(c[i]);
417 : :
418 : : // Search all candidates:
419 : 246650 : vec<CRef>& _cs = occurs.lookup(best);
420 : 246650 : CRef* cs = (CRef*)_cs;
421 : :
422 [ + + ]: 2366199 : for (int j = 0; j < _cs.size(); j++)
423 [ - + ]: 2119551 : if (c.mark())
424 : 0 : break;
425 [ + + ][ + + ]: 2119551 : else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
[ + - ][ + - ]
[ + + ]
426 : 1901139 : Lit l = c.subsumes(ca[cs[j]]);
427 : :
428 [ + + ]: 1901139 : if (l == lit_Undef)
429 : 20689 : subsumed++, removeClause(cs[j]);
430 [ + + ]: 1880450 : else if (l != lit_Error){
431 : 18080 : deleted_literals++;
432 : :
433 [ + + ]: 18080 : if (!strengthenClause(cs[j], ~l))
434 : 2 : return false;
435 : :
436 : : // Did current candidate get deleted from cs? Then check candidate at index j again:
437 [ + + ]: 18078 : if (var(l) == best)
438 : 15165 : j--;
439 : : }
440 : : }
441 : : }
442 : :
443 : 9664 : return true;
444 : : }
445 : :
446 : :
447 : 0 : bool SimpSolver::asymm(Var v, CRef cr)
448 : : {
449 : 0 : Clause& c = ca[cr];
450 : 0 : Assert(decisionLevel() == 0);
451 : :
452 : 0 : if (c.mark() || satisfied(c)) return true;
453 : :
454 : 0 : trail_lim.push(trail.size());
455 : 0 : Lit l = lit_Undef;
456 [ - - ]: 0 : for (int i = 0; i < c.size(); i++)
457 : 0 : if (var(c[i]) != v && value(c[i]) != l_False)
458 : 0 : uncheckedEnqueue(~c[i]);
459 : : else
460 : 0 : l = c[i];
461 : :
462 [ - - ]: 0 : if (propagate(CHECK_WITHOUT_THEORY) != CRef_Undef){
463 : 0 : cancelUntil(0);
464 : 0 : asymm_lits++;
465 [ - - ]: 0 : if (!strengthenClause(cr, l))
466 : 0 : return false;
467 : : }else
468 : 0 : cancelUntil(0);
469 : :
470 : 0 : return true;
471 : : }
472 : :
473 : :
474 : 0 : bool SimpSolver::asymmVar(Var v)
475 : : {
476 : 0 : Assert(use_simplification);
477 : :
478 : 0 : const vec<CRef>& cls = occurs.lookup(v);
479 : :
480 : 0 : if (value(v) != l_Undef || cls.size() == 0) return true;
481 : :
482 [ - - ]: 0 : for (int i = 0; i < cls.size(); i++)
483 [ - - ]: 0 : if (!asymm(v, cls[i])) return false;
484 : :
485 : 0 : return backwardSubsumptionCheck();
486 : : }
487 : :
488 : :
489 : 6428 : static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
490 : : {
491 : 6428 : elimclauses.push(toInt(x));
492 : 6428 : elimclauses.push(1);
493 : 6428 : }
494 : :
495 : :
496 : 13184 : static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
497 : : {
498 : 13184 : int first = elimclauses.size();
499 : 13184 : int v_pos = -1;
500 : :
501 : : // Copy clause to elimclauses-vector. Remember position where the
502 : : // variable 'v' occurs:
503 [ + + ]: 58300 : for (int i = 0; i < c.size(); i++){
504 : 45116 : elimclauses.push(toInt(c[i]));
505 [ + + ]: 45116 : if (var(c[i]) == v)
506 : 13184 : v_pos = i + first;
507 : : }
508 [ - + ][ - + ]: 13184 : Assert(v_pos != -1);
[ - - ]
509 : :
510 : : // Swap the first literal with the 'v' literal, so that the literal
511 : : // containing 'v' will occur first in the clause:
512 : 13184 : uint32_t tmp = elimclauses[v_pos];
513 : 13184 : elimclauses[v_pos] = elimclauses[first];
514 : 13184 : elimclauses[first] = tmp;
515 : :
516 : : // Store the length of the clause last:
517 : 13184 : elimclauses.push(c.size());
518 : 13184 : }
519 : :
520 : :
521 : :
522 : 16047 : bool SimpSolver::eliminateVar(Var v)
523 : : {
524 [ - + ][ - + ]: 16047 : Assert(!frozen[v]);
[ - - ]
525 [ - + ][ - + ]: 16047 : Assert(!isEliminated(v));
[ - - ]
526 [ - + ][ - + ]: 16047 : Assert(value(v) == l_Undef);
[ - - ]
527 : :
528 : : // Split the occurrences into positive and negative:
529 : : //
530 : 16047 : const vec<CRef>& cls = occurs.lookup(v);
531 : 16047 : vec<CRef> pos, neg;
532 [ + + ]: 212630 : for (int i = 0; i < cls.size(); i++)
533 [ + + ]: 196583 : (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
534 : :
535 : : // Check whether the increase in number of clauses stays within the allowed
536 : : // ('grow'). Moreover, no clause must exceed the limit on the maximal clause
537 : : // size (if it is set):
538 : : //
539 : 16047 : int cnt = 0;
540 : 16047 : int clause_size = 0;
541 : :
542 [ + + ]: 57580 : for (int i = 0; i < pos.size(); i++)
543 [ + + ]: 326564 : for (int j = 0; j < neg.size(); j++)
544 : 285031 : if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
545 [ + + ][ + + ]: 447497 : && (++cnt > cls.size() + grow
[ + + ]
546 [ + - ][ + + ]: 162466 : || (clause_lim != -1 && clause_size > clause_lim)))
547 : 9619 : return true;
548 : :
549 : : // Delete and store old clauses:
550 : 6428 : eliminated[v] = true;
551 : 6428 : setDecisionVar(v, false);
552 : 6428 : eliminated_vars++;
553 : :
554 [ + + ]: 6428 : if (pos.size() > neg.size())
555 : : {
556 [ + + ]: 4555 : for (int i = 0; i < neg.size(); i++)
557 : 2890 : mkElimClause(elimclauses, v, ca[neg[i]]);
558 : 1665 : mkElimClause(elimclauses, mkLit(v));
559 : : }
560 : : else
561 : : {
562 [ + + ]: 15057 : for (int i = 0; i < pos.size(); i++)
563 : 10294 : mkElimClause(elimclauses, v, ca[pos[i]]);
564 : 4763 : mkElimClause(elimclauses, ~mkLit(v));
565 : : }
566 : :
567 [ + + ]: 41046 : for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
568 : :
569 : 6428 : ClauseId id = ClauseIdUndef;
570 : : // Produce clauses in cross product:
571 : 6428 : vec<Lit>& resolvent = add_tmp;
572 [ + + ]: 22816 : for (int i = 0; i < pos.size(); i++)
573 [ + + ]: 66402 : for (int j = 0; j < neg.size(); j++) {
574 [ - + ][ - - ]: 50014 : bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
575 [ + + ][ - + ]: 71501 : if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
576 [ - + ]: 21487 : !addClause_(resolvent, removable, id)) {
577 : 0 : return false;
578 : : }
579 : : }
580 : :
581 : : // Free occurs list for this variable:
582 : 6428 : occurs[v].clear(true);
583 : :
584 : : // Free watchers lists for this variable, if possible:
585 [ + + ]: 6428 : if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
586 [ + + ]: 6428 : if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
587 : :
588 : 6428 : return backwardSubsumptionCheck();
589 : 16047 : }
590 : :
591 : :
592 : 0 : bool SimpSolver::substitute(Var v, Lit x)
593 : : {
594 : 0 : Assert(!frozen[v]);
595 : 0 : Assert(!isEliminated(v));
596 : 0 : Assert(value(v) == l_Undef);
597 : :
598 [ - - ]: 0 : if (!ok) return false;
599 : :
600 : 0 : eliminated[v] = true;
601 : 0 : setDecisionVar(v, false);
602 : 0 : const vec<CRef>& cls = occurs.lookup(v);
603 : :
604 : 0 : vec<Lit>& subst_clause = add_tmp;
605 [ - - ]: 0 : for (int i = 0; i < cls.size(); i++)
606 : : {
607 : 0 : Clause& c = ca[cls[i]];
608 : :
609 : 0 : subst_clause.clear();
610 [ - - ]: 0 : for (int j = 0; j < c.size(); j++)
611 : : {
612 : 0 : Lit p = c[j];
613 [ - - ]: 0 : subst_clause.push(var(p) == v ? x ^ sign(p) : p);
614 : : }
615 : :
616 : 0 : removeClause(cls[i]);
617 : 0 : ClauseId id = ClauseIdUndef;
618 [ - - ]: 0 : if (!addClause_(subst_clause, c.removable(), id))
619 : : {
620 : 0 : return ok = false;
621 : : }
622 : : }
623 : :
624 : 0 : return true;
625 : : }
626 : :
627 : :
628 : 24727 : void SimpSolver::extendModel()
629 : : {
630 : : int i, j;
631 : : Lit x;
632 : :
633 [ + + ]: 34091 : for (i = elimclauses.size()-1; i > 0; i -= j){
634 [ + + ]: 14092 : for (j = elimclauses[i--]; j > 1; j--, i--)
635 [ + + ]: 9217 : if (modelValue(toLit(elimclauses[i])) != l_False)
636 : 4489 : goto next;
637 : :
638 : 4875 : x = toLit(elimclauses[i]);
639 : 4875 : model[var(x)] = lbool(!sign(x));
640 : 9364 : next:;
641 : : }
642 : 24727 : }
643 : :
644 : :
645 : 4211 : bool SimpSolver::eliminate(bool turn_off_elim)
646 : : {
647 [ + + ]: 4211 : if (!simplify())
648 : 1055 : return false;
649 [ - + ]: 3156 : else if (!use_simplification)
650 : 0 : return true;
651 : :
652 : : // Main simplification loop:
653 : : //
654 [ + + ][ + + ]: 6394 : while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
[ - + ][ + + ]
655 : :
656 : 3240 : gatherTouchedClauses();
657 : : // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
658 [ + + ]: 4536 : if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
659 [ + + ][ + + ]: 4536 : && !backwardSubsumptionCheck(true))
[ + + ]
660 : : {
661 : 1 : ok = false;
662 : 1 : goto cleanup;
663 : : }
664 : :
665 : : // Empty elim_heap and return immediately on user-interrupt:
666 [ - + ]: 3239 : if (asynch_interrupt){
667 : 0 : Assert(bwdsub_assigns == trail.size());
668 : 0 : Assert(subsumption_queue.size() == 0);
669 : 0 : Assert(n_touched == 0);
670 : 0 : elim_heap.clear();
671 : 0 : goto cleanup;
672 : : }
673 : :
674 : : // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
675 [ + + ]: 92645 : for (int cnt = 0; !elim_heap.empty(); cnt++){
676 : 89407 : Var elim = elim_heap.removeMin();
677 : :
678 [ - + ]: 89407 : if (asynch_interrupt) break;
679 : :
680 [ + - ][ + + ]: 89407 : if (isEliminated(elim) || value(elim) != l_Undef) continue;
[ + + ]
681 : :
682 [ - + ][ - - ]: 58408 : if (verbosity >= 2 && cnt % 100 == 0)
683 : 0 : printf("elimination left: %10d\r", elim_heap.size());
684 : :
685 [ - + ]: 58408 : if (use_asymm){
686 : : // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
687 : 0 : bool was_frozen = frozen[elim];
688 : 0 : frozen[elim] = true;
689 [ - - ]: 0 : if (!asymmVar(elim)){
690 : 0 : ok = false; goto cleanup; }
691 : 0 : frozen[elim] = was_frozen; }
692 : :
693 : : // At this point, the variable may have been set by assymetric branching, so check it
694 : : // again. Also, don't eliminate frozen variables:
695 : 58408 : if (options().prop.minisatSimpMode
696 : : != options::MinisatSimpMode::CLAUSE_ELIM
697 [ + - ][ + + ]: 30007 : && value(elim) == l_Undef && !frozen[elim]
698 [ + + ][ + + ]: 88415 : && !eliminateVar(elim))
[ + + ]
699 : : {
700 : 1 : ok = false;
701 : 1 : goto cleanup;
702 : : }
703 : :
704 : 58407 : checkGarbage(simp_garbage_frac);
705 : : }
706 : :
707 [ - + ][ - + ]: 3238 : Assert(subsumption_queue.size() == 0);
[ - - ]
708 : : }
709 : 3154 : cleanup:
710 : :
711 : : // If no more simplification is needed, free all simplification-related data structures:
712 [ - + ]: 3156 : if (turn_off_elim){
713 : 0 : touched .clear(true);
714 : 0 : occurs .clear(true);
715 : 0 : n_occ .clear(true);
716 : 0 : elim_heap.clear(true);
717 : 0 : subsumption_queue.clear(true);
718 : :
719 : 0 : use_simplification = false;
720 : 0 : remove_satisfied = true;
721 : 0 : ca.extra_clause_field = false;
722 : :
723 : : // Force full cleanup (this is safe and desirable since it only happens once):
724 : 0 : rebuildOrderHeap();
725 : 0 : garbageCollect();
726 : : }else{
727 : : // Cheaper cleanup:
728 : 3156 : cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
729 : 3156 : checkGarbage();
730 : : }
731 : :
732 [ + + ][ - + ]: 3156 : if (verbosity >= 1 && elimclauses.size() > 0)
[ - + ]
733 : 0 : printf(
734 : : "| Eliminated clauses: %10.2f Mb "
735 : : " |\n",
736 : 0 : double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
737 : :
738 : 3156 : return ok;
739 : : }
740 : :
741 : :
742 : 6745 : void SimpSolver::cleanUpClauses()
743 : : {
744 : 6745 : occurs.cleanAll();
745 : : int i,j;
746 [ + + ]: 1211614 : for (i = j = 0; i < clauses_persistent.size(); i++)
747 [ + + ]: 1204869 : if (ca[clauses_persistent[i]].mark() == 0)
748 : 1146565 : clauses_persistent[j++] = clauses_persistent[i];
749 : 6745 : clauses_persistent.shrink(i - j);
750 : 6745 : }
751 : :
752 : : //=================================================================================================
753 : : // Garbage Collection methods:
754 : :
755 : :
756 : 3589 : void SimpSolver::relocAll(ClauseAllocator& to)
757 : : {
758 [ + + ]: 3589 : if (!use_simplification) return;
759 : :
760 : : // All occurs lists:
761 : : //
762 [ + + ]: 294519 : for (int i = 0; i < nVars(); i++){
763 : 293280 : vec<CRef>& cs = occurs[i];
764 [ + + ]: 688269 : for (int j = 0; j < cs.size(); j++)
765 : 394989 : ca.reloc(cs[j], to);
766 : : }
767 : :
768 : : // Subsumption queue:
769 : : //
770 [ + + ]: 1247 : for (int i = 0; i < subsumption_queue.size(); i++)
771 : 8 : ca.reloc(subsumption_queue[i], to);
772 : : // TODO reloc now takes the proof form the core solver
773 : : // Temporary clause:
774 : : //
775 : 1239 : ca.reloc(bwdsub_tmpunit, to);
776 : : // TODO reloc now takes the proof form the core solver
777 : : }
778 : :
779 : :
780 : 3589 : void SimpSolver::garbageCollect()
781 : : {
782 : : // Initialize the next region to a size corresponding to the estimated utilization degree. This
783 : : // is not precise but should avoid some unnecessary reallocations for the new region:
784 : 3589 : ClauseAllocator to(ca.size() - ca.wasted());
785 : :
786 : 3589 : cleanUpClauses();
787 : 3589 : to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
788 : 3589 : relocAll(to);
789 : 3589 : Solver::relocAll(to);
790 [ - + ]: 3589 : if (verbosity >= 2)
791 : 0 : printf(
792 : : "| Garbage collection: %12d bytes => %12d bytes |\n",
793 : 0 : ca.size() * ClauseAllocator::Unit_Size,
794 : 0 : to.size() * ClauseAllocator::Unit_Size);
795 : 3589 : to.moveTo(ca);
796 : : // TODO: proof.finalizeUpdateId();
797 : 3589 : }
|
