596a346dea06e361566188fe628119f9b4c3e3c6
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_manager.h"
28 * A lemma base class. This class is an abstract data structure for storing
29 * pending lemmas in the inference manager below.
34 Lemma(Node n
, LemmaProperty p
, ProofGenerator
* pg
)
35 : d_node(n
), d_property(p
), d_pg(pg
)
40 * Called just before this lemma is sent on the output channel. The purpose
41 * of this callback is to do any specific process of the lemma, e.g. take
42 * debug statistics, cache, etc.
44 * @return true if the lemma should be sent on the output channel.
46 virtual bool notifySend() { return true; }
47 /** The lemma to send */
49 /** The lemma property (see OutputChannel::lemma) */
50 LemmaProperty d_property
;
52 * The proof generator for this lemma, which if non-null, is wrapped in a
53 * TrustNode to be set on the output channel via trustedLemma at the time
54 * the lemma is sent. This proof generator must be able to provide a proof
55 * for d_node in the remainder of the user context.
61 * The buffered inference manager. This class implements standard methods
62 * for buffering facts, lemmas and phase requirements.
64 class InferenceManagerBuffered
: public TheoryInferenceManager
67 InferenceManagerBuffered(Theory
& t
,
69 ProofNodeManager
* pnm
);
70 ~InferenceManagerBuffered() {}
72 * Have we processed an inference during this call to check? In particular,
73 * this returns true if we have a pending fact or lemma, or have encountered
76 bool hasProcessed() const;
78 * Do we have a pending fact to add as an internal fact to the equality
81 bool hasPendingFact() const;
82 /** Do we have a pending lemma to send on the output channel? */
83 bool hasPendingLemma() const;
85 * Add pending lemma lem with property p, with proof generator pg. If
86 * non-null, pg must be able to provide a proof for lem for the remainder
87 * of the user context. Pending lemmas are sent to the output channel using
90 void addPendingLemma(Node lem
,
91 LemmaProperty p
= LemmaProperty::NONE
,
92 ProofGenerator
* pg
= nullptr);
94 * Add pending lemma, where lemma can be a (derived) class of the
95 * above one. Pending lemmas are sent to the output channel using
98 void addPendingLemma(std::shared_ptr
<Lemma
> lemma
);
100 * Add pending fact, which adds a fact on the pending fact queue. It must
102 * (1) exp => fact is valid,
103 * (2) exp is a literal (or conjunction of literals) that holds in the
104 * equality engine of the theory.
106 * Pending facts are sent to the equality engine of this class using
109 void addPendingFact(Node fact
, Node exp
);
110 /** Add pending phase requirement
112 * This method is called to indicate this class should send a phase
113 * requirement request to the output channel for literal lit to be
114 * decided with polarity pol. The literal lit should be a SAT literal
115 * by the time that doPendingPhaseRequirements is called. Typically,
116 * lit is a literal that is a subformula of a pending lemma that is processed
117 * prior to sending the phase requirement.
119 void addPendingPhaseRequirement(Node lit
, bool pol
);
122 * This method asserts pending facts (d_pendingFact) with explanations
123 * to the equality engine of the theory via calls
124 * to assertInternalFact.
126 * It terminates early if a conflict is encountered, for instance, by
127 * equality reasoning within the equality engine.
129 * Regardless of whether a conflict is encountered, the vector d_pendingFact
130 * is cleared after this call.
132 void doPendingFacts();
133 /** Do pending lemmas
135 * This method send all pending lemmas (d_pendingLem) on the output
136 * channel of the theory.
138 * Unlike doPendingFacts, this function will not terminate early if a conflict
139 * has already been encountered by the theory. The vector d_pendingLem is
140 * cleared after this call.
142 void doPendingLemmas();
144 * Do pending phase requirements. Calls the output channel for all pending
145 * phase requirements and clears d_pendingReqPhase.
147 void doPendingPhaseRequirements();
148 /** Clear pending facts, without processing */
149 void clearPendingFacts();
150 /** Clear pending lemmas, without processing */
151 void clearPendingLemmas();
152 /** Clear pending phase requirements, without processing */
153 void clearPendingPhaseRequirements();
156 /** A set of pending lemmas */
157 std::vector
<std::shared_ptr
<Lemma
>> d_pendingLem
;
158 /** A set of pending facts, paired with their explanations */
159 std::vector
<std::pair
<Node
, Node
>> d_pendingFact
;
160 /** A map from literals to their pending phase requirement */
161 std::map
<Node
, bool> d_pendingReqPhase
;
164 } // namespace theory