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

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_engine_proof_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 theory engine proof generator
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
18
#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
19
20
#include <memory>
21
22
#include "context/cdhashmap.h"
23
#include "context/context.h"
24
#include "expr/lazy_proof.h"
25
#include "expr/proof_generator.h"
26
#include "expr/proof_node_manager.h"
27
#include "theory/trust_node.h"
28
29
namespace CVC4 {
30
31
/**
32
 * A simple proof generator class used by the theory engine. This class
33
 * stores proofs for TheoryEngine::getExplanation.
34
 *
35
 * Notice that this class could be made general purpose. Its main feature is
36
 * storing lazy proofs for facts in a context-dependent manner.
37
 */
38
class TheoryEngineProofGenerator : public ProofGenerator
39
{
40
  typedef context::
41
      CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
42
          NodeLazyCDProofMap;
43
44
 public:
45
  TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
46
17988
  ~TheoryEngineProofGenerator() {}
47
  /**
48
   * Make trust explanation. Called when lpf has a proof of lit from free
49
   * assumptions in exp.
50
   *
51
   * This stores lpf in the map d_proofs below and returns the trust node for
52
   * this propagation, which has TrustNodeKind TrustNodeKind::PROP_EXP. If this
53
   * explanation already exists, then the previous explanation is taken, which
54
   * also suffices for proving the implication.
55
   */
56
  theory::TrustNode mkTrustExplain(TNode lit,
57
                                   Node exp,
58
                                   std::shared_ptr<LazyCDProof> lpf);
59
  /**
60
   * Get proof for, which expects implications corresponding to explained
61
   * propagations (=> exp lit) registered by the above method. This currently
62
   * involves calling the mkScope method of ProofNodeManager internally, which
63
   * returns a closed proof.
64
   */
65
  std::shared_ptr<ProofNode> getProofFor(Node f) override;
66
  /** Identify this generator (for debugging, etc..) */
67
  std::string identify() const override;
68
69
 private:
70
  /** The proof manager, used for allocating new ProofNode objects */
71
  ProofNodeManager* d_pnm;
72
  /** Map from formulas to lazy CD proofs */
73
  NodeLazyCDProofMap d_proofs;
74
  /** The false node */
75
  Node d_false;
76
};
77
78
}  // namespace CVC4
79
80
#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */