CVC3
dpllt_basic.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file dpllt_basic.cpp
4  *\brief Basic implementation of dpllt module using generic sat solver
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Dec 12 19:09:43 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 "dpllt_basic.h"
23 #include "cnf.h"
24 #include "sat_api.h"
25 #include "exception.h"
26 
27 
28 using namespace std;
29 using namespace CVC3;
30 using namespace SAT;
31 
32 
33 //int level_ = 0;
34 
35 static void SATDLevelHook(void *cookie, int change)
36 {
37  //cout << "backtrack to: " << level_ << " " << change << endl;
38  //level_ += change;
39  // cout<<"decision level called"<<endl;
40  DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
41  for (; change > 0; change--) {
42  db->theoryAPI()->push();
43  }
44  for (; change < 0; change++) {
45  db->theoryAPI()->pop();
46  }
47 }
48 
49 
50 static SatSolver::Lit SATDecisionHook(void *cookie, bool *done)
51 {
52  // cout<<"sat decision called"<<endl;
53  DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
54 
55  if (db->theoryAPI()->outOfResources()) {
56  // Tell SAT solver to exit with satisfiable result
57  *done = true;
58  return SatSolver::Lit();
59  }
60 
61  if (!db->decider()) {
62  // Tell SAT solver to make its own choice
63  if (!*done) return SatSolver::Lit();
64  }
65  else {
66  Lit lit = db->decider()->makeDecision();
67  if (!lit.isNull()) {
68  //cout << "Split: " << lit.getVar().getIndex() << endl;
69  // Tell SAT solver which literal to split on
70  *done = false;
71  return db->cvc2SAT(lit);
72  }
73  }
74 
75  CNF_Formula_Impl cnf;
77  result = db->theoryAPI()->checkConsistent(cnf, true);
78 
79  if (result == DPLLT::MAYBE_CONSISTENT) {
80  IF_DEBUG(bool added = ) db->theoryAPI()->getNewClauses(cnf);
81  DebugAssert(added, "Expected new clauses");
82  db->addNewClauses(cnf);
83  *done = true;
85  l.id = 0;
86  return l;
87  }
88  else if (result == DPLLT::INCONSISTENT) {
89  db->addNewClauses(cnf);
90  }
91 
92  // Tell SAT solver that we are done
93  *done = true;
94  return SatSolver::Lit();
95 }
96 
97 
98 static void SATAssignmentHook(void *cookie, SatSolver::Var var, int value)
99 {
100  // cout<<"assignment called"<<endl;
101  DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
102  TRACE("DPLL Assign", var.id, " := ", value);
103  if (value == 0)
104  db->theoryAPI()->assertLit(Lit(db->satSolver()->GetVarIndex(var), false));
105  else if (value == 1)
106  db->theoryAPI()->assertLit(Lit(db->satSolver()->GetVarIndex(var), true));
107  else return;
108  CNF_Formula_Impl cnf;
110  result = db->theoryAPI()->checkConsistent(cnf, false);
111  if (result == DPLLT::INCONSISTENT) {
112  db->addNewClauses(cnf);
113  }
114 }
115 
116 
117 static void SATDeductionHook(void *cookie)
118 {
119  // cout<<"deduction called"<<endl;;
120  DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
121  Clause c;
122  CNF_Formula_Impl cnf;
123  if (db->theoryAPI()->getNewClauses(cnf)) {
124  db->addNewClauses(cnf);
125  cnf.reset();
126  }
127  Lit l = db->theoryAPI()->getImplication();
128  while (!l.isNull()) {
129  db->theoryAPI()->getExplanation(l, cnf);
130  db->addNewClauses(cnf);
131  cnf.reset();
132  l = db->theoryAPI()->getImplication();
133  }
134 }
135 
136 
137 void DPLLTBasic::createManager()
138 {
139  d_mng = SatSolver::Create();
140  d_mng->RegisterDLevelHook(SATDLevelHook, this);
141  d_mng->RegisterDecisionHook(SATDecisionHook, this);
142  d_mng->RegisterAssignmentHook(SATAssignmentHook, this);
143  d_mng->RegisterDeductionHook(SATDeductionHook, this);
144 }
145 
146 
147 void DPLLTBasic::generate_CDB (CNF_Formula_Impl& cnf)
148 {
150  Clause::const_iterator j, jend;
151  vector<SatSolver::Lit> clause;
152  if (cnf.numVars() > unsigned(d_mng->NumVariables())) {
153  d_mng->AddVariables(cnf.numVars() - d_mng->NumVariables());
154  }
155  cnf.simplify();
156  for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
157  //for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
158  if ((*i).isSatisfied()) continue;
159  for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
160  if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
161  }
162  if (clause.size() != 0) {
163  d_mng->AddClause(clause);
164  clause.clear();
165  }
166  }
167 }
168 
169 
170 void DPLLTBasic::handle_result(SatSolver::SATStatus outcome)
171 {
172  const char * result = "UNKNOWN";
173  switch (outcome) {
175 // if (d_printStats) {
176 // cout << "Instance satisfiable" << endl;
177 // for (int i=1, sz = d_mng->NumVariables(); i <= sz; ++i) {
178 // switch(d_mng->GetVarAssignment(d_mng->GetVar(i))) {
179 // case -1:
180 // cout <<"("<< i<<")"; break;
181 // case 0:
182 // cout << "-" << i; break;
183 // case 1:
184 // cout << i ; break;
185 // default:
186 // throw Exception("Unknown variable value state");
187 // }
188 // cout << " ";
189 // }
190 // cout << endl;
191 // }
192  result = "SAT";
193  break;
195  result = "UNSAT";
196  if (d_printStats) cout << "Instance unsatisfiable" << endl;
197  break;
199  result = "ABORT : TIME OUT";
200  cout << "Time out, unable to determine the satisfiablility of the instance";
201  cout << endl;
202  break;
204  result = "ABORT : MEM OUT";
205  cout << "Memory out, unable to determing the satisfiablility of the instance";
206  cout << endl;
207  break;
208  default:
209  throw Exception("DPLTBasic::handle_result: Unknown outcome");
210  }
211  if (d_printStats) d_mng->PrintStatistics();
212 }
213 
214 
215 void DPLLTBasic::verify_solution()
216 {
217  // Used to check that all clauses are true, but our decision maker
218  // may ignore some clauses that are no longer relevant, so now we check to
219  // make sure no clause is false.
220  for (SatSolver::Clause cl = d_mng->GetFirstClause(); !cl.IsNull();
221  cl = d_mng->GetNextClause(cl)) {
222  vector<SatSolver::Lit> lits;
223  d_mng->GetClauseLits(cl, &lits);
224  for (; lits.size() != 0;) {
225  SatSolver::Lit lit = lits.back();
226  SatSolver::Var var = d_mng->GetVarFromLit(lit);
227  int sign = d_mng->GetPhaseFromLit(lit);
228  int var_value = d_mng->GetVarAssignment(var);
229  if( (var_value == 1 && sign == 0) ||
230  (var_value == 0 && sign == 1) ||
231  (var_value == -1) ) break;
232  lits.pop_back();
233  }
234  DebugAssert(lits.size() != 0, "DPLLTBasic::verify_solution failed");
235  }
236 }
237 
238 
239 DPLLTBasic::DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider, ContextManager* cm,
240  bool printStats)
241  : DPLLT(theoryAPI, decider), d_cm(cm), d_ready(true),
242  d_printStats(printStats),
243  d_pushLevel(cm->getCurrentContext(), 0),
244  d_readyPrev(cm->getCurrentContext(), true),
245  d_prevStackSize(cm->getCurrentContext(), 0),
246  d_prevAStackSize(cm->getCurrentContext(), 0)
247 {
248  createManager();
249  d_cnf = new CNF_Formula_Impl();
251 }
252 
253 
255 {
256  if (d_assertions) delete d_assertions;
257  if (d_cnf) delete d_cnf;
258  if (d_mng) delete d_mng;
259  while (d_assertionsStack.size() > 0) {
261  d_assertionsStack.pop_back();
262  delete d_assertions;
263  }
264  while (d_mngStack.size() > 0) {
265  d_mng = d_mngStack.back();
266  d_mngStack.pop_back();
267  delete d_mng;
268  d_cnf = d_cnfStack.back();
269  d_cnfStack.pop_back();
270  delete d_cnf;
271  }
272 }
273 
274 
276 {
277  DebugAssert(c.size() > 0, "Expected non-empty clause");
278  DebugAssert(c.getMaxVar() <= unsigned(d_mng->NumVariables()),
279  "Expected no new variables");
280  vector<SatSolver::Lit> lits;
281  for (Clause::const_iterator i = c.begin(), iend = c.end(); i < iend; ++i) {
282  if (!(*i).isFalse()) lits.push_back(cvc2SAT(*i));
283  }
284  satSolver()->AddClause(lits);
285  (*d_cnf) += c;
286 }
287 
288 
290 {
292  Clause::const_iterator j, jend;
293  vector<SatSolver::Lit> clause;
294  if (cnf.numVars() > unsigned(d_mng->NumVariables())) {
296  }
297  cnf.simplify();
298  for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
299  //for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
300  if ((*i).isSatisfied()) continue;
301  for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
302  if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
303  }
304  if (clause.size() != 0) {
305  d_mng->AddClause(clause);
306  clause.clear();
307  }
308  }
309  generate_CDB(cnf);
310  (*d_cnf) += cnf;
311 }
312 
313 
315 {
316  d_theoryAPI->push();
317  d_pushLevel = d_pushLevel + 1;
318  d_prevStackSize = d_mngStack.size();
321 }
322 
323 
325 {
326  unsigned pushLevel = d_pushLevel;
327  unsigned prevStackSize = d_prevStackSize;
328  unsigned prevAStackSize = d_prevAStackSize;
329  bool readyPrev = d_readyPrev;
330 
331  while (d_assertionsStack.size() > prevAStackSize) {
332  delete d_assertions;
334  d_assertionsStack.pop_back();
335  }
336 
337  while (d_mngStack.size() > prevStackSize) {
338  delete d_mng;
339  delete d_cnf;
340  d_mng = d_mngStack.back();
341  d_mngStack.pop_back();
342  d_cnf = d_cnfStack.back();
343  d_cnfStack.pop_back();
344  DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
345  }
346 
347  if (d_mngStack.size() == 0) {
348  if (readyPrev && !d_ready) {
349  delete d_mng;
350  delete d_cnf;
351  createManager();
352  d_cnf = new CNF_Formula_Impl();
353  d_ready = true;
354  }
355  else {
356  DebugAssert(readyPrev == d_ready, "Unexpected ready values");
357  }
358  }
359  else {
360  DebugAssert(!d_ready, "Expected ready to be false");
361  }
362 
363  while (d_pushLevel == pushLevel)
364  d_theoryAPI->pop();
365 
366 }
367 
368 std::vector<SAT::Lit> DPLLTBasic::getCurAssignments(){
369  std::vector<SAT::Lit> nothing;
370  return nothing;
371 }
372 
373 std::vector<std::vector<SAT::Lit> > DPLLTBasic::getCurClauses(){
374  std::vector<std::vector<SAT::Lit> > nothing;
375  return nothing;
376 }
377 
378 
380 {
381  // Immediately assert unit clauses
383  Clause::const_iterator j, jend;
384  for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
385  if ((*i).isUnit()) {
386  j = (*i).begin();
387  d_theoryAPI->assertLit(*j);
388  }
389  }
390 
391  // Accumulate assertions in d_assertions
392  (*d_assertions) += cnf;
393 }
394 
395 
397 {
398  SatSolver::SATStatus result;
399 
400  if (!d_ready) {
401  // Copy current formula
402  d_cnfStack.push_back(d_cnf);
403  d_cnf = new CNF_Formula_Impl(*d_cnf);
404 
405  // make unit clauses for current assignment
406  int value;
407  for (int i = 1; i <= d_mng->NumVariables(); ++i) {
408  value = d_mng->GetVarAssignment(d_mng->GetVar(i));
409  if (value == 1) {
410  d_cnf->newClause();
411  d_cnf->addLiteral(Lit(i));
412  }
413  else if (value == 0) {
414  d_cnf->newClause();
415  d_cnf->addLiteral(Lit(i, false));
416  }
417  }
418 
419  // Create new manager
420  d_mngStack.push_back(d_mng);
421  DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
422  createManager();
423  }
424  d_ready = false;
425 
426  if (d_assertions) (*d_cnf) += (*d_assertions);
427 
428  (*d_cnf) += cnf;
430 
431  d_theoryAPI->push();
432 
433  result = d_mng->Satisfiable(true);
434  if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources())
436 
437  // Print result
438 
439  if (result == SatSolver::SATISFIABLE) {
440  verify_solution();
441  if (d_assertions->numClauses() > 0) {
442  d_assertionsStack.push_back(d_assertions);
444  }
445  }
446  handle_result (result);
447 
448  if (result == SatSolver::UNSATISFIABLE) {
449  d_theoryAPI->pop();
450  delete d_mng;
451  delete d_cnf;
452  if (d_mngStack.size() == 0) {
453  createManager();
454  d_cnf = new CNF_Formula_Impl();
455  d_ready = true;
456  }
457  else {
458  d_mng = d_mngStack.back();
459  d_mngStack.pop_back();
460  d_cnf = d_cnfStack.back();
461  d_cnfStack.pop_back();
462  DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
463  }
464  }
465 
466  return (result == SatSolver::UNSATISFIABLE ? UNSATISFIABLE :
467  result == SatSolver::SATISFIABLE ? SATISFIABLE :
468  ABORT);
469 }
470 
471 
473 {
474  SatSolver::SATStatus result;
475 
476  if (d_ready) {
477  throw Exception
478  ("continueCheck should be called after a previous satisfiable result");
479  }
480  if (d_assertions->numClauses() > 0) {
481  throw Exception
482  ("a check cannot be continued if new assertions have been made");
483  }
484  CNF_Formula_Impl cnfImpl(cnf);
485 
486  generate_CDB(cnfImpl);
487  (*d_cnf) += cnfImpl;
488 
489  result = d_mng->Continue();
490  if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources())
492 
493  // Print result
494 
495  if (result == SatSolver::SATISFIABLE)
496  verify_solution();
497  handle_result (result);
498 
499  if (result == SatSolver::UNSATISFIABLE) {
500  d_theoryAPI->pop();
501  delete d_mng;
502  delete d_cnf;
503  if (d_mngStack.size() == 0) {
504  createManager();
505  d_cnf = new CNF_Formula_Impl();
506  d_ready = true;
507  }
508  else {
509  d_mng = d_mngStack.back();
510  d_mngStack.pop_back();
511  d_cnf = d_cnfStack.back();
512  d_cnfStack.pop_back();
513  DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
514  }
515  }
516 
517  return (result == SatSolver::UNSATISFIABLE ? UNSATISFIABLE :
518  result == SatSolver::SATISFIABLE ? SATISFIABLE :
519  ABORT);
520 }
521 
523  CVC3::Proof temp;
524  return temp;
525 }
526