GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/proof_post_processor.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_post_processor.h
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 The module for processing proof nodes in the prop engine
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__PROP__PROOF_POST_PROCESSOR_H
18
#define CVC4__PROP__PROOF_POST_PROCESSOR_H
19
20
#include <map>
21
#include <unordered_set>
22
23
#include "expr/proof_node_updater.h"
24
#include "prop/proof_cnf_stream.h"
25
26
namespace CVC4 {
27
28
namespace prop {
29
30
/**
31
 * A callback class used by PropEngine for post-processing proof nodes by
32
 * connecting proofs of resolution, whose leaves are clausified preprocessed
33
 * assertions and lemmas, with the CNF transformation of these formulas, while
34
 * expanding the generators of lemmas.
35
 */
36
class ProofPostprocessCallback : public ProofNodeUpdaterCallback
37
{
38
 public:
39
  ProofPostprocessCallback(ProofNodeManager* pnm,
40
                           ProofCnfStream* proofCnfStream);
41
966
  ~ProofPostprocessCallback() {}
42
  /**
43
   * Initialize, called once for each new ProofNode to process. This initializes
44
   * static information to be used by successive calls to update. For this
45
   * callback it resets d_assumpToProof.
46
   */
47
  void initializeUpdate();
48
  /** Should proof pn be updated?
49
   *
50
   * For this callback a proof node is updatable if it's an assumption for which
51
   * the proof cnf straem has a proof. However if the proof node is blocked
52
   * (which is the case for proof nodes introduced into the proof cnf stream's
53
   * proof via expansion of its generators) then traversal is the proof node is
54
   * cancelled, i.e., continueUpdate is set to false.
55
   */
56
  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
57
                    bool& continueUpdate) override;
58
  /** Update the proof rule application.
59
   *
60
   * Replaces assumptions by their proof in proof cnf stream. Note that in doing
61
   * this the proof node is blocked, so that future post-processing does not
62
   * traverse it.
63
   *
64
   * This method uses the cache in d_assumpToProof to avoid recomputing proofs
65
   * for the same assumption (in the same scope).
66
   */
67
  bool update(Node res,
68
              PfRule id,
69
              const std::vector<Node>& children,
70
              const std::vector<Node>& args,
71
              CDProof* cdp,
72
              bool& continueUpdate) override;
73
74
 private:
75
  /** The proof node manager */
76
  ProofNodeManager* d_pnm;
77
  /** The cnf stream proof generator */
78
  ProofCnfStream* d_proofCnfStream;
79
  //---------------------------------reset at the begining of each update
80
  /** Mapping assumptions to their proof from cnf transformation */
81
  std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
82
  //---------------------------------end reset at the begining of each update
83
};
84
85
/**
86
 * The proof postprocessor module. This postprocesses the refutation proof
87
 * produced by the SAT solver. Its main task is to connect the refutation's
88
 * assumptions to the CNF transformation proof in ProofCnfStream.
89
 */
90
class ProofPostproccess
91
{
92
 public:
93
  ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream);
94
  ~ProofPostproccess();
95
  /** post-process
96
   *
97
   * The post-processing is done via a proof node updater run on pf with this
98
   * class's callback d_cb.
99
   */
100
  void process(std::shared_ptr<ProofNode> pf);
101
102
 private:
103
  /** The post process callback */
104
  ProofPostprocessCallback d_cb;
105
  /** The proof node manager */
106
  ProofNodeManager* d_pnm;
107
};
108
109
}  // namespace prop
110
}  // namespace CVC4
111
112
#endif