1 /********************* */
2 /*! \file inference_manager_buffered.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief A buffered inference manager
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
18 #define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
20 #include "context/cdhashmap.h"
21 #include "expr/node.h"
22 #include "theory/theory_inference.h"
23 #include "theory/theory_inference_manager.h"
29 * The buffered inference manager. This class implements standard methods
30 * for buffering facts, lemmas and phase requirements.
32 class InferenceManagerBuffered
: public TheoryInferenceManager
35 InferenceManagerBuffered(Theory
& t
,
37 ProofNodeManager
* pnm
);
38 virtual ~InferenceManagerBuffered() {}
40 * Have we processed an inference during this call to check? In particular,
41 * this returns true if we have a pending fact or lemma, or have encountered
44 bool hasProcessed() const;
46 * Do we have a pending fact to add as an internal fact to the equality
49 bool hasPendingFact() const;
50 /** Do we have a pending lemma to send on the output channel? */
51 bool hasPendingLemma() const;
53 * Add pending lemma lem with property p, with proof generator pg. If
54 * non-null, pg must be able to provide a proof for lem for the remainder
55 * of the user context. Pending lemmas are sent to the output channel using
58 void addPendingLemma(Node lem
,
59 LemmaProperty p
= LemmaProperty::NONE
,
60 ProofGenerator
* pg
= nullptr);
62 * Add pending lemma, where lemma can be a (derived) class of the
63 * theory inference base class.
65 void addPendingLemma(std::unique_ptr
<TheoryInference
> lemma
);
67 * Add pending fact, which adds a fact on the pending fact queue. It must
69 * (1) exp => conc is valid,
70 * (2) exp is a literal (or conjunction of literals) that holds in the
71 * equality engine of the theory.
73 * Pending facts are sent to the equality engine of this class using
76 void addPendingFact(Node conc
, Node exp
, ProofGenerator
* pg
= nullptr);
78 * Add pending fact, where fact can be a (derived) class of the
79 * theory inference base class.
81 void addPendingFact(std::unique_ptr
<TheoryInference
> fact
);
82 /** Add pending phase requirement
84 * This method is called to indicate this class should send a phase
85 * requirement request to the output channel for literal lit to be
86 * decided with polarity pol. The literal lit should be a SAT literal
87 * by the time that doPendingPhaseRequirements is called. Typically,
88 * lit is a literal that is a subformula of a pending lemma that is processed
89 * prior to sending the phase requirement.
91 void addPendingPhaseRequirement(Node lit
, bool pol
);
94 * This method asserts pending facts (d_pendingFact) with explanations
95 * to the equality engine of the theory via calls
96 * to assertInternalFact.
98 * It terminates early if a conflict is encountered, for instance, by
99 * equality reasoning within the equality engine.
101 * Regardless of whether a conflict is encountered, the vector d_pendingFact
102 * is cleared after this call.
104 void doPendingFacts();
105 /** Do pending lemmas
107 * This method send all pending lemmas (d_pendingLem) on the output
108 * channel of the theory.
110 * Unlike doPendingFacts, this function will not terminate early if a conflict
111 * has already been encountered by the theory. The vector d_pendingLem is
112 * cleared after this call.
114 void doPendingLemmas();
116 * Do pending phase requirements. Calls the output channel for all pending
117 * phase requirements and clears d_pendingReqPhase.
119 void doPendingPhaseRequirements();
120 /** Clear pending facts, without processing */
121 void clearPendingFacts();
122 /** Clear pending lemmas, without processing */
123 void clearPendingLemmas();
124 /** Clear pending phase requirements, without processing */
125 void clearPendingPhaseRequirements();
127 /** Returns the number of pending lemmas. */
128 std::size_t numPendingLemmas() const;
129 /** Returns the number of pending facts. */
130 std::size_t numPendingFacts() const;
133 /** A set of pending inferences to be processed as lemmas */
134 std::vector
<std::unique_ptr
<TheoryInference
>> d_pendingLem
;
135 /** A set of pending inferences to be processed as facts */
136 std::vector
<std::unique_ptr
<TheoryInference
>> d_pendingFact
;
137 /** A map from literals to their pending phase requirement */
138 std::map
<Node
, bool> d_pendingReqPhase
;
141 } // namespace theory