GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/proof_post_processor.cpp Lines: 40 44 90.9 %
Date: 2021-03-23 Branches: 51 154 33.1 %

Line Exec Source
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-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.\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
966
ProofPostprocessCallback::ProofPostprocessCallback(
24
966
    ProofNodeManager* pnm, ProofCnfStream* proofCnfStream)
25
966
    : d_pnm(pnm), d_proofCnfStream(proofCnfStream)
26
{
27
966
}
28
29
2292
void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); }
30
31
523730
bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
32
                                            bool& continueUpdate)
33
{
34
523730
  bool result = pn->getRule() == PfRule::ASSUME
35
1047460
                && d_proofCnfStream->hasProofFor(pn->getResult());
36
  // check if should continue traversing
37
523730
  if (d_proofCnfStream->isBlocked(pn))
38
  {
39
    continueUpdate = false;
40
    result = false;
41
  }
42
523730
  return result;
43
}
44
45
389236
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
778472
  Trace("prop-proof-pp-debug")
53
389236
      << "- Post process " << id << " " << children << " / " << args << "\n";
54
389236
  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
778472
  Node f = args[0];
58
778472
  std::shared_ptr<ProofNode> pfn;
59
  std::map<Node, std::shared_ptr<ProofNode>>::iterator it =
60
389236
      d_assumpToProof.find(f);
61
389236
  if (it != d_assumpToProof.end())
62
  {
63
311626
    Trace("prop-proof-pp-debug") << "...already computed" << std::endl;
64
311626
    pfn = it->second;
65
  }
66
  else
67
  {
68
77610
    Assert(d_proofCnfStream != nullptr);
69
    // get proof from proof cnf stream
70
77610
    pfn = d_proofCnfStream->getProofFor(f);
71
77610
    Assert(pfn != nullptr && pfn->getResult() == f);
72
77610
    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
77610
    d_assumpToProof[f] = pfn;
78
  }
79
  // connect the proof
80
389236
  cdp->addProof(pfn);
81
  // do not recursively process the result
82
389236
  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
389236
  d_proofCnfStream->addBlocked(pfn);
86
778472
  return true;
87
}
88
89
966
ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
90
966
                                     ProofCnfStream* proofCnfStream)
91
966
    : d_cb(pnm, proofCnfStream), d_pnm(pnm)
92
{
93
966
}
94
95
966
ProofPostproccess::~ProofPostproccess() {}
96
97
2292
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
2292
  d_cb.initializeUpdate();
102
  // now, process
103
4584
  ProofNodeUpdater updater(d_pnm, d_cb);
104
2292
  updater.process(pf);
105
2292
}
106
107
}  // namespace prop
108
26685
}  // namespace CVC4