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