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

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager_buffered.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 A buffered inference manager
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
18
#define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
19
20
#include "expr/node.h"
21
#include "theory/theory_inference.h"
22
#include "theory/theory_inference_manager.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
/**
28
 * The buffered inference manager.  This class implements standard methods
29
 * for buffering facts, lemmas and phase requirements.
30
 */
31
class InferenceManagerBuffered : public TheoryInferenceManager
32
{
33
 public:
34
  InferenceManagerBuffered(Theory& t,
35
                           TheoryState& state,
36
                           ProofNodeManager* pnm,
37
                           const std::string& name,
38
                           bool cacheLemmas = true);
39
62958
  virtual ~InferenceManagerBuffered() {}
40
  /**
41
   * Do we have a pending fact or lemma?
42
   */
43
  bool hasPending() const;
44
  /**
45
   * Do we have a pending fact to add as an internal fact to the equality
46
   * engine?
47
   */
48
  bool hasPendingFact() const;
49
  /** Do we have a pending lemma to send on the output channel? */
50
  bool hasPendingLemma() const;
51
  /**
52
   * Add pending lemma lem with property p, with proof generator pg. If
53
   * non-null, pg must be able to provide a proof for lem for the remainder
54
   * of the user context. Pending lemmas are sent to the output channel using
55
   * doPendingLemmas.
56
   *
57
   * @param lem The lemma to send
58
   * @param id The identifier of the inference
59
   * @param p The property of the lemma
60
   * @param pg The proof generator which can provide a proof for lem
61
   * @param checkCache Whether we want to check that the lemma is already in
62
   * the cache.
63
   * @return true if the lemma was added to the list of pending lemmas and
64
   * false if the lemma is already cached.
65
   */
66
  bool addPendingLemma(Node lem,
67
                       InferenceId id,
68
                       LemmaProperty p = LemmaProperty::NONE,
69
                       ProofGenerator* pg = nullptr,
70
                       bool checkCache = true);
71
  /**
72
   * Add pending lemma, where lemma can be a (derived) class of the
73
   * theory inference base class.
74
   */
75
  void addPendingLemma(std::unique_ptr<TheoryInference> lemma);
76
  /**
77
   * Add pending fact, which adds a fact on the pending fact queue. It must
78
   * be the case that:
79
   * (1) exp => conc is valid,
80
   * (2) exp is a literal (or conjunction of literals) that holds in the
81
   * equality engine of the theory.
82
   *
83
   * Pending facts are sent to the equality engine of this class using
84
   * doPendingFacts.
85
   * @param conc The conclustion
86
   * @param id The identifier of the inference
87
   * @param exp The explanation in the equality engine of the theory
88
   * @param pg The proof generator which can provide a proof for conc
89
   */
90
  void addPendingFact(Node conc, InferenceId id, Node exp, ProofGenerator* pg = nullptr);
91
  /**
92
   * Add pending fact, where fact can be a (derived) class of the
93
   * theory inference base class.
94
   */
95
  void addPendingFact(std::unique_ptr<TheoryInference> fact);
96
  /** Add pending phase requirement
97
   *
98
   * This method is called to indicate this class should send a phase
99
   * requirement request to the output channel for literal lit to be
100
   * decided with polarity pol. The literal lit should be a SAT literal
101
   * by the time that doPendingPhaseRequirements is called. Typically,
102
   * lit is a literal that is a subformula of a pending lemma that is processed
103
   * prior to sending the phase requirement.
104
   */
105
  void addPendingPhaseRequirement(Node lit, bool pol);
106
  /** Do pending facts
107
   *
108
   * This method asserts pending facts (d_pendingFact) with explanations
109
   * to the equality engine of the theory via calls
110
   * to assertInternalFact.
111
   *
112
   * It terminates early if a conflict is encountered, for instance, by
113
   * equality reasoning within the equality engine.
114
   *
115
   * Regardless of whether a conflict is encountered, the vector d_pendingFact
116
   * is cleared after this call.
117
   */
118
  void doPendingFacts();
119
  /** Do pending lemmas
120
   *
121
   * This method send all pending lemmas (d_pendingLem) on the output
122
   * channel of the theory.
123
   *
124
   * Unlike doPendingFacts, this function will not terminate early if a conflict
125
   * has already been encountered by the theory. The vector d_pendingLem is
126
   * cleared after this call.
127
   */
128
  void doPendingLemmas();
129
  /**
130
   * Do pending phase requirements. Calls the output channel for all pending
131
   * phase requirements and clears d_pendingReqPhase.
132
   */
133
  void doPendingPhaseRequirements();
134
  /** Clear pending facts, lemmas, and phase requirements without processing */
135
  void clearPending();
136
  /** Clear pending facts, without processing */
137
  void clearPendingFacts();
138
  /** Clear pending lemmas, without processing */
139
  void clearPendingLemmas();
140
  /** Clear pending phase requirements, without processing */
141
  void clearPendingPhaseRequirements();
142
143
  /** Returns the number of pending lemmas. */
144
  std::size_t numPendingLemmas() const;
145
  /** Returns the number of pending facts. */
146
  std::size_t numPendingFacts() const;
147
148
  /**
149
   * Send the given theory inference as a lemma on the output channel of this
150
   * inference manager. This calls TheoryInferenceManager::trustedLemma based
151
   * on the provided theory inference.
152
   */
153
  void lemmaTheoryInference(TheoryInference* lem);
154
  /**
155
   * Add the given theory inference as an internal fact. This calls
156
   * TheoryInferenceManager::assertInternalFact based on the provided theory
157
   * inference.
158
   */
159
  void assertInternalFactTheoryInference(TheoryInference* fact);
160
161
 protected:
162
  /** A set of pending inferences to be processed as lemmas */
163
  std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;
164
  /** A set of pending inferences to be processed as facts */
165
  std::vector<std::unique_ptr<TheoryInference>> d_pendingFact;
166
  /** A map from literals to their pending phase requirement */
167
  std::map<Node, bool> d_pendingReqPhase;
168
  /**
169
   * Whether we are currently processing pending lemmas. This flag ensures
170
   * that we do not call pending lemmas recursively, which may lead to
171
   * segfaults.
172
   */
173
  bool d_processingPendingLemmas;
174
};
175
176
}  // namespace theory
177
}  // namespace CVC4
178
179
#endif