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/lfsc_proof_printer.h"
  28 #include "proof/proof_utils.h"
  29 #include "proof/sat_proof_implementation.h"
  30 #include "proof/theory_proof.h"
  31 #include "smt/smt_engine.h"
  32 #include "smt/smt_engine_scope.h"
  33 #include "smt_util/node_visitor.h"
  34 #include "theory/arrays/theory_arrays.h"
  35 #include "theory/output_channel.h"
  36 #include "theory/term_registration_visitor.h"
  37 #include "theory/uf/equality_engine.h"
  38 #include "theory/uf/theory_uf.h"
  39 #include "theory/valuation.h"
  40 #include "util/hash.h"
  41 #include "util/proof.h"
  42
  43 namespace CVC4 {
  44
  45 std::string nodeSetToString(const std::set<Node>& nodes) {
  46   std::ostringstream os;
  47   std::set<Node>::const_iterator it;
  48   for (it = nodes.begin(); it != nodes.end(); ++it) {
  49     os << *it << " ";
  50   }
  51   return os.str();
  52 }
  53
  54 std::string append(const std::string& str, uint64_t num) {
  55   std::ostringstream os;
  56   os << str << num;
  57   return os.str();
  58 }
  59
  60 ProofManager::ProofManager(context::Context* context, ProofFormat format)
  61     : d_context(context),
  62       d_satProof(NULL),
  63       d_cnfProof(NULL),
  64       d_theoryProof(NULL),
  65       d_inputFormulas(),
  66       d_inputCoreFormulas(context),
  67       d_outputCoreFormulas(context),
  68       d_nextId(0),
  69       d_fullProof(),
  70       d_format(format),
  71       d_deps(context)
  72 {
  73 }
  74
  75 ProofManager::~ProofManager() {
  76   if (d_satProof) delete d_satProof;
  77   if (d_cnfProof) delete d_cnfProof;
  78   if (d_theoryProof) delete d_theoryProof;
  79 }
  80
  81 ProofManager* ProofManager::currentPM() {
  82   return smt::currentProofManager();
  83 }
  84 const Proof& ProofManager::getProof(SmtEngine* smt)
  85 {
  86   if (!currentPM()->d_fullProof)
  87   {
  88     Assert(currentPM()->d_format == LFSC);
  89     currentPM()->d_fullProof.reset(new LFSCProof(
  90         smt,
  91         static_cast<CoreSatProof*>(getSatProof()),
  92         static_cast<LFSCCnfProof*>(getCnfProof()),
  93         static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine())));
  94   }
  95   return *(currentPM()->d_fullProof);
  96 }
  97
  98 CoreSatProof* ProofManager::getSatProof() {
  99   Assert (currentPM()->d_satProof);
 100   return currentPM()->d_satProof;
 101 }
 102
 103 CnfProof* ProofManager::getCnfProof() {
 104   Assert (currentPM()->d_cnfProof);
 105   return currentPM()->d_cnfProof;
 106 }
 107
 108 TheoryProofEngine* ProofManager::getTheoryProofEngine() {
 109   Assert (currentPM()->d_theoryProof != NULL);
 110   return currentPM()->d_theoryProof;
 111 }
 112
 113 UFProof* ProofManager::getUfProof() {
 114   Assert (options::proof());
 115   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF);
 116   return (UFProof*)pf;
 117 }
 118
 119 BitVectorProof* ProofManager::getBitVectorProof() {
 120   Assert (options::proof());
 121   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV);
 122   return (BitVectorProof*)pf;
 123 }
 124
 125 ArrayProof* ProofManager::getArrayProof() {
 126   Assert (options::proof());
 127   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS);
 128   return (ArrayProof*)pf;
 129 }
 130
 131 ArithProof* ProofManager::getArithProof() {
 132   Assert (options::proof());
 133   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH);
 134   return (ArithProof*)pf;
 135 }
 136
 137 SkolemizationManager* ProofManager::getSkolemizationManager() {
 138   Assert (options::proof() || options::unsatCores());
 139   return &(currentPM()->d_skolemizationManager);
 140 }
 141
 142 void ProofManager::initSatProof(Minisat::Solver* solver) {
 143   Assert (currentPM()->d_satProof == NULL);
 144   Assert(currentPM()->d_format == LFSC);
 145   currentPM()->d_satProof = new CoreSatProof(solver, d_context, "");
 146 }
 147
 148 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
 149                                 context::Context* ctx) {
 150   ProofManager* pm = currentPM();
 151   Assert(pm->d_satProof != NULL);
 152   Assert (pm->d_cnfProof == NULL);
 153   Assert (pm->d_format == LFSC);
 154   CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, "");
 155   pm->d_cnfProof = 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 LFSCProof::LFSCProof(SmtEngine* smtEngine,
 545                      CoreSatProof* sat,
 546                      LFSCCnfProof* cnf,
 547                      LFSCTheoryProofEngine* theory)
 548     : d_satProof(sat),
 549       d_cnfProof(cnf),
 550       d_theoryProof(theory),
 551       d_smtEngine(smtEngine)
 552 {}
 553
 554 void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
 555 {
 556   Unreachable();
 557 }
 558
 559 void LFSCProof::toStream(std::ostream& out) const
 560 {
 561   Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
 562
 563   Assert(!d_satProof->proofConstructed());
 564   d_satProof->constructProof();
 565
 566   // collecting leaf clauses in resolution proof
 567   IdToSatClause used_lemmas;
 568   IdToSatClause used_inputs;
 569   d_satProof->collectClausesUsed(used_inputs,
 570                                  used_lemmas);
 571
 572   IdToSatClause::iterator it2;
 573   Debug("pf::pm") << std::endl << "Used inputs: " << std::endl;
 574   for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
 575     Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl;
 576   }
 577   Debug("pf::pm") << std::endl;
 578
 579   // Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
 580   // for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
 581   //   Debug("pf::pm") << "\t lemma = " << *(it2->second) << std::endl;
 582   // }
 583   // Debug("pf::pm") << std::endl;
 584   Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
 585   for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
 586
 587     std::vector<Expr> clause_expr;
 588     for(unsigned i = 0; i < it2->second->size(); ++i) {
 589       prop::SatLiteral lit = (*(it2->second))[i];
 590       Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
 591       if (atom.isConst()) {
 592         Assert (atom == utils::mkTrue());
 593         continue;
 594       }
 595       Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
 596       clause_expr.push_back(expr_lit);
 597     }
 598
 599     Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second) << std::endl;
 600     Debug("pf::pm") << "\t";
 601     for (unsigned i = 0; i < clause_expr.size(); ++i) {
 602       Debug("pf::pm") << clause_expr[i] << " ";
 603     }
 604     Debug("pf::pm") << std::endl;
 605   }
 606   Debug("pf::pm") << std::endl;
 607
 608   // collecting assertions that lead to the clauses being asserted
 609   NodeSet used_assertions;
 610   d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
 611
 612   NodeSet::iterator it3;
 613   Debug("pf::pm") << std::endl << "Used assertions: " << std::endl;
 614   for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
 615     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 616
 617   std::set<Node> atoms;
 618
 619   NodePairSet rewrites;
 620   // collects the atoms in the clauses
 621   d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
 622
 623   if (!rewrites.empty()) {
 624     Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
 625     NodePairSet::const_iterator rewriteIt;
 626     for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
 627       Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
 628     }
 629     Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
 630   } else {
 631     Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
 632   }
 633
 634   // The derived/unrewritten atoms may not have CNF literals required later on.
 635   // If they don't, add them.
 636   std::set<Node>::const_iterator it;
 637   for (it = atoms.begin(); it != atoms.end(); ++it) {
 638     Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
 639     if (!d_cnfProof->hasLiteral(*it)) {
 640       // For arithmetic: these literals are not normalized, causing an error in Arith.
 641       if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
 642         d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
 643       } else {
 644         d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
 645       }
 646     }
 647   }
 648
 649   d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
 650   d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
 651
 652   // collects the atoms in the assertions
 653   for (NodeSet::const_iterator it = used_assertions.begin();
 654        it != used_assertions.end(); ++it) {
 655     utils::collectAtoms(*it, atoms);
 656     // utils::collectAtoms(*it, newAtoms);
 657   }
 658
 659   std::set<Node>::iterator atomIt;
 660   Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
 661                   << std::endl << std::endl;
 662   for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
 663     Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
 664   }
 665   smt::SmtScope scope(d_smtEngine);
 666   std::ostringstream paren;
 667   out << "(check\n";
 668   paren << ")";
 669   out << " ;; Declarations\n";
 670
 671   // declare the theory atoms
 672   Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
 673   for(it = atoms.begin(); it != atoms.end(); ++it) {
 674     Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
 675     d_theoryProof->registerTerm((*it).toExpr());
 676   }
 677
 678   Debug("pf::pm") << std::endl << "Term registration done!" << std::endl << std::endl;
 679
 680   Debug("pf::pm") << std::endl << "LFSCProof::toStream: starting to print assertions" << std::endl;
 681
 682   // print out all the original assertions
 683   d_theoryProof->registerTermsFromAssertions();
 684   d_theoryProof->printSortDeclarations(out, paren);
 685   d_theoryProof->printTermDeclarations(out, paren);
 686   d_theoryProof->printAssertions(out, paren);
 687
 688   Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl;
 689
 690   out << "(: (holds cln)\n\n";
 691   paren << ")";
 692
 693   // Have the theory proofs print deferred declarations, e.g. for skolem variables.
 694   out << " ;; Printing deferred declarations \n\n";
 695   d_theoryProof->printDeferredDeclarations(out, paren);
 696
 697   out << "\n ;; Printing the global let map";
 698   d_theoryProof->finalizeBvConflicts(used_lemmas, out);
 699   ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
 700   ProofLetMap globalLetMap;
 701   if (options::lfscLetification()) {
 702     ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
 703   }
 704
 705   out << " ;; Printing aliasing declarations \n\n";
 706   d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
 707
 708   out << " ;; Rewrites for Lemmas \n";
 709   d_theoryProof->printLemmaRewrites(rewrites, out, paren);
 710
 711   // print trust that input assertions are their preprocessed form
 712   printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
 713
 714   // print mapping between theory atoms and internal SAT variables
 715   out << ";; Printing mapping from preprocessed assertions into atoms \n";
 716   d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
 717
 718   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl;
 719
 720   IdToSatClause::const_iterator cl_it = used_inputs.begin();
 721   // print CNF conversion proof for each clause
 722   for (; cl_it != used_inputs.end(); ++cl_it) {
 723     d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren);
 724   }
 725
 726   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
 727
 728   Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
 729   d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
 730   Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
 731
 732   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
 733     proof::LFSCProofPrinter::printResolutionEmptyClause(
 734         ProofManager::getBitVectorProof()->getSatProof(), out, paren);
 735   } else {
 736     // print actual resolution proof
 737     proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
 738     proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof, out, paren);
 739   }
 740
 741   out << paren.str();
 742   out << "\n;;\n";
 743 }
 744
 745 void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 746                                             std::ostream& os,
 747                                             std::ostream& paren,
 748                                             ProofLetMap& globalLetMap) const
 749 {
 750   os << "\n ;; In the preprocessor we trust \n";
 751   NodeSet::const_iterator it = assertions.begin();
 752   NodeSet::const_iterator end = assertions.end();
 753
 754   Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
 755
 756   if (options::fewerPreprocessingHoles()) {
 757     // Check for assertions that did not get rewritten, and update the printing filter.
 758     checkUnrewrittenAssertion(assertions);
 759
 760     // For the remaining assertions, bind them to input assertions.
 761     for (; it != end; ++it) {
 762       // Rewrite preprocessing step if it cannot be eliminated
 763       if (!ProofManager::currentPM()->have_input_assertion((*it).toExpr())) {
 764         os << "(th_let_pf _ (trust_f (iff ";
 765
 766         Expr inputAssertion;
 767
 768         if (((*it).isConst() && *it == NodeManager::currentNM()->mkConst<bool>(true)) ||
 769             ((*it).getKind() == kind::NOT && (*it)[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
 770           inputAssertion = NodeManager::currentNM()->mkConst<bool>(true).toExpr();
 771         } else {
 772           // Figure out which input assertion led to this assertion
 773           ExprSet inputAssertions;
 774           ProofManager::currentPM()->traceDeps(*it, &inputAssertions);
 775
 776           Debug("pf::pm") << "Original assertions for " << *it << " are: " << std::endl;
 777
 778           ProofManager::assertions_iterator assertionIt;
 779           for (assertionIt = inputAssertions.begin(); assertionIt != inputAssertions.end(); ++assertionIt) {
 780             Debug("pf::pm") << "\t" << *assertionIt << std::endl;
 781           }
 782
 783           if (inputAssertions.size() == 0) {
 784             Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl;
 785             // For now just use the first assertion...
 786             inputAssertion = *(ProofManager::currentPM()->begin_assertions());
 787           } else {
 788             if (inputAssertions.size() != 1) {
 789               Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl;
 790             }
 791             inputAssertion = *inputAssertions.begin();
 792           }
 793         }
 794
 795         if (!ProofManager::currentPM()->have_input_assertion(inputAssertion)) {
 796           // The thing returned by traceDeps does not appear in the input assertions...
 797           Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl;
 798           // For now just use the first assertion...
 799           inputAssertion = *(ProofManager::currentPM()->begin_assertions());
 800         }
 801
 802         Debug("pf::pm") << "Original assertion for " << *it
 803                         << " is: "
 804                         << inputAssertion
 805                         << ", AKA "
 806                         << ProofManager::currentPM()->getInputFormulaName(inputAssertion)
 807                         << std::endl;
 808
 809         ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap);
 810         os << " ";
 811         ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap);
 812         os << "))";
 813         os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
 814         paren << "))";
 815
 816         std::ostringstream rewritten;
 817
 818         rewritten << "(or_elim_1 _ _ ";
 819         rewritten << "(not_not_intro _ ";
 820         rewritten << ProofManager::currentPM()->getInputFormulaName(inputAssertion);
 821         rewritten << ") (iff_elim_1 _ _ ";
 822         rewritten << ProofManager::getPreprocessedAssertionName(*it, "");
 823         rewritten << "))";
 824
 825         ProofManager::currentPM()->addAssertionFilter(*it, rewritten.str());
 826       }
 827     }
 828   } else {
 829     for (; it != end; ++it) {
 830       os << "(th_let_pf _ ";
 831
 832       //TODO
 833       os << "(trust_f ";
 834       ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap);
 835       os << ") ";
 836
 837       os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
 838       paren << "))";
 839     }
 840   }
 841
 842   os << "\n";
 843 }
 844
 845 void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) const
 846 {
 847   Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl;
 848
 849   NodeSet::const_iterator rewrite;
 850   for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) {
 851     Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl;
 852     if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) {
 853       Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr()));
 854       Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
 855                       << "\tAdding filter: "
 856                       << ProofManager::getPreprocessedAssertionName(*rewrite, "")
 857                       << " --> "
 858                       << ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr())
 859                       << std::endl;
 860       ProofManager::currentPM()->addAssertionFilter(*rewrite,
 861         ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr()));
 862     } else {
 863       Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite << std::endl;
 864     }
 865   }
 866 }
 867
 868 //---from Morgan---
 869
 870 bool ProofManager::hasOp(TNode n) const {
 871   return d_bops.find(n) != d_bops.end();
 872 }
 873
 874 Node ProofManager::lookupOp(TNode n) const {
 875   std::map<Node, Node>::const_iterator i = d_bops.find(n);
 876   Assert(i != d_bops.end());
 877   return (*i).second;
 878 }
 879
 880 Node ProofManager::mkOp(TNode n) {
 881   Trace("mgd-pm-mkop") << "MkOp : " << n << " " << n.getKind() << std::endl;
 882   if(n.getKind() != kind::BUILTIN) {
 883     return n;
 884   }
 885
 886   Node& op = d_ops[n];
 887   if(op.isNull()) {
 888     Assert((n.getConst<Kind>() == kind::SELECT) || (n.getConst<Kind>() == kind::STORE));
 889
 890     Debug("mgd-pm-mkop") << "making an op for " << n << "\n";
 891
 892     std::stringstream ss;
 893     ss << n;
 894     std::string s = ss.str();
 895     Debug("mgd-pm-mkop") << " : " << s << std::endl;
 896     std::vector<TypeNode> v;
 897     v.push_back(NodeManager::currentNM()->integerType());
 898     if(n.getConst<Kind>() == kind::SELECT) {
 899       v.push_back(NodeManager::currentNM()->integerType());
 900       v.push_back(NodeManager::currentNM()->integerType());
 901     } else if(n.getConst<Kind>() == kind::STORE) {
 902       v.push_back(NodeManager::currentNM()->integerType());
 903       v.push_back(NodeManager::currentNM()->integerType());
 904       v.push_back(NodeManager::currentNM()->integerType());
 905     }
 906     TypeNode type = NodeManager::currentNM()->mkFunctionType(v);
 907     Debug("mgd-pm-mkop") << "typenode is: " << type << "\n";
 908     op = NodeManager::currentNM()->mkSkolem(s, type, " ignore", NodeManager::SKOLEM_NO_NOTIFY);
 909     d_bops[op] = n;
 910   }
 911   Debug("mgd-pm-mkop") << "returning the op: " << op << "\n";
 912   return op;
 913 }
 914 //---end from Morgan---
 915
 916 bool ProofManager::wasPrinted(const Type& type) const {
 917   return d_printedTypes.find(type) != d_printedTypes.end();
 918 }
 919
 920 void ProofManager::markPrinted(const Type& type) {
 921   d_printedTypes.insert(type);
 922 }
 923
 924 void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) {
 925   d_rewriteFilters[original] = substitute;
 926 }
 927
 928 bool ProofManager::haveRewriteFilter(TNode lit) {
 929   std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit));
 930   return d_rewriteFilters.find(litName) != d_rewriteFilters.end();
 931 }
 932
 933 void ProofManager::clearRewriteFilters() {
 934   d_rewriteFilters.clear();
 935 }
 936
 937 std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
 938   switch(k) {
 939   case RULE_GIVEN:
 940     out << "RULE_GIVEN";
 941     break;
 942   case RULE_DERIVED:
 943     out << "RULE_DERIVED";
 944     break;
 945   case RULE_RECONSTRUCT:
 946     out << "RULE_RECONSTRUCT";
 947     break;
 948   case RULE_TRUST:
 949     out << "RULE_TRUST";
 950     break;
 951   case RULE_INVALID:
 952     out << "RULE_INVALID";
 953     break;
 954   case RULE_CONFLICT:
 955     out << "RULE_CONFLICT";
 956     break;
 957   case RULE_TSEITIN:
 958     out << "RULE_TSEITIN";
 959     break;
 960   case RULE_SPLIT:
 961     out << "RULE_SPLIT";
 962     break;
 963   case RULE_ARRAYS_EXT:
 964     out << "RULE_ARRAYS";
 965     break;
 966   case RULE_ARRAYS_ROW:
 967     out << "RULE_ARRAYS";
 968     break;
 969   default:
 970     out << "ProofRule Unknown! [" << unsigned(k) << "]";
 971   }
 972
 973   return out;
 974 }
 975
 976 void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){
 977   Assert (currentPM()->d_theoryProof != NULL);
 978   currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result));
 979 }
 980
 981 void ProofManager::clearRewriteLog() {
 982   Assert (currentPM()->d_theoryProof != NULL);
 983   currentPM()->d_rewriteLog.clear();
 984 }
 985
 986 std::vector<RewriteLogEntry> ProofManager::getRewriteLog() {
 987   return currentPM()->d_rewriteLog;
 988 }
 989
 990 void ProofManager::dumpRewriteLog() const {
 991   Debug("pf::rr") << "Dumpign rewrite log:" << std::endl;
 992
 993   for (unsigned i = 0; i < d_rewriteLog.size(); ++i) {
 994     Debug("pf::rr") << "\tRule " << d_rewriteLog[i].getRuleId()
 995                     << ": "
 996                     << d_rewriteLog[i].getOriginal()
 997                     << " --> "
 998                     << d_rewriteLog[i].getResult() << std::endl;
 999   }
1000 }
1001
1002 void bind(Expr term, ProofLetMap& map, Bindings& letOrder) {
1003   ProofLetMap::iterator it = map.find(term);
1004   if (it != map.end())
1005     return;
1006
1007   for (unsigned i = 0; i < term.getNumChildren(); ++i)
1008     bind(term[i], map, letOrder);
1009
1010   // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)).
1011   // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too.
1012   Kind k = term.getKind();
1013   if (((k == kind::OR) || (k == kind::AND)) && term.getNumChildren() > 2) {
1014     Node currentExpression = term[term.getNumChildren() - 1];
1015     for (int i = term.getNumChildren() - 2; i >= 0; --i) {
1016       NodeBuilder<> builder(k);
1017       builder << term[i];
1018       builder << currentExpression.toExpr();
1019       currentExpression = builder;
1020       bind(currentExpression.toExpr(), map, letOrder);
1021     }
1022   } else {
1023     unsigned newId = ProofLetCount::newId();
1024     ProofLetCount letCount(newId);
1025     map[term] = letCount;
1026     letOrder.push_back(LetOrderElement(term, newId));
1027   }
1028 }
1029
1030 void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
1031                                      ProofLetMap& letMap,
1032                                      std::ostream& out,
1033                                      std::ostringstream& paren) {
1034   Bindings letOrder;
1035   std::set<Node>::const_iterator atom;
1036   for (atom = atoms.begin(); atom != atoms.end(); ++atom) {
1037     bind(atom->toExpr(), letMap, letOrder);
1038   }
1039
1040   // TODO: give each theory a chance to add atoms. For now, just query BV directly...
1041   const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
1042   for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) {
1043     bind(atom->toExpr(), letMap, letOrder);
1044   }
1045
1046   for (unsigned i = 0; i < letOrder.size(); ++i) {
1047     Expr currentExpr = letOrder[i].expr;
1048     unsigned letId = letOrder[i].id;
1049     ProofLetMap::iterator it = letMap.find(currentExpr);
1050     Assert(it != letMap.end());
1051     out << "\n(@ let" << letId << " ";
1052     d_theoryProof->printBoundTerm(currentExpr, out, letMap);
1053     paren << ")";
1054     it->second.increment();
1055   }
1056
1057   out << std::endl << std::endl;
1058 }
1059
1060 void ProofManager::ensureLiteral(Node node) {
1061   d_cnfProof->ensureLiteral(node);
1062 }
1063 void ProofManager::printTrustedTerm(Node term,
1064                                     std::ostream& os,
1065                                     ProofLetMap& globalLetMap)
1066 {
1067   TheoryProofEngine* tpe = ProofManager::currentPM()->getTheoryProofEngine();
1068   if (tpe->printsAsBool(term)) os << "(p_app ";
1069   tpe->printTheoryTerm(term.toExpr(), os, globalLetMap);
1070   if (tpe->printsAsBool(term)) os << ")";
1071 }
1072 } /* CVC4  namespace */