CVC3
minisat_derivation.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file minisat_derivation.cpp
4  *\brief MiniSat proof logging
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Sun Dec 07 11:09:00 2007
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 "minisat_derivation.h"
23 #include "minisat_solver.h"
24 #include "sat_proof.h"
25 #include <set>
26 #include <iostream>
27 
28 using namespace MiniSat;
29 using namespace std;
30 
31 std::string Inference::toString() const {
32  ostringstream buffer;
33  buffer << getStart();
34  for (Inference::TSteps::const_iterator step = d_steps.begin(); step != d_steps.end(); ++step) {
35  buffer << " " << step->first.toString() << " " << step->second;
36  }
37  return buffer.str();
38 }
39 
40 
41 
42 
43 
45  // deallocate generated unit clauses
46  for (TClauses::iterator i = d_unitClauses.begin(); i != d_unitClauses.end(); ++i) {
47  xfree(i->second);
48  }
49 
50  // deallocate removed clauses
51  for (std::deque<Clause*>::iterator i = d_removedClauses.begin(); i != d_removedClauses.end(); ++i) {
52  xfree(*i);
53  }
54 
55  // deallocate inferences
56  for (TInferences::iterator i = d_inferences.begin(); i != d_inferences.end(); ++i) {
57  delete i->second;
58  }
59 }
60 
61 
62 int Derivation::computeRootReason(Lit implied, Solver* solver) {
63  Clause* reason = solver->getReason(implied);
64  // cout << "computeRootReason " << reason->id() << endl;
65  FatalAssert(d_clauses.find(reason->id()) != d_clauses.end(),
66  "MiniSat::Derivation::computeRootReason: implied reason not registered");
67  FatalAssert(reason == d_clauses.find(reason->id())->second,
68  "MiniSat::Derivation::computeRootReason: implied reason not same as registered");
69  FatalAssert(reason != NULL, "MiniSat::Derivation::computeRootReason: implied reason is NULL");
70  FatalAssert(reason != Clause::Decision(), "MiniSat::Derivation::computeRootReason: implied is a decision");
71  FatalAssert((*reason)[0] == implied, "MiniSat::Derivation::computeRootReason: implied is not in its reason");
72  IF_DEBUG (
73  FatalAssert(solver->getValue((*reason)[0]) == l_True,
74  "MiniSat::Derivation::computeRootReason: literal not implied (TRUE)");
75  for (int i = 1; i < reason->size(); ++i) {
76  FatalAssert(solver->getValue((*reason)[i]) == l_False,
77  "MiniSat::Derivation::computeRootReason: literal not implied (FALSE)");
78  }
79  )
80 
81  // already a unit clause, so done
82  if (reason->size() == 1) {
83  return reason->id();
84  }
85 
86  // already derived the unit clause internally
87  TClauses::const_iterator iter = d_unitClauses.find(implied.index());
88  if (iter != d_unitClauses.end()) {
89  return iter->second->id();
90  }
91 
92 
93  // otherwise resolve the reason ...
94  Inference* inference = new Inference(reason->id());
95  for (int i = 1; i < reason->size(); ++i) {
96  Lit lit((*reason)[i]);
97  inference->add(lit, computeRootReason(~lit, solver));
98  }
99 
100  // and create the new unit clause
101  // (after resolve, so that clause ids are chronological wrt. inference)
102  vector<Lit> literals;
103  literals.push_back(implied);
104  Clause* unit = Clause_new(literals, CVC3::Theorem(), solver->nextClauseID());
105 
106  d_unitClauses[implied.index()] = unit;
107  // cout << "compute root reason : " << unit->id() << endl;
108  registerClause(unit);
109  registerInference(unit->id(), inference);
110 
111  return unit->id();
112 }
113 
114 
115 void Derivation::finish(Clause* clause, Solver* solver) {
116  FatalAssert(clause != NULL, "MiniSat::derivation:finish:");
117 
118  // already the empty clause
119  if (clause->size() == 0) {
120  d_emptyClause = clause;
121  }
122  // derive the empty clause
123  else {
124  Inference* inference = new Inference(clause->id());
125  for (int i = 0; i < clause->size(); ++i) {
126  Lit lit((*clause)[i]);
127  inference->add(lit, computeRootReason(~lit, solver));
128  }
129  vector<Lit> literals;
130  Clause* empty = Clause_new(literals, CVC3::Theorem(), solver->nextClauseID());
131  removedClause(empty);
132  d_emptyClause = empty;
133  registerClause(empty);
134  registerInference(empty->id(), inference);
135  }
136 
137  checkDerivation(clause);
138  IF_DEBUG (checkDerivation(clause));
139 
140 // cout << "PROOF_START" << endl;
141 // printDerivation();
142 // cout << "PROOF_END" << endl;
143 
144 }
145 
146 
147 
149  // find all relevant clauses
150 
151  // - relevant: set clauses used in derivation
152  // - regress: relevant clauses whose antecedents have to be checked
153  std::set<int> relevant;
154  std::set<int> regress;
155 
156  regress.insert(clause->id());
157  while (!regress.empty()) {
158  // pick next clause to derive - start from bottom, i.e. latest derived clause
159  int clauseID = *(regress.rbegin());
160  regress.erase(clauseID);
161 
162  // move to clauses relevant for the derivation
163  FatalAssert(relevant.count(clauseID) == 0, "Solver::printProof: already in relevant");
164  relevant.insert(clauseID);
165 
166  // process antecedents
167  TInferences::const_iterator iter = d_inferences.find(clauseID);
168  // input clause
169  if (iter == d_inferences.end()) {
170  FatalAssert(d_inputClauses.contains(clauseID),
171  "Solver::printProof: clause without antecedents is not marked as input clause");
172  }
173 
174  else {
175  Inference* inference = iter->second;
176  regress.insert(inference->getStart());
177  const Inference::TSteps& steps = inference->getSteps();
178  for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
179  regress.insert(step->second);
180  }
181  }
182  }
183 
184 
185  // check derivation
186  for (std::set<int>::iterator i = relevant.begin(); i != relevant.end(); ++i) {
187  int clauseID = *i;
188  FatalAssert(d_clauses.contains(clauseID),
189  "MiniSat::Derivation::printProof: clause id in proof is not in clauses");
190  Clause* clause = d_clauses.find(clauseID)->second;
191 
192  Inference* inference = NULL;
193  TInferences::const_iterator j = d_inferences.find(clauseID);
194  if (j != d_inferences.end()) {
195  inference = j->second;
196  }
197 
198  FatalAssert(inference != NULL || d_inputClauses.contains(clauseID),
199  "MiniSat::Derivation::printProof: derivation of input clause");
200  FatalAssert(inference == NULL || !d_inputClauses.contains(clauseID),
201  "MiniSat::Derivation::printProof: no derivation for derived clause");
202 
203  if (inference != NULL) {
204  // cout << "Regress: " << clause->id() << " : " << clause->toString() << endl;
205  FatalAssert(d_clauses.find(inference->getStart()) != d_clauses.end(),
206  "MiniSat::Derivation::printProof: first not in clauses");
207 
208  Clause* first = d_clauses.find(inference->getStart())->second;
209  // cout << "Derived from : " << first->id() << " : " << first->toString() << endl;
210 
211  set<Lit> derived;
212  for (int i = 0; i < first->size(); ++i) {
213  derived.insert((*first)[i]);
214  }
215 
216  // retrace derivation
217  for (Inference::TSteps::const_iterator step = inference->getSteps().begin();
218  step != inference->getSteps().end(); ++step) {
219  Lit lit = step->first;
220  // cout << " over " << lit.toString() << endl;
221  // cout << "Derived from ... : " << step->second << " : " << d_clauses.find(step->second)->second->toString() << endl;
222 
223  FatalAssert(d_clauses.find(step->second) != d_clauses.end(),
224  "MiniSat::Derivation::printProof: next not in clauses");
225  Clause* next = d_clauses.find(step->second)->second;
226 
227  FatalAssert(derived.find(lit) != derived.end(),
228  "MiniSat::Derivation::printProof: lit not in derived");
229  FatalAssert(next->contains(~lit),
230  "MiniSat::Derivation::printProof: ~lit not in next");
231 
232  derived.erase(lit);
233  for (int i = 0; i < next->size(); ++i) {
234  if ((*next)[i] != ~lit) {
235  derived.insert((*next)[i]);
236  }
237  }
238  }
239 
240  // check that we got the expected clause
241  for (int i = 0; i < clause->size(); ++i) {
242  FatalAssert(derived.find((*clause)[i]) != derived.end(),
243  "MiniSat::Derivation::printProof: didn't derive expected clause");
244  derived.erase((*clause)[i]);
245  }
246  FatalAssert(derived.empty(),
247  "MiniSat::Derivation::printProof: didn't derive expected clause 2");
248  };
249  }
250 }
251 
252 
254  FatalAssert(d_emptyClause != NULL, "MiniSat::Derivation:createProof: no empty clause");
255  FatalAssert(d_emptyClause->size() == 0,
256  "MiniSat::Derivation:createProof: empty clause is not empty");
257  return createProof(d_emptyClause);
258 }
259 
261  checkDerivation(clause);
262  // IF_DEBUG (checkDerivation(clause));
263 
264  // find all relevant clauses
265 
266  // - relevant: set clauses used in derivation
267  // - regress: relevant clauses whose antecedents have to be checked
268  std::set<int> relevant;
269  std::set<int> regress;
270  regress.insert(clause->id());
271  while (!regress.empty()) {
272  // pick next clause to derive - start from bottom, i.e. latest derived clause
273  int clauseID = *(regress.rbegin());
274  regress.erase(clauseID);
275  relevant.insert(clauseID);
276 
277  // process antecedents
278  TInferences::const_iterator iter = d_inferences.find(clauseID);
279  // input clause
280  if (iter != d_inferences.end()) {
281  Inference* inference = iter->second;
282  regress.insert(inference->getStart());
283  const Inference::TSteps& steps = inference->getSteps();
284  for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
285  regress.insert(step->second);
286  }
287  }
288  }
289 
290  // create proof
291  SAT::SatProof* proof = new SAT::SatProof();
293 
294  for (std::set<int>::iterator i = relevant.begin(); i != relevant.end(); ++i) {
295  int clauseID = *i;
296  Clause* clause = d_clauses.find(clauseID)->second;
297 
298  Inference* inference = NULL;
299  TInferences::const_iterator j = d_inferences.find(clauseID);
300  if (j == d_inferences.end()) {
301  /*
302 <<<<<<< minisat_derivation.cpp
303  FatalAssert(clause->getCvcClause() != NULL, "createProof: leaf without clause");
304  FatalAssert(clause->getCvcClause() != NULL, "createProof: leaf without clause");
305  proofNodes[clause->id()] = proof->registerLeaf(clause->getCvcClause());
306  // cout<<"cluase with :" << clause->id() << " ---> " ;
307  // clause->getCvcClause()->print();
308  // cout << endl;
309 =======
310  */
311  FatalAssert(!clause->getTheorem().isNull(), "createProof: leaf without clause");
312  proofNodes[clause->id()] = proof->registerLeaf(clause->getTheorem());
313  /*
314 >>>>>>> 1.9
315  */
316  }
317 
318  else {
319  inference = j->second;
320  FatalAssert(proofNodes.contains(inference->getStart()), "createProof: contains inference start");
321  SAT::SatProofNode* left = proofNodes.find(inference->getStart())->second;
322  const Inference::TSteps& steps = inference->getSteps();
323  for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
324  FatalAssert(proofNodes.contains(step->second), "createProof: contains inference start");
325  SAT::SatProofNode* right = proofNodes.find(step->second)->second;
326  left = proof->registerNode(left, right, miniSatToCVC(step->first));
327  }
328  proofNodes[clause->id()] = left;
329  }
330  }
331  proof->setRoot(proofNodes[clause->id()]);
332  return proof;
333 }
334 
335 
337  FatalAssert(d_emptyClause != NULL, "MiniSat::Derivation:printDerivation: no empty clause");
338  FatalAssert(d_emptyClause->size() == 0,
339  "MiniSat::Derivation:printDerivation: empty clause is not empty");
340  printDerivation(d_emptyClause);
341 }
342 
344  IF_DEBUG (checkDerivation(clause));
345 
346  // find all relevant clauses
347 
348  // - relevant: set clauses used in derivation
349  // - regress: relevant clauses whose antecedents have to be checked
350  std::set<int> relevant;
351  std::set<int> regress;
352 
353  regress.insert(clause->id());
354  while (!regress.empty()) {
355  // pick next clause to derive - start from bottom, i.e. latest derived clause
356  int clauseID = *(regress.rbegin());
357  regress.erase(clauseID);
358 
359  // move to clauses relevant for the derivation
360  relevant.insert(clauseID);
361 
362  // process antecedents
363  TInferences::const_iterator iter = d_inferences.find(clauseID);
364  // input clause
365  if (iter != d_inferences.end()) {
366  Inference* inference = iter->second;
367  regress.insert(inference->getStart());
368  const Inference::TSteps& steps = inference->getSteps();
369  for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
370  regress.insert(step->second);
371  }
372  }
373  }
374 
375 
376  // print proof
377  for (std::set<int>::iterator i = relevant.begin(); i != relevant.end(); ++i) {
378  int clauseID = *i;
379  Clause* clause = d_clauses.find(clauseID)->second;
380 
381  Inference* inference = NULL;
382  TInferences::const_iterator j = d_inferences.find(clauseID);
383  if (j != d_inferences.end()) {
384  inference = j->second;
385  }
386 
387  // ID D : L1 ... Ln : C1 K1 C2 K2 ... Cm
388  cout << clauseID;
389  // input clause or derived clause?
390  if (d_inputClauses.contains(clauseID)) {
391  cout << " I ";
392  } else {
393  cout << " D ";
394  }
395  cout << ": " << clause->toString() << " : ";
396  if (inference != NULL) cout << inference->toString();
397  cout << endl;
398  }
399 }
400 
401 
402 void Derivation::push(int clauseID) {
403  // cout << "derivation push: " << clauseID << endl;
404 }
405 
406 void Derivation::pop(int clauseID) {
407  // cout << "derivation pop: " << clauseID << endl;
408  // remove all popped clauses
409  TClauses::const_iterator i = d_clauses.begin();
410  while (i != d_clauses.end()) {
411  Clause* clause = (*i).second;
412  if (
413  // Warning: clause removal needs to be done
414  // exactly the same way in minisat_solver!!!
415 
416  // remove theory lemmas
417  // :TODO: can't do that: kept lemmas might depend on them
418  // (!clause->learnt() && clause->pushID() < 0)
419  // ||
420  // remove clauses added after the last push
421  clause->pushID() > clauseID) {
422  int id = clause->id();
423  // cout << "derivation pop now: " << id << endl;
424  d_inputClauses.erase(id);
425  d_inferences.erase(id);
426 
427  if (clause->size() == 1) {
428  int index = (*clause)[0].index();
429  if (d_unitClauses.contains(index) && d_unitClauses[index] == clause) {
430  d_unitClauses.erase(index);
431  FatalAssert(!d_unitClauses.contains(index), "AHA");
432  }
433  }
434 
435  i = d_clauses.erase(i);
436  }
437  else {
438  ++i;
439  }
440  }
441 
442  // undo conflicting clause
443  if (d_emptyClause != NULL && d_emptyClause->pushID() > clauseID)
444  d_emptyClause = NULL;
445 
446  // delete popped and removed clauses
447  std::deque<Clause*>::iterator j = d_removedClauses.begin();
448  while (j != d_removedClauses.end()) {
449  if ((*j)->pushID() > clauseID) {
450  xfree(*j);
451  j = d_removedClauses.erase(j);
452  } else {
453  ++j;
454  }
455  }
456 }