CVC3  2.4.1
minisat_solver.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file minisat_solver.cpp
4  *\brief Adaptation of MiniSat to DPLL(T)
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Fri Sep 08 11:04:00 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 /****************************************************************************************[Solver.C]
22 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
23 
24 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
25 associated documentation files (the "Software"), to deal in the Software without restriction,
26 including without limitation the rights to use, copy, modify, merge, publish, distribute,
27 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
28 furnished to do so, subject to the following conditions:
29 
30 The above copyright notice and this permission notice shall be included in all copies or
31 substantial portions of the Software.
32 
33 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
34 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
36 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
37 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
38 **************************************************************************************************/
39 
40 #include "minisat_solver.h"
41 #include "minisat_types.h"
42 #include <cmath>
43 #include <iostream>
44 #include <algorithm>
45 
46 using namespace std;
47 using namespace MiniSat;
48 
49 
50 ///
51 /// Constants
52 ///
53 
54 
55 // if true do propositional propagation to exhaustion
56 // before asserting propagated literals to the theories.
57 // that is, a SAT propagation is not immediately asserted to the theories as well,
58 // but only when the SAT core has to do a decision.
59 //
60 // this way a branch may be closed propositionally only,
61 // which avoids work on the theory part,
62 // and introduction of new theory clauses and implications.
63 const bool defer_theory_propagation = true;
64 
65 
66 /// theory implications
67 
68 // retrieve explanations of theory implications eagerly
69 // and store them right away as clauses
70 const bool eager_explanation = true;
71 
72 // if explanations for theory implications are retrieved lazily
73 // during regressions, should they be added as clauses?
74 //
75 // only used if eager_explanation is false.
76 const bool keep_lazy_explanation = true;
77 
78 
79 /// pushes
80 
81 // determines which theory operations are done,
82 // when unit propagation is done to exhaustion at the root level
83 // because a push is done.
84 
85 // if true then assert propositional propagations to theories as well
86 // (this is done anyway when defer_theory_propagation is false)
87 const bool push_theory_propagation = true;
88 
89 // if push_theory_propagation is also true,
90 // retrieve and propagate theory implications as well
91 const bool push_theory_implication = true;
92 
93 // if push_theory_propagation is also true,
94 // retrieve and add theory clauses as well (and handle their propagations)
95 const bool push_theory_clause = true;
96 
97 
98 
99 
100 // the number of literals considered in propLookahead()
102 
103 
104 // print the derivation
105 const bool protocol = false;
106 //const bool protocol = true;
107 
108 
109 
110 
111 // perform expensive assertion checks
112 const bool debug_full = false;
113 
114 
115 
116 
117 ///
118 /// conversions between MiniSat and CVC data types:
119 ///
120 
121 bool MiniSat::cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals) {
122  // register all clause literals
124 
125  for (j = clause.begin(), jend = clause.end(); j != jend; ++j) {
126  const SAT::Lit& literal = *j;
127 
128  // simplify based on true/false literals
129  if (literal.isTrue())
130  return false;
131 
132  if (!literal.isFalse())
133  literals.push_back(cvcToMiniSat(literal));
134  }
135 
136  return true;
137 }
138 
139 Clause* Solver::cvcToMiniSat(const SAT::Clause& clause, int id) {
140  vector<MiniSat::Lit> literals;
141  if (MiniSat::cvcToMiniSat(clause, literals)) {
142  if (getDerivation() != NULL)
143  return Clause_new(literals, clause.getClauseTheorem(), id);
144  else
145  return Clause_new(literals, CVC3::Theorem(), id);
146  }
147  else {
148  return NULL;
149  }
150 }
151 
152 
153 
154 
155 
156 /// Initialization
157 
158 Solver::Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider,
159  bool logDerivation) :
160  d_inSearch(false),
161  d_ok(true),
162  d_conflict(NULL),
163  d_qhead (0),
164  d_thead (0),
165  d_registeredVars (1),
166  d_clauseIDCounter (3), // -1 and -2 are used in Clause for special clauses,
167  // and negative ids are in general used for theory clauses,
168  // so avoid overlap by setting 3 as the possible first clause id.
169  d_popRequests (0),
170  d_cla_inc (1),
171  d_cla_decay (1),
172  d_var_inc (1),
173  d_var_decay (1),
174  d_order (d_assigns, d_activity),
175  d_simpDB_assigns (0),
176  d_simpDB_props (0),
177  d_simpRD_learnts (0),
178  d_theoryAPI(theoryAPI),
179  d_decider(decider),
180  d_derivation(NULL),
181  d_default_params(SearchParams(0.95, 0.999, 0.02)),
182  d_expensive_ccmin(true)
183 {
184  if (logDerivation) d_derivation = new Derivation();
185 }
186 
187 
188 // add a lemma which has not been computed just now (see push(), createFrom()),
189 // so it is not necessarily propagating
190 void Solver::insertLemma(const Clause* lemma, int clauseID, int pushID) {
191  // need to add lemmas manually,
192  // as addClause/insertClause assume that the lemma has just been computed and is propagating,
193  // and as we want to keep the activity.
194  vector<Lit> literals;
195  lemma->toLit(literals);
196 
197  // If a lemma is based purely on theory lemmas (i.e. theory clauses),
198  // then in backtracking those theory lemmas might be retracted,
199  // and literals occurring in the lemma might not occur in any remaining clauses.
200  // When creating a new solver based on an existing instance
201  // (i.e. in continuing the search after finding a model),
202  // then those literals have to be registered here.
203  for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i) {
204  registerVar(i->var());
205  }
206 
207  // While lemma simplification might be nice to have,
208  // this poses a problem with derivation recording,
209  // as we would also have to modify the derivation of the original
210  // lemma towards a derivation of the new lemma.
211  // In the case of a new solver inheriting the lemmas of the previous solver
212  // the lemma is registered for the first time in the derivation.
213  // In the case where the lemma was kept over a push the old lemma
214  // is registered with the derivation, but about to be removed from memory (xfree).
215  // So the simplest thing is to just replace any previous registration of the
216  // lemma with a new identical lemma, and not do any simplification at all.
217  //if (!simplifyClause(literals, clauseID)) {
218  // ensure that order is appropriate for watched literals
219  orderClause(literals);
220 
221  Clause* newLemma = Lemma_new(literals, clauseID, pushID);
222  if (getDerivation() != NULL) getDerivation()->registerClause(newLemma);
223 
224  newLemma->setActivity(lemma->activity());
225 
226  // add to watches and lemmas
227  if (newLemma->size() >= 2) {
228  addWatch(~(*newLemma)[0], newLemma);
229  addWatch(~(*newLemma)[1], newLemma);
230  }
231  d_learnts.push_back(newLemma);
232  d_stats.learnts_literals += newLemma->size();
233 
234  // unsatisfiable
235  if (newLemma->size() == 0 || getValue((*newLemma)[0]) == l_False) {
236  updateConflict(newLemma);
237  }
238  // propagate
239  if (newLemma->size() == 1 || getValue((*newLemma)[1]) == l_False) {
240  if (!enqueue((*newLemma)[0], d_rootLevel, newLemma)) {
241  DebugAssert(false, "MiniSat::Solver::insertLemma: conflicting/implying lemma");
242  }
243  }
244  //}
245 }
246 
247 
248 Solver* Solver::createFrom(const Solver* oldSolver) {
249  Solver* solver = new MiniSat::Solver(oldSolver->d_theoryAPI,
250  oldSolver->d_decider, oldSolver->d_derivation != NULL);
251 
252  // reuse literal activity
253  // assigning d_activity before the clauses are added
254  // will automatically rebuild d_order in the right way.
255  solver->d_cla_inc = oldSolver->d_cla_inc;
256  solver->d_var_inc = oldSolver->d_var_inc;
257  solver->d_activity = oldSolver->d_activity;
258 
259 
260  // build the current formula
261 
262  // add the formula and assignment from the previous solver
263  // first assignment, as this contains only unit clauses, then clauses,
264  // as these are immediately simplified by the assigned unit clauses
265 
266  // get the old assignment
267  const vector<MiniSat::Lit>& trail = oldSolver->getTrail();
268  for (vector<MiniSat::Lit>::const_iterator i = trail.begin(); i != trail.end(); ++i) {
269  //:TODO: use special clause as reason instead of NULL
270  solver->addClause(*i, CVC3::Theorem());
271  }
272 
273  // get the old clause set
274  const vector<MiniSat::Clause*>& clauses = oldSolver->getClauses();
275  for (vector<MiniSat::Clause*>::const_iterator i = clauses.begin(); i != clauses.end(); ++i) {
276  solver->addClause(**i, false);
277  }
278 
279  // get the old lemmas
280  const vector<MiniSat::Clause*>& lemmas = oldSolver->getLemmas();
281  for (vector<MiniSat::Clause*>::const_iterator i = lemmas.begin();
282  !solver->isConflicting() && i != lemmas.end(); ++i) {
283  // can use clauseID for clause id as well as push id -
284  // after all this is the root level, so all lemmas are ok in any push level anyway
285  int clauseID = solver->nextClauseID();
286  solver->insertLemma(*i, clauseID, clauseID);
287  }
288 
289  return solver;
290 }
291 
293  for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); ++i)
294  remove(*i, true);
295 
296  for (vector<Clause*>::const_iterator i = d_clauses.begin(); i != d_clauses.end(); ++i)
297  remove(*i, true);
298 
299  while (!d_pendingClauses.empty()) {
300  xfree(d_pendingClauses.front());
301  d_pendingClauses.pop();
302  }
303 
304  while (!d_theoryExplanations.empty()) {
305  xfree(d_theoryExplanations.top().second);
306  d_theoryExplanations.pop();
307  }
308 
309  delete d_derivation;
310 }
311 
312 
313 
314 
315 ///
316 /// String representation
317 //
318 
319 std::string Solver::toString(Lit literal, bool showAssignment) const {
320  ostringstream buffer;
321  buffer << literal.toString();
322 
323  if (showAssignment) {
324  if (getValue(literal) == l_True)
325  buffer << "(+)";
326  else if (getValue(literal) == l_False)
327  buffer << "(-)";
328  }
329 
330  return buffer.str();
331 }
332 
333 
334 std::string Solver::toString(const std::vector<Lit>& clause, bool showAssignment) const {
335  ostringstream buffer;
336  for (size_type j = 0; j < clause.size(); ++j) {
337  buffer << toString(clause[j], showAssignment) << " ";
338  }
339  buffer << endl;
340 
341  return buffer.str();
342 }
343 
344 std::string Solver::toString(const Clause& clause, bool showAssignment) const {
345  std::vector<Lit> literals;
346  clause.toLit(literals);
347  return toString(literals, showAssignment);
348 }
349 
350 
351 std::vector<SAT::Lit> Solver::curAssigns(){
352  vector<SAT::Lit> res;
353  cout << "current Assignment: " << endl;
354  for (size_type i = 0; i < d_trail.size(); ++i) {
355  res.push_back(miniSatToCVC(d_trail[i]));
356  }
357  return res;
358 }
359 
360 std::vector<std::vector<SAT::Lit> > Solver::curClauses(){
361  std::vector<std::vector< SAT::Lit> > res;
362  cout << "current Clauses: " << endl;
363  for (size_t i = 0; i < d_clauses.size(); ++i) {
364  std::vector<SAT::Lit> oneClause;
365  oneClause.clear();
366  for (int j = 0; j < (*d_clauses[i]).size(); ++j) {
367  oneClause.push_back(miniSatToCVC((*d_clauses[i])[j]));
368  }
369  res.push_back(oneClause);
370  }
371  return res;
372 }
373 
374 
375 void Solver::printState() const {
376  cout << "Lemmas: " << endl;
377  for (size_type i = 0; i < d_learnts.size(); ++i) {
378  cout << toString(*(d_learnts[i]), true);
379  }
380 
381  cout << endl;
382 
383  cout << "Clauses: " << endl;
384  for (size_type i = 0; i < d_clauses.size(); ++i) {
385  cout << toString(*(d_clauses[i]), true);
386  }
387 
388  cout << endl;
389 
390  cout << "Assignment: " << endl;
391  // for (size_type i = 0; i < d_qhead; ++i) {
392  for (size_type i = 0; i < d_trail.size(); ++i) {
393  string split = "";
394  if (getReason(d_trail[i].var()) == Clause::Decision()) {
395  split = "(S)";
396  }
397  cout << toString(d_trail[i], false) << split << " ";
398  }
399  cout << endl;
400 }
401 
402 
403 
404 
405 void Solver::printDIMACS() const {
406  int max_id = nVars();
407  int num_clauses = d_clauses.size() + d_trail.size();// + learnts.size() ;
408 
409  // header
410  cout << "c minisat test" << endl;
411  cout << "p cnf " << max_id << " " << num_clauses << endl;
412 
413  // clauses
414  for (size_type i = 0; i < d_clauses.size(); ++i) {
415  Clause& clause = *d_clauses[i];
416  for (int j = 0; j < clause.size(); ++j) {
417  Lit lit = clause[j];
418  cout << toString(lit, false) << " ";
419  }
420  cout << "0" << endl;
421  }
422 
423  // lemmas
424  //for (int i = 0; i < learnts.size(); ++i) {
425  // Clause& clause = *learnts[i];
426  // for (int j = 0; j < clause.size(); ++j) {
427  // Lit lit = clause[j];
428  // cout << toString(lit, false) << " ";
429  // }
430  // cout << "0" << endl;
431  //}
432 
433  // context
434  for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
435  Lit lit(*i);
436  if (getReason(lit.var()) == Clause::Decision())
437  cout << toString(lit, false) << " 0" << endl;
438  else
439  cout << toString(lit, false) << " 0" << endl;
440  }
441 }
442 
443 
444 
445 /// Operations on clauses:
446 
447 
449  for (vector<Hash::hash_set<Var> >::const_iterator i = d_registeredVars.begin();
450  i != d_registeredVars.end(); ++i) {
451  if ((*i).count(var) > 0) return true;
452  }
453  return false;
454 }
455 
456 // registers var with given index to all data structures
458  if (isRegistered(index)) return;
459 
460  // register variables to all data structures
461  if (nVars() <= index) {
462  // 2 * index + 1 will be accessed for neg. literal,
463  // so we need + 1 fiels for 0 field
464  d_watches .resize(2 * index + 2);
465  d_reason .resize(index + 1, NULL);
466  d_assigns .resize(index + 1, toInt(l_Undef));
467  d_level .resize(index + 1, -1);
468  d_activity .resize(index + 1, 0);
469  d_analyze_seen.resize(index + 1, 0);
470  d_pushIDs .resize(index + 1, -1);
471  if (d_derivation != NULL) d_trail_pos.resize(index + 1, d_trail.max_size());
472  }
473 
474  // register with internal variable selection heuristics
475  d_order .newVar(index);
476 
477  // marks as registered
478  DebugAssert(!d_registeredVars.empty(), "MiniSat::Solver::registerVar: d_registeredVars is empty");
479  d_registeredVars.back().insert(index);
480 }
481 
483  vector<Lit> literals;
484  literals.push_back(p);
485  addClause(literals, theorem, nextClauseID());
486 }
487 
488 void Solver::addClause(const SAT::Clause& clause, bool isTheoryClause) {
489  vector<MiniSat::Lit> literals;
490  if (MiniSat::cvcToMiniSat(clause, literals)) {
491  int clauseID = nextClauseID();
492  // theory clauses have negative ids:
493  if (isTheoryClause) clauseID = -clauseID;
494  CVC3::Theorem theorem;
495  if (getDerivation() != NULL) {
496  getDerivation()->registerInputClause(clauseID);
497  theorem = clause.getClauseTheorem();
498  }
499  addClause(literals, theorem, clauseID);
500  }
501  else {
502  // ignore tautologies
503  return;
504  }
505 }
506 
507 void Solver::addClause(const Clause& clause, bool keepClauseID) {
508  vector<Lit> literals;
509  for (int i = 0; i < clause.size(); ++i) {
510  literals.push_back(clause[i]);
511  }
512  if (keepClauseID) {
513  addClause(literals, clause.getTheorem(), clause.id());
514  } else {
515  addClause(literals, clause.getTheorem(), nextClauseID());
516  }
517 }
518 
519 // Note:
520 // tried to improve efficiency by asserting unit clauses first,
521 // then clauses of size 2, and so on,
522 // in the hope to immediately simplify or remove clauses.
523 //
524 // didn't work well with the theories, though,
525 // lead to significant overhead, even when the derivation did not change much.
526 // presumably as this interleaves clauses belonging to different 'groups',
527 // which describe different concepts and are better handled in sequence
528 // without interleaving them.
529 void Solver::addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause) {
531  // for comparison: this is the order used by -sat sat
532  //for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
533  for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
534 // if(i->d_reason.isNull()){
535 // cout<<"found null thm in Solver::addFormula"<<endl<<flush;
536 // }
537  addClause(*i, isTheoryClause);
538  }
539 }
540 
541 
542 
543 // based on root level assignment removes all permanently falsified literals.
544 // return true if clause is permanently satisfied.
545 bool Solver::simplifyClause(vector<Lit>& literals, int clausePushID) const {
546  // Check if clause is a tautology: p \/ -p \/ C:
547  for (size_type i = 1; i < literals.size(); i++){
548  if (literals[i-1] == ~literals[i]){
549  return true;
550  }
551  }
552 
553  // Remove permanently satisfied clauses and falsified literals:
554  size_type i, j;
555  for (i = j = 0; i < literals.size(); i++) {
556  bool rootAssign = (
557  getLevel(literals[i]) == d_rootLevel
558  && isImpliedAt(literals[i], clausePushID) );
559 
560  if (rootAssign && (getValue(literals[i]) == l_True)){
561  return true;
562  }
563  else if (rootAssign && (getValue(literals[i]) == l_False)){
564 
565  ;
566  }
567  else{
568  literals[j++] = literals[i];
569  }
570  }
571  literals.resize(j);
572  return false;
573 }
574 
575 
576 
577 // need the invariant, that
578 // a) either two undefined literals are chosen as watched literals,
579 // or b) that after backtracking either a) kicks in
580 // or the clause is still satisfied/unit
581 //
582 // so either:
583 // - find two literals which are undefined or satisfied
584 // - or find a literal that is satisfied or unsatisfied
585 // and the most recently falsified literal
586 // - or the two most recently falsified literals
587 // and put these two literals at the first two positions
588 void Solver::orderClause(vector<Lit>& literals) const {
589  if (literals.size() >= 2) {
590  int first = 0;
591  int levelFirst = getLevel(literals[first]);
592  lbool valueFirst = getValue(literals[first]);
593  int second = 1;
594  int levelSecond = getLevel(literals[second]);
595  lbool valueSecond = getValue(literals[second]);
596  for (size_type i = 2; i < literals.size(); i++) {
597  // found two watched or satisfied literals
598  if (!(valueFirst == l_False) && !(valueSecond == l_False))
599  break;
600 
601  // check if new literal is better than the currently picked ones
602  int levelNew = getLevel(literals[i]);
603  lbool valueNew = getValue(literals[i]);
604 
605  // usable, take instead of previously chosen literal
606  if (!(valueNew == l_False)) {
607  if ((valueFirst == l_False) && (valueSecond == l_False)) {
608  if (levelFirst > levelSecond) {
609  second = i; levelSecond = levelNew; valueSecond = valueNew;
610  } else {
611  first = i; levelFirst = levelNew; valueFirst = valueNew;
612  }
613  }
614  else if (valueFirst == l_False) {
615  first = i; levelFirst = levelNew; valueFirst = valueNew;
616  }
617  else {
618  second = i; levelSecond = levelNew; valueSecond = valueNew;
619  }
620  }
621  // check if new pick was falsified more recently than the others
622  else {
623  if ((valueFirst == l_False) && (valueSecond == l_False)) {
624  if ((levelNew > levelFirst) && (levelNew > levelSecond)) {
625  if (levelSecond > levelFirst) {
626  first = i; levelFirst = levelNew; valueFirst = valueNew;
627  }
628  else {
629  second = i; levelSecond = levelNew; valueSecond = valueNew;
630  }
631  }
632  else if (levelNew > levelFirst) {
633  first = i; levelFirst = levelNew; valueFirst = valueNew;
634  }
635  else if (levelNew > levelSecond) {
636  second = i; levelSecond = levelNew; valueSecond = valueNew;
637  }
638  }
639  else if (valueFirst == l_False) {
640  if (levelNew > levelFirst) {
641  first = i; levelFirst = levelNew; valueFirst = valueNew;
642  }
643  }
644  else { // valueSecond == l_false
645  if (levelNew > levelSecond) {
646  second = i; levelSecond = levelNew; valueSecond = valueNew;
647  }
648  }
649  }
650  }
651 
652  Lit swap = literals[0]; literals[0] = literals[first]; literals[first] = swap;
653  swap = literals[1]; literals[1] = literals[second]; literals[second] = swap;
654 
655  // if a literal is satisfied, the first literal is satisfied,
656  // otherwise if a literal is falsified, the second literal is falsified.
657  if (
658  // satisfied literal at first position
659  ((getValue(literals[0]) != l_True) && (getValue(literals[1]) == l_True))
660  ||
661  // falsified literal at second position
662  (getValue(literals[0]) == l_False)
663  )
664  {
665  Lit swap = literals[0]; literals[0] = literals[1]; literals[1] = swap;
666  }
667  }
668 }
669 
670 
671 void Solver::addClause(vector<Lit>& literals, CVC3::Theorem theorem, int clauseID) {
672  // sort clause
673  std::sort(literals.begin(), literals.end());
674 
675  // remove duplicates
676  vector<Lit>::iterator end = std::unique(literals.begin(), literals.end());
677  literals.erase(end, literals.end());
678 
679  // register var for each clause literal
680  for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i){
681  registerVar(i->var());
682  }
683 
684  // simplify clause
685  vector<Lit> simplified(literals);
686 
687  bool replaceReason = false;
688  if (simplifyClause(simplified, clauseID)) {
689  // it can happen that a unit clause was contradictory when it was added (in a non-root state).
690  // then it was first added to list of pending clauses,
691  // and the conflict analyzed and retracted:
692  // this lead to the computation of a lemma which was used as a reason for the literal
693  // instead of the unit clause itself.
694  // so fix this here
695  if (literals.size() == 1 && getReason(literals[0].var())->learnt()) {
696  replaceReason = true;
697  }
698  else {
699  // permanently satisfied clause
700  return;
701  }
702  }
703 
704  // record derivation for a simplified clause
705  if (getDerivation() != NULL && simplified.size() < literals.size()) {
706  // register original clause as start of simplification
707  Clause* c = Clause_new(literals, theorem, clauseID);
710 
711  // register simplification steps
712  Inference* inference = new Inference(clauseID);
713  size_type j = 0;
714  for (size_type i = 0; i < literals.size(); ++i) {
715  // literal removed in simplification
716  if (j >= simplified.size() || literals[i] != simplified[j]) {
717  inference->add(literals[i], getDerivation()->computeRootReason(~literals[i], this));
718  }
719  // keep literal
720  else {
721  ++j;
722  }
723  }
724 
725  // register resolution leading to simplified clause
726  clauseID = nextClauseID();
727  getDerivation()->registerInference(clauseID, inference);
728  }
729 
730  // insert simplified clause
731  orderClause(simplified);
732  Clause* c;
733  if (simplified.size() < literals.size()) {
734  c = Clause_new(simplified, CVC3::Theorem(), clauseID);
735  } else {
736  c = Clause_new(simplified, theorem, clauseID);
737  }
738 
739  // cout<<"clause size" << c->size() << endl << flush;
740 
741  insertClause(c);
742  // cout<<"after clause size" << c->size() << endl << flush;
743  if (replaceReason) {
744  d_reason[literals[0].var()] = c;
745  }
746 // cout<<"after after clause size" << c->size() << endl << flush;
747 }
748 
749 
751  // clause set is unsatisfiable
752  if (!d_ok) {
753  remove(c, true);
754  return;
755  }
756 
757  if (getDerivation() != NULL) getDerivation()->registerClause(c);
758 
759  if (c->size() == 0){
760  d_conflict = c;
761 
762  // for garbage collection: need to put clause somewhere
763  if (!c->learnt()) {
764  d_clauses.push_back(c);
765  } else {
766  d_learnts.push_back(c);
767  }
768 
769  d_ok = false;
770  return;
771  }
772 
773  // process clause -
774  // if clause is conflicting add it to pending clause and return
775 
776  // unit clause
777  if (c->size() == 1) {
778  if (!enqueue((*c)[0], d_rootLevel, c)) {
779  // this backtracks to d_rootLevel, as reason c is just one literal,
780  // which is immediately UIP, so c will be learned as a lemma as well.
781  updateConflict(c);
782  d_pendingClauses.push(c);
783  return;
784  }
785  }
786  // non-unit clause
787  else {
788  // ensure that for a lemma the second literal has the highest decision level
789  if (c->learnt()){
790  DebugAssert(getValue((*c)[0]) == l_Undef,
791  "MiniSat::Solver::insertClause: first literal of new lemma not undefined");
792  IF_DEBUG (
793  for (int i = 1; i < c->size(); ++i) {
794  DebugAssert(getValue((*c)[i]) == l_False,
795  "MiniSat::Solver::insertClause: lemma literal not false");
796  }
797  )
798 
799  // Put the second watch on the literal with highest decision level:
800  int max_i = 1;
801  int max = getLevel((*c)[1]);
802  for (int i = 2; i < c->size(); i++) {
803  if (getLevel((*c)[i]) > max) {
804  max = getLevel((*c)[i]);
805  max_i = i;
806  }
807  }
808  Lit swap((*c)[1]);
809  (*c)[1] = (*c)[max_i];
810  (*c)[max_i] = swap;
811 
812  // (newly learnt clauses should be considered active)
813  claBumpActivity(c);
814  }
815 
816  // satisfied
817  if (getValue((*c)[0]) == l_True) {
818  ;
819  }
820  // conflicting
821  else if (getValue((*c)[0]) == l_False) {
822  IF_DEBUG (
823  for (int i = 1; i < c->size(); ++i) {
824  DebugAssert(getValue((*c)[i]) == l_False,
825  "MiniSat::Solver::insertClause: bogus conflicting clause");
826  }
827  )
828 
829  updateConflict(c);
830  d_pendingClauses.push(c);
831  return;
832  }
833  // propagation
834  else if (getValue((*c)[1]) == l_False) {
835  DebugAssert(getValue((*c)[0]) == l_Undef,
836  "MiniSat::Solver::insertClause: bogus propagating clause");
837  IF_DEBUG (
838  for (int i = 1; i < c->size(); ++i) {
839  DebugAssert(getValue((*c)[i]) == l_False,
840  "MiniSat::Solver::insertClause: bogus propagating clause");
841  }
842  )
843  if (!enqueue((*c)[0], getImplicationLevel(*c), c)) {
844  DebugAssert(false, "MiniSat::Solver::insertClause: conflicting/implying clause");
845  }
846  }
847 
848  // Watch clause:
849  addWatch(~(*c)[0], c);
850  addWatch(~(*c)[1], c);
851  }
852 
853  // clause is not conflicting, so insert it into the clause list.
854  d_stats.max_literals += c->size();
855  if (!c->learnt()) {
856  d_clauses.push_back(c);
857  d_stats.clauses_literals += c->size();
858  } else {
859  d_learnts.push_back(c);
860  d_stats.learnts_literals += c->size();
861  }
862 }
863 
864 
865 
866 
867 // Disposes a clauses and removes it from watcher lists.
868 // NOTE! Low-level; does NOT change the 'clauses' and 'learnts' vector.
869 void Solver::remove(Clause* c, bool just_dealloc) {
870  // no watches added for clauses of size < 2
871  if (!just_dealloc && c->size() >= 2){
872  removeWatch(getWatches(~(*c)[0]), c);
873  removeWatch(getWatches(~(*c)[1]), c);
874  }
875 
876  if (c->learnt()) d_stats.learnts_literals -= c->size();
877  else d_stats.clauses_literals -= c->size();
878 
879  if (getDerivation() == NULL) xfree(c);
880  else getDerivation()->removedClause(c);
881 }
882 
883 
884 
885 
886 /// Conflict handling
887 
888 // Pre-condition: 'elem' must exists in 'ws' OR 'ws' must be empty.
889 void Solver::removeWatch(std::vector<Clause*>& ws, Clause* elem) {
890  if (ws.size() == 0) return; // (skip lists that are already cleared)
891  size_type j = 0;
892  for (; ws[j] != elem; j++) {
893  // want to find the right j, so the loop should be executed
894  // and not wrapped in a debug guard
895  DebugAssert(j < ws.size(), "MiniSat::Solver::removeWatch: elem not in watched list");
896  }
897 
898  ws[j] = ws.back();
899  ws.pop_back();
900 }
901 
902 
903 // for a clause, of which the first literal is implied,
904 // get the highest decision level of the implying literals,
905 // i.e. the decision level from which on the literal is implied
906 //
907 // as theory clauses can be added at any time,
908 // this is not necessarily the level of the second literal.
909 // thus, all literals have to be checked.
910 int Solver::getImplicationLevel(const Clause& clause) const {
911  int currentLevel = decisionLevel();
912  int maxLevel = d_rootLevel;
913 
914  for (int i = 1; i < clause.size(); ++i) {
915  DebugAssert(getValue(clause[i]) == l_False,
916  "MiniSat::Solver::getImplicationLevelFull: literal not false");
917 
918  int newLevel = getLevel(clause[i]);
919 
920  // highest possible level
921  if (newLevel == currentLevel)
922  return currentLevel;
923 
924  // highest level up to now
925  if (newLevel > maxLevel)
926  maxLevel = newLevel;
927  }
928 
929  return maxLevel;
930 }
931 
932 
933 // like getImplicationLevel, but for all literals,
934 // i.e. for conflicting instead of propagating clause
935 int Solver::getConflictLevel(const Clause& clause) const {
937 
938  for (int i = 0; i < clause.size(); ++i) {
939  DebugAssert(getValue(clause[i]) == l_False, "MiniSat::Solver::getConflictLevel: literal not false");
940 
941  int newLevel = getLevel(clause[i]);
942  if (newLevel > decisionLevel)
943  decisionLevel = newLevel;
944  }
945 
946  return decisionLevel;
947 }
948 
949 
950 Clause* Solver::getReason(Lit literal, bool _resolveTheoryImplication) {
951  Var var = literal.var();
952  Clause* reason = d_reason[var];
953 
954  if (!_resolveTheoryImplication)
955  return reason;
956 
957  DebugAssert(reason != NULL, "MiniSat::getReason: reason[var] == NULL.");
958 
959  if (reason == Clause::TheoryImplication()) {
960  if (getValue(literal) == l_True)
961  resolveTheoryImplication(literal);
962  else
963  resolveTheoryImplication(~literal);
964  reason = d_reason[var];
965  }
966 
968  "MiniSat::getReason: reason[var] == TheoryImplication.");
969 
970  return reason;
971 }
972 
973 bool Solver::isConflicting() const {
974  return (d_conflict != NULL);
975 }
976 
978  DebugAssert(clause != NULL, "MiniSat::updateConflict: clause == NULL.");
979  IF_DEBUG (
980  for (int i = 0; i < clause->size(); ++i) {
981  DebugAssert(getValue((*clause)[i]) == l_False, "MiniSat::Solver::updateConflict: literal not false");
982  }
983  )
984 
985  if (
986  (d_conflict == NULL)
987  ||
988  (clause->size() < d_conflict->size())
989  ) {
990  d_conflict = clause;
991  }
992 }
993 
994 
995 
996 // retrieve the explanation and update the implication level of a theory implied literal.
997 // if necessary, do this recursively (bottom up) for the literals in the explanation.
998 // assumes that the literal is true in the current context
1000  if (eager_explanation) return;
1001 
1002  if (d_reason[literal.var()] == Clause::TheoryImplication()) {
1003  // instead of recursion put the theory implications to check in toRegress,
1004  // and the theory implications depending on them in toComplete
1005  stack<Lit> toRegress;
1006  stack<Clause*> toComplete;
1007  toRegress.push(literal);
1008 
1009  SAT::Clause clauseCVC;
1010  while (!toRegress.empty()) {
1011  // get the explanation for the first theory implication
1012  literal = toRegress.top();
1013  DebugAssert(getValue(literal) == l_True,
1014  "MiniSat::Solver::resolveTheoryImplication: literal is not true");
1015  toRegress.pop();
1016  FatalAssert(false, "Not implemented yet");
1017  // d_theoryAPI->getExplanation(miniSatToCVC(literal), clauseCVC);
1018  Clause* explanation = cvcToMiniSat(clauseCVC, nextClauseID());
1019 
1020  // must ensure that propagated literal is at first position
1021  for (int i = 0; i < (*explanation).size(); ++i) {
1022  if ((*explanation)[i] == literal) {
1023  MiniSat::Lit swap = (*explanation)[0];
1024  (*explanation)[0] = (*explanation)[i];
1025  (*explanation)[i] = swap;
1026  break;
1027  }
1028  }
1029  // assert that clause is implying the first literal
1030  IF_DEBUG(
1031  DebugAssert((*explanation)[0] == literal,
1032  "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 1");
1033  DebugAssert(getValue((*explanation)[0]) == l_True,
1034  "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 2");
1035  for (int i = 1; i < (*explanation).size(); ++i) {
1036  DebugAssert(getValue((*explanation)[i]) == l_False,
1037  "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 3");
1038  }
1039  )
1040  d_reason[literal.var()] = explanation;
1041 
1042  // if any of the reasons is also a theory implication,
1043  // then need to know its level first, so add it to toRegress
1044  for (int i = 1; i < (*explanation).size(); ++i) {
1045  if (d_reason[(*explanation)[i].var()] == Clause::TheoryImplication()) {
1046  toRegress.push((*explanation)[i]);
1047  }
1048  }
1049  // set literal and its explanation aside for later processing
1050  toComplete.push(explanation);
1051  }
1052 
1053  // now set the real implication levels after they have been resolved
1054  // std::pair<Lit, Clause*> pair;
1055  while (!toComplete.empty()) {
1056  Clause* explanation = toComplete.top();
1057  toComplete.pop();
1058 
1059  IF_DEBUG (
1060  for (int i = 1; i < explanation->size(); ++i) {
1061  DebugAssert (d_reason[(*explanation)[i].var()] != Clause::TheoryImplication(),
1062  "MiniSat::Solver::resolveTheoryImplication: not done to completion");
1063  }
1064  )
1065 
1066  // update propagation information
1067  int level = getImplicationLevel(*explanation);
1068  setLevel((*explanation)[0], level);
1069  setPushID((*explanation)[0].var(), explanation);
1070 
1071  if (keep_lazy_explanation) {
1072  // the reason can be added to the clause set without any effect,
1073  // as the explanation implies the first literal, which is currently true
1074  // so neither propagation nor conflict are triggered,
1075  // only the correct literals are registered as watched literals.
1076  addClause(*explanation, true);
1077  xfree(explanation);
1078  } else {
1079  // store explanation for later deallocation
1080  d_theoryExplanations.push(std::make_pair(level, explanation));
1081  }
1082  }
1083  }
1084 
1085 }
1086 
1087 
1088 
1089 /// Conflict handling
1090 
1091 Clause* Solver::analyze(int& out_btlevel) {
1092  DebugAssert(d_conflict != NULL, "MiniSat::Solver::analyze called when no conflict was detected");
1093 
1094  // compute the correct decision level for theory propagated literals
1095  //
1096  // need to find the most recent implication level of any of the literals in d_conflict,
1097  // after updating conflict levels due to lazy retrieval of theory implications.
1098  //
1099  // that is, really need to do:
1100  // 1) assume that the currently highest known level is the UIP Level,
1101  // initially this is the decision level
1102  // 2) find a literal in the conflict clause whose real implication level is the UIP Level
1103  // 3) if their is no such literal, pick the new UIP level as the highest of their implication levels,
1104  // and repeat
1105  //
1106  // unfortunately, 2) is not that easy:
1107  // - if the literals' level is smaller than the UIP level the literal can be ignored
1108  // - otherwise, it might depend on theory implications,
1109  // who have just been assumed to be of the UIP level, but which in reality are of lower levels.
1110  // So, must check all literals the literal depends on,
1111  // until the real level of all of them is determined,
1112  // and thus also of the literal we are really interested in.
1113  // this can be stopped if the level must be lower than the (currently assumed) UIP level,
1114  // or if it is sure that the literal really has the UIP level.
1115  // but this is only the case if it depends on the decision literal of the UIP level.
1116  //
1117  // but how to find this out efficiently?
1118  //
1119  // so, this is done as an approximation instead:
1120  // 1) if the explanation of a (conflict clause) literal is known, stop and take the literal's level
1121  // 2) otherwise, retrieve its explanation,
1122  // and do 1) and 2) on each literal in the explanation.
1123  // then set the original literal's level to the highest level of its explanation.
1124  //
1125  // as an example, if we have:
1126  // - theory implication A in level n
1127  // - propositional implication B depending on A and literals below level n
1128  // - propositional implication C depending on B and literals below level n
1129  // then A, B, C will all be assumed to be of level n,
1130  // and if C is in a conflict it will be assumed to be of level n
1131  // in the conflict analysis
1132  //
1133  // this is fast to compute,
1134  // but it is not clear if starting from the real UIP level
1135  // would lead to a significantly better lemma
1136  for (int j = 0; j < d_conflict->size(); j++){
1138  }
1139  int UIPLevel = getConflictLevel(*d_conflict);
1140 
1141  // clause literals to regress are marked by setting analyze_d_seen[var]
1142  // seen should be false for all variables
1143  IF_DEBUG (
1144  for (size_type i = 0; i < d_analyze_seen.size(); ++i) {
1145  DebugAssert (d_analyze_seen[i] == 0, "MiniSat::Solver::analyze: analyze_seen is not clear at: " /*+ i*/);
1146  }
1147  )
1148  // index into trail, regression is done chronologically (in combination with analyze_seen)
1149  int index = d_trail.size() - 1;
1150  // lemma is generated here;
1151  vector<Lit> out_learnt;
1152  // number of literals to regress in current decision level
1153  int pathC = 0;
1154  // highest level below UIP level, i.e. the level to backtrack to
1155  out_btlevel = 0;
1156  // current literal to regress
1157  Lit p = lit_Undef;
1158 
1159  // derivation logging
1160  Inference* inference = NULL;
1161  if (getDerivation() != NULL) inference = new Inference(d_conflict->id());
1162 
1163  // conflict clause is the initial clause to regress
1164  Clause* confl = d_conflict;
1165  d_conflict = NULL;
1166 
1167  // compute pushID as max pushID of all regressed clauses
1168  int pushID = confl->pushID();
1169 
1170  // do until pathC == 1, i.e. UIP found
1171  if (confl->size() == 1) {
1172  out_learnt.push_back((*confl)[0]);
1173  } else {
1174  // leave room for the asserting literal -
1175  // we might get an empty lemma if a new clause is conflicting at the root level.
1176  if (UIPLevel != d_rootLevel) out_learnt.push_back(lit_Undef);
1177 
1178  do {
1179  DebugAssert (confl != Clause::Decision(), "MiniSat::Solver::analyze: no reason for conflict");
1180  DebugAssert (confl != Clause::TheoryImplication(), "MiniSat::Solver::analyze: theory implication not resolved");
1181 
1182  if (confl->learnt()) claBumpActivity(confl);
1183 
1184  // regress p
1185  for (int j = (p == lit_Undef) ? 0 : 1; j < confl->size(); j++){
1186  Lit q = (*confl)[j];
1187  DebugAssert(getValue(q) == l_False, "MiniSat::Solver::analyze: literal to regress is not false");
1188  DebugAssert(getLevel(q) <= UIPLevel, "MiniSat::Solver::analyze: literal above UIP level");
1189 
1190  // get explanation and compute implication level for theory implication
1192 
1193  // first time that q is in a reason, so process it
1194  if (!d_analyze_seen[q.var()]) {
1195  // q is falsified at root level, so it can be dropped
1196  if (getLevel(q) == d_rootLevel) {
1197  d_analyze_redundant.push_back(q);
1198  d_analyze_seen[q.var()] = 1;
1199  }
1200  else {
1201  varBumpActivity(q);
1202  d_analyze_seen[q.var()] = 1;
1203  // mark q to regress
1204  if (getLevel(q) == UIPLevel)
1205  pathC++;
1206  // add q to lemma
1207  else{
1208  out_learnt.push_back(q);
1209  out_btlevel = max(out_btlevel, getLevel(q));
1210  }
1211  }
1212  }
1213  }
1214 
1215  // for clause conflicting at root level pathC can be 0 right away
1216  if (pathC == 0) break;
1217 
1218  // pick next literal in UIP level to regress.
1219  // as trail is not ordered wrt. implication level (theory clause/ implications),
1220  // check also if the next literal is really from the UIP level.
1221  while (!d_analyze_seen[d_trail[index].var()] || (getLevel(d_trail[index])) != UIPLevel) {
1222  --index;
1223  }
1224  --index;
1225  // this could theoretically happen if UIP Level is 0,
1226  // but should be catched as then the conflict clause
1227  // is simplified to the empty clause.
1228  DebugAssert(index >= -1, "MiniSat::Solver::analyze: index out of bound");
1229 
1230  // set up p to be regressed
1231  p = d_trail[index+1];
1232  d_analyze_seen[p.var()] = 0;
1233  pathC--;
1234 
1235  confl = getReason(p);
1236  pushID = max(pushID, confl->pushID());
1237  if (getDerivation() != NULL && pathC > 0) inference->add(~p, confl);
1238  } while (pathC > 0);
1239  // add the UIP - except in root level, here all literals have been resolved.
1240  if (UIPLevel != d_rootLevel) out_learnt[0] = ~p;
1241  }
1242 
1243  // check that the UIP has been found
1244  IF_DEBUG (
1245  DebugAssert ((out_learnt.size() == 0 && UIPLevel == d_rootLevel)
1246  || getLevel(out_learnt[0]) == UIPLevel,
1247  "MiniSat::Solver::analyze: backtracked past UIP level.");
1248  for (size_type i = 1; i < out_learnt.size(); ++i) {
1249  DebugAssert (getLevel(out_learnt[i]) < UIPLevel,
1250  "MiniSat::Solver::analyze: conflict clause contains literal from UIP level or higher.");
1251  }
1252  )
1253 
1254  analyze_minimize(out_learnt, inference, pushID);
1255 
1256  // clear seen for lemma
1257  for (vector<Lit>::const_iterator j = out_learnt.begin(); j != out_learnt.end(); ++j) {
1258  d_analyze_seen[j->var()] = 0;
1259  }
1260 
1261  // finish logging of conflict clause generation
1262  int clauseID = nextClauseID();
1263  if (getDerivation() != NULL) getDerivation()->registerInference(clauseID, inference);
1264 
1265  return Lemma_new(out_learnt, clauseID, pushID);
1266 }
1267 
1268 class lastToFirst_lt { // Helper class to 'analyze' -- order literals from last to first occurance in 'trail[]'.
1269  const vector<MiniSat::size_type>& d_trail_pos;
1270 public:
1271  lastToFirst_lt(const vector<MiniSat::size_type>& trail_pos) : d_trail_pos(trail_pos) {}
1272 
1273  bool operator () (Lit p, Lit q) {
1274  return d_trail_pos[p.var()] > d_trail_pos[q.var()];
1275  }
1276 };
1277 
1278 void Solver::analyze_minimize(vector<Lit>& out_learnt, Inference* inference, int& pushID) {
1279  // for empty clause current analyze_minimize will actually do something wrong
1280  if (out_learnt.size() > 1) {
1281 
1282  // literals removed from out_learnt in conflict clause minimization,
1283  // including reason literals which had to be removed as well
1284  // (except for literals implied at root level).
1285  size_type i, j;
1286  // 1) Simplify conflict clause (a lot):
1287  // drop a literal if it is implied by the remaining lemma literals:
1288  // that is, as in 2), but also recursively taking the reasons
1289  // for the implying clause, and their reasone, and so on into consideration.
1290  if (d_expensive_ccmin){
1291  // (maintain an abstraction of levels involved in conflict)
1292  unsigned int min_level = 0;
1293  for (i = 1; i < out_learnt.size(); i++)
1294  min_level |= 1 << (getLevel(out_learnt[i]) & 31);
1295 
1296  for (i = j = 1; i < out_learnt.size(); i++) {
1297  Lit lit(out_learnt[i]);
1298  if (getReason(lit) == Clause::Decision() || !analyze_removable(lit, min_level, pushID))
1299  out_learnt[j++] = lit;
1300  }
1301  }
1302  // 2) Simplify conflict clause (a little):
1303  // drop a literal if it is implied by the remaining lemma literals:
1304  // that is, if the other literals of its implying clause
1305  // are falsified by the other lemma literals.
1306  else {
1307  for (i = j = 1; i < out_learnt.size(); i++) {
1308  Lit lit(out_learnt[i]);
1309  Clause& c = *getReason(lit);
1310  if (&c == Clause::Decision()) {
1311  out_learnt[j++] = lit;
1312  } else {
1313  bool keep = false;
1314  // all literals of the implying clause must be:
1315  for (int k = 1; !keep && k < c.size(); k++) {
1316  if (
1317  // already part of the lemma
1318  !d_analyze_seen[c[k].var()]
1319  &&
1320  // or falsified in the root level
1321  getLevel(c[k]) != d_rootLevel
1322  ) {
1323  // failed, can't remove lit
1324  out_learnt[j++] = lit;
1325  keep = true;
1326  }
1327  }
1328  if (!keep) {
1329  d_analyze_redundant.push_back(lit);
1330  }
1331  }
1332  }
1333  }
1334 
1335  out_learnt.resize(j);
1336  }
1337 
1338  // clean seen for simplification and log derivation
1339  // do this in reverse chronological order of variable assignment
1340  // in combination with removing duplication literals after each resolution step
1341  // this allows to resolve on each literal only once,
1342  // as it depends only on literals (its clause contains only literals)
1343  // which were assigned earlier.
1344  if (getDerivation() != NULL) {
1346  }
1347  for (vector<Lit>::const_iterator i = d_analyze_redundant.begin(); i != d_analyze_redundant.end(); ++i) {
1348  Lit lit(*i);
1349  d_analyze_seen[lit.var()] = 0;
1350 
1351  // if this literal is falsified in the root level,
1352  // but not implied in the current push level,
1353  // and the lemma is currently valid in levels lower than the current push level,
1354  // then don't remove the literal.
1355  // instead move it to the end of the lemma,
1356  // so that it won't hurt performance.
1357  if (out_learnt.size() > 0 // found the empty clause, so remove all literals
1358  &&
1359  getLevel(lit) == d_rootLevel
1360  &&
1361  getPushID(lit) > pushID
1362  &&
1363  !d_pushes.empty()
1364  &&
1365  getPushID(lit) > d_pushes.front().d_clauseID
1366  ) {
1367  out_learnt.push_back(lit);
1368  continue;
1369  }
1370 
1371  // update the push level and the derivation wrt. the removed literal
1372 
1373  pushID = max(pushID, getPushID(lit));
1374 
1375  if (getDerivation() != NULL) {
1376  // resolve on each removed literal with its reason
1377  if (getLevel(lit) == d_rootLevel) {
1378  inference->add(lit, getDerivation()->computeRootReason(~lit, this));
1379  }
1380  else {
1381  Clause* reason = getReason(lit);
1382  inference->add(lit, reason);
1383  }
1384  }
1385  }
1386 
1387  d_analyze_redundant.clear();
1388 }
1389 
1390 
1391 // Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
1392 //
1393 // 'p' can be removed if it depends only on literals
1394 // on which they other conflict clause literals do depend as well.
1395 bool Solver::analyze_removable(Lit p, unsigned int min_level, int pushID) {
1396  DebugAssert(getReason(p) != Clause::Decision(), "MiniSat::Solver::analyze_removable: p is a decision.");
1397 
1398  d_analyze_stack.clear();
1399  d_analyze_stack.push_back(p);
1400  int top = d_analyze_redundant.size();
1401 
1402  while (d_analyze_stack.size() > 0){
1404  "MiniSat::Solver::analyze_removable: stack var is a decision.");
1406  "MiniSat::Solver::analyze_removable: stack var is an unresolved theory implication.");
1407  Clause& c = *getReason(d_analyze_stack.back()); d_analyze_stack.pop_back();
1408  for (int i = 1; i < c.size(); i++) {
1409  Lit p = c[i];
1410  // ignore literals already considered or implied at root level
1411  if (!d_analyze_seen[p.var()]) {
1412  if (getLevel(p) == d_rootLevel) {
1413  d_analyze_redundant.push_back(p);
1414  d_analyze_seen[p.var()] = 1;
1415  }
1416  else {
1417  // min_level is a precheck,
1418  // only try to remove literals which might be implied,
1419  // at least wrt. to the abstraction min_level
1420  if (getReason(p) != Clause::Decision() && ((1 << (getLevel(p) & 31)) & min_level) != 0){
1421  d_analyze_seen[p.var()] = 1;
1422  d_analyze_stack.push_back(p);
1423  d_analyze_redundant.push_back(p);
1424  } else {
1425  // failed, so undo changes to seen literals/redundant and return
1426  for (size_type j = top; j < d_analyze_redundant.size(); ++j) {
1427  d_analyze_seen[d_analyze_redundant[j].var()] = 0;
1428  }
1429  d_analyze_redundant.resize(top);
1430  return false;
1431  }
1432  }
1433  }
1434  }
1435  }
1436 
1437  d_analyze_redundant.push_back(p);
1438  return true;
1439 }
1440 
1441 
1442 
1443 bool Solver::isImpliedAt(Lit lit, int clausePushID) const {
1444  return
1445  // literal asserted before first push
1446  (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
1447  ||
1448  // or literal depends only on clauses added before given clause
1449  getPushID(lit) < clausePushID;
1450 
1451 }
1452 
1453 
1454 // Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
1455 // the clause is binary and satisfied, in which case the first literal is true)
1456 // Returns True if clause is satisfied (will be removed), False otherwise.
1457 //
1459  for (int i = 0; i < c->size(); i++){
1460  Lit lit((*c)[i]);
1461  if (getValue(lit) == l_True
1462  && getLevel(lit) == d_rootLevel
1463  && isImpliedAt(lit, c->pushID())
1464  )
1465  return true;
1466  }
1467  return false;
1468 }
1469 
1470 
1471 
1472 // a split decision, returns FALSE if immediate conflict.
1474  d_trail_lim.push_back(d_trail.size());
1476  return enqueue(p, decisionLevel(), Clause::Decision());
1477 }
1478 
1479 
1480 // Revert to the state at given level, assert conflict clause and pending clauses
1481 void Solver::backtrack(int toLevel, Clause* learnt_clause) {
1482  DebugAssert (decisionLevel() > toLevel, "MiniSat::Solver::backtrack: backtrack not to previous level");
1483 
1484  // backtrack theories
1485  DebugAssert(toLevel >= d_rootLevel, "MiniSat::Solver::backtrack: backtrack beyond root level");
1486  for (int i = toLevel; i < decisionLevel(); ++i) {
1487  d_theoryAPI->pop();
1488  }
1489 
1490  // backtrack trail
1491  int trail_size = d_trail.size();
1492  int trail_jump = d_trail_lim[toLevel];
1493  int first_invalid = d_trail_lim[toLevel];
1494  for (int c = first_invalid; c < trail_size; ++c) {
1495  Var x = d_trail[c].var();
1496  // only remove enqueued elements which are not still implied after backtracking
1497  if (getLevel(x) > toLevel) {
1498  //setLevel(x, -1);
1499  d_assigns[x] = toInt(l_Undef);
1500  d_reason [x] = NULL;
1501  //d_pushIDs[x] = -1;
1502  d_order.undo(x);
1503  }
1504  else {
1505  d_trail[first_invalid] = d_trail[c];
1506  if (d_derivation != NULL) d_trail_pos[x] = first_invalid;
1507  ++first_invalid;
1508  }
1509  }
1510  // shrink queue
1511  d_trail.resize(first_invalid);
1512  d_trail_lim.resize(toLevel);
1513  d_qhead = trail_jump;
1514  d_thead = d_qhead;
1515 
1516  // insert lemma
1517  // we want to insert the lemma before the original conflicting clause,
1518  // so that propagation is done on the lemma instead of that clause.
1519  // as that clause might be a theory clause in d_pendingClauses,
1520  // the lemma has to be inserted before the pending clauses are added.
1521  insertClause(learnt_clause);
1522 
1523 
1524  // enqueue clauses which were conflicting in previous assignment
1525  while (!isConflicting() && !d_pendingClauses.empty()) {
1526  Clause* c = d_pendingClauses.front();
1527  d_pendingClauses.pop();
1528  addClause(*c, true);
1529  xfree(c);
1530  }
1531 
1532 
1533  // deallocate explanations for theory implications
1534  // which have been retracted and are thus not needed anymore.
1535  //
1536  // not necessarily ordered by level,
1537  // so stackwise deallocation by level does not necessarily remove
1538  // all possible explanations as soon as possible.
1539  // still, should be a good enough compromise between speed and completeness.
1540  bool done = false;
1541  while (!done && !d_theoryExplanations.empty()) {
1542  std::pair<int, Clause*> pair = d_theoryExplanations.top();
1543  if (pair.first > toLevel) {
1544  d_theoryExplanations.pop();
1545  remove(pair.second, true);
1546  }
1547  else {
1548  done = true;
1549  }
1550  }
1551 }
1552 
1553 
1554 /*_________________________________________________________________________________________________
1555 |
1556 | enqueue : (p : Lit) (from : Clause*) -> [bool]
1557 |
1558 | Description:
1559 | Puts a new fact on the propagation queue as well as immediately updating the variable's value.
1560 | Should a conflict arise, FALSE is returned.
1561 |
1562 | Input:
1563 | p - The fact to enqueue
1564 | decisionLevel - The level from which on this propagation/decision holds.
1565 | if a clause is added in a non-root level, there might be propagations
1566 | which are not only valid in the current, but also earlier levels.
1567 | from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
1568 | Default value is NULL (no reason).
1569 | GClause::s_theoryImplication means theory implication where explanation
1570 | has not been retrieved yet.
1571 |
1572 | Output:
1573 | TRUE if fact was enqueued without conflict, FALSE otherwise.
1574 |________________________________________________________________________________________________@*/
1575 bool Solver::enqueue(Lit p, int decisionLevel, Clause* from) {
1576  lbool value(getValue(p));
1577  if (value != l_Undef) {
1578  return value != l_False;
1579  }
1580  else {
1581  Var var(p.var());
1582  d_assigns[var] = toInt(lbool(p.sign()));
1583  setLevel(var, decisionLevel);
1584  d_reason [var] = from;
1585  setPushID(var, from);
1586  d_trail.push_back(p);
1587  if (d_derivation != NULL) d_trail_pos[var] = d_trail.size();
1588  return true;
1589  }
1590 }
1591 
1592 
1593 /*_________________________________________________________________________________________________
1594 |
1595 | propagate : [void] -> [Clause*]
1596 |
1597 | Description:
1598 | Propagates one enqueued fact. If a conflict arises, updateConflict is called.
1599 |________________________________________________________________________________________________@*/
1600 
1601 // None:
1602 //
1603 // due to theory clauses and lazy retrieval of theory implications we get propagations
1604 // out of any chronological order.
1605 // therefore it is not guaranteed that in a propagating clause
1606 // the first two literals (the watched literals) have the highest decision level.
1607 //
1608 // this doesn't matter, though, it suffices to ensure that
1609 // if there are less than two undefined literals in a clause,
1610 // than these are at the first two positions?
1611 //
1612 // Reasoning, for eager retrieval of explanations for theory implications:
1613 // case analysis for first two positions:
1614 // 1) TRUE, TRUE
1615 // then the clause is satisfied until after backtracking
1616 // the first two literals are undefined, or we get case 2) TRUE, FALSE
1617 //
1618 // 2) TRUE, FALSE
1619 // if TRUE is true because it is a theory implication of FALSE,
1620 // this is fine, as TRUE and FALSE will be backtracked at the same time,
1621 // and then both literals will be undefined.
1622 //
1623 // this holds in general if TRUE was set before FALSE was set,
1624 // so this case is fine.
1625 //
1626 // and TRUE can't be set after FALSE was set,
1627 // as this would imply that all other literals are falsified as well
1628 // (otherwise the FALSE literal would be replace by an undefined/satisfied literal),
1629 // and then TRUE would be implied at the same level as FALSE
1630 //
1631 // 3) FALSE, TRUE
1632 // can not happen, falsifying the first literal will reorder this to TRUE, FALSE
1633 //
1634 // 4) FALSE, FALSE
1635 // Both literals must be falsified at the current level,
1636 // as falsifying one triggers unit propagation on the other in the same level.
1637 // so after backtracking both are undefined.
1638 //
1639 //
1640 // now, if explanations for theory implications are retrieved lazily,
1641 // then the level in which a literal was set might change later on.
1642 // i.e. first it is assumed to be of the level in which the theory implication happened,
1643 // but later on, when checking its explanation,
1644 // the real level might be calculated to be an earlier level.
1645 //
1646 // this means, when the original level was L and the real level is K,
1647 // that this literal is going to be undefined when backtracking before L,
1648 // but is immediately propagated again if the new level is >= K.
1649 // this is done until level K is reached,
1650 // then this literal behaves like any ordinary literal.
1651 // (ensured by backtrack)
1652 //
1653 // case analysis for first two positions:
1654 // 1) TRUE, TRUE
1655 // same as before
1656 //
1657 // 2) TRUE, FALSE
1658 // the new case is that TRUE was initially of level <= FALSE,
1659 // but now FALSE is set to a level < TRUE.
1660 //
1661 // then when on backtracking TRUE is unset,
1662 // FALSE will also be unset, but then right away be set to FALSE again,
1663 // so they work fine as watched literals.
1664 //
1665 // 3) FALSE, TRUE
1666 // same as before
1667 //
1668 // 4) FALSE, FALSE
1669 // if the level of both literals is unchanged,
1670 // changes in other literals don't matter,
1671 // as after backtracking both are undefined (same as before)
1672 //
1673 // if for one of the two (or both) the level is changed,
1674 // after backtracking it will be falsified again immediately,
1675 // and the watched literal works as expected:
1676 // either the other literal is propagated,
1677 // or there is now an undefined literal in the rest of the clause
1678 // which becomes the new watched literal.
1679 //
1680 // changes in the rest of the clause are of no consequence,
1681 // as they are assumed to be false in the conflict level,
1682 // changes in their level do not change this,
1683 // and after backtracking they are again taken into consideration
1684 // for finding a new watched literal.
1685 //
1686 // so, even for lazy retrieval of theory implication explanations
1687 // there is no need to explicitly set the 2nd watched literal
1688 // to the most recently falsified one.
1690  Lit p = d_trail[d_qhead++]; // 'p' is enqueued fact to propagate.
1691  vector<Clause*>& ws = getWatches(p);
1692 
1694  --d_simpDB_props;
1695  if (getLevel(p) == d_rootLevel) ++d_simpDB_assigns;
1696 
1697  // propagate p to theories
1698  if (!defer_theory_propagation) {
1700  ++d_thead;
1701  }
1702 
1703  vector<Clause*>::iterator j = ws.begin();
1704  vector<Clause*>::iterator i = ws.begin();
1705  vector<Clause*>::iterator end = ws.end();
1706  while (i != end) {
1707  Clause& c = **i;
1708  ++i;
1709 
1710  // Make sure the false literal is data[1]:
1711  Lit false_lit = ~p;
1712  if (c[0] == false_lit) {
1713  c[0] = c[1];
1714  c[1] = false_lit;
1715  }
1716 
1717  Lit first = c[0];
1718  lbool val = getValue(first);
1719 
1720  // If 0th watch is true, then clause is already satisfied.
1721  if (val == l_True) {
1722  DebugAssert(getValue(c[0]) == l_True && getValue(c[1]) == l_False,
1723  "MiniSat::Solver:::propagate: True/False");
1724  *j = &c; ++j;
1725  }
1726  // Look for new watch:
1727  else {
1728  for (int k = 2; k < c.size(); k++) {
1729  if (getValue(c[k]) != l_False) {
1730  c[1] = c[k];
1731  c[k] = false_lit;
1732  addWatch(~c[1], &c);
1733  goto FoundWatch;
1734  }
1735  }
1736 
1737  // Did not find watch -- clause is unit under assignment:
1738 
1739  // check that all other literals are false
1740  IF_DEBUG(
1741  for (int z = 1; z < c.size(); ++z) {
1742  DebugAssert(getValue(c[z]) == l_False,
1743  "MiniSat::Solver:::propagate: Unit Propagation");
1744  }
1745  )
1746 
1747  *j = &c; ++j;
1748  if (!enqueue(first, getImplicationLevel(c), &c)){
1749  // clause is conflicting
1750  updateConflict(&c);
1751  d_qhead = d_trail.size();
1752 
1753  // remove gap created by watches for which a new watch has been picked
1754  if (i != j) ws.erase(j, i);
1755  return;
1756  }
1757 
1758  FoundWatch:;
1759  }
1760  }
1761 
1762  // remove gap created by watches for which a new watch has been picked
1763  ws.erase(j, ws.end());
1764 }
1765 
1766 
1767 /*_________________________________________________________________________________________________
1768 |
1769 | reduceDB : () -> [void]
1770 |
1771 | Description:
1772 | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
1773 | clauses are clauses that are reason to some assignment. Binary clauses are never removed.
1774 |________________________________________________________________________________________________@*/
1775 struct reduceDB_lt {
1776  bool operator () (Clause* x, Clause* y) {
1777  return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity());
1778  }
1779 };
1780 
1782  d_stats.lm_simpl++;
1783 
1784  size_type i, j;
1785  double extra_lim = d_cla_inc / d_learnts.size(); // Remove any clause below this activity
1786 
1787  std::sort(d_learnts.begin(), d_learnts.end(), reduceDB_lt());
1788  for (i = j = 0; i < d_learnts.size() / 2; i++){
1789  if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]))
1790  remove(d_learnts[i]);
1791  else
1792  d_learnts[j++] = d_learnts[i];
1793  }
1794  for (; i < d_learnts.size(); i++){
1795  if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]) && d_learnts[i]->activity() < extra_lim)
1796  remove(d_learnts[i]);
1797  else
1798  d_learnts[j++] = d_learnts[i];
1799  }
1800 
1801  d_learnts.resize(d_learnts.size() - (i - j), NULL);
1802  d_stats.del_lemmas += (i - j);
1803 
1804  d_simpRD_learnts = d_learnts.size();
1805 }
1806 
1807 
1808 /*_________________________________________________________________________________________________
1809 |
1810 | simplifyDB : [void] -> [bool]
1811 |
1812 | Description:
1813 | Simplify the clause database according to the current top-level assigment. Currently, the only
1814 | thing done here is the removal of satisfied clauses, but more things can be put here.
1815 |________________________________________________________________________________________________@*/
1817  // clause set is unsatisfiable
1818  if (isConflicting()) return;
1819 
1820  // need to do propagation to exhaustion before watches can be removed below.
1821  // e.g. in a <- b, c, where b an c are satisfied by unit clauses,
1822  // and b and c have been added to the propagation queue,
1823  // but not propagated yet: then the watches are not evaluated yet,
1824  // and a has not been propapagated.
1825  // thus by removing the watches on b and c,
1826  // the propagation of a would be lost.
1827  DebugAssert(d_qhead == d_trail.size(),
1828  "MiniSat::Solver::simplifyDB: called while propagation queue was not empty");
1829 
1830  d_stats.db_simpl++;
1831 
1832  // Clear watcher lists:
1833  // could do that only for literals which are implied permanently,
1834  // but we don't know that anymore with the push/pop interface:
1835  // even if the push id of a literal is less than the first push clause id,
1836  // it might depend on theory clauses,
1837  // which will be retracted after a pop,
1838  // so that the literal is not implied anymore.
1839  // thus, this faster way of cleaning watches can not be used,
1840  // instead they have to removed per clause below
1841  /*
1842  Lit lit;
1843  for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
1844  lit = *i;
1845  if (getLevel(lit) == d_rootLevel
1846  &&
1847  // must be in the root push
1848  (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
1849  ) {
1850  getWatches(lit).clear();
1851  getWatches(~(lit)).clear();
1852  }
1853  }
1854  */
1855 
1856  // Remove satisfied clauses:
1857  for (int type = 0; type < 2; type++){
1858  vector<Clause*>& cs = type ? d_learnts : d_clauses;
1859  size_type j = 0;
1860  bool satisfied = false;
1861  for (vector<Clause*>::const_iterator i = cs.begin(); i != cs.end(); ++i) {
1862  Clause* clause = *i;
1863 
1864 
1865  if (isReason(clause)) {
1866  cs[j++] = clause;
1867  }
1868  else {
1869  satisfied = false;
1870  // falsified = 0;
1871  int k = 0;
1872  int end = clause->size() - 1;
1873  // skip the already permanently falsified tail
1874  // clause should not be permanently falsified,
1875  // as simplifyDB should only be called in a consistent state.
1876  while (
1877  (getLevel((*clause)[end]) == d_rootLevel)
1878  &&
1879  (getValue((*clause)[end]) == l_False)) {
1880  DebugAssert(end > 0,
1881  "MiniSat::Solver::simplifyDB: permanently falsified clause found");
1882  --end;
1883  }
1884 
1885  while (k < end) {
1886  Lit lit((*clause)[k]);
1887  if (getLevel(lit) != d_rootLevel) {
1888  ++k;
1889  }
1890  else if (getValue(lit) == l_True) {
1891  if (isImpliedAt(lit, clause->pushID())) {
1892  satisfied = true;
1893  break;
1894  }
1895  else {
1896  ++k;
1897  }
1898  }
1899  else if (k > 1 && getValue(lit) == l_False) {
1900  --end;
1901  (*clause)[k] = (*clause)[end];
1902  (*clause)[end] = lit;
1903  } else {
1904  ++k;
1905  }
1906  }
1907 
1908  if (satisfied) {
1909  d_stats.del_clauses++;
1910  remove(clause);
1911  }
1912  else {
1913  cs[j++] = clause;
1914  }
1915  }
1916 
1917 
1918  // isReason also ensures that unit clauses are kept
1919  /*
1920  if (!isReason(clause) && isPermSatisfied(clause)) {
1921  d_stats.del_clauses++;
1922  remove(clause);
1923  }
1924  else {
1925  cs[j++] = clause;
1926  }*/
1927 
1928  }
1929  cs.resize(j);
1930  }
1931 
1932  d_simpDB_assigns = 0;
1934 }
1935 
1936 
1938  if (protocol) {
1939  Lit lit(d_trail[d_qhead]);
1940  cout << "propagate: " << decisionLevel() << " : " << lit.index() << endl;
1941  cout << "propagate: " << decisionLevel() << " : " << toString(lit, true)
1942  << " at: " << getLevel(lit);
1943  if (getReason(lit.var()) != Clause::Decision())
1944  cout << " from: " << toString(*getReason(lit.var()), true);
1945  cout << endl;
1946  }
1947 }
1948 
1949 
1951  // retrieve the best vars according to the heuristic
1952  vector<Var> nextVars(prop_lookahead);
1953  vector<Var>::size_type fetchedVars = 0;
1954  while (fetchedVars < nextVars.size()) {
1955  Var nextVar = d_order.select(params.random_var_freq);
1956  if (isRegistered(nextVar) || nextVar == var_Undef) {
1957  nextVars[fetchedVars] = nextVar;
1958  ++fetchedVars;
1959  }
1960  }
1961  // and immediately put the variables back
1962  for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
1963  if (nextVars[i] != var_Undef) d_order.undo(nextVars[i]);
1964  }
1965 
1966 
1967  // propagate on these vars
1968  int level = decisionLevel();
1969  int first_invalid = d_trail.size();
1970 
1971  for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
1972  Var nextVar = nextVars[i];
1973  if (nextVar == var_Undef) continue;
1974 
1975  for (int sign = 0; sign < 2; ++sign) {
1976  // first propagate on +var, then on -var
1977  if (sign == 0) {
1978  assume(Lit(nextVar, true));
1979  } else {
1980  assume(Lit(nextVar, false));
1981  }
1982 
1983  while (d_qhead < d_trail.size() && !isConflicting()) {
1985  propagate();
1986  }
1987  // propagation found a conflict
1988  if (isConflicting()) return;
1989 
1990  // otherwise remove assumption and backtrack
1991  for (int i = d_trail.size() - 1; i >= first_invalid; --i) {
1992  Var x = d_trail[i].var();
1993  d_assigns[x] = toInt(l_Undef);
1994  d_reason [x] = NULL;
1995  d_order.undo(x);
1996  }
1997  d_trail.resize(first_invalid);
1998  d_trail_lim.resize(level);
1999  d_qhead = first_invalid;
2000  }
2001  }
2002 }
2003 
2004 
2006  DebugAssert(d_popRequests == 0, "MiniSat::Solver::search: pop requests pending");
2007  DebugAssert(!d_pushes.empty(), "MiniSat::Solver::search: no push before search");
2008 
2009  d_inSearch = true;
2010 
2012  d_stats.starts++;
2013  d_var_decay = 1 / params.var_decay;
2014  d_cla_decay = 1 / params.clause_decay;
2015 
2016  if (protocol) printState();
2017 
2018  // initial unit propagation has been done in push -
2019  // already unsatisfiable without search
2020  if (!d_ok) {
2021  if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
2022  return CVC3::UNSATISFIABLE;
2023  }
2024 
2025  // main search loop
2026  SAT::Lit literal;
2027  SAT::CNF_Formula_Impl clauses;
2028  for (;;){
2029  // if (d_learnts.size() == 1 && decisionLevel() == 3) printState();
2030  // -1 needed if the current 'propagation' is a split
2031  DebugAssert(d_thead <= d_qhead, "MiniSat::Solver::search: thead <= qhead");
2033  "MiniSat::Solver::search: qhead >= trail_lim[decisionLevel()");
2035  "MiniSat::Solver::search: thead >= trail_lim[decisionLevel()");
2036 
2037  // 1. clause set detected to be unsatisfiable
2038  if (!d_ok) {
2039  d_stats.conflicts++;
2040  if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
2041  return CVC3::UNSATISFIABLE;
2042  }
2043 
2044  // 2. out of resources, e.g. quantifier instantiation aborted
2045  if (d_theoryAPI->outOfResources()) {
2046  return CVC3::ABORT;
2047  }
2048 
2049  // 3. boolean conflict, backtrack
2050  if (d_conflict != NULL){
2051  d_stats.conflicts++;
2052 
2053  // unsatisfiability detected
2054  if (decisionLevel() == d_rootLevel){
2055  d_ok = false;
2056  if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
2057  return CVC3::UNSATISFIABLE;
2058  }
2059 
2060  int backtrack_level;
2061  Clause* learnt_clause = analyze(backtrack_level);
2062  backtrack(backtrack_level, learnt_clause);
2063  if (protocol) {
2064  cout << "conflict clause: " << toString(*learnt_clause, true);
2065  clauses.print();
2066  }
2067  varDecayActivity();
2068  claDecayActivity();
2069 
2070  if (protocol) {
2071  cout << "backtrack to: " << backtrack_level << endl;
2072  }
2073  }
2074 
2075  // 4. theory conflict - cheap theory consistency check
2076  else if (d_theoryAPI->checkConsistent(clauses, false) == SAT::DPLLT::INCONSISTENT) {
2077  if (protocol) {
2078  cout << "theory inconsistency: " << endl;
2079  clauses.print();
2080  }
2082  addFormula(clauses, true);
2083  clauses.reset();
2084  while (!isConflicting() && d_ok && d_qhead < d_trail.size() && !isConflicting()) {
2086  propagate();
2087  }
2088  DebugAssert(isConflicting(), "expected conflict");
2089  }
2090 
2091  // 5. boolean propagation
2092  else if (d_qhead < d_trail.size()) {
2093  // do boolean propagation to exhaustion
2094  // before telling the theories about propagated literals
2096  while (d_ok && d_qhead < d_trail.size() && !isConflicting()) {
2098  propagate();
2099  }
2100  }
2101  // immediately tell theories about boolean propagations
2102  else {
2104  propagate();
2105  }
2106  }
2107 
2108  // :TODO: move to 8. tell theories about new boolean propagations
2109  // problem: can lead to worse performance,
2110  // apparently then to many theory clauses are learnt,
2111  // so need to forget them (database cleanup), or limit them (subsumption test)
2112  else if (defer_theory_propagation && d_thead < d_qhead) {
2113  while (d_thead < d_qhead) {
2115  ++d_thead;
2116  }
2117  }
2118 
2119  // everything else
2120  else {
2121  DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
2122 
2123  // 6. theory clauses
2124  if (d_theoryAPI->getNewClauses(clauses)) {
2125  if (protocol) {
2126  cout << "theory clauses: " << endl;
2127  clauses.print();
2128  printState();
2129  }
2130 
2131  addFormula(clauses, true);
2132  clauses.reset();
2133  continue;
2134  }
2135 
2136  // 7. theory implication
2137  literal = d_theoryAPI->getImplication();
2138  if (!literal.isNull()) {
2139  Lit lit = MiniSat::cvcToMiniSat(literal);
2140  if (protocol) {
2141  cout << "theory implication: " << lit.index() << endl;
2142  }
2143  if (
2144  // get explanation now
2146  ||
2147  // enqueue, and retrieve explanation (as a conflict clause)
2148  // only if this implication is responsible for a conflict.
2150  ) {
2151  d_theoryAPI->getExplanation(literal, clauses);
2152  if (protocol) {
2153  cout << "theory implication reason: " << endl;
2154  clauses.print();
2155  }
2156  addFormula(clauses, true);
2157  clauses.reset();
2158  }
2159  continue;
2160  }
2161 
2162 // // 8. tell theories about new boolean propagations
2163 // if (defer_theory_propagation && d_thead < d_qhead) {
2164 // d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
2165 // ++d_thead;
2166 // continue;
2167 // }
2168 // DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
2169 
2170  // 9. boolean split
2171  Lit next = lit_Undef;
2172 
2173 
2174  // use CVC decider
2175  if (d_decider != NULL) {
2176  literal = d_decider->makeDecision();
2177  if (!literal.isNull()) {
2178  next = MiniSat::cvcToMiniSat(literal);
2179  }
2180  }
2181  // use MiniSat's decision heuristic
2182  else {
2183  Var nextVar = d_order.select(params.random_var_freq);
2184  if (nextVar != var_Undef){
2185  next = ~Lit(nextVar, false);
2186  }
2187  }
2188  if (next != lit_Undef) {
2189  // Simplify the set of problem clauses:
2190  // there must have been enough propagations in root level,
2191  // and no simplification too recently
2192  if (false && d_simpDB_props <= 0 && d_simpDB_assigns > (nAssigns() / 10)) {
2193  simplifyDB();
2194  DebugAssert(d_ok, "MiniSat::Solver::search: simplifyDB resulted in conflict");
2195  }
2196 
2197  // Reduce the set of learnt clauses:
2198  //if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
2199  //if (learnts.size()-nAssigns() >= nClauses() / 3)
2200  // don't remove lemmas unless there are a significant number
2201  //if (d_learnts.size() - nAssigns() < nClauses() / 3)
2202  //return;
2203  // don't remove lemmas unless there are lots of new ones
2204  // if (d_learnts.size() - nAssigns() < 3 * d_simpRD_learnts)
2205  // return;
2206  // :TODO:
2207  //reduceDB();
2208 
2209  d_stats.decisions++;
2210  d_theoryAPI->push();
2211 
2212  DebugAssert(getValue(next) == l_Undef,
2213  "MiniSat::Solver::search not undefined split variable chosen.");
2214 
2215  if (protocol) {
2216  cout << "Split: " << next.index() << endl;
2217  }
2218 
2219  // do lookahead based on MiniSat's decision heuristic
2220  if (d_decider != NULL) propLookahead(params);
2221  if (isConflicting()) {
2222  ++d_stats.debug;
2223  continue;
2224  }
2225 
2226 
2227  if (!assume(next)) {
2228  DebugAssert(false, "MiniSat::Solver::search contradictory split variable chosen.");
2229  }
2230  continue;
2231  }
2232 
2233  // 10. full theory consistency check
2234  SAT::DPLLT::ConsistentResult result = d_theoryAPI->checkConsistent(clauses, true);
2235  // inconsistency detected
2236  if (result == SAT::DPLLT::INCONSISTENT) {
2237  if (protocol) {
2238  cout << "theory conflict (FULL): " << endl;
2239  clauses.print();
2240  printState();
2241  }
2243  addFormula(clauses, true);
2244  clauses.reset();
2245  while (!isConflicting() && d_ok && d_qhead < d_trail.size() && !isConflicting()) {
2247  propagate();
2248  }
2249  DebugAssert(isConflicting(), "expected conflict");
2250  continue;
2251  }
2252  // perhaps consistent, new clauses added by theory propagation
2253  if (result == SAT::DPLLT::MAYBE_CONSISTENT) {
2254  if (d_theoryAPI->getNewClauses(clauses)) {
2255  if (protocol) {
2256  cout << "theory clauses: " << endl;
2257  clauses.print();
2258  }
2259  addFormula(clauses, true);
2260  clauses.reset();
2261  }
2262  // it can happen that after doing a full consistency check
2263  // there are actually no new theory clauses,
2264  // but then there will be new decisions in the next round.
2265  continue;
2266  }
2267  // consistent
2268  if (result == SAT::DPLLT::CONSISTENT) {
2270  "DPLLTMiniSat::search: consistent result, but decider not done yet.");
2272  "DPLLTMiniSat::search: consistent result, but not all clauses satisfied.");
2273  return CVC3::SATISFIABLE;
2274  }
2275 
2276  FatalAssert(false, "DPLLTMiniSat::search: unreachable");
2277  return CVC3::SATISFIABLE;
2278  }
2279  }
2280 }
2281 
2282 
2283 
2284 
2285 /// Activity
2286 
2287 
2288 // Divide all variable activities by 1e100.
2289 //
2291  for (int i = 0; i < nVars(); i++)
2292  d_activity[i] *= 1e-100;
2293  d_var_inc *= 1e-100;
2294 }
2295 
2296 
2297 // Divide all constraint activities by 1e100.
2298 //
2300  for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); i++) {
2301  (*i)->setActivity((*i)->activity() * (float)1e-20);
2302  }
2303  d_cla_inc *= 1e-20;
2304 }
2305 
2306 
2307 
2308 
2309 ///
2310 /// expensive debug checks
2311 ///
2312 
2314  if (!debug_full) return true;
2315 
2316  for (size_type i = 0; i < d_clauses.size(); ++i) {
2317  Clause& clause = *d_clauses[i];
2318  int size = clause.size();
2319  bool satisfied = false;
2320  for (int j = 0; j < size; ++j) {
2321  if (getValue(clause[j]) == l_True) {
2322  satisfied = true;
2323  break;
2324  }
2325  }
2326  if (!satisfied) {
2327  cout << "Clause not satisfied:" << endl;
2328  cout << toString(clause, true);
2329 
2330  for (int j = 0; j < size; ++j) {
2331  Lit lit = clause[j];
2332  bool found = false;
2333  const vector<Clause*>& ws = getWatches(~lit);
2334  if (getLevel(lit) == d_rootLevel) {
2335  found = true;
2336  } else {
2337  for (size_type j = 0; !found && j < ws.size(); ++j) {
2338  if (ws[j] == &clause) {
2339  found = true;
2340  break;
2341  }
2342  }
2343  }
2344 
2345  if (found) {
2346  cout << " watched: " << toString(lit, true) << endl;
2347  } else {
2348  cout << "not watched: " << toString(lit, true) << endl;
2349  }
2350  }
2351 
2352  return false;
2353  }
2354  }
2355  return true;
2356 }
2357 
2358 
2359 void Solver::checkWatched(const Clause& clause) const {
2360  // unary clauses are not watched
2361  if (clause.size() < 2) return;
2362 
2363  for (int i = 0; i < 2; ++i) {
2364  Lit lit = clause[i];
2365  bool found = false;
2366  const vector<Clause*>& ws = getWatches(~lit);
2367 
2368  // simplifyDB removes watches on permanently set literals
2369  if (getLevel(lit) == d_rootLevel) found = true;
2370 
2371  // search for clause in watches
2372  for (size_type j = 0; !found && j < ws.size(); ++j) {
2373  if (ws[j] == &clause) found = true;
2374  }
2375 
2376  if (!found) {
2377  printState();
2378  cout << toString(clause, true) << " : " << toString(clause[i], false) << endl;
2379  FatalAssert(false, "MiniSat::Solver::checkWatched");
2380  }
2381  }
2382 }
2383 
2384 void Solver::checkWatched() const {
2385  if (!debug_full) return;
2386 
2387  for (size_type i = 0; i < d_clauses.size(); ++i) {
2388  checkWatched(*d_clauses[i]);
2389  }
2390 
2391  for (size_type i = 0; i < d_learnts.size(); ++i) {
2392  checkWatched(*d_learnts[i]);
2393  }
2394 }
2395 
2396 
2397 
2398 void Solver::checkClause(const Clause& clause) const {
2399  // unary clauses are true anyway
2400  if (clause.size() < 2) return;
2401 
2402  // 1) the first two literals are undefined
2403  if (getValue(clause[0]) == l_Undef && getValue(clause[1]) == l_Undef)
2404  return;
2405 
2406  // 2) one of the first two literals is satisfied
2407  else if (getValue(clause[0]) == l_True || getValue(clause[1]) == l_True)
2408  return;
2409 
2410  // 3) the first literal is undefined and all other literals are falsified
2411  // 4) all literals are falsified
2412  else {
2413  bool ok = true;
2414  if (getValue(clause[0]) == l_True)
2415  ok = false;
2416 
2417  for (int j = 1; ok && j < clause.size(); ++j) {
2418  if (getValue(clause[j]) != l_False) {
2419  ok = false;
2420  }
2421  }
2422 
2423  if (ok) return;
2424  }
2425 
2426  printState();
2427  cout << endl;
2428  cout << toString(clause, true) << endl;
2429  FatalAssert(false, "MiniSat::Solver::checkClause");
2430 }
2431 
2432 void Solver::checkClauses() const {
2433  if (!debug_full) return;
2434 
2435  for (size_type i = 0; i < d_clauses.size(); ++i) {
2436  checkClause(*d_clauses[i]);
2437  }
2438 
2439  for (size_type i = 0; i < d_learnts.size(); ++i) {
2440  checkClause(*d_learnts[i]);
2441  }
2442 }
2443 
2444 
2445 
2446 void Solver::checkTrail() const {
2447  if (!debug_full) return;
2448 
2449  for (size_type i = 0; i < d_trail.size(); ++i) {
2450  Lit lit = d_trail[i];
2451  Var var = lit.var();
2452  Clause* reason = d_reason[var];
2453 
2454  if (reason == Clause::Decision()
2455  ||
2456  reason == Clause::TheoryImplication()) {
2457  }
2458 
2459  else {
2460  const Clause& clause = *reason;
2461 
2462  // check that the first clause literal is the implied literal
2463  FatalAssert(clause.size() > 0, "MiniSat::Solver::checkTrail: empty clause as reason for " /*+ var*/);
2464  FatalAssert(lit == clause[0], "MiniSat::Solver::checkTrail: incorrect reason for " /*+ var*/);
2465  FatalAssert(d_assigns[var] == toInt(lbool(lit.sign())), "MiniSat::Solver::checkTrail: incorrect value for " /*+ var*/);
2466 
2467  // check that other literals are in the trail before this literal and this literal's level
2468  for (int j = 1; j < clause.size(); ++j) {
2469  Lit clauseLit = clause[j];
2470  Var clauseVar = clauseLit.var();
2471  FatalAssert(getLevel(var) >= getLevel(clauseVar),
2472  "MiniSat::Solver::checkTrail: depends on later asserted literal " /*+ var*/);
2473 
2474  bool found = false;
2475  for (size_type k = 0; k < i; ++k) {
2476  if (d_trail[k] == ~clauseLit) {
2477  found = true;
2478  break;
2479  }
2480  }
2481  FatalAssert(found, "MiniSat::Solver::checkTrail: depends on literal not in context " /*+ var*/);
2482  }
2483  }
2484  }
2485 }
2486 
2487 
2488 
2489 
2490 
2491 
2492 
2493 
2494 
2495 
2496 void Solver::setPushID(Var var, Clause* from) {
2497  // check that var is implied by from
2498  DebugAssert(getReason(var) == from, "MiniSat::Solver::setPushID: wrong reason given");
2499  int pushID = std::numeric_limits<int>::max();
2500  if (from != Clause::Decision() && from != Clause::TheoryImplication()) {
2501  pushID = from->pushID();
2502  for (int i = 1; i < from->size(); ++i) {
2503  pushID = std::max(pushID, getPushID((*from)[i]));
2504  }
2505  }
2506  d_pushIDs[var] = pushID;
2507 }
2508 
2509 
2511  DebugAssert(!inSearch(), "MiniSat::Solver::push: already in search");
2512 
2513  // inconsistency before this push, so nothing can happen after it,
2514  // so just mark this push as useless.
2515  // (can happen if before checkSat initial unit propagation finds an inconsistency)
2516  if (!d_ok) {
2517  d_pushes.push_back(PushEntry(-1, 0, 0, 0, true));
2518  return;
2519  }
2520 
2521  d_registeredVars.resize(d_registeredVars.size() + 1);
2522 
2523  // reinsert lemmas kept over the last pop
2524  for (vector<Clause*>::const_iterator i = d_popLemmas.begin(); i != d_popLemmas.end(); ++i) {
2525  Clause* lemma = *i;
2526  insertLemma(lemma, lemma->id(), lemma->pushID());
2527  d_stats.learnts_literals -= lemma->size();
2528  remove(lemma, true);
2529  }
2530  d_popLemmas.clear();
2531 
2532  // do propositional propagation to exhaustion, including the theory
2534  SAT::Lit literal;
2535  SAT::Clause clause;
2536  SAT::CNF_Formula_Impl clauses;
2537  // while more can be propagated
2538  while (!isConflicting() && (d_qhead < d_trail.size() || d_thead < d_qhead)) {
2539  // do propositional propagation to exhaustion
2540  while (!isConflicting() && d_qhead < d_trail.size()) {
2542  propagate();
2543  }
2544 
2545  // also propagate to theories right away
2547  while (!isConflicting() && d_thead < d_qhead) {
2549  ++d_thead;
2550  }
2551  }
2552 
2553  // propagate a theory implication
2555  literal = d_theoryAPI->getImplication();
2556  if (!literal.isNull()) {
2557  Lit lit = MiniSat::cvcToMiniSat(literal);
2558  if (protocol) {
2559  cout << "theory implication: " << lit.index() << endl;
2560  }
2561  if (
2562  // get explanation now
2564  ||
2565  // enqueue, and retrieve explanation (as a conflict clause)
2566  // only if this implication is responsible for a conflict.
2568  ) {
2569  d_theoryAPI->getExplanation(literal, clauses);
2570  if (protocol) {
2571  cout << "theory implication reason: " << endl;
2572  clauses.print();
2573  }
2574  addFormula(clauses, false);
2575  clauses.reset();
2576  }
2577  continue;
2578  }
2579  }
2580 
2581  // add a theory clause
2582 
2583  // if (push_theory_clause && d_theoryAPI->getNewClauses(clauses)) {
2584  if (push_theory_clause ) {
2585  bool hasNewClauses = d_theoryAPI->getNewClauses(clauses);
2586  if(hasNewClauses){
2587  if (protocol) {
2588  cout << "theory clauses: " << endl;
2589  clauses.print();
2590  printState();
2591  }
2592  addFormula(clauses, false);
2593  clauses.reset();
2594  continue;
2595  }
2596  }
2597  }
2598  }
2599  // do propositional propagation to exhaustion, but only on the propositional level
2600  else {
2601  while (!isConflicting() && d_qhead < d_trail.size()) {
2603  propagate();
2604  }
2605  }
2606 
2607 
2608  simplifyDB();
2609 
2610  // can happen that conflict is detected in propagate
2611  // but d_ok is not immediately set to false
2612 
2613  if (isConflicting()) d_ok = false;
2614 
2615  if (d_derivation != NULL) d_derivation->push(d_clauseIDCounter - 1);
2616  d_pushes.push_back(PushEntry(d_clauseIDCounter - 1, d_trail.size(), d_qhead, d_thead, d_ok));
2617 }
2618 
2619 
2620 
2622  DebugAssert(inPush(), "MiniSat::Solver::requestPop: no more pushes");
2623 
2624  // pop theories on first pop of consistent solver,
2625  // for inconsistent solver this is done in dpllt_minisat before the pop
2626  if (d_popRequests == 0 && isConsistent()) popTheories();
2627  ++d_popRequests;
2628 }
2629 
2631  if (d_popRequests == 0) return;
2632 
2633  while (d_popRequests > 1) {
2634  --d_popRequests;
2635  d_pushes.pop_back();
2636  }
2637 
2638  pop();
2639 }
2640 
2642  for (int i = d_rootLevel; i < decisionLevel(); ++i) {
2643  d_theoryAPI->pop();
2644  }
2645 }
2646 
2647 void Solver::popClauses(const PushEntry& pushEntry, vector<Clause*>& clauses) {
2648  size_type i = 0;
2649  while (i != clauses.size()) {
2650  // keep clause
2651  if (clauses[i]->pushID() >= 0
2652  &&
2653  clauses[i]->pushID() <= pushEntry.d_clauseID) {
2654  // cout << "solver keep : " << clauses[i]->id() << endl;
2655  // cout << "solver keep2 : " << clauses[i]->pushID() << endl;
2656  ++i;
2657  }
2658  // remove clause
2659  else {
2660  // cout << "solver pop : " << clauses[i]->id() << endl;
2661  remove(clauses[i]);
2662  clauses[i] = clauses.back();
2663  clauses.pop_back();
2664  }
2665  }
2666 }
2667 
2668 void Solver::pop() {
2669  DebugAssert(d_popRequests == 1, "Minisat::Solver::pop: d_popRequests != 1");
2670 
2671  --d_popRequests;
2672  PushEntry pushEntry = d_pushes.back();
2673  d_pushes.pop_back();
2674 
2675  // solver was already inconsistent before the push
2676  if (pushEntry.d_clauseID == -1) {
2677  DebugAssert(!d_ok, "Minisat::Solver::pop: inconsistent push, but d_ok == true");
2678  return;
2679  }
2680 
2681  // backtrack trail
2682  //
2683  // Note:
2684  // the entries that were added to the trail after the push,
2685  // and are kept over the pop,
2686  // are all based on propagating clauses/lemmas also kept after the push.
2687  // as they are not yet propagated yet, but only in the propagation queue,
2688  // watched literals will work fine.
2689  size_type first_invalid = pushEntry.d_trailSize;
2690  for (size_type i = pushEntry.d_trailSize; i != d_trail.size(); ++i) {
2691  Var x = d_trail[i].var();
2692  //setLevel(x, -1);
2693  d_assigns[x] = toInt(l_Undef);
2694  d_reason [x] = NULL;
2695  //d_pushIDs[x] = -1;
2696  d_order.undo(x);
2697  }
2698  d_trail.resize(first_invalid);
2699  d_trail_lim.resize(0);
2700  d_qhead = pushEntry.d_qhead;
2701  d_thead = pushEntry.d_thead;
2702 
2703  // remove clauses added after push
2704  popClauses(pushEntry, d_clauses);
2705 
2706 
2707  // move all lemmas that are not already the reason for an implication
2708  // to pending lemmas - these are to be added when the next push is done.
2709  size_type i = 0;
2710  while (i != d_popLemmas.size()) {
2711  if (d_popLemmas[i]->pushID() <= pushEntry.d_clauseID) {
2712  ++i;
2713  } else {
2714  remove(d_popLemmas[i], true);
2715  d_popLemmas[i] = d_popLemmas.back();
2716  d_popLemmas.pop_back();
2717  }
2718  }
2719 
2720  i = 0;
2721  while (i != d_learnts.size()) {
2722  Clause* lemma = d_learnts[i];
2723  // lemma is propagating, so it was already present before the push
2724  if (isReason(lemma)) {
2725  // cout << "solver keep lemma reason : " << lemma->id() << endl;
2726  // cout << "solver keep lemma reason2 : " << lemma->pushID() << endl;
2727  ++i;
2728  }
2729  // keep lemma?
2730  else {
2731  d_stats.learnts_literals -= lemma->size();
2732  // lemma ok after push, mark it for reinsertion in the next push
2733  if (lemma->pushID() <= pushEntry.d_clauseID) {
2734  // cout << "solver keep lemma : " << lemma->id() << endl;
2735  // cout << "solver keep lemma2 : " << lemma->pushID() << endl;
2736  if (lemma->size() >= 2) {
2737  removeWatch(getWatches(~(*lemma)[0]), lemma);
2738  removeWatch(getWatches(~(*lemma)[1]), lemma);
2739  }
2740  d_popLemmas.push_back(lemma);
2741  }
2742  // lemma needs to be removed
2743  else {
2744  // cout << "solver pop lemma : " << lemma->id() << endl;
2745  remove(lemma);
2746  }
2747 
2748  d_learnts[i] = d_learnts.back();
2749  d_learnts.pop_back();
2750  }
2751  }
2752  d_stats.debug += d_popLemmas.size();
2753 
2754 
2755  // remove all pending clauses and explanations
2756  while (!d_pendingClauses.empty()) {
2757  remove(d_pendingClauses.front(), true);
2758  d_pendingClauses.pop();
2759  }
2760  while (!d_theoryExplanations.empty()) {
2761  remove(d_theoryExplanations.top().second, true);
2762  d_theoryExplanations.pop();
2763  }
2764 
2765 
2766  // backtrack registered variables
2767  d_registeredVars.resize(d_pushes.size() + 1);
2768 
2769  if (pushEntry.d_ok) {
2770  // this needs to be done _after_ clauses have been removed above,
2771  // as it might deallocate removed clauses
2772  if (d_derivation != NULL) d_derivation->pop(pushEntry.d_clauseID);
2773 
2774  // not conflicting or in search anymore
2775  d_conflict = NULL;
2776  d_ok = true;
2777  d_inSearch = false;
2778  } else {
2779  DebugAssert(d_conflict != NULL, "MiniSat::Solver::pop: not in conflict 1");
2780  DebugAssert(!d_ok, "MiniSat::Solver::pop: not in conflict 2");
2781  }
2782 }