src/prop/proof_post_processor.cpp

   1 /*********************                                                        */
   2 /*! \file proof_post_processor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa
   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  ** \brief Implementation of the module for processing proof nodes in the prop
  13  ** engine
  14  **/
  15
  16 #include "prop/proof_post_processor.h"
  17
  18 #include "theory/builtin/proof_checker.h"
  19
  20 namespace CVC4 {
  21 namespace prop {
  22
  23 ProofPostprocessCallback::ProofPostprocessCallback(
  24     ProofNodeManager* pnm, ProofCnfStream* proofCnfStream)
  25     : d_pnm(pnm), d_proofCnfStream(proofCnfStream)
  26 {
  27 }
  28
  29 void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); }
  30
  31 bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
  32                                             bool& continueUpdate)
  33 {
  34   bool result = pn->getRule() == PfRule::ASSUME
  35                 && d_proofCnfStream->hasProofFor(pn->getResult());
  36   // check if should continue traversing
  37   if (d_proofCnfStream->isBlocked(pn))
  38   {
  39     continueUpdate = false;
  40     result = false;
  41   }
  42   return result;
  43 }
  44
  45 bool ProofPostprocessCallback::update(Node res,
  46                                       PfRule id,
  47                                       const std::vector<Node>& children,
  48                                       const std::vector<Node>& args,
  49                                       CDProof* cdp,
  50                                       bool& continueUpdate)
  51 {
  52   Trace("prop-proof-pp-debug")
  53       << "- Post process " << id << " " << children << " / " << args << "\n";
  54   Assert(id == PfRule::ASSUME);
  55   // we cache based on the assumption node, not the proof node, since there
  56   // may be multiple occurrences of the same node.
  57   Node f = args[0];
  58   std::shared_ptr<ProofNode> pfn;
  59   std::map<Node, std::shared_ptr<ProofNode>>::iterator it =
  60       d_assumpToProof.find(f);
  61   if (it != d_assumpToProof.end())
  62   {
  63     Trace("prop-proof-pp-debug") << "...already computed" << std::endl;
  64     pfn = it->second;
  65   }
  66   else
  67   {
  68     Assert(d_proofCnfStream != nullptr);
  69     // get proof from proof cnf stream
  70     pfn = d_proofCnfStream->getProofFor(f);
  71     Assert(pfn != nullptr && pfn->getResult() == f);
  72     if (Trace.isOn("prop-proof-pp"))
  73     {
  74       Trace("prop-proof-pp") << "=== Connect CNF proof for: " << f << "\n";
  75       Trace("prop-proof-pp") << *pfn.get() << "\n";
  76     }
  77     d_assumpToProof[f] = pfn;
  78   }
  79   // connect the proof
  80   cdp->addProof(pfn);
  81   // do not recursively process the result
  82   continueUpdate = false;
  83   // moreover block the fact f so that its proof node is not traversed if we run
  84   // this post processor again (which can happen in incremental benchmarks)
  85   d_proofCnfStream->addBlocked(pfn);
  86   return true;
  87 }
  88
  89 ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
  90                                      ProofCnfStream* proofCnfStream)
  91     : d_cb(pnm, proofCnfStream), d_pnm(pnm)
  92 {
  93 }
  94
  95 ProofPostproccess::~ProofPostproccess() {}
  96
  97 void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
  98 {
  99   // Initialize the callback, which computes necessary static information about
 100   // how to process, including how to process assumptions in pf.
 101   d_cb.initializeUpdate();
 102   // now, process
 103   ProofNodeUpdater updater(d_pnm, d_cb);
 104   updater.process(pf);
 105 }
 106
 107 }  // namespace prop
 108 }  // namespace CVC4