GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/buffered_proof_generator.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file buffered_proof_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
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 A proof generator for buffered proof steps
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
18
#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
19
20
#include "context/cdhashmap.h"
21
#include "expr/proof_generator.h"
22
23
namespace CVC4 {
24
25
class ProofNodeManager;
26
class ProofStep;
27
28
/**
29
 * The proof generator for buffered steps. This class is a context-dependent
30
 * mapping from formulas to proof steps. It does not generate ProofNodes until it
31
 * is asked to provide a proof for a given fact.
32
 */
33
class BufferedProofGenerator : public ProofGenerator
34
{
35
  typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
36
      NodeProofStepMap;
37
38
 public:
39
  BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
40
8131
  ~BufferedProofGenerator() {}
41
  /** add step
42
   * Unless the overwrite policy is ALWAYS it does not replace previously
43
   * registered steps (modulo (dis)equality symmetry).
44
   */
45
  bool addStep(Node fact,
46
               ProofStep ps,
47
               CDPOverwrite opolicy = CDPOverwrite::NEVER);
48
  /** Get proof for. It is robust to (dis)equality symmetry. */
49
  std::shared_ptr<ProofNode> getProofFor(Node f) override;
50
  /** identify */
51
773533
  std::string identify() const override { return "BufferedProofGenerator"; }
52
53
 private:
54
  /** maps expected to ProofStep */
55
  NodeProofStepMap d_facts;
56
  /** the proof node manager */
57
  ProofNodeManager* d_pnm;
58
};
59
60
}  // namespace CVC4
61
62
#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */