src/proof/sat_proof.cpp

   1 /*********************                                                        */
   2 /*! \file sat_proof.cpp
   3  ** \verbatim
   4  ** Original author: Liana Hadarean
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "proof/sat_proof.h"
  19 #include "proof/proof_manager.h"
  20 #include "prop/minisat/core/Solver.h"
  21 #include "prop/minisat/minisat.h"
  22
  23 using namespace std;
  24 using namespace Minisat;
  25 using namespace CVC4::prop;
  26 namespace CVC4 {
  27
  28 /// some helper functions
  29
  30 void printLit (Minisat::Lit l) {
  31   Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
  32 }
  33
  34 void printClause (Minisat::Clause& c) {
  35   for (int i = 0; i < c.size(); i++) {
  36     Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
  37   }
  38 }
  39
  40 void printLitSet(const LitSet& s) {
  41   for(LitSet::iterator it = s.begin(); it != s.end(); ++it) {
  42     printLit(*it);
  43     Debug("proof:sat") << " ";
  44   }
  45   Debug("proof:sat") << endl;
  46 }
  47
  48 // purely debugging functions
  49 void printDebug (Minisat::Lit l) {
  50   Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << endl;
  51 }
  52
  53 void printDebug (Minisat::Clause& c) {
  54   for (int i = 0; i < c.size(); i++) {
  55     Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
  56   }
  57   Debug("proof:sat") << endl;
  58 }
  59
  60 /**
  61  * Converts the clause associated to id to a set of literals
  62  *
  63  * @param id the clause id
  64  * @param set the clause converted to a set of literals
  65  */
  66 void SatProof::createLitSet(ClauseId id, LitSet& set) {
  67   Assert(set.empty());
  68   if(isUnit(id)) {
  69     set.insert(getUnit(id));
  70     return;
  71   }
  72   if ( id == d_emptyClauseId) {
  73     return;
  74   }
  75   CRef ref = getClauseRef(id);
  76   Clause& c = getClause(ref);
  77   for (int i = 0; i < c.size(); i++) {
  78     set.insert(c[i]);
  79   }
  80 }
  81
  82
  83 /**
  84  * Resolves clause1 and clause2 on variable var and stores the
  85  * result in clause1
  86  * @param v
  87  * @param clause1
  88  * @param clause2
  89  */
  90 bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) {
  91   Assert(!clause1.empty());
  92   Assert(!clause2.empty());
  93   Lit var = sign(v) ? ~v : v;
  94   if (s) {
  95     // literal appears positive in the first clause
  96     if( !clause2.count(~var)) {
  97       if(Debug.isOn("proof:sat")) {
  98         Debug("proof:sat") << "proof:resolve: Missing literal ";
  99         printLit(var);
 100         Debug("proof:sat") << endl;
 101       }
 102       return false;
 103     }
 104     clause1.erase(var);
 105     clause2.erase(~var);
 106     for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
 107       clause1.insert(*it);
 108     }
 109   } else {
 110     // literal appears negative in the first clause
 111     if( !clause1.count(~var) || !clause2.count(var)) {
 112       if(Debug.isOn("proof:sat")) {
 113         Debug("proof:sat") << "proof:resolve: Missing literal ";
 114         printLit(var);
 115         Debug("proof:sat") << endl;
 116       }
 117       return false;
 118     }
 119     clause1.erase(~var);
 120     clause2.erase(var);
 121     for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
 122       clause1.insert(*it);
 123     }
 124   }
 125   return true;
 126 }
 127
 128 /// ResChain
 129
 130 ResChain::ResChain(ClauseId start) :
 131     d_start(start),
 132     d_steps(),
 133     d_redundantLits(NULL)
 134   {}
 135
 136 void ResChain::addStep(Lit lit, ClauseId id, bool sign) {
 137   ResStep step(lit, id, sign);
 138   d_steps.push_back(step);
 139 }
 140
 141
 142 void ResChain::addRedundantLit(Lit lit) {
 143   if (d_redundantLits) {
 144     d_redundantLits->insert(lit);
 145   } else {
 146     d_redundantLits = new LitSet();
 147     d_redundantLits->insert(lit);
 148   }
 149 }
 150
 151
 152 /// ProxyProof
 153
 154 ProofProxy::ProofProxy(SatProof* proof):
 155   d_proof(proof)
 156 {}
 157
 158 void ProofProxy::updateCRef(CRef oldref, CRef newref) {
 159   d_proof->updateCRef(oldref, newref);
 160 }
 161
 162
 163 /// SatProof
 164
 165 SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
 166     d_solver(solver),
 167     d_idClause(),
 168     d_clauseId(),
 169     d_idUnit(),
 170     d_deleted(),
 171     d_inputClauses(),
 172     d_lemmaClauses(),
 173     d_resChains(),
 174     d_resStack(),
 175     d_checkRes(checkRes),
 176     d_emptyClauseId(-1),
 177     d_nullId(-2),
 178     d_temp_clauseId(),
 179     d_temp_idClause(),
 180     d_unitConflictId(),
 181     d_storedUnitConflict(false),
 182     d_seenLearnt(),
 183     d_seenInput(),
 184     d_seenLemmas()
 185   {
 186     d_proxy = new ProofProxy(this);
 187   }
 188
 189 /**
 190  * Returns true if the resolution chain corresponding to id
 191  * does resolve to the clause associated to id
 192  * @param id
 193  *
 194  * @return
 195  */
 196 bool SatProof::checkResolution(ClauseId id) {
 197   if(d_checkRes) {
 198     bool validRes = true;
 199     Assert(d_resChains.find(id) != d_resChains.end());
 200     ResChain* res = d_resChains[id];
 201     LitSet clause1;
 202     createLitSet(res->getStart(), clause1);
 203     ResSteps& steps = res->getSteps();
 204     for (unsigned i = 0; i < steps.size(); i++) {
 205       Lit    var = steps[i].lit;
 206       LitSet clause2;
 207       createLitSet (steps[i].id, clause2);
 208       bool res = resolve (var, clause1, clause2, steps[i].sign);
 209       if(res == false) {
 210         validRes = false;
 211         break;
 212       }
 213     }
 214     // compare clause we claimed to prove with the resolution result
 215     if (isUnit(id)) {
 216       // special case if it was a unit clause
 217       Lit unit = getUnit(id);
 218       validRes = clause1.size() == clause1.count(unit) && !clause1.empty();
 219       return validRes;
 220     }
 221     if (id == d_emptyClauseId) {
 222       return clause1.empty();
 223     }
 224     CRef ref = getClauseRef(id);
 225     Clause& c = getClause(ref);
 226     for (int i = 0; i < c.size(); ++i) {
 227       int count = clause1.erase(c[i]);
 228       if (count == 0) {
 229         if(Debug.isOn("proof:sat")) {
 230           Debug("proof:sat") << "proof:checkResolution::literal not in computed result ";
 231           printLit(c[i]);
 232           Debug("proof:sat") << "\n";
 233         }
 234         validRes = false;
 235       }
 236     }
 237     validRes = clause1.empty();
 238     if (! validRes) {
 239       if(Debug.isOn("proof:sat")) {
 240         Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n";
 241         printLitSet(clause1);
 242         Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
 243         printClause(c);
 244       }
 245     }
 246     return validRes;
 247
 248   } else {
 249     return true;
 250   }
 251 }
 252
 253
 254
 255
 256 /// helper methods
 257
 258 ClauseId SatProof::getClauseId(::Minisat::CRef ref) {
 259   if(d_clauseId.find(ref) == d_clauseId.end()) {
 260     Debug("proof:sat") << "Missing clause \n";
 261   }
 262   Assert(d_clauseId.find(ref) != d_clauseId.end());
 263   return d_clauseId[ref];
 264 }
 265
 266
 267 ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
 268   Assert(d_unitId.find(toInt(lit)) != d_unitId.end());
 269   return d_unitId[toInt(lit)];
 270 }
 271
 272 Minisat::CRef SatProof::getClauseRef(ClauseId id) {
 273   if (d_idClause.find(id) == d_idClause.end()) {
 274     Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " "
 275                        << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
 276                        << (isUnit(id)? "Unit" : "") << endl;
 277   }
 278   Assert(d_idClause.find(id) != d_idClause.end());
 279   return d_idClause[id];
 280 }
 281
 282 Clause& SatProof::getClause(CRef ref) {
 283   Assert(ref != CRef_Undef);
 284   Assert(ref >= 0 && ref < d_solver->ca.size());
 285   return d_solver->ca[ref];
 286 }
 287
 288 Minisat::Lit SatProof::getUnit(ClauseId id) {
 289   Assert(d_idUnit.find(id) != d_idUnit.end());
 290   return d_idUnit[id];
 291 }
 292
 293 bool SatProof::isUnit(ClauseId id) {
 294   return d_idUnit.find(id) != d_idUnit.end();
 295 }
 296
 297 bool SatProof::isUnit(::Minisat::Lit lit) {
 298   return d_unitId.find(toInt(lit)) != d_unitId.end();
 299 }
 300
 301 ClauseId SatProof::getUnitId(::Minisat::Lit lit) {
 302   Assert(isUnit(lit));
 303   return d_unitId[toInt(lit)];
 304 }
 305
 306 bool SatProof::hasResolution(ClauseId id) {
 307   return d_resChains.find(id) != d_resChains.end();
 308 }
 309
 310 bool SatProof::isInputClause(ClauseId id) {
 311   return (d_inputClauses.find(id) != d_inputClauses.end());
 312 }
 313
 314 bool SatProof::isLemmaClause(ClauseId id) {
 315   return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
 316 }
 317
 318 void SatProof::print(ClauseId id) {
 319   if (d_deleted.find(id) != d_deleted.end()) {
 320     Debug("proof:sat") << "del" << id;
 321   } else if (isUnit(id)) {
 322     printLit(getUnit(id));
 323   } else if (id == d_emptyClauseId) {
 324     Debug("proof:sat") << "empty " << endl;
 325   } else {
 326     CRef ref = getClauseRef(id);
 327     printClause(getClause(ref));
 328   }
 329 }
 330
 331 void SatProof::printRes(ClauseId id) {
 332   Assert(hasResolution(id));
 333   Debug("proof:sat") << "id " << id << ": ";
 334   printRes(d_resChains[id]);
 335 }
 336
 337 void SatProof::printRes(ResChain* res) {
 338   ClauseId start_id = res->getStart();
 339
 340   if(Debug.isOn("proof:sat")) {
 341     Debug("proof:sat") << "(";
 342     print(start_id);
 343   }
 344
 345   ResSteps& steps = res->getSteps();
 346   for(unsigned i = 0; i < steps.size(); i++ ) {
 347     Lit v = steps[i].lit;
 348     ClauseId id = steps[i].id;
 349
 350     if(Debug.isOn("proof:sat")) {
 351       Debug("proof:sat") << "[";
 352       printLit(v);
 353       Debug("proof:sat") << "] ";
 354       print(id);
 355     }
 356   }
 357   Debug("proof:sat") << ") \n";
 358 }
 359
 360 /// registration methods
 361
 362 ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
 363   Debug("cores") << "registerClause " << proof_id << std::endl;
 364   Assert(clause != CRef_Undef);
 365   ClauseIdMap::iterator it = d_clauseId.find(clause);
 366   if (it == d_clauseId.end()) {
 367     ClauseId newId = ProofManager::currentPM()->nextId();
 368     d_clauseId[clause] = newId;
 369     d_idClause[newId] = clause;
 370     if (kind == INPUT) {
 371       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
 372       d_inputClauses[newId] = proof_id;
 373     }
 374     if (kind == THEORY_LEMMA) {
 375       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
 376       d_lemmaClauses[newId] = proof_id;
 377     }
 378   }
 379   Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n";
 380   return d_clauseId[clause];
 381 }
 382
 383 ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) {
 384   Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl;
 385   UnitIdMap::iterator it = d_unitId.find(toInt(lit));
 386   if (it == d_unitId.end()) {
 387     ClauseId newId = ProofManager::currentPM()->nextId();
 388     d_unitId[toInt(lit)] = newId;
 389     d_idUnit[newId] = lit;
 390     if (kind == INPUT) {
 391       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
 392       d_inputClauses[newId] = proof_id;
 393     }
 394     if (kind == THEORY_LEMMA) {
 395       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
 396       d_lemmaClauses[newId] = proof_id;
 397     }
 398   }
 399   Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
 400   return d_unitId[toInt(lit)];
 401 }
 402
 403 void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) {
 404   // if we already added the literal return
 405   if (seen.count(lit)) {
 406     return;
 407   }
 408
 409   CRef reason_ref = d_solver->reason(var(lit));
 410   if (reason_ref == CRef_Undef) {
 411     seen.insert(lit);
 412     removeStack.push_back(lit);
 413     return;
 414   }
 415
 416   int size = getClause(reason_ref).size();
 417   for (int i = 1; i < size; i++ ) {
 418     Lit v = getClause(reason_ref)[i];
 419     if(inClause.count(v) == 0 && seen.count(v) == 0) {
 420       removedDfs(v, removedSet, removeStack, inClause, seen);
 421     }
 422   }
 423   if(seen.count(lit) == 0) {
 424     seen.insert(lit);
 425     removeStack.push_back(lit);
 426   }
 427 }
 428
 429
 430 void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
 431   LitSet* removed = res->getRedundant();
 432   if (removed == NULL) {
 433     return;
 434   }
 435
 436   LitSet inClause;
 437   createLitSet(id, inClause);
 438
 439   LitVector removeStack;
 440   LitSet seen;
 441   for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) {
 442     removedDfs(*it, removed, removeStack, inClause, seen);
 443   }
 444
 445   for (int i = removeStack.size() - 1; i >= 0; --i) {
 446     Lit lit = removeStack[i];
 447     CRef reason_ref = d_solver->reason(var(lit));
 448     ClauseId reason_id;
 449
 450     if (reason_ref == CRef_Undef) {
 451       Assert(isUnit(~lit));
 452       reason_id = getUnitId(~lit);
 453     } else {
 454       reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
 455     }
 456     res->addStep(lit, reason_id, !sign(lit));
 457   }
 458   removed->clear();
 459 }
 460
 461 void SatProof::registerResolution(ClauseId id, ResChain* res) {
 462   Assert(res != NULL);
 463
 464   removeRedundantFromRes(res, id);
 465   Assert(res->redundantRemoved());
 466
 467   d_resChains[id] = res;
 468   if(Debug.isOn("proof:sat")) {
 469     printRes(id);
 470   }
 471   if(d_checkRes) {
 472     Assert(checkResolution(id));
 473   }
 474 }
 475
 476
 477 /// recording resolutions
 478
 479 void SatProof::startResChain(::Minisat::CRef start) {
 480   ClauseId id = getClauseId(start);
 481   ResChain* res = new ResChain(id);
 482   d_resStack.push_back(res);
 483 }
 484
 485 void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
 486   ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
 487   ResChain* res = d_resStack.back();
 488   res->addStep(lit, id, sign);
 489 }
 490
 491 void SatProof::endResChain(CRef clause) {
 492   Assert(d_resStack.size() > 0);
 493   ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
 494   ResChain* res = d_resStack.back();
 495   registerResolution(id, res);
 496   d_resStack.pop_back();
 497 }
 498
 499
 500 void SatProof::endResChain(::Minisat::Lit lit) {
 501   Assert(d_resStack.size() > 0);
 502   ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1));
 503   ResChain* res = d_resStack.back();
 504   registerResolution(id, res);
 505   d_resStack.pop_back();
 506 }
 507
 508 void SatProof::storeLitRedundant(::Minisat::Lit lit) {
 509   Assert(d_resStack.size() > 0);
 510   ResChain* res = d_resStack.back();
 511   res->addRedundantLit(lit);
 512 }
 513
 514 /// constructing resolutions
 515
 516 void SatProof::resolveOutUnit(::Minisat::Lit lit) {
 517   ClauseId id = resolveUnit(~lit);
 518   ResChain* res = d_resStack.back();
 519   res->addStep(lit, id, !sign(lit));
 520 }
 521
 522 void SatProof::storeUnitResolution(::Minisat::Lit lit) {
 523   Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
 524   resolveUnit(lit);
 525 }
 526
 527 ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
 528   // first check if we already have a resolution for lit
 529   if(isUnit(lit)) {
 530     ClauseId id = getClauseId(lit);
 531     Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id));
 532     return id;
 533   }
 534   CRef reason_ref = d_solver->reason(var(lit));
 535   Assert(reason_ref != CRef_Undef);
 536
 537   ClauseId reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
 538
 539   ResChain* res = new ResChain(reason_id);
 540   // Here, the call to resolveUnit() can reallocate memory in the
 541   // clause allocator.  So reload reason ptr each time.
 542   Clause* reason = &getClause(reason_ref);
 543   for (int i = 0;
 544        i < reason->size();
 545        i++, reason = &getClause(reason_ref)) {
 546     Lit l = (*reason)[i];
 547     if(lit != l) {
 548       ClauseId res_id = resolveUnit(~l);
 549       res->addStep(l, res_id, !sign(l));
 550     }
 551   }
 552   ClauseId unit_id = registerUnitClause(lit, LEARNT, uint64_t(-1));
 553   registerResolution(unit_id, res);
 554   return unit_id;
 555 }
 556
 557 void SatProof::toStream(std::ostream& out) {
 558   Debug("proof:sat") << "SatProof::printProof\n";
 559   Unimplemented("native proof printing not supported yet");
 560 }
 561
 562 void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) {
 563   Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
 564   Assert(!d_storedUnitConflict);
 565   d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id);
 566   d_storedUnitConflict = true;
 567   Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n";
 568 }
 569
 570 void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
 571   Assert(d_resStack.size() == 0);
 572   Assert(conflict_ref != ::Minisat::CRef_Undef);
 573   ClauseId conflict_id;
 574   if (conflict_ref == ::Minisat::CRef_Lazy) {
 575     Assert(d_storedUnitConflict);
 576     conflict_id = d_unitConflictId;
 577
 578     ResChain* res = new ResChain(conflict_id);
 579     Lit lit = d_idUnit[conflict_id];
 580     ClauseId res_id = resolveUnit(~lit);
 581     res->addStep(lit, res_id, !sign(lit));
 582
 583     registerResolution(d_emptyClauseId, res);
 584
 585     return;
 586   } else {
 587     Assert(!d_storedUnitConflict);
 588     conflict_id = registerClause(conflict_ref, LEARNT, uint64_t(-1)); //FIXME
 589   }
 590
 591   if(Debug.isOn("proof:sat")) {
 592     Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
 593     print(conflict_id);
 594   }
 595
 596   ResChain* res = new ResChain(conflict_id);
 597   // Here, the call to resolveUnit() can reallocate memory in the
 598   // clause allocator.  So reload conflict ptr each time.
 599   Clause* conflict = &getClause(conflict_ref);
 600   for (int i = 0;
 601        i < conflict->size();
 602        ++i, conflict = &getClause(conflict_ref)) {
 603     Lit lit = (*conflict)[i];
 604     ClauseId res_id = resolveUnit(~lit);
 605     res->addStep(lit, res_id, !sign(lit));
 606   }
 607   registerResolution(d_emptyClauseId, res);
 608 }
 609
 610 /// CRef manager
 611
 612 void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) {
 613   if (d_clauseId.find(oldref) == d_clauseId.end()) {
 614     return;
 615   }
 616   ClauseId id = getClauseId(oldref);
 617   Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end());
 618   Assert(d_temp_idClause.find(id) == d_temp_idClause.end());
 619   d_temp_clauseId[newref] = id;
 620   d_temp_idClause[id] = newref;
 621 }
 622
 623 void SatProof::finishUpdateCRef() {
 624   d_clauseId.swap(d_temp_clauseId);
 625   d_temp_clauseId.clear();
 626
 627   d_idClause.swap(d_temp_idClause);
 628   d_temp_idClause.clear();
 629 }
 630
 631 void SatProof::markDeleted(CRef clause) {
 632   if (d_clauseId.find(clause) != d_clauseId.end()) {
 633     ClauseId id = getClauseId(clause);
 634     Assert(d_deleted.find(id) == d_deleted.end());
 635     d_deleted.insert(id);
 636     if (isLemmaClause(id)) {
 637       const Clause& minisat_cl = getClause(clause);
 638       SatClause* sat_cl = new SatClause();
 639       MinisatSatSolver::toSatClause(minisat_cl, *sat_cl);
 640       d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
 641     }
 642   }
 643 }
 644
 645 void SatProof::constructProof() {
 646   collectClauses(d_emptyClauseId);
 647 }
 648
 649 std::string SatProof::clauseName(ClauseId id) {
 650   ostringstream os;
 651   if (isInputClause(id)) {
 652     os << ProofManager::getInputClauseName(id);
 653     return os.str();
 654   } else if (isLemmaClause(id)) {
 655     os << ProofManager::getLemmaClauseName(id);
 656     return os.str();
 657   } else {
 658     os << ProofManager::getLearntClauseName(id);
 659     return os.str();
 660   }
 661 }
 662
 663 void SatProof::addToProofManager(ClauseId id, ClauseKind kind) {
 664   if (isUnit(id)) {
 665     Minisat::Lit lit = getUnit(id);
 666     prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit);
 667     prop::SatClause* clause = new SatClause();
 668     clause->push_back(sat_lit);
 669     ProofManager::currentPM()->addClause(id, clause, kind);
 670     return;
 671   }
 672
 673   if (isDeleted(id)) {
 674     Assert(kind == THEORY_LEMMA);
 675     SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
 676     ProofManager::currentPM()->addClause(id, clause, kind);
 677     return;
 678   }
 679
 680   CRef ref = getClauseRef(id);
 681   const Clause& minisat_cl = getClause(ref);
 682   SatClause* clause = new SatClause();
 683   MinisatSatSolver::toSatClause(minisat_cl, *clause);
 684   ProofManager::currentPM()->addClause(id, clause, kind);
 685 }
 686
 687 void SatProof::collectClauses(ClauseId id) {
 688   if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
 689     return;
 690   }
 691   if (d_seenInput.find(id) != d_seenInput.end()) {
 692     return;
 693   }
 694   if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
 695     return;
 696   }
 697
 698   if (isInputClause(id)) {
 699     addToProofManager(id, INPUT);
 700     d_seenInput.insert(id);
 701     return;
 702   } else if (isLemmaClause(id)) {
 703     addToProofManager(id, THEORY_LEMMA);
 704     d_seenLemmas.insert(id);
 705     return;
 706   } else {
 707     d_seenLearnt.insert(id);
 708   }
 709
 710   Assert(d_resChains.find(id) != d_resChains.end());
 711   ResChain* res = d_resChains[id];
 712   ClauseId start = res->getStart();
 713   collectClauses(start);
 714
 715   ResSteps steps = res->getSteps();
 716   for(size_t i = 0; i < steps.size(); i++) {
 717     collectClauses(steps[i].id);
 718   }
 719 }
 720
 721 /// LFSCSatProof class
 722
 723 void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
 724   out << "(satlem_simplify _ _ _ ";
 725
 726   ResChain* res = d_resChains[id];
 727   ResSteps& steps = res->getSteps();
 728
 729   for (int i = steps.size() - 1; i >= 0; --i) {
 730     out << "(";
 731     out << (steps[i].sign? "R" : "Q") << " _ _ ";
 732   }
 733
 734   ClauseId start_id = res->getStart();
 735   // WHY DID WE NEED THIS?
 736   // if(isInputClause(start_id)) {
 737   //   d_seenInput.insert(start_id);
 738   // }
 739   out << clauseName(start_id) << " ";
 740
 741   for(unsigned i = 0; i < steps.size(); i++) {
 742     out << clauseName(steps[i].id) << " "
 743         << ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit)))
 744         << ") ";
 745   }
 746
 747   if (id == d_emptyClauseId) {
 748     out << "(\\empty empty)";
 749     return;
 750   }
 751
 752   out << "(\\" << clauseName(id) << "\n";   // bind to lemma name
 753   paren << "))";                            // closing parethesis for lemma binding and satlem
 754 }
 755
 756 void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
 757   for(IdSet::iterator it = d_seenLearnt.begin(); it!= d_seenLearnt.end(); ++it) {
 758     if(*it != d_emptyClauseId) {
 759       printResolution(*it, out, paren);
 760     }
 761   }
 762   printResolution(d_emptyClauseId, out, paren);
 763 }
 764
 765 } /* CVC4 namespace */