src/proof/proof_manager.cpp

   1 /*********************                                                        */
   2 /*! \file proof_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz, Liana Hadarean, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** [[ Add lengthier description here ]]
  13
  14  ** \todo document this file
  15
  16 **/
  17
  18 #include "proof/proof_manager.h"
  19
  20 #include "base/cvc4_assert.h"
  21 #include "context/context.h"
  22 #include "options/bv_options.h"
  23 #include "options/proof_options.h"
  24 #include "proof/bitvector_proof.h"
  25 #include "proof/clause_id.h"
  26 #include "proof/cnf_proof.h"
  27 #include "proof/proof_utils.h"
  28 #include "proof/sat_proof_implementation.h"
  29 #include "proof/theory_proof.h"
  30 #include "smt/smt_engine.h"
  31 #include "smt/smt_engine_scope.h"
  32 #include "smt_util/node_visitor.h"
  33 #include "theory/arrays/theory_arrays.h"
  34 #include "theory/output_channel.h"
  35 #include "theory/term_registration_visitor.h"
  36 #include "theory/uf/equality_engine.h"
  37 #include "theory/uf/theory_uf.h"
  38 #include "theory/valuation.h"
  39 #include "util/hash.h"
  40 #include "util/proof.h"
  41
  42 namespace CVC4 {
  43
  44 std::string nodeSetToString(const std::set<Node>& nodes) {
  45   std::ostringstream os;
  46   std::set<Node>::const_iterator it;
  47   for (it = nodes.begin(); it != nodes.end(); ++it) {
  48     os << *it << " ";
  49   }
  50   return os.str();
  51 }
  52
  53 std::string append(const std::string& str, uint64_t num) {
  54   std::ostringstream os;
  55   os << str << num;
  56   return os.str();
  57 }
  58
  59 ProofManager::ProofManager(context::Context* context, ProofFormat format)
  60     : d_context(context),
  61       d_satProof(NULL),
  62       d_cnfProof(NULL),
  63       d_theoryProof(NULL),
  64       d_inputFormulas(),
  65       d_inputCoreFormulas(context),
  66       d_outputCoreFormulas(context),
  67       d_nextId(0),
  68       d_fullProof(),
  69       d_format(format),
  70       d_deps(context)
  71 {
  72 }
  73
  74 ProofManager::~ProofManager() {
  75   if (d_satProof) delete d_satProof;
  76   if (d_cnfProof) delete d_cnfProof;
  77   if (d_theoryProof) delete d_theoryProof;
  78 }
  79
  80 ProofManager* ProofManager::currentPM() {
  81   return smt::currentProofManager();
  82 }
  83 const Proof& ProofManager::getProof(SmtEngine* smt)
  84 {
  85   if (!currentPM()->d_fullProof)
  86   {
  87     Assert(currentPM()->d_format == LFSC);
  88     currentPM()->d_fullProof.reset(new LFSCProof(
  89         smt,
  90         static_cast<LFSCCoreSatProof*>(getSatProof()),
  91         static_cast<LFSCCnfProof*>(getCnfProof()),
  92         static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine())));
  93   }
  94   return *(currentPM()->d_fullProof);
  95 }
  96
  97 CoreSatProof* ProofManager::getSatProof() {
  98   Assert (currentPM()->d_satProof);
  99   return currentPM()->d_satProof;
 100 }
 101
 102 CnfProof* ProofManager::getCnfProof() {
 103   Assert (currentPM()->d_cnfProof);
 104   return currentPM()->d_cnfProof;
 105 }
 106
 107 TheoryProofEngine* ProofManager::getTheoryProofEngine() {
 108   Assert (currentPM()->d_theoryProof != NULL);
 109   return currentPM()->d_theoryProof;
 110 }
 111
 112 UFProof* ProofManager::getUfProof() {
 113   Assert (options::proof());
 114   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF);
 115   return (UFProof*)pf;
 116 }
 117
 118 BitVectorProof* ProofManager::getBitVectorProof() {
 119   Assert (options::proof());
 120   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV);
 121   return (BitVectorProof*)pf;
 122 }
 123
 124 ArrayProof* ProofManager::getArrayProof() {
 125   Assert (options::proof());
 126   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS);
 127   return (ArrayProof*)pf;
 128 }
 129
 130 ArithProof* ProofManager::getArithProof() {
 131   Assert (options::proof());
 132   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH);
 133   return (ArithProof*)pf;
 134 }
 135
 136 SkolemizationManager* ProofManager::getSkolemizationManager() {
 137   Assert (options::proof() || options::unsatCores());
 138   return &(currentPM()->d_skolemizationManager);
 139 }
 140
 141 void ProofManager::initSatProof(Minisat::Solver* solver) {
 142   Assert (currentPM()->d_satProof == NULL);
 143   Assert(currentPM()->d_format == LFSC);
 144   currentPM()->d_satProof = new LFSCCoreSatProof(solver, d_context, "");
 145 }
 146
 147 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
 148                                 context::Context* ctx) {
 149   ProofManager* pm = currentPM();
 150   Assert (pm->d_cnfProof == NULL);
 151   Assert (pm->d_format == LFSC);
 152   CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, "");
 153   pm->d_cnfProof = cnf;
 154   Assert(pm-> d_satProof != NULL);
 155   pm->d_satProof->setCnfProof(cnf);
 156
 157   // true and false have to be setup in a special way
 158   Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
 159   Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
 160
 161   pm->d_cnfProof->pushCurrentAssertion(true_node);
 162   pm->d_cnfProof->pushCurrentDefinition(true_node);
 163   pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getTrueUnit());
 164   pm->d_cnfProof->popCurrentAssertion();
 165   pm->d_cnfProof->popCurrentDefinition();
 166
 167   pm->d_cnfProof->pushCurrentAssertion(false_node);
 168   pm->d_cnfProof->pushCurrentDefinition(false_node);
 169   pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getFalseUnit());
 170   pm->d_cnfProof->popCurrentAssertion();
 171   pm->d_cnfProof->popCurrentDefinition();
 172
 173 }
 174
 175 void ProofManager::initTheoryProofEngine() {
 176   Assert (currentPM()->d_theoryProof == NULL);
 177   Assert (currentPM()->d_format == LFSC);
 178   currentPM()->d_theoryProof = new LFSCTheoryProofEngine();
 179 }
 180
 181 std::string ProofManager::getInputClauseName(ClauseId id,
 182                                              const std::string& prefix) {
 183   return append(prefix+".pb", id);
 184 }
 185
 186 std::string ProofManager::getLemmaClauseName(ClauseId id,
 187                                              const std::string& prefix) {
 188   return append(prefix+".lemc", id);
 189 }
 190
 191 std::string ProofManager::getLemmaName(ClauseId id, const std::string& prefix) {
 192   return append(prefix+"lem", id);
 193 }
 194
 195 std::string ProofManager::getLearntClauseName(ClauseId id,
 196                                               const std::string& prefix) {
 197   return append(prefix+".cl", id);
 198 }
 199 std::string ProofManager::getVarName(prop::SatVariable var,
 200                                      const std::string& prefix) {
 201   return append(prefix+".v", var);
 202 }
 203 std::string ProofManager::getAtomName(prop::SatVariable var,
 204                                       const std::string& prefix) {
 205   return append(prefix+".a", var);
 206 }
 207 std::string ProofManager::getLitName(prop::SatLiteral lit,
 208                                      const std::string& prefix) {
 209   return append(prefix+".l", lit.toInt());
 210 }
 211
 212 std::string ProofManager::getPreprocessedAssertionName(Node node,
 213                                                        const std::string& prefix) {
 214   if (currentPM()->d_assertionFilters.find(node) != currentPM()->d_assertionFilters.end()) {
 215     return currentPM()->d_assertionFilters[node];
 216   }
 217
 218   node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
 219   return append(prefix+".PA", node.getId());
 220 }
 221 std::string ProofManager::getAssertionName(Node node,
 222                                            const std::string& prefix) {
 223   return append(prefix+".A", node.getId());
 224 }
 225 std::string ProofManager::getInputFormulaName(const Expr& expr) {
 226   return currentPM()->d_inputFormulaToName[expr];
 227 }
 228
 229 std::string ProofManager::getAtomName(TNode atom,
 230                                       const std::string& prefix) {
 231   prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom);
 232   Assert(!lit.isNegated());
 233   return getAtomName(lit.getSatVariable(), prefix);
 234 }
 235
 236 std::string ProofManager::getLitName(TNode lit,
 237                                      const std::string& prefix) {
 238   std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
 239   if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) {
 240     return currentPM()->d_rewriteFilters[litName];
 241   }
 242
 243   return litName;
 244 }
 245
 246 bool ProofManager::hasLitName(TNode lit) {
 247   return currentPM()->d_cnfProof->hasLiteral(lit);
 248 }
 249
 250 std::string ProofManager::sanitize(TNode node) {
 251   Assert (node.isVar() || node.isConst());
 252
 253   std::string name = node.toString();
 254   if (node.isVar()) {
 255     std::replace(name.begin(), name.end(), ' ', '_');
 256   } else if (node.isConst()) {
 257     name.erase(std::remove(name.begin(), name.end(), '('), name.end());
 258     name.erase(std::remove(name.begin(), name.end(), ')'), name.end());
 259     name.erase(std::remove(name.begin(), name.end(), ' '), name.end());
 260     name = "const" + name;
 261   }
 262
 263   return name;
 264 }
 265
 266 void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) {
 267   Debug("cores") << "trace deps " << n << std::endl;
 268   if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
 269       (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
 270     return;
 271   }
 272   if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
 273     // originating formula was in core set
 274     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
 275     coreAssertions->insert(n.toExpr());
 276   } else {
 277     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
 278     if(d_deps.find(n) == d_deps.end()) {
 279       if (options::allowEmptyDependencies()) {
 280         Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl;
 281         return;
 282       }
 283       InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
 284     }
 285     Assert(d_deps.find(n) != d_deps.end());
 286     std::vector<Node> deps = (*d_deps.find(n)).second;
 287     for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
 288       Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
 289       if( !(*i).isNull() ){
 290         traceDeps(*i, coreAssertions);
 291       }
 292     }
 293   }
 294 }
 295
 296 void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
 297   Debug("cores") << "trace deps " << n << std::endl;
 298   if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
 299       (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
 300     return;
 301   }
 302   if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
 303     // originating formula was in core set
 304     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
 305     coreAssertions->insert(n.toExpr());
 306   } else {
 307     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
 308     if(d_deps.find(n) == d_deps.end()) {
 309       if (options::allowEmptyDependencies()) {
 310         Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl;
 311         return;
 312       }
 313       InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
 314     }
 315     Assert(d_deps.find(n) != d_deps.end());
 316     std::vector<Node> deps = (*d_deps.find(n)).second;
 317
 318     for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
 319       Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
 320       if( !(*i).isNull() ){
 321         traceDeps(*i, coreAssertions);
 322       }
 323     }
 324   }
 325 }
 326
 327 void ProofManager::traceUnsatCore() {
 328   Assert (options::unsatCores());
 329   d_satProof->refreshProof();
 330   IdToSatClause used_lemmas;
 331   IdToSatClause used_inputs;
 332   d_satProof->collectClausesUsed(used_inputs,
 333                                  used_lemmas);
 334
 335   // At this point, there should be no assertions without a clause id
 336   Assert(d_cnfProof->isAssertionStackEmpty());
 337
 338   IdToSatClause::const_iterator it = used_inputs.begin();
 339   for(; it != used_inputs.end(); ++it) {
 340     Node node = d_cnfProof->getAssertionForClause(it->first);
 341     ProofRule rule = d_cnfProof->getProofRule(node);
 342
 343     Debug("cores") << "core input assertion " << node << std::endl;
 344     Debug("cores") << "with proof rule " << rule << std::endl;
 345     if (rule == RULE_TSEITIN ||
 346         rule == RULE_GIVEN) {
 347       // trace dependences back to actual assertions
 348       // (this adds them to the unsat core)
 349       traceDeps(node, &d_outputCoreFormulas);
 350     }
 351   }
 352 }
 353
 354 bool ProofManager::unsatCoreAvailable() const {
 355   return d_satProof->derivedEmptyClause();
 356 }
 357
 358 std::vector<Expr> ProofManager::extractUnsatCore() {
 359   std::vector<Expr> result;
 360   output_core_iterator it = begin_unsat_core();
 361   output_core_iterator end = end_unsat_core();
 362   while ( it != end ) {
 363     result.push_back(*it);
 364     ++it;
 365   }
 366   return result;
 367 }
 368
 369 void ProofManager::constructSatProof() {
 370   if (!d_satProof->proofConstructed()) {
 371     d_satProof->constructProof();
 372   }
 373 }
 374
 375 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) {
 376   Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
 377   Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
 378
 379   constructSatProof();
 380
 381   IdToSatClause used_lemmas;
 382   IdToSatClause used_inputs;
 383   d_satProof->collectClausesUsed(used_inputs, used_lemmas);
 384
 385   IdToSatClause::const_iterator it;
 386   std::set<Node> seen;
 387
 388   Debug("pf::lemmasUnsatCore") << "Dumping all lemmas in unsat core" << std::endl;
 389   for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
 390     std::set<Node> lemma = satClauseToNodeSet(it->second);
 391     Debug("pf::lemmasUnsatCore") << nodeSetToString(lemma);
 392
 393     // TODO: we should be able to drop the "haveProofRecipe" check.
 394     // however, there are some rewrite issues with the arith solver, resulting
 395     // in non-registered recipes. For now we assume no one is requesting arith lemmas.
 396     LemmaProofRecipe recipe;
 397     if (!getCnfProof()->haveProofRecipe(lemma)) {
 398       Debug("pf::lemmasUnsatCore") << "\t[no recipe]" << std::endl;
 399       continue;
 400     }
 401
 402     recipe = getCnfProof()->getProofRecipe(lemma);
 403     Debug("pf::lemmasUnsatCore") << "\t[owner = " << recipe.getTheory()
 404                                  << ", original = " << recipe.getOriginalLemma() << "]" << std::endl;
 405     if (recipe.simpleLemma() && recipe.getTheory() == theory && seen.find(recipe.getOriginalLemma()) == seen.end()) {
 406       lemmas.push_back(recipe.getOriginalLemma());
 407       seen.insert(recipe.getOriginalLemma());
 408     }
 409   }
 410 }
 411
 412 std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) {
 413   std::set<Node> result;
 414   for (unsigned i = 0; i < clause->size(); ++i) {
 415     prop::SatLiteral lit = (*clause)[i];
 416     Node node = getCnfProof()->getAtom(lit.getSatVariable());
 417     Expr atom = node.toExpr();
 418     if (atom != utils::mkTrue())
 419       result.insert(lit.isNegated() ? node.notNode() : node);
 420   }
 421
 422   return result;
 423 }
 424
 425 Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
 426   Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
 427   Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
 428
 429   // If we're doing aggressive minimization, work on all lemmas, not just conjunctions.
 430   if (!options::aggressiveCoreMin() && (lemma.getKind() != kind::AND))
 431     return lemma;
 432
 433   constructSatProof();
 434
 435   NodeBuilder<> builder(kind::AND);
 436
 437   IdToSatClause used_lemmas;
 438   IdToSatClause used_inputs;
 439   d_satProof->collectClausesUsed(used_inputs, used_lemmas);
 440
 441   IdToSatClause::const_iterator it;
 442   std::set<Node>::iterator lemmaIt;
 443
 444   if (!options::aggressiveCoreMin()) {
 445     for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
 446       std::set<Node> currentLemma = satClauseToNodeSet(it->second);
 447
 448       // TODO: we should be able to drop the "haveProofRecipe" check.
 449       // however, there are some rewrite issues with the arith solver, resulting
 450       // in non-registered recipes. For now we assume no one is requesting arith lemmas.
 451       LemmaProofRecipe recipe;
 452       if (!getCnfProof()->haveProofRecipe(currentLemma))
 453         continue;
 454
 455       recipe = getCnfProof()->getProofRecipe(currentLemma);
 456       if (recipe.getOriginalLemma() == lemma) {
 457         for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
 458           builder << *lemmaIt;
 459
 460           // Check that each conjunct appears in the original lemma.
 461           bool found = false;
 462           for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
 463             if (lemma[i] == *lemmaIt)
 464               found = true;
 465           }
 466
 467           if (!found)
 468             return lemma;
 469         }
 470       }
 471     }
 472   } else {
 473     // Aggressive mode
 474     for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
 475       std::set<Node> currentLemma = satClauseToNodeSet(it->second);
 476
 477       // TODO: we should be able to drop the "haveProofRecipe" check.
 478       // however, there are some rewrite issues with the arith solver, resulting
 479       // in non-registered recipes. For now we assume no one is requesting arith lemmas.
 480       LemmaProofRecipe recipe;
 481       if (!getCnfProof()->haveProofRecipe(currentLemma))
 482         continue;
 483
 484       recipe = getCnfProof()->getProofRecipe(currentLemma);
 485       if (recipe.getOriginalLemma() == lemma) {
 486         NodeBuilder<> disjunction(kind::OR);
 487         for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
 488           disjunction << *lemmaIt;
 489         }
 490
 491         Node conjunct = (disjunction.getNumChildren() == 1) ? disjunction[0] : disjunction;
 492         builder << conjunct;
 493       }
 494     }
 495   }
 496
 497   AlwaysAssert(builder.getNumChildren() != 0);
 498
 499   if (builder.getNumChildren() == 1)
 500     return builder[0];
 501
 502   return builder;
 503 }
 504
 505 void ProofManager::addAssertion(Expr formula) {
 506   Debug("proof:pm") << "assert: " << formula << std::endl;
 507   d_inputFormulas.insert(formula);
 508   std::ostringstream name;
 509   name << "A" << d_inputFormulaToName.size();
 510   d_inputFormulaToName[formula] = name.str();
 511 }
 512
 513 void ProofManager::addCoreAssertion(Expr formula) {
 514   Debug("cores") << "assert: " << formula << std::endl;
 515   d_deps[Node::fromExpr(formula)]; // empty vector of deps
 516   d_inputCoreFormulas.insert(formula);
 517 }
 518
 519 void ProofManager::addDependence(TNode n, TNode dep) {
 520   if(dep != n) {
 521     Debug("cores") << "dep: " << n << " : " << dep << std::endl;
 522     if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) {
 523       Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
 524     }
 525     std::vector<Node> deps = d_deps[n].get();
 526     deps.push_back(dep);
 527     d_deps[n].set(deps);
 528   }
 529 }
 530
 531 void ProofManager::addUnsatCore(Expr formula) {
 532   Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
 533   d_outputCoreFormulas.insert(formula);
 534 }
 535
 536 void ProofManager::addAssertionFilter(const Node& node, const std::string& rewritten) {
 537   d_assertionFilters[node] = rewritten;
 538 }
 539
 540 void ProofManager::setLogic(const LogicInfo& logic) {
 541   d_logic = logic;
 542 }
 543
 544
 545
 546 LFSCProof::LFSCProof(SmtEngine* smtEngine,
 547                      LFSCCoreSatProof* sat,
 548                      LFSCCnfProof* cnf,
 549                      LFSCTheoryProofEngine* theory)
 550   : d_satProof(sat)
 551   , d_cnfProof(cnf)
 552   , d_theoryProof(theory)
 553   , d_smtEngine(smtEngine)
 554 {}
 555
 556 void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
 557 {
 558   Unreachable();
 559 }
 560
 561 void LFSCProof::toStream(std::ostream& out) const
 562 {
 563   Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
 564
 565   Assert(!d_satProof->proofConstructed());
 566   d_satProof->constructProof();
 567
 568   // collecting leaf clauses in resolution proof
 569   IdToSatClause used_lemmas;
 570   IdToSatClause used_inputs;
 571   d_satProof->collectClausesUsed(used_inputs,
 572                                  used_lemmas);
 573
 574   IdToSatClause::iterator it2;
 575   Debug("pf::pm") << std::endl << "Used inputs: " << std::endl;
 576   for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
 577     Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl;
 578   }
 579   Debug("pf::pm") << std::endl;
 580
 581   // Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
 582   // for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
 583   //   Debug("pf::pm") << "\t lemma = " << *(it2->second) << std::endl;
 584   // }
 585   // Debug("pf::pm") << std::endl;
 586   Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
 587   for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
 588
 589     std::vector<Expr> clause_expr;
 590     for(unsigned i = 0; i < it2->second->size(); ++i) {
 591       prop::SatLiteral lit = (*(it2->second))[i];
 592       Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
 593       if (atom.isConst()) {
 594         Assert (atom == utils::mkTrue());
 595         continue;
 596       }
 597       Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
 598       clause_expr.push_back(expr_lit);
 599     }
 600
 601     Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second) << std::endl;
 602     Debug("pf::pm") << "\t";
 603     for (unsigned i = 0; i < clause_expr.size(); ++i) {
 604       Debug("pf::pm") << clause_expr[i] << " ";
 605     }
 606     Debug("pf::pm") << std::endl;
 607   }
 608   Debug("pf::pm") << std::endl;
 609
 610   // collecting assertions that lead to the clauses being asserted
 611   NodeSet used_assertions;
 612   d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
 613
 614   NodeSet::iterator it3;
 615   Debug("pf::pm") << std::endl << "Used assertions: " << std::endl;
 616   for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
 617     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 618
 619   std::set<Node> atoms;
 620
 621   NodePairSet rewrites;
 622   // collects the atoms in the clauses
 623   d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
 624
 625   if (!rewrites.empty()) {
 626     Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
 627     NodePairSet::const_iterator rewriteIt;
 628     for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
 629       Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
 630     }
 631     Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
 632   } else {
 633     Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
 634   }
 635
 636   // The derived/unrewritten atoms may not have CNF literals required later on.
 637   // If they don't, add them.
 638   std::set<Node>::const_iterator it;
 639   for (it = atoms.begin(); it != atoms.end(); ++it) {
 640     Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
 641     if (!d_cnfProof->hasLiteral(*it)) {
 642       // For arithmetic: these literals are not normalized, causing an error in Arith.
 643       if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
 644         d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
 645       } else {
 646         d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
 647       }
 648     }
 649   }
 650
 651   d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
 652   d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
 653
 654   // collects the atoms in the assertions
 655   for (NodeSet::const_iterator it = used_assertions.begin();
 656        it != used_assertions.end(); ++it) {
 657     utils::collectAtoms(*it, atoms);
 658     // utils::collectAtoms(*it, newAtoms);
 659   }
 660
 661   std::set<Node>::iterator atomIt;
 662   Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
 663                   << std::endl << std::endl;
 664   for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
 665     Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
 666   }
 667   smt::SmtScope scope(d_smtEngine);
 668   std::ostringstream paren;
 669   out << "(check\n";
 670   paren << ")";
 671   out << " ;; Declarations\n";
 672
 673   // declare the theory atoms
 674   Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
 675   for(it = atoms.begin(); it != atoms.end(); ++it) {
 676     Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
 677     d_theoryProof->registerTerm((*it).toExpr());
 678   }
 679
 680   Debug("pf::pm") << std::endl << "Term registration done!" << std::endl << std::endl;
 681
 682   Debug("pf::pm") << std::endl << "LFSCProof::toStream: starting to print assertions" << std::endl;
 683
 684   // print out all the original assertions
 685   d_theoryProof->registerTermsFromAssertions();
 686   d_theoryProof->printSortDeclarations(out, paren);
 687   d_theoryProof->printTermDeclarations(out, paren);
 688   d_theoryProof->printAssertions(out, paren);
 689
 690   Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl;
 691
 692   out << "(: (holds cln)\n\n";
 693   paren << ")";
 694
 695   // Have the theory proofs print deferred declarations, e.g. for skolem variables.
 696   out << " ;; Printing deferred declarations \n\n";
 697   d_theoryProof->printDeferredDeclarations(out, paren);
 698
 699   out << "\n ;; Printing the global let map";
 700   d_theoryProof->finalizeBvConflicts(used_lemmas, out);
 701   ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
 702   ProofLetMap globalLetMap;
 703   if (options::lfscLetification()) {
 704     ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
 705   }
 706
 707   out << " ;; Printing aliasing declarations \n\n";
 708   d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
 709
 710   out << " ;; Rewrites for Lemmas \n";
 711   d_theoryProof->printLemmaRewrites(rewrites, out, paren);
 712
 713   // print trust that input assertions are their preprocessed form
 714   printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
 715
 716   // print mapping between theory atoms and internal SAT variables
 717   out << ";; Printing mapping from preprocessed assertions into atoms \n";
 718   d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
 719
 720   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl;
 721
 722   IdToSatClause::const_iterator cl_it = used_inputs.begin();
 723   // print CNF conversion proof for each clause
 724   for (; cl_it != used_inputs.end(); ++cl_it) {
 725     d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren);
 726   }
 727
 728   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
 729
 730   Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
 731   d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
 732   Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
 733
 734   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
 735     ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren);
 736   } else {
 737     // print actual resolution proof
 738     d_satProof->printResolutions(out, paren);
 739     d_satProof->printResolutionEmptyClause(out, paren);
 740   }
 741
 742   out << paren.str();
 743   out << "\n;;\n";
 744 }
 745
 746 void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 747                                             std::ostream& os,
 748                                             std::ostream& paren,
 749                                             ProofLetMap& globalLetMap) const
 750 {
 751   os << "\n ;; In the preprocessor we trust \n";
 752   NodeSet::const_iterator it = assertions.begin();
 753   NodeSet::const_iterator end = assertions.end();
 754
 755   Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
 756
 757   if (options::fewerPreprocessingHoles()) {
 758     // Check for assertions that did not get rewritten, and update the printing filter.
 759     checkUnrewrittenAssertion(assertions);
 760
 761     // For the remaining assertions, bind them to input assertions.
 762     for (; it != end; ++it) {
 763       // Rewrite preprocessing step if it cannot be eliminated
 764       if (!ProofManager::currentPM()->have_input_assertion((*it).toExpr())) {
 765         os << "(th_let_pf _ (trust_f (iff ";
 766
 767         Expr inputAssertion;
 768
 769         if (((*it).isConst() && *it == NodeManager::currentNM()->mkConst<bool>(true)) ||
 770             ((*it).getKind() == kind::NOT && (*it)[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
 771           inputAssertion = NodeManager::currentNM()->mkConst<bool>(true).toExpr();
 772         } else {
 773           // Figure out which input assertion led to this assertion
 774           ExprSet inputAssertions;
 775           ProofManager::currentPM()->traceDeps(*it, &inputAssertions);
 776
 777           Debug("pf::pm") << "Original assertions for " << *it << " are: " << std::endl;
 778
 779           ProofManager::assertions_iterator assertionIt;
 780           for (assertionIt = inputAssertions.begin(); assertionIt != inputAssertions.end(); ++assertionIt) {
 781             Debug("pf::pm") << "\t" << *assertionIt << std::endl;
 782           }
 783
 784           if (inputAssertions.size() == 0) {
 785             Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl;
 786             // For now just use the first assertion...
 787             inputAssertion = *(ProofManager::currentPM()->begin_assertions());
 788           } else {
 789             if (inputAssertions.size() != 1) {
 790               Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl;
 791             }
 792             inputAssertion = *inputAssertions.begin();
 793           }
 794         }
 795
 796         if (!ProofManager::currentPM()->have_input_assertion(inputAssertion)) {
 797           // The thing returned by traceDeps does not appear in the input assertions...
 798           Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl;
 799           // For now just use the first assertion...
 800           inputAssertion = *(ProofManager::currentPM()->begin_assertions());
 801         }
 802
 803         Debug("pf::pm") << "Original assertion for " << *it
 804                         << " is: "
 805                         << inputAssertion
 806                         << ", AKA "
 807                         << ProofManager::currentPM()->getInputFormulaName(inputAssertion)
 808                         << std::endl;
 809
 810         ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap);
 811         os << " ";
 812         ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
 813
 814         os << "))";
 815         os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
 816         paren << "))";
 817
 818         std::ostringstream rewritten;
 819
 820         rewritten << "(or_elim_1 _ _ ";
 821         rewritten << "(not_not_intro _ ";
 822         rewritten << ProofManager::currentPM()->getInputFormulaName(inputAssertion);
 823         rewritten << ") (iff_elim_1 _ _ ";
 824         rewritten << ProofManager::getPreprocessedAssertionName(*it, "");
 825         rewritten << "))";
 826
 827         ProofManager::currentPM()->addAssertionFilter(*it, rewritten.str());
 828       }
 829     }
 830   } else {
 831     for (; it != end; ++it) {
 832       os << "(th_let_pf _ ";
 833
 834       //TODO
 835       os << "(trust_f ";
 836       if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app ";
 837       ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
 838       if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")";
 839       os << ") ";
 840
 841       os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
 842       paren << "))";
 843     }
 844   }
 845
 846   os << "\n";
 847 }
 848
 849 void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) const
 850 {
 851   Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl;
 852
 853   NodeSet::const_iterator rewrite;
 854   for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) {
 855     Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl;
 856     if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) {
 857       Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr()));
 858       Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
 859                       << "\tAdding filter: "
 860                       << ProofManager::getPreprocessedAssertionName(*rewrite, "")
 861                       << " --> "
 862                       << ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr())
 863                       << std::endl;
 864       ProofManager::currentPM()->addAssertionFilter(*rewrite,
 865         ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr()));
 866     } else {
 867       Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite << std::endl;
 868     }
 869   }
 870 }
 871
 872 //---from Morgan---
 873
 874 bool ProofManager::hasOp(TNode n) const {
 875   return d_bops.find(n) != d_bops.end();
 876 }
 877
 878 Node ProofManager::lookupOp(TNode n) const {
 879   std::map<Node, Node>::const_iterator i = d_bops.find(n);
 880   Assert(i != d_bops.end());
 881   return (*i).second;
 882 }
 883
 884 Node ProofManager::mkOp(TNode n) {
 885   Trace("mgd-pm-mkop") << "MkOp : " << n << " " << n.getKind() << std::endl;
 886   if(n.getKind() != kind::BUILTIN) {
 887     return n;
 888   }
 889
 890   Node& op = d_ops[n];
 891   if(op.isNull()) {
 892     Assert((n.getConst<Kind>() == kind::SELECT) || (n.getConst<Kind>() == kind::STORE));
 893
 894     Debug("mgd-pm-mkop") << "making an op for " << n << "\n";
 895
 896     std::stringstream ss;
 897     ss << n;
 898     std::string s = ss.str();
 899     Debug("mgd-pm-mkop") << " : " << s << std::endl;
 900     std::vector<TypeNode> v;
 901     v.push_back(NodeManager::currentNM()->integerType());
 902     if(n.getConst<Kind>() == kind::SELECT) {
 903       v.push_back(NodeManager::currentNM()->integerType());
 904       v.push_back(NodeManager::currentNM()->integerType());
 905     } else if(n.getConst<Kind>() == kind::STORE) {
 906       v.push_back(NodeManager::currentNM()->integerType());
 907       v.push_back(NodeManager::currentNM()->integerType());
 908       v.push_back(NodeManager::currentNM()->integerType());
 909     }
 910     TypeNode type = NodeManager::currentNM()->mkFunctionType(v);
 911     Debug("mgd-pm-mkop") << "typenode is: " << type << "\n";
 912     op = NodeManager::currentNM()->mkSkolem(s, type, " ignore", NodeManager::SKOLEM_NO_NOTIFY);
 913     d_bops[op] = n;
 914   }
 915   Debug("mgd-pm-mkop") << "returning the op: " << op << "\n";
 916   return op;
 917 }
 918 //---end from Morgan---
 919
 920 bool ProofManager::wasPrinted(const Type& type) const {
 921   return d_printedTypes.find(type) != d_printedTypes.end();
 922 }
 923
 924 void ProofManager::markPrinted(const Type& type) {
 925   d_printedTypes.insert(type);
 926 }
 927
 928 void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) {
 929   d_rewriteFilters[original] = substitute;
 930 }
 931
 932 bool ProofManager::haveRewriteFilter(TNode lit) {
 933   std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit));
 934   return d_rewriteFilters.find(litName) != d_rewriteFilters.end();
 935 }
 936
 937 void ProofManager::clearRewriteFilters() {
 938   d_rewriteFilters.clear();
 939 }
 940
 941 std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
 942   switch(k) {
 943   case RULE_GIVEN:
 944     out << "RULE_GIVEN";
 945     break;
 946   case RULE_DERIVED:
 947     out << "RULE_DERIVED";
 948     break;
 949   case RULE_RECONSTRUCT:
 950     out << "RULE_RECONSTRUCT";
 951     break;
 952   case RULE_TRUST:
 953     out << "RULE_TRUST";
 954     break;
 955   case RULE_INVALID:
 956     out << "RULE_INVALID";
 957     break;
 958   case RULE_CONFLICT:
 959     out << "RULE_CONFLICT";
 960     break;
 961   case RULE_TSEITIN:
 962     out << "RULE_TSEITIN";
 963     break;
 964   case RULE_SPLIT:
 965     out << "RULE_SPLIT";
 966     break;
 967   case RULE_ARRAYS_EXT:
 968     out << "RULE_ARRAYS";
 969     break;
 970   case RULE_ARRAYS_ROW:
 971     out << "RULE_ARRAYS";
 972     break;
 973   default:
 974     out << "ProofRule Unknown! [" << unsigned(k) << "]";
 975   }
 976
 977   return out;
 978 }
 979
 980 void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){
 981   Assert (currentPM()->d_theoryProof != NULL);
 982   currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result));
 983 }
 984
 985 void ProofManager::clearRewriteLog() {
 986   Assert (currentPM()->d_theoryProof != NULL);
 987   currentPM()->d_rewriteLog.clear();
 988 }
 989
 990 std::vector<RewriteLogEntry> ProofManager::getRewriteLog() {
 991   return currentPM()->d_rewriteLog;
 992 }
 993
 994 void ProofManager::dumpRewriteLog() const {
 995   Debug("pf::rr") << "Dumpign rewrite log:" << std::endl;
 996
 997   for (unsigned i = 0; i < d_rewriteLog.size(); ++i) {
 998     Debug("pf::rr") << "\tRule " << d_rewriteLog[i].getRuleId()
 999                     << ": "
1000                     << d_rewriteLog[i].getOriginal()
1001                     << " --> "
1002                     << d_rewriteLog[i].getResult() << std::endl;
1003   }
1004 }
1005
1006 void bind(Expr term, ProofLetMap& map, Bindings& letOrder) {
1007   ProofLetMap::iterator it = map.find(term);
1008   if (it != map.end())
1009     return;
1010
1011   for (unsigned i = 0; i < term.getNumChildren(); ++i)
1012     bind(term[i], map, letOrder);
1013
1014   // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)).
1015   // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too.
1016   Kind k = term.getKind();
1017   if (((k == kind::OR) || (k == kind::AND)) && term.getNumChildren() > 2) {
1018     Node currentExpression = term[term.getNumChildren() - 1];
1019     for (int i = term.getNumChildren() - 2; i >= 0; --i) {
1020       NodeBuilder<> builder(k);
1021       builder << term[i];
1022       builder << currentExpression.toExpr();
1023       currentExpression = builder;
1024       bind(currentExpression.toExpr(), map, letOrder);
1025     }
1026   } else {
1027     unsigned newId = ProofLetCount::newId();
1028     ProofLetCount letCount(newId);
1029     map[term] = letCount;
1030     letOrder.push_back(LetOrderElement(term, newId));
1031   }
1032 }
1033
1034 void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
1035                                      ProofLetMap& letMap,
1036                                      std::ostream& out,
1037                                      std::ostringstream& paren) {
1038   Bindings letOrder;
1039   std::set<Node>::const_iterator atom;
1040   for (atom = atoms.begin(); atom != atoms.end(); ++atom) {
1041     bind(atom->toExpr(), letMap, letOrder);
1042   }
1043
1044   // TODO: give each theory a chance to add atoms. For now, just query BV directly...
1045   const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
1046   for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) {
1047     bind(atom->toExpr(), letMap, letOrder);
1048   }
1049
1050   for (unsigned i = 0; i < letOrder.size(); ++i) {
1051     Expr currentExpr = letOrder[i].expr;
1052     unsigned letId = letOrder[i].id;
1053     ProofLetMap::iterator it = letMap.find(currentExpr);
1054     Assert(it != letMap.end());
1055     out << "\n(@ let" << letId << " ";
1056     d_theoryProof->printBoundTerm(currentExpr, out, letMap);
1057     paren << ")";
1058     it->second.increment();
1059   }
1060
1061   out << std::endl << std::endl;
1062 }
1063
1064 void ProofManager::ensureLiteral(Node node) {
1065   d_cnfProof->ensureLiteral(node);
1066 }
1067
1068 } /* CVC4  namespace */