src/proof/proof_manager.cpp

   1 /*********************                                                        */
   2 /*! \file proof_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Morgan Deters, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 "expr/node_visitor.h"
  23 #include "options/bv_options.h"
  24 #include "options/smt_options.h"
  25 #include "proof/clause_id.h"
  26 #include "proof/cnf_proof.h"
  27 #include "proof/sat_proof_implementation.h"
  28 #include "smt/smt_engine.h"
  29 #include "smt/smt_engine_scope.h"
  30 #include "smt/smt_statistics_registry.h"
  31 #include "theory/arrays/theory_arrays.h"
  32 #include "theory/output_channel.h"
  33 #include "theory/term_registration_visitor.h"
  34 #include "theory/uf/equality_engine.h"
  35 #include "theory/uf/theory_uf.h"
  36 #include "theory/valuation.h"
  37 #include "util/hash.h"
  38
  39 namespace CVC4 {
  40
  41 ProofManager::ProofManager(context::Context* context)
  42     : d_context(context),
  43       d_satProof(nullptr),
  44       d_cnfProof(nullptr),
  45       d_inputCoreFormulas(context),
  46       d_outputCoreFormulas(context),
  47       d_nextId(0),
  48       d_deps(context)
  49 {
  50 }
  51
  52 ProofManager::~ProofManager() {}
  53
  54 ProofManager* ProofManager::currentPM() {
  55   return smt::currentProofManager();
  56 }
  57
  58 CoreSatProof* ProofManager::getSatProof()
  59 {
  60   Assert(currentPM()->d_satProof);
  61   return currentPM()->d_satProof.get();
  62 }
  63
  64 CnfProof* ProofManager::getCnfProof()
  65 {
  66   Assert(currentPM()->d_cnfProof);
  67   return currentPM()->d_cnfProof.get();
  68 }
  69
  70 void ProofManager::initSatProof(Minisat::Solver* solver)
  71 {
  72   // Destroy old instance before initializing new one to avoid issues with
  73   // registering stats
  74   d_satProof.reset();
  75   d_satProof.reset(new CoreSatProof(solver, d_context, ""));
  76 }
  77
  78 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
  79                                 context::Context* ctx)
  80 {
  81   Assert(d_satProof != nullptr);
  82
  83   d_cnfProof.reset(new CnfProof(cnfStream, ctx, ""));
  84
  85   // true and false have to be setup in a special way
  86   Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
  87   Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
  88
  89   d_cnfProof->pushCurrentAssertion(true_node);
  90   d_cnfProof->registerConvertedClause(d_satProof->getTrueUnit());
  91   d_cnfProof->popCurrentAssertion();
  92
  93   d_cnfProof->pushCurrentAssertion(false_node);
  94   d_cnfProof->registerConvertedClause(d_satProof->getFalseUnit());
  95   d_cnfProof->popCurrentAssertion();
  96 }
  97
  98
  99 void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
 100   Debug("cores") << "trace deps " << n << std::endl;
 101   if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
 102       (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
 103     return;
 104   }
 105   if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
 106     // originating formula was in core set
 107     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
 108     coreAssertions->insert(n.toExpr());
 109   } else {
 110     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
 111     if(d_deps.find(n) == d_deps.end()) {
 112       InternalError()
 113           << "Cannot trace dependence information back to input assertion:\n`"
 114           << n << "'";
 115     }
 116     Assert(d_deps.find(n) != d_deps.end());
 117     std::vector<Node> deps = (*d_deps.find(n)).second;
 118
 119     for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
 120       Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
 121       if( !(*i).isNull() ){
 122         traceDeps(*i, coreAssertions);
 123       }
 124     }
 125   }
 126 }
 127
 128 void ProofManager::traceUnsatCore() {
 129   Assert(options::unsatCores());
 130   d_satProof->refreshProof();
 131   IdToSatClause used_lemmas;
 132   IdToSatClause used_inputs;
 133   d_satProof->collectClausesUsed(used_inputs,
 134                                  used_lemmas);
 135
 136   // At this point, there should be no assertions without a clause id
 137   Assert(d_cnfProof->isAssertionStackEmpty());
 138
 139   IdToSatClause::const_iterator it = used_inputs.begin();
 140   for(; it != used_inputs.end(); ++it) {
 141     Node node = d_cnfProof->getAssertionForClause(it->first);
 142
 143     Debug("cores") << "core input assertion " << node << "\n";
 144     // trace dependences back to actual assertions
 145     // (this adds them to the unsat core)
 146     traceDeps(node, &d_outputCoreFormulas);
 147   }
 148 }
 149
 150 bool ProofManager::unsatCoreAvailable() const {
 151   return d_satProof->derivedEmptyClause();
 152 }
 153
 154 std::vector<Expr> ProofManager::extractUnsatCore() {
 155   std::vector<Expr> result;
 156   output_core_iterator it = begin_unsat_core();
 157   output_core_iterator end = end_unsat_core();
 158   while ( it != end ) {
 159     result.push_back(*it);
 160     ++it;
 161   }
 162   return result;
 163 }
 164
 165 void ProofManager::constructSatProof()
 166 {
 167   if (!d_satProof->proofConstructed())
 168   {
 169     d_satProof->constructProof();
 170   }
 171 }
 172
 173 void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
 174 {
 175   Assert(options::unsatCores())
 176       << "Cannot compute unsat core when proofs are off";
 177   Assert(unsatCoreAvailable())
 178       << "Cannot get unsat core at this time. Mabye the input is SAT?";
 179   constructSatProof();
 180   IdToSatClause used_lemmas;
 181   IdToSatClause used_inputs;
 182   d_satProof->collectClausesUsed(used_inputs, used_lemmas);
 183   Debug("pf::lemmasUnsatCore") << "Retrieving all lemmas in unsat core\n";
 184   IdToSatClause::const_iterator it;
 185   for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it)
 186   {
 187     Node lemma = d_cnfProof->getAssertionForClause(it->first);
 188     Debug("pf::lemmasUnsatCore") << "Retrieved lemma " << lemma << "\n";
 189     lemmas.push_back(lemma);
 190   }
 191 }
 192
 193 void ProofManager::addCoreAssertion(Expr formula) {
 194   Debug("cores") << "assert: " << formula << std::endl;
 195   d_deps[Node::fromExpr(formula)]; // empty vector of deps
 196   d_inputCoreFormulas.insert(formula);
 197 }
 198
 199 void ProofManager::addDependence(TNode n, TNode dep) {
 200   if(dep != n) {
 201     Debug("cores") << "dep: " << n << " : " << dep << std::endl;
 202     if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) {
 203       Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
 204     }
 205     std::vector<Node> deps = d_deps[n].get();
 206     deps.push_back(dep);
 207     d_deps[n].set(deps);
 208   }
 209 }
 210
 211 void ProofManager::addUnsatCore(Expr formula) {
 212   Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
 213   d_outputCoreFormulas.insert(formula);
 214 }
 215
 216 } /* CVC4  namespace */