GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/infer_proof_cons.h Lines: 1 1 100.0 %
Date: 2021-03-22 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
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H
18
#define CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "expr/proof_checker.h"
24
#include "expr/proof_rule.h"
25
#include "theory/builtin/proof_checker.h"
26
#include "theory/strings/infer_info.h"
27
#include "theory/strings/sequences_stats.h"
28
#include "theory/theory_proof_step_buffer.h"
29
#include "theory/uf/proof_equality_engine.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace strings {
34
35
/**
36
 * Converts between the strings-specific (untrustworthy) InferInfo class and
37
 * information about how to construct a trustworthy proof step
38
 * (PfRule, children, args). It acts as a (lazy) proof generator where the
39
 * former is registered via notifyFact and the latter is asked for in
40
 * getProofFor, typically by the proof equality engine.
41
 *
42
 * The main (private) method of this class is convert below, which is
43
 * called when we need to construct a proof node from an InferInfo.
44
 */
45
class InferProofCons : public ProofGenerator
46
{
47
  typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>, NodeHashFunction>
48
      NodeInferInfoMap;
49
50
 public:
51
  InferProofCons(context::Context* c,
52
                 ProofNodeManager* pnm,
53
                 SequencesStatistics& statistics);
54
1924
  ~InferProofCons() {}
55
  /**
56
   * This is called to notify that ii is an inference that may need a proof
57
   * in the future.
58
   *
59
   * In detail, this class should be prepared to respond to a call to:
60
   *   getProofFor(ii.d_conc)
61
   * in the remainder of the SAT context. This method copies ii and stores it
62
   * in the context-dependent map d_lazyFactMap below.
63
   *
64
   * This is used for lazy proof construction, where proofs are constructed
65
   * only for facts that are explained.
66
   */
67
  void notifyFact(const InferInfo& ii);
68
69
  /**
70
   * This returns the proof for fact. This is required for using this class as
71
   * a lazy proof generator.
72
   *
73
   * It should be the case that a call was made to notifyFact(ii) where
74
   * ii.d_conc is fact in this SAT context.
75
   */
76
  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
77
  /** Identify this generator (for debugging, etc..) */
78
  virtual std::string identify() const override;
79
80
 private:
81
  /** convert
82
   *
83
   * This method is called when the theory of strings makes an inference
84
   * described by an InferInfo, whose fields are given by the first four
85
   * arguments of this method.
86
   *
87
   * This method converts this call to instructions on what the proof rule
88
   * step(s) are for concluding the conclusion of the inference. This
89
   * information is either:
90
   *
91
   * (A) stored in the argument ps, which consists of:
92
   * - A proof rule identifier (ProofStep::d_rule).
93
   * - The premises of the proof step (ProofStep::d_children).
94
   * - Arguments to the proof step (ProofStep::d_args).
95
   *
96
   * (B) If the proof for the inference cannot be captured by a single
97
   * step, then the d_rule field of ps is not set, and useBuffer is set to
98
   * true. In this case, the argument psb is updated to contain (possibly
99
   * multiple) proof steps for how to construct a proof for the given inference.
100
   * In particular, psb will contain a set of steps that form a proof
101
   * whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant.
102
   */
103
  void convert(InferenceId infer,
104
               bool isRev,
105
               Node conc,
106
               const std::vector<Node>& exp,
107
               ProofStep& ps,
108
               TheoryProofStepBuffer& psb,
109
               bool& useBuffer);
110
  /**
111
   * Convert length proof. If this method returns true, it adds proof step(s)
112
   * to the buffer psb that conclude lenReq from premises lenExp.
113
   */
114
  bool convertLengthPf(Node lenReq,
115
                       const std::vector<Node>& lenExp,
116
                       TheoryProofStepBuffer& psb);
117
  /**
118
   * Helper method, adds the proof of (TRANS eqa eqb) into the proof step
119
   * buffer psb, where eqa and eqb are flipped as needed. Returns the
120
   * conclusion, or null if we were not able to construct a TRANS step.
121
   */
122
  Node convertTrans(Node eqa, Node eqb, TheoryProofStepBuffer& psb);
123
  /** the proof node manager */
124
  ProofNodeManager* d_pnm;
125
  /** The lazy fact map */
126
  NodeInferInfoMap d_lazyFactMap;
127
  /** Reference to the statistics for the theory of strings/sequences. */
128
  SequencesStatistics& d_statistics;
129
};
130
131
}  // namespace strings
132
}  // namespace theory
133
}  // namespace CVC4
134
135
#endif /* CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H */