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

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_proof_cons.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Inference to proof conversion for datatypes
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
18
#define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
19
20
#include "context/cdhashmap.h"
21
#include "expr/node.h"
22
#include "expr/proof_generator.h"
23
#include "theory/datatypes/inference.h"
24
25
namespace CVC4 {
26
27
class ProofNodeManager;
28
29
namespace theory {
30
namespace datatypes {
31
32
/**
33
 * Converts between the datatype-specific (untrustworthy) DatatypesInference
34
 * class and information about how to construct a trustworthy proof step
35
 * (PfRule, children, args). It acts as a (lazy) proof generator where the
36
 * former is registered via notifyFact and the latter is asked for in
37
 * getProofFor, typically by the proof equality engine.
38
 *
39
 * The main (private) method of this class is convert below, which is
40
 * called when we need to construct a proof node from an InferInfo.
41
 */
42
class InferProofCons : public ProofGenerator
43
{
44
  typedef context::
45
      CDHashMap<Node, std::shared_ptr<DatatypesInference>, NodeHashFunction>
46
          NodeDatatypesInferenceMap;
47
48
 public:
49
  InferProofCons(context::Context* c, ProofNodeManager* pnm);
50
2681
  ~InferProofCons() {}
51
  /**
52
   * This is called to notify that di is an inference that may need a proof
53
   * in the future.
54
   *
55
   * In detail, this class should be prepared to respond to a call to:
56
   *   getProofFor(di.d_conc)
57
   * in the remainder of the SAT context. This method copies di and stores it
58
   * in the context-dependent map d_lazyFactMap below.
59
   *
60
   * This is used for lazy proof construction, where proofs are constructed
61
   * only for facts that are explained.
62
   */
63
  void notifyFact(const std::shared_ptr<DatatypesInference>& di);
64
65
  /**
66
   * This returns the proof for fact. This is required for using this class as
67
   * a lazy proof generator.
68
   *
69
   * It should be the case that a call was made to notifyFact(di) where
70
   * di.d_conc is fact in this SAT context.
71
   */
72
  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
73
  /** Identify this generator (for debugging, etc..) */
74
  virtual std::string identify() const override;
75
76
 private:
77
  /** convert
78
   *
79
   * This method is called when the theory of strings makes an inference
80
   * described by an InferInfo, whose fields are given by the first four
81
   * arguments of this method.
82
   *
83
   * This method converts this call to instructions on what the proof rule
84
   * step(s) are for concluding the conclusion of the inference. This
85
   * information is stored in cdp.
86
   */
87
  void convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp);
88
  /** A dummy context used by this class if none is provided */
89
  context::Context d_context;
90
  /** the proof node manager */
91
  ProofNodeManager* d_pnm;
92
  /** The lazy fact map */
93
  NodeDatatypesInferenceMap d_lazyFactMap;
94
};
95
96
}  // namespace datatypes
97
}  // namespace theory
98
}  // namespace CVC4
99
100
#endif /* CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H */