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