CVC3
search_sat.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file search_sat.cpp
4  *\brief Implementation of Search engine with generic external sat solver
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Wed Dec 7 21:00:24 2005
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 
22 #include "search_sat.h"
23 #ifdef DPLL_BASIC
24 #include "dpllt_basic.h"
25 #endif
26 #include "dpllt_minisat.h"
27 #include "theory_core.h"
28 #include "eval_exception.h"
29 #include "typecheck_exception.h"
30 #include "expr_transform.h"
31 #include "search_rules.h"
32 #include "command_line_flags.h"
33 #include "theorem_manager.h"
34 #include "theory.h"
35 #include "debug.h"
36 
37 
38 using namespace std;
39 using namespace CVC3;
40 using namespace SAT;
41 
42 
43 namespace CVC3 {
44 
45 
48 public:
49  SearchSatCoreSatAPI(SearchSat* ss) : d_ss(ss) {}
51  void addLemma(const Theorem& thm, int priority, bool atBottomScope)
52  { d_ss->addLemma(thm, priority, atBottomScope); }
53  Theorem addAssumption(const Expr& assump)
54  { return d_ss->newUserAssumption(assump); }
55  void addSplitter(const Expr& e, int priority)
56  { d_ss->addSplitter(e, priority); }
57  bool check(const Expr& e);
58 
59 };
60 
61 
62 bool SearchSatCoreSatAPI::check(const Expr& e)
63 {
64  Theorem thm;
65  d_ss->push();
66  QueryResult res = d_ss->check(e, thm);
67  d_ss->pop();
68  return res == VALID;
69 }
70 
71 
75 public:
77  : d_cm(ss->theoryCore()->getCM()), d_ss(ss) {}
79  void push() { return d_cm->push(); }
80  void pop() { return d_cm->pop(); }
81  void assertLit(Lit l) { d_ss->assertLit(l); }
82  SAT::DPLLT::ConsistentResult checkConsistent(CNF_Formula& cnf, bool fullEffort)
83  { return d_ss->checkConsistent(cnf, fullEffort); }
84  bool outOfResources() { return d_ss->theoryCore()->outOfResources(); }
85  Lit getImplication() { return d_ss->getImplication(); }
86  void getExplanation(Lit l, CNF_Formula& cnf) { return d_ss->getExplanation(l, cnf); }
87  bool getNewClauses(CNF_Formula& cnf) { return d_ss->getNewClauses(cnf); }
88 };
89 
90 
93 public:
94  SearchSatDecider(SearchSat* ss) : d_ss(ss) {}
96 
97  Lit makeDecision() { return d_ss->makeDecision(); }
98 };
99 
100 
103 public:
104  SearchSatCNFCallback(SearchSat* ss) : d_ss(ss) {}
106 
107  void registerAtom(const Expr& e, const Theorem& thm)
108  { d_ss->theoryCore()->theoryOf(e)->registerAtom(e, thm); }
109 };
110 
111 
112 }
113 
114 
115 void SearchSat::restorePre()
116 {
117  if (d_core->getCM()->scopeLevel() == d_bottomScope) {
118  DebugAssert(d_prioritySetBottomEntriesSizeStack.size() > 0, "Expected non-empty stack");
119  d_prioritySetBottomEntriesSize = d_prioritySetBottomEntriesSizeStack.back();
120  d_prioritySetBottomEntriesSizeStack.pop_back();
121  while (d_prioritySetBottomEntriesSize < d_prioritySetBottomEntries.size()) {
122  d_prioritySet.erase(d_prioritySetBottomEntries.back());
123  d_prioritySetBottomEntries.pop_back();
124  }
125  }
126 }
127 
128 
129 void SearchSat::restore()
130 {
131  while (d_prioritySetEntriesSize < d_prioritySetEntries.size()) {
132  d_prioritySet.erase(d_prioritySetEntries.back());
133  d_prioritySetEntries.pop_back();
134  }
135  while (d_pendingLemmasSize < d_pendingLemmas.size()) {
136  d_pendingLemmas.pop_back();
137  d_pendingScopes.pop_back();
138  }
139  while (d_varsUndoListSize < d_varsUndoList.size()) {
140  d_vars[d_varsUndoList.back()] = SAT::Var::UNKNOWN;
141  d_varsUndoList.pop_back();
142  }
143 }
144 
145 
146 bool SearchSat::recordNewRootLit(Lit lit, int priority, bool atBottomScope)
147 {
148  DebugAssert(d_prioritySetEntriesSize == d_prioritySetEntries.size() &&
149  d_prioritySetBottomEntriesSize == d_prioritySetBottomEntries.size(),
150  "Size mismatch");
151  pair<set<LitPriorityPair>::iterator,bool> status =
152  d_prioritySet.insert(LitPriorityPair(lit, priority));
153  if (!status.second) return false;
154  if (!atBottomScope || d_bottomScope == d_core->getCM()->scopeLevel()) {
155  d_prioritySetEntries.push_back(status.first);
156  d_prioritySetEntriesSize = d_prioritySetEntriesSize + 1;
157  }
158  else {
159  d_prioritySetBottomEntries.push_back(status.first);
160  ++d_prioritySetBottomEntriesSize;
161  }
162 
163  if (d_prioritySetStart.get() == d_prioritySet.end() ||
164  ((*status.first) < (*(d_prioritySetStart.get()))))
165  d_prioritySetStart = status.first;
166  return true;
167 }
168 
169 
170 void SearchSat::addLemma(const Theorem& thm, int priority, bool atBottomScope)
171 {
172  IF_DEBUG(
173  string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');
174  TRACE("addLemma", indentStr, "AddLemma: ", thm.getExpr().toString(PRESENTATION_LANG));
175  )
176  // DebugAssert(!thm.getExpr().isAbsLiteral(), "Expected non-literal");
177  DebugAssert(d_pendingLemmasSize == d_pendingLemmas.size(), "Size mismatch");
178  DebugAssert(d_pendingLemmasSize == d_pendingScopes.size(), "Size mismatch");
179  DebugAssert(d_pendingLemmasNext <= d_pendingLemmas.size(), "Size mismatch");
180  d_pendingLemmas.push_back(pair<Theorem,int>(thm, priority));
181  d_pendingScopes.push_back(atBottomScope);
182  d_pendingLemmasSize = d_pendingLemmasSize + 1;
183 }
184 
185 
186 void SearchSat::addSplitter(const Expr& e, int priority)
187 {
188  DebugAssert(!e.isEq() || e[0] != e[1], "Expected non-trivial splitter");
189  addLemma(d_commonRules->excludedMiddle(e), priority);
190 }
191 
192 
193 void SearchSat::assertLit(Lit l)
194 {
195  // DebugAssert(d_inCheckSat, "Should only be used as a call-back");
196  Expr e = d_cnfManager->concreteLit(l);
197 
198  IF_DEBUG(
199  string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');
200  string val = " := ";
201 
202  std::stringstream ss;
203  ss<<theoryCore()->getCM()->scopeLevel();
204  std::string temp;
205  ss>>temp;
206 
207  if (l.isPositive()) val += "1"; else val += "0";
208  TRACE("assertLit", "", "", "");
209  TRACE("assertLitScope", indentStr, "Scope level = ", temp);
210  TRACE("assertLit", indentStr, l.getVar(), val+": "+e.toString());
211  )
212 
213  //=======
214  // IF_DEBUG(
215  // string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');
216  // string val = " := ";
217  // if (l.isPositive()) val += "1"; else val += "0";
218  // TRACE("assertLit", indentStr, l.getVar(), val);
219  // )
220 
221  // This can happen if the SAT solver propagates a learned unit clause from a p
222  bool isSATLemma = false;
223  if (e.isNull()) {
224  e = d_cnfManager->concreteLit(l, false);
225  DebugAssert(!e.isNull(), "Expected known expr");
226  isSATLemma = true;
227  TRACE("quant-level", "found null expr ",e, "");
228  }
229 
230  DebugAssert(!e.isNull(), "Expected known expr");
231  DebugAssert(!e.isIntAssumption() || getValue(l) == SAT::Var::TRUE_VAL,
232  "internal assumptions should be true");
233  // This happens if the SAT solver has been restarted--it re-asserts its old assumptions
234  if (e.isIntAssumption()) return;
235  if (getValue(l) == SAT::Var::UNKNOWN) {
236  setValue(l.getVar(), l.isPositive() ? Var::TRUE_VAL : Var::FALSE_VAL);
237  }
238  else {
239  DebugAssert(!e.isAbsLiteral(), "invariant violated");
240  DebugAssert(getValue(l) == Var::TRUE_VAL, "invariant violated");
241  return;
242  }
243  if (!e.isAbsLiteral()) return;
244  e.setIntAssumption();
245 
246  Theorem thm = d_commonRules->assumpRule(e);
247  if (isSATLemma) {
248  CNF_Formula_Impl cnf;
249  d_cnfManager->addAssumption(thm, cnf);
250  }
251 
252  thm.setQuantLevel(theoryCore()->getQuantLevelForTerm(e.isNot() ? e[0] : e));
253  d_intAssumptions.push_back(thm);
254  d_core->addFact(thm);
255 }
256 
257 
258 SAT::DPLLT::ConsistentResult SearchSat::checkConsistent(SAT::CNF_Formula& cnf, bool fullEffort)
259 {
260  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
261  if (d_core->inconsistent()) {
262  d_cnfManager->convertLemma(d_core->inconsistentThm(), cnf);
263  if (d_cnfManager->numVars() > d_vars.size()) {
264  d_vars.resize(d_cnfManager->numVars(), SAT::Var::UNKNOWN);
265  }
266  return DPLLT::INCONSISTENT;
267  }
268  if (fullEffort) {
269  if (d_core->checkSATCore() && d_pendingLemmasNext == d_pendingLemmas.size() && d_lemmasNext == d_lemmas.numClauses()) {
270  if (d_core->inconsistent()) {
271  d_cnfManager->convertLemma(d_core->inconsistentThm(), cnf);
272  if (d_cnfManager->numVars() > d_vars.size()) {
273  d_vars.resize(d_cnfManager->numVars(), SAT::Var::UNKNOWN);
274  }
275  return DPLLT::INCONSISTENT;
276  }
277  else return DPLLT::CONSISTENT;
278  }
279  }
280  return DPLLT::MAYBE_CONSISTENT;
281 }
282 
283 
284 Lit SearchSat::getImplication()
285 {
286  // DebugAssert(d_inCheckSat, "Should only be used as a call-back");
287  Lit l;
288  Theorem imp = d_core->getImpliedLiteral();
289  while (!imp.isNull()) {
290  l = d_cnfManager->getCNFLit(imp.getExpr());
292  "implied literals should be registered by cnf or by user");
293  if (!l.isNull() && getValue(l) != Var::TRUE_VAL) {
294  d_theorems.insert(imp.getExpr(), imp);
295  break;
296  }
297  l.reset();
298  imp = d_core->getImpliedLiteral();
299  }
300  return l;
301 }
302 
303 
304 void SearchSat::getExplanation(Lit l, SAT::CNF_Formula& cnf)
305 {
306  // DebugAssert(d_inCheckSat, "Should only be used as a call-back");
307  DebugAssert(cnf.empty(), "Expected empty cnf");
308  Expr e = d_cnfManager->concreteLit(l);
309  CDMap<Expr, Theorem>::iterator i = d_theorems.find(e);
310  DebugAssert(i != d_theorems.end(), "getExplanation: no explanation found");
311  d_cnfManager->convertLemma((*i).second, cnf);
312  if (d_cnfManager->numVars() > d_vars.size()) {
313  d_vars.resize(d_cnfManager->numVars(), SAT::Var::UNKNOWN);
314  }
315 }
316 
317 
318 bool SearchSat::getNewClauses(CNF_Formula& cnf)
319 {
320  unsigned i;
321 
322  Lit l;
323  for (i = d_pendingLemmasNext; i < d_pendingLemmas.size(); ++i) {
324  l = d_cnfManager->addLemma(d_pendingLemmas[i].first, d_lemmas);
325  if (!recordNewRootLit(l, d_pendingLemmas[i].second, d_pendingScopes[i])) {
326  // Already have this lemma: delete it
327  d_lemmas.deleteLast();
328  }
329  }
330  d_pendingLemmasNext = d_pendingLemmas.size();
331 
332  if (d_cnfManager->numVars() > d_vars.size()) {
333  d_vars.resize(d_cnfManager->numVars(), SAT::Var::UNKNOWN);
334  }
335 
336  DebugAssert(d_lemmasNext <= d_lemmas.numClauses(), "");
337  if (d_lemmasNext == d_lemmas.numClauses()) return false;
338  do {
339  cnf += d_lemmas[d_lemmasNext];
340  d_lemmasNext = d_lemmasNext + 1;
341  } while (d_lemmasNext < d_lemmas.numClauses());
342  return true;
343 }
344 
345 
346 Lit SearchSat::makeDecision()
347 {
348  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
349  Lit litDecision;
350 
351  set<LitPriorityPair>::const_iterator i, iend;
352  Lit lit;
353  for (i = d_prioritySetStart, iend = d_prioritySet.end(); i != iend; ++i) {
354  lit = (*i).getLit();
355  if (findSplitterRec(lit, getValue(lit), &litDecision)) {
356  break;
357  }
358  }
359  d_prioritySetStart = i;
360  return litDecision;
361 }
362 
363 
364 bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
365 {
366  if (lit.isFalse() || lit.isTrue()) return false;
367 
368  unsigned i, n;
369  Lit litTmp;
370  Var varTmp;
371  bool ret;
372  Var v = lit.getVar();
373 
374  DebugAssert(value != Var::UNKNOWN, "expected known value");
375  DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
376  "invariant violated");
377 
378  if (checkJustified(v)) return false;
379 
380  if (lit.isInverted()) {
381  value = Var::invertValue(value);
382  }
383 
384  if (d_cnfManager->numFanins(v) == 0) {
385  if (getValue(v) != Var::UNKNOWN) {
386  setJustified(v);
387  return false;
388  }
389  else {
390  *litDecision = Lit(v, value == Var::TRUE_VAL);
391  return true;
392  }
393  }
394  else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
395  // This node represents a predicate with embedded ITE's
396  // We handle this case specially in order to catch the
397  // corner case when a variable is in its own fanin.
398  n = d_cnfManager->numFanins(v);
399  for (i=0; i < n; ++i) {
400  litTmp = d_cnfManager->getFanin(v, i);
401  varTmp = litTmp.getVar();
402  DebugAssert(!litTmp.isInverted(),"Expected positive fanin");
403  if (checkJustified(varTmp)) continue;
404  DebugAssert(d_cnfManager->concreteVar(varTmp).getKind() == ITE,
405  "Expected ITE");
406  DebugAssert(getValue(varTmp) == Var::TRUE_VAL,"Expected TRUE");
407  Lit cIf = d_cnfManager->getFanin(varTmp,0);
408  Lit cThen = d_cnfManager->getFanin(varTmp,1);
409  Lit cElse = d_cnfManager->getFanin(varTmp,2);
410  if (getValue(cIf) == Var::UNKNOWN) {
411  if (getValue(cElse) == Var::TRUE_VAL ||
412  getValue(cThen) == Var::FALSE_VAL) {
413  ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
414  }
415  else {
416  ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
417  }
418  if (!ret) {
419  cout << d_cnfManager->concreteVar(cIf.getVar()) << endl;
420  DebugAssert(false,"No controlling input found (1)");
421  }
422  return true;
423  }
424  else if (getValue(cIf) == Var::TRUE_VAL) {
425  if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
426  return true;
427  }
428  if (cThen.getVar() != v &&
429  (getValue(cThen) == Var::UNKNOWN ||
430  getValue(cThen) == Var::TRUE_VAL) &&
431  findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) {
432  return true;
433  }
434  }
435  else {
436  if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
437  return true;
438  }
439  if (cElse.getVar() != v &&
440  (getValue(cElse) == Var::UNKNOWN ||
441  getValue(cElse) == Var::TRUE_VAL) &&
442  findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) {
443  return true;
444  }
445  }
446  setJustified(varTmp);
447  }
448  if (getValue(v) != Var::UNKNOWN) {
449  setJustified(v);
450  return false;
451  }
452  else {
453  *litDecision = Lit(v, value == Var::TRUE_VAL);
454  return true;
455  }
456  }
457 
458  int kind = d_cnfManager->concreteVar(v).getKind();
459  Var::Val valHard = Var::FALSE_VAL;
460  switch (kind) {
461  case AND:
462  valHard = Var::TRUE_VAL;
463  case OR:
464  if (value == valHard) {
465  n = d_cnfManager->numFanins(v);
466  for (i=0; i < n; ++i) {
467  litTmp = d_cnfManager->getFanin(v, i);
468  if (findSplitterRec(litTmp, valHard, litDecision)) {
469  return true;
470  }
471  }
472  DebugAssert(getValue(v) == valHard, "Output should be justified");
473  setJustified(v);
474  return false;
475  }
476  else {
477  Var::Val valEasy = Var::invertValue(valHard);
478  n = d_cnfManager->numFanins(v);
479  for (i=0; i < n; ++i) {
480  litTmp = d_cnfManager->getFanin(v, i);
481  if (getValue(litTmp) != valHard) {
482  if (findSplitterRec(litTmp, valEasy, litDecision)) {
483  return true;
484  }
485  DebugAssert(getValue(v) == valEasy, "Output should be justified");
486  setJustified(v);
487  return false;
488  }
489  }
490  DebugAssert(false, "No controlling input found (2)");
491  }
492  break;
493  case IMPLIES:
494  DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins");
495  if (value == Var::FALSE_VAL) {
496  litTmp = d_cnfManager->getFanin(v, 0);
497  if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
498  return true;
499  }
500  litTmp = d_cnfManager->getFanin(v, 1);
501  if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
502  return true;
503  }
504  DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified");
505  setJustified(v);
506  return false;
507  }
508  else {
509  litTmp = d_cnfManager->getFanin(v, 0);
510  if (getValue(litTmp) != Var::TRUE_VAL) {
511  if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
512  return true;
513  }
514  DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
515  setJustified(v);
516  return false;
517  }
518  litTmp = d_cnfManager->getFanin(v, 1);
519  if (getValue(litTmp) != Var::FALSE_VAL) {
520  if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
521  return true;
522  }
523  DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
524  setJustified(v);
525  return false;
526  }
527  DebugAssert(false, "No controlling input found (3)");
528  }
529  break;
530  case IFF: {
531  litTmp = d_cnfManager->getFanin(v, 0);
532  Var::Val val = getValue(litTmp);
533  if (val != Var::UNKNOWN) {
534  if (findSplitterRec(litTmp, val, litDecision)) {
535  return true;
536  }
537  if (value == Var::FALSE_VAL) val = Var::invertValue(val);
538  litTmp = d_cnfManager->getFanin(v, 1);
539 
540  if (findSplitterRec(litTmp, val, litDecision)) {
541  return true;
542  }
543  DebugAssert(getValue(v) == value, "Output should be justified");
544  setJustified(v);
545  return false;
546  }
547  else {
548  val = getValue(d_cnfManager->getFanin(v, 1));
549  if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
550  if (value == Var::FALSE_VAL) val = Var::invertValue(val);
551  if (findSplitterRec(litTmp, val, litDecision)) {
552  return true;
553  }
554  DebugAssert(false, "Unable to find controlling input (4)");
555  }
556  break;
557  }
558  case XOR: {
559  litTmp = d_cnfManager->getFanin(v, 0);
560  Var::Val val = getValue(litTmp);
561  if (val != Var::UNKNOWN) {
562  if (findSplitterRec(litTmp, val, litDecision)) {
563  return true;
564  }
565  if (value == Var::TRUE_VAL) val = Var::invertValue(val);
566  litTmp = d_cnfManager->getFanin(v, 1);
567  if (findSplitterRec(litTmp, val, litDecision)) {
568  return true;
569  }
570  DebugAssert(getValue(v) == value, "Output should be justified");
571  setJustified(v);
572  return false;
573  }
574  else {
575  val = getValue(d_cnfManager->getFanin(v, 1));
576  if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
577  if (value == Var::TRUE_VAL) val = Var::invertValue(val);
578  if (findSplitterRec(litTmp, val, litDecision)) {
579  return true;
580  }
581  DebugAssert(false, "Unable to find controlling input (5)");
582  }
583  break;
584  }
585  case ITE: {
586  Lit cIf = d_cnfManager->getFanin(v, 0);
587  Lit cThen = d_cnfManager->getFanin(v, 1);
588  Lit cElse = d_cnfManager->getFanin(v, 2);
589  if (getValue(cIf) == Var::UNKNOWN) {
590  if (getValue(cElse) == value ||
591  getValue(cThen) == Var::invertValue(value)) {
592  ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
593  }
594  else {
595  ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
596  }
597  if (!ret) {
598  cout << d_cnfManager->concreteVar(cIf.getVar()) << endl;
599  DebugAssert(false,"No controlling input found (6)");
600  }
601  return true;
602  }
603  else if (getValue(cIf) == Var::TRUE_VAL) {
604  if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
605  return true;
606  }
607  if (cThen.isVar() && cThen.getVar() != v &&
608  (getValue(cThen) == Var::UNKNOWN ||
609  getValue(cThen) == value) &&
610  findSplitterRec(cThen, value, litDecision)) {
611  return true;
612  }
613  }
614  else {
615  if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
616  return true;
617  }
618  if (cElse.isVar() && cElse.getVar() != v &&
619  (getValue(cElse) == Var::UNKNOWN ||
620  getValue(cElse) == value) &&
621  findSplitterRec(cElse, value, litDecision)) {
622  return true;
623  }
624  }
625  DebugAssert(getValue(v) == value, "Output should be justified");
626  setJustified(v);
627  return false;
628  }
629  default:
630  DebugAssert(false, "Unexpected Boolean operator");
631  break;
632  }
633  FatalAssert(false, "Should be unreachable");
634  return false;
635 }
636 
637 
638 QueryResult SearchSat::check(const Expr& e, Theorem& result, bool isRestart)
639 {
640  DebugAssert(d_dplltReady, "SAT solver is not ready");
641  if (isRestart && d_lastCheck.get().isNull()) {
642  throw Exception
643  ("restart called without former call to checkValid");
644  }
645 
646  DebugAssert(!d_inCheckSat, "checkValid should not be called recursively");
647  TRACE("searchsat", "checkValid: ", e, "");
648 
649  if (!e.getType().isBool())
650  throw TypecheckException
651  ("checking validity of a non-Boolean expression:\n\n "
652  + e.toString()
653  + "\n\nwhich has the following type:\n\n "
654  + e.getType().toString());
655 
656  Expr e2 = e;
657 
658  // Set up and quick exits
659  if (isRestart) {
660  while (e2.isNot() && e2[0].isNot()) e2 = e2[0][0];
661  if (e2.isTrue() || (e2.isNot() && e2[0].isFalse())) {
662  result = d_lastValid;
663  return INVALID;
664  }
665  if (e2.isFalse() || (e2.isNot() && e2[0].isTrue())) {
666  pop();
667  //TODO: real theorem
668  d_lastValid = d_commonRules->assumpRule(d_lastCheck);
669  result = d_lastValid;
670  return VALID;
671  }
672  }
673  else {
674  if (e.isTrue()) {
675  d_lastValid = d_commonRules->trueTheorem();
676  result = d_lastValid;
677  return VALID;
678  }
679  push();
680  d_bottomScope = d_core->getCM()->scopeLevel();
681  d_prioritySetBottomEntriesSizeStack.push_back(d_prioritySetBottomEntriesSize);
682  d_lastCheck = e;
683  e2 = !e;
684  }
685 
686  Theorem thm;
687  CNF_Formula_Impl cnf;
688  QueryResult qres;
689  d_cnfManager->setBottomScope(d_bottomScope);
690  d_dplltReady = false;
691 
692  newUserAssumptionInt(e2, cnf, true);
693 
694  d_inCheckSat = true;
695 
696  getNewClauses(cnf);
697 
698  if (!isRestart && d_core->inconsistent()) {
699  qres = UNSATISFIABLE;
700  thm = d_rules->proofByContradiction(e, d_core->inconsistentThm());
701  pop();
702  d_lastValid = thm;
703  d_cnfManager->setBottomScope(-1);
704  d_inCheckSat = false;
705  result = d_lastValid;
706  return qres;
707  }
708  else {
709  // Run DPLLT engine
710  qres = isRestart ? d_dpllt->continueCheck(cnf) : d_dpllt->checkSat(cnf);
711  }
712 
713  if (qres == UNSATISFIABLE) {
714  DebugAssert(d_core->getCM()->scopeLevel() == d_bottomScope,
715  "Expected unchanged context after unsat");
716  e2 = d_lastCheck;
717  pop();
718  if (d_core->getTM()->withProof()) {
719  Proof pf = d_dpllt->getSatProof(d_cnfManager, d_core);
720  // std::cout<<"WITH PROOF:"<<pf<<std::endl;
721  d_lastValid = d_rules->satProof(e2, pf);
722  }
723  else {
724  d_lastValid = d_commonRules->assumpRule(d_lastCheck);
725  }
726  }
727  else {
728  DebugAssert(d_lemmasNext == d_lemmas.numClauses(),
729  "Expected no lemmas after satisfiable check");
730  d_dplltReady = true;
731  d_lastValid = Theorem();
732  if (qres == SATISFIABLE && d_core->incomplete()) qres = UNKNOWN;
733 
734 #ifdef _CVC3_DEBUG_MODE
735 
736  if( CVC3::debugger.trace("quant debug") ){
737  d_core->theoryOf(FORALL)->debug(1);
738  }
739 
740 
741  if( CVC3::debugger.trace("sat model unknown") ){
742  std::vector<SAT::Lit> cur_assigns = d_dpllt->getCurAssignments();
743  cout<<"Current assignments"<<endl;
744  {
745  for(size_t i = 0 ; i < cur_assigns.size(); i++){
746  Lit l = cur_assigns[i];
747  Expr e = d_cnfManager->concreteLit(l);
748 
749  string val = " := ";
750 
751  if (l.isPositive()) val += "1"; else val += "0";
752  cout<<l.getVar()<<val<<endl;
753  // cout<<e<<endl;
754 
755  }
756  }
757 
758 
759  std::vector< std::vector<SAT::Lit> > cur_clauses = d_dpllt->getCurClauses();
760  cout<<"Current Clauses"<<endl;
761  {
762  for(size_t i = 0 ; i < cur_clauses.size(); i++){
763  // cout<<"clause "<<i<<"================="<<endl;
764  for(size_t j = 0; j < cur_clauses[i].size(); j++){
765 
766  Lit l = cur_clauses[i][j];
767  string val ;
768  if (l.isPositive()) val += "+"; else val += "-";
769  cout<<val<<l.getVar()<<" ";
770  }
771  cout<<endl;
772  }
773  }
774  }
775 
776  if( CVC3::debugger.trace("model unknown") ){
777  const CDList<Expr>& allterms = d_core->getTerms();
778  cout<<"===========terms begin=========="<<endl;
779 
780  for (size_t i=0; i<allterms.size(); i++){
781  // cout<<"i="<<i<<" :"<<allterms[i].getFindLevel()<<":"<<d_core->simplifyExpr(allterms[i])<<"|"<<allterms[i]<<endl;
782  cout<<"i="<<i<<" :"<<allterms[i].getFindLevel()<<":"<<d_core->simplifyExpr(allterms[i])<<"|"<<allterms[i]<<endl;
783 
784  //<<" and type is "<<allterms[i].getType()
785  // << " and kind is" << allterms[i].getEM()->getKindName(allterms[i].getKind())<<endl;
786  }
787  cout<<"-----------term end ---------"<<endl;
788  const CDList<Expr>& allpreds = d_core->getPredicates();
789  cout<<"===========pred begin=========="<<endl;
790 
791  for (size_t i=0; i<allpreds.size(); i++){
792  if(allpreds[i].hasFind()){
793  if( (d_core->findExpr(allpreds[i])).isTrue()){
794  cout<<"ASSERT "<< allpreds[i] <<";" <<endl;
795  }
796  else{
797  cout<<"ASSERT NOT("<< allpreds[i] <<");" <<endl;
798  }
799  // cout<<"i="<<i<<" :";
800  // cout<<allpreds[i].getFindLevel();
801  // cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
802  }
803  // else cout<<"U "<<endl;;
804 
805 
806  //" and type is "<<allpreds[i].getType()
807  // << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;
808  }
809  cout<<"-----------end----------pred"<<endl;
810  }
811 
812  if( CVC3::debugger.trace("model unknown quant") ){
813  cout<<"=========== quant pred begin=========="<<endl;
814  const CDList<Expr>& allpreds = d_core->getPredicates();
815  for (size_t i=0; i<allpreds.size(); i++){
816 
817  Expr cur = allpreds[i];
818  if(cur.isForall() || cur.isExists() || (cur.isNot() && (cur[0].isForall()||cur[0].isExists()))){
819  if(allpreds[i].hasFind()) {
820  cout<<"i="<<i<<" :";
821  cout<<allpreds[i].getFindLevel();
822  cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
823  }
824  }
825  }
826  cout<<"-----------end----------pred"<<endl;
827  }
828 
829  if( CVC3::debugger.trace("model unknown nonquant") ){
830  cout<<"=========== quant pred begin=========="<<endl;
831  const CDList<Expr>& allpreds = d_core->getPredicates();
832  for (size_t i=0; i<allpreds.size(); i++){
833 
834  Expr cur = allpreds[i];
835  if(cur.isForall() || cur.isExists() ||
836  (cur.isNot() && (cur[0].isForall()||cur[0].isExists())) ||
837  cur.isEq() ||
838  (cur.isNot() && cur[0].isEq())){
839  }
840  else{
841  if(allpreds[i].hasFind()) {
842  cout<<"i="<<i<<" :";
843  cout<<allpreds[i].getFindLevel();
844  cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
845  }
846  }
847  }
848  cout<<"-----------end----------pred"<<endl;
849  }
850 
851  if( CVC3::debugger.trace("unknown state") ){
852  const CDList<Expr>& allpreds = d_core->getPredicates();
853  cout<<"===========pred begin=========="<<endl;
854 
855  for (size_t i=0; i<allpreds.size(); i++){
856  if(allpreds[i].hasFind()){
857  // Expr cur(allpreds[i]);
858 // if(cur.isForall() || cur.isExists() ||
859 // (cur.isNot() && (cur[0].isForall()||cur[0].isExists()))
860 // ){
861 // continue;
862 // }
863 
864  if( (d_core->findExpr(allpreds[i])).isTrue()){
865  cout<<":assumption "<< allpreds[i] <<"" <<endl;
866  }
867  else{
868  cout<<":assumption(not "<< allpreds[i] <<")" <<endl;
869  }
870  // cout<<"i="<<i<<" :";
871  // cout<<allpreds[i].getFindLevel();
872  // cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
873  }
874  // else cout<<"U "<<endl;;
875 
876 
877  //" and type is "<<allpreds[i].getType()
878  // << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;
879  }
880  cout<<"-----------end----------pred"<<endl;
881  }
882 
883  if( CVC3::debugger.trace("unknown state noforall") ){
884  const CDList<Expr>& allpreds = d_core->getPredicates();
885  cout<<"===========pred begin=========="<<endl;
886 
887  for (size_t i=0; i<allpreds.size(); i++){
888  if(allpreds[i].hasFind()){
889  Expr cur(allpreds[i]);
890 // if(cur.isForall() || cur.isExists() ||
891 // (cur.isNot() && (cur[0].isForall()||cur[0].isExists()))
892 // ){
893 // continue;
894 // }
895 
896  if( (d_core->findExpr(allpreds[i])).isTrue()){
897 // if(cur.isExists()){
898 // continue;
899 // }
900  cout<<"ASSERT "<< allpreds[i] <<";" <<endl;
901 // cout<<":assumption "<< allpreds[i] <<"" <<endl;
902  }
903  else if ( (d_core->findExpr(allpreds[i])).isFalse()){
904 // if (cur.isForall()){
905 // continue;
906 // }
907  cout<<"ASSERT (NOT "<< allpreds[i] <<");" <<endl;
908 // cout<<":assumption(not "<< allpreds[i] <<")" <<endl;
909  }
910  else{
911  cout<<"--ERROR"<<endl;
912  }
913  // cout<<"i="<<i<<" :";
914  // cout<<allpreds[i].getFindLevel();
915  // cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
916  }
917  // else cout<<"U "<<endl;;
918 
919 
920  //" and type is "<<allpreds[i].getType()
921  // << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;
922  }
923  cout<<"-----------end----------pred"<<endl;
924  }
925 
926 
927 #endif
928  }
929  d_cnfManager->setBottomScope(-1);
930  d_inCheckSat = false;
931  result = d_lastValid;
932  return qres;
933 }
934 
935 
936 SearchSat::SearchSat(TheoryCore* core, const string& name)
937  : SearchEngine(core),
938  d_name(name),
939  d_bottomScope(core->getCM()->getCurrentContext(), -1),
940  d_lastCheck(core->getCM()->getCurrentContext()),
941  d_lastValid(core->getCM()->getCurrentContext(),
942  d_commonRules->trueTheorem()),
943  d_userAssumptions(core->getCM()->getCurrentContext()),
944  d_intAssumptions(core->getCM()->getCurrentContext()),
945  d_idxUserAssump(core->getCM()->getCurrentContext(), 0),
946  d_decider(NULL),
947  d_theorems(core->getCM()->getCurrentContext()),
948  d_inCheckSat(false),
949  d_lemmas(core->getCM()->getCurrentContext()),
950  d_pendingLemmasSize(core->getCM()->getCurrentContext(), 0),
951  d_pendingLemmasNext(core->getCM()->getCurrentContext(), 0),
952  d_lemmasNext(core->getCM()->getCurrentContext(), 0),
953  d_varsUndoListSize(core->getCM()->getCurrentContext(), 0),
954  d_prioritySetStart(core->getCM()->getCurrentContext()),
955  d_prioritySetEntriesSize(core->getCM()->getCurrentContext(), 0),
956  d_prioritySetBottomEntriesSize(0),
957  d_lastRegisteredVar(core->getCM()->getCurrentContext(), 0),
958  d_dplltReady(core->getCM()->getCurrentContext(), true),
959  d_nextImpliedLiteral(core->getCM()->getCurrentContext(), 0),
960  d_restorer(core->getCM()->getCurrentContext(), this)
961 {
962  d_cnfManager = new CNF_Manager(core->getTM(), core->getStatistics(),
963  core->getFlags());
964 
966  d_cnfManager->registerCNFCallback(d_cnfCallback);
967  d_coreSatAPI = new SearchSatCoreSatAPI(this);
969  d_theoryAPI = new SearchSatTheoryAPI(this);
970  if (core->getFlags()["de"].getString() == "dfs") d_decider = new SearchSatDecider(this);
971 
972  if (core->getFlags()["sat"].getString() == "sat") {
973 #ifdef DPLL_BASIC
974  d_dpllt = new DPLLTBasic(d_theoryAPI, d_decider, core->getCM(),
975  core->getFlags()["stats"].getBool());
976 #else
977  throw CLException("SAT solver 'sat' not supported in this build");
978 #endif
979  } else if (core->getFlags()["sat"].getString() == "minisat") {
981  core->getFlags()["stats"].getBool(),
982  core->getTM()->withProof());
983  } else {
984  throw CLException("Unrecognized SAT solver name: " + (core->getFlags()["sat"].getString()));
985  }
986 
988 }
989 
990 
992 {
993  delete d_dpllt;
994  delete d_decider;
995  delete d_theoryAPI;
996  delete d_coreSatAPI;
997  delete d_cnfCallback;
998  delete d_cnfManager;
999 }
1000 
1001 
1003 {
1005  if (!e.isRegisteredAtom())
1006  d_core->registerAtom(e, Theorem());
1007 }
1008 
1009 
1011 {
1012  Theorem imp;
1013  while (d_nextImpliedLiteral < d_core->numImpliedLiterals()) {
1016  if (imp.getExpr().unnegate().isUserRegisteredAtom()) return imp;
1017  }
1018  return Theorem();
1019 }
1020 
1021 
1023 {
1024  if (d_bottomScope < 0) {
1025  throw Exception
1026  ("returnFromCheck called with no previous invalid call to checkValid");
1027  }
1028  pop();
1029 }
1030 
1031 
1032 static void setRecursiveInUserAssumption(const Expr& e, int scope)
1033 {
1034  if (e.inUserAssumption()) return;
1035  for (int i = 0; i < e.arity(); ++i) {
1036  setRecursiveInUserAssumption(e[i], scope);
1037  }
1038  e.setInUserAssumption(scope);
1039 }
1040 
1041 
1042 void SearchSat::newUserAssumptionIntHelper(const Theorem& thm, CNF_Formula_Impl& cnf, bool atBottomScope)
1043 {
1044  Expr e = thm.getExpr();
1045  if (e.isAnd()) {
1046  for (int i = 0; i < e.arity(); ++i) {
1047  newUserAssumptionIntHelper(d_commonRules->andElim(thm, i), cnf, atBottomScope);
1048  }
1049  }
1050  else {
1051  if ( ! d_core->getFlags()["cnf-formula"].getBool()) {
1052  if (!recordNewRootLit(d_cnfManager->addAssumption(thm, cnf), 0, atBottomScope)) {
1053  cnf.deleteLast();
1054  }
1055  }
1056  else{
1057  d_cnfManager->addAssumption(thm, cnf);
1058  }
1059  // if cnf-formula is enabled, d_cnfManager->addAssumption returns a random literal, not a RootLit. A random lit can make recordNewRootLit return false, which in turn makes cnf.deleteLast() to delete the last clause, which is not correct.
1060  }
1061 }
1062 
1063 
1065 {
1067  "User assumptions should be added before calling checkSat");
1068  Theorem thm;
1069  int scope;
1070  if (atBottomScope) scope = d_bottomScope;
1071  else scope = -1;
1072  setRecursiveInUserAssumption(e, scope);
1073  if (!isAssumption(e)) {
1074  e.setUserAssumption(scope);
1075  thm = d_commonRules->assumpRule(e, scope);
1076  d_userAssumptions.push_back(thm, scope);
1077 
1078  if (atBottomScope && d_bottomScope != d_core->getCM()->scopeLevel()) {
1079  //TODO: run preprocessor without using context-dependent information
1080  //TODO: this will break if we have stuff like the BVDIV rewrite that needs to get enqueued during preprocessing
1081  newUserAssumptionIntHelper(thm, cnf, true);
1082  }
1083  else {
1084  Theorem thm2 = d_core->getExprTrans()->preprocess(thm);
1085  Expr e2 = thm2.getExpr();
1086  if (e2.isFalse()) {
1087  d_core->addFact(thm2);
1088  return thm;
1089  }
1090  else if (!e2.isTrue()) {
1091  newUserAssumptionIntHelper(thm2, cnf, false);
1092  }
1093  }
1094  if (d_cnfManager->numVars() > d_vars.size()) {
1096  }
1097  }
1098  return thm;
1099 }
1100 
1101 
1103 {
1104  CNF_Formula_Impl cnf;
1105  Theorem thm = newUserAssumptionInt(e, cnf, false);
1106  d_dpllt->addAssertion(cnf);
1107  return thm;
1108 }
1109 
1110 
1111 void SearchSat::getUserAssumptions(vector<Expr>& assumptions)
1112 {
1114  iend=d_userAssumptions.end(); i!=iend; ++i)
1115  assumptions.push_back((*i).getExpr());
1116 }
1117 
1118 
1119 void SearchSat::getInternalAssumptions(vector<Expr>& assumptions)
1120 {
1122  iend=d_intAssumptions.end(); i!=iend; ++i)
1123  assumptions.push_back((*i).getExpr());
1124 }
1125 
1126 
1127 
1128 void SearchSat::getAssumptions(vector<Expr>& assumptions)
1129 {
1131  iUend=d_userAssumptions.end(), iI = d_intAssumptions.begin(),
1132  iIend=d_intAssumptions.end();
1133  while (true) {
1134  if (iI == iIend) {
1135  if (iU == iUend) break;
1136  assumptions.push_back((*iU).getExpr());
1137  ++iU;
1138  }
1139  else if (iU == iUend) {
1140  Expr intAssump = (*iI).getExpr();
1141  if (!intAssump.isUserAssumption()) {
1142  assumptions.push_back(intAssump);
1143  }
1144  ++iI;
1145  }
1146  else {
1147  if ((*iI).getScope() <= (*iU).getScope()) {
1148  Expr intAssump = (*iI).getExpr();
1149  if (!intAssump.isUserAssumption()) {
1150  assumptions.push_back(intAssump);
1151  }
1152  ++iI;
1153  }
1154  else {
1155  assumptions.push_back((*iU).getExpr());
1156  ++iU;
1157  }
1158  }
1159  }
1160 }
1161 
1162 
1164 {
1165  return e.isUserAssumption() || e.isIntAssumption();
1166 }
1167 
1168 
1169 void SearchSat::getCounterExample(vector<Expr>& assumptions, bool inOrder)
1170 {
1171  if (!d_lastValid.get().isNull()) {
1172  throw Exception("Expected last query to be invalid");
1173  }
1174  getInternalAssumptions(assumptions);
1175 }
1176 
1177 
1179 {
1180  if(!d_core->getTM()->withProof())
1181  throw EvalException
1182  ("getProof cannot be called without proofs activated");
1183  if(d_lastValid.get().isNull())
1184  throw EvalException
1185  ("getProof must be called only after a successful check");
1186  if(d_lastValid.get().isNull()) return Proof();
1187  else return d_lastValid.get().getProof();
1188 }