src/smt/proof_manager.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Haniel Barbosa, Diego Della Rocca de Camargos
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * The proof manager of the SMT engine.
  14  */
  15
  16 #include "smt/proof_manager.h"
  17
  18 #include "options/base_options.h"
  19 #include "options/main_options.h"
  20 #include "options/proof_options.h"
  21 #include "options/smt_options.h"
  22 #include "proof/dot/dot_printer.h"
  23 #include "proof/proof_checker.h"
  24 #include "proof/proof_node_algorithm.h"
  25 #include "proof/proof_node_manager.h"
  26 #include "smt/assertions.h"
  27 #include "smt/env.h"
  28 #include "smt/preprocess_proof_generator.h"
  29 #include "smt/proof_post_processor.h"
  30
  31 namespace cvc5 {
  32 namespace smt {
  33
  34 PfManager::PfManager(Env& env, SmtEngine* smte)
  35     : d_env(env),
  36       d_pchecker(new ProofChecker(options::proofPedantic())),
  37       d_pnm(new ProofNodeManager(d_pchecker.get())),
  38       d_pppg(new PreprocessProofGenerator(
  39           d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
  40       d_pfpp(new ProofPostproccess(
  41           d_pnm.get(),
  42           smte,
  43           d_pppg.get(),
  44           // by default the post-processor will update all assumptions, which
  45           // can lead to SCOPE subproofs of the form
  46           //   A
  47           //  ...
  48           //   B1    B2
  49           //  ...   ...
  50           // ------------
  51           //      C
  52           // ------------- SCOPE [B1, B2]
  53           // B1 ^ B2 => C
  54           //
  55           // where A is an available assumption from outside the scope (note
  56           // that B1 was an assumption of this SCOPE subproof but since it could
  57           // be inferred from A, it was updated). This shape is problematic for
  58           // the veriT reconstruction, so we disable the update of scoped
  59           // assumptions (which would disable the update of B1 in this case).
  60           options::proofFormatMode() != options::ProofFormatMode::VERIT)),
  61       d_finalProof(nullptr)
  62 {
  63   // add rules to eliminate here
  64   if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
  65   {
  66     d_pfpp->setEliminateRule(PfRule::MACRO_SR_EQ_INTRO);
  67     d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
  68     d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM);
  69     d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM);
  70     d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST);
  71     d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION);
  72     d_pfpp->setEliminateRule(PfRule::MACRO_ARITH_SCALE_SUM_UB);
  73     if (options::proofGranularityMode()
  74         != options::ProofGranularityMode::REWRITE)
  75     {
  76       d_pfpp->setEliminateRule(PfRule::SUBS);
  77       d_pfpp->setEliminateRule(PfRule::REWRITE);
  78       if (options::proofGranularityMode()
  79           != options::ProofGranularityMode::THEORY_REWRITE)
  80       {
  81         // this eliminates theory rewriting steps with finer-grained DSL rules
  82         d_pfpp->setEliminateRule(PfRule::THEORY_REWRITE);
  83       }
  84     }
  85     d_pfpp->setEliminateRule(PfRule::BV_BITBLAST);
  86   }
  87   d_false = NodeManager::currentNM()->mkConst(false);
  88 }
  89
  90 PfManager::~PfManager() {}
  91
  92 void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
  93 {
  94   // Note this assumes that setFinalProof is only called once per unsat
  95   // response. This method would need to cache its result otherwise.
  96   Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n";
  97
  98   if (Trace.isOn("smt-proof-debug"))
  99   {
 100     Trace("smt-proof-debug")
 101         << "SmtEngine::setFinalProof(): Proof node for false:\n";
 102     Trace("smt-proof-debug") << *pfn.get() << std::endl;
 103     Trace("smt-proof-debug") << "=====" << std::endl;
 104   }
 105
 106   std::vector<Node> assertions;
 107   getAssertions(as, assertions);
 108
 109   if (Trace.isOn("smt-proof"))
 110   {
 111     Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..."
 112                        << std::endl;
 113     std::vector<Node> fassumps;
 114     expr::getFreeAssumptions(pfn.get(), fassumps);
 115     Trace("smt-proof")
 116         << "SmtEngine::setFinalProof(): initial free assumptions are:\n";
 117     for (const Node& a : fassumps)
 118     {
 119       Trace("smt-proof") << "- " << a << std::endl;
 120     }
 121
 122     Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n";
 123     for (const Node& n : assertions)
 124     {
 125       Trace("smt-proof") << "- " << n << std::endl;
 126     }
 127     Trace("smt-proof") << "=====" << std::endl;
 128   }
 129
 130   Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
 131   Assert(d_pfpp != nullptr);
 132   d_pfpp->process(pfn);
 133
 134   Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
 135
 136   // Now make the final scope, which ensures that the only open leaves of the
 137   // proof are the assertions.
 138   d_finalProof = d_pnm->mkScope(pfn, assertions);
 139   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 140 }
 141
 142 void PfManager::printProof(std::ostream& out,
 143                            std::shared_ptr<ProofNode> pfn,
 144                            Assertions& as)
 145 {
 146   Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
 147   std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
 148   // if we are in incremental mode, we don't want to invalidate the proof
 149   // nodes in fp, since these may be reused in further check-sat calls
 150   if (options::incrementalSolving()
 151       && options::proofFormatMode() != options::ProofFormatMode::NONE)
 152   {
 153     fp = d_pnm->clone(fp);
 154   }
 155   // TODO (proj #37) according to the proof format, post process the proof node
 156   // TODO (proj #37) according to the proof format, print the proof node
 157
 158   if (options::proofFormatMode() == options::ProofFormatMode::DOT)
 159   {
 160     proof::DotPrinter dotPrinter;
 161     dotPrinter.print(out, fp.get());
 162   }
 163   else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
 164   {
 165     out << "% SZS output start Proof for " << d_env.getOptions().driver.filename << std::endl;
 166     // TODO (proj #37) print in TPTP compliant format
 167     out << *fp << std::endl;
 168     out << "% SZS output end Proof for " << d_env.getOptions().driver.filename << std::endl;
 169   }
 170   else
 171   {
 172     out << "(proof\n";
 173     out << *fp;
 174     out << "\n)\n";
 175   }
 176 }
 177 void PfManager::checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
 178 {
 179   Trace("smt-proof") << "PfManager::checkProof: start" << std::endl;
 180   std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
 181   Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get()
 182                            << std::endl;
 183 }
 184
 185 ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
 186
 187 ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
 188
 189 smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
 190 {
 191   return d_pppg.get();
 192 }
 193
 194 std::shared_ptr<ProofNode> PfManager::getFinalProof(
 195     std::shared_ptr<ProofNode> pfn, Assertions& as)
 196 {
 197   setFinalProof(pfn, as);
 198   Assert(d_finalProof);
 199   return d_finalProof;
 200 }
 201
 202 void PfManager::getAssertions(Assertions& as,
 203                               std::vector<Node>& assertions)
 204 {
 205   context::CDList<Node>* al = as.getAssertionList();
 206   Assert(al != nullptr);
 207   for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
 208        ++i)
 209   {
 210     assertions.push_back(*i);
 211   }
 212 }
 213
 214 }  // namespace smt
 215 }  // namespace cvc5