1 /********************* */
2 /*! \file theory_inference_manager.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 An inference manager for Theory
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
18 #define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
22 #include "context/cdhashset.h"
23 #include "expr/node.h"
24 #include "theory/output_channel.h"
25 #include "theory/theory_state.h"
26 #include "theory/trust_node.h"
27 #include "theory/uf/proof_equality_engine.h"
31 class ProofNodeManager
;
41 * The base class for inference manager. An inference manager is a wrapper
42 * around the output channel and the official equality engine of a Theory.
43 * It is used for ensuring that the equality engine and output channel
44 * are used properly. This includes the following invariants:
46 * (1) The state tracks conflicts.
47 * In particular, TheoryState::isInConflict returns true whenever we have
48 * called OutputChannel::conflict in the current context, which we enforce
49 * by always setting d_state.notifyInConflict at the same time we send
50 * conflicts on the output channel.
52 * (2) The theory is notified of (internal) facts.
53 * In particular, Theory::preNotifyFact and Theory::notifyFact are called
54 * (with isInternal = true) whenever we assert internal facts using
55 * assertFactInernal below, mirroring what is done for facts from the fact
56 * queue (where isInternal = false).
58 * (3) The proof equality engine is used whenever proofs are enabled (when
59 * the proof node manager provided to this class is non-null). Notice this
60 * class automatically will construct a proof equality engine during
61 * setEqualityEngine, and use it for handling variants of assertInternalFact
62 * below that involve proofs.
64 class TheoryInferenceManager
66 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
70 * Constructor, note that state should be the official state of theory t.
72 TheoryInferenceManager(Theory
& t
, TheoryState
& state
, ProofNodeManager
* pnm
);
73 virtual ~TheoryInferenceManager() {}
75 * Set equality engine, ee is a pointer to the official equality engine
78 void setEqualityEngine(eq::EqualityEngine
* ee
);
80 * Reset, which resets counters regarding the number of added lemmas and
81 * internal facts. This method should be manually called by the theory at
82 * the appropriate time for the purpose of tracking the usage of this
85 * For example, some theories implement an internal checking loop that
86 * repeats while new facts are added. The theory should call reset at the
87 * beginning of this loop and repeat its strategy while hasAddedFact is true.
90 //--------------------------------------- propagations
92 * T-propagate literal lit, possibly encountered by equality engine,
93 * returns false if we are in conflict.
95 * Note that this is the preferred method to call on
96 * EqualityEngineNotify::eqNotifyTriggerPredicate and
97 * EqualityEngineNotify::eqNotifyTriggerTermEquality.
99 bool propagateLit(TNode lit
);
101 * Return an explanation for the literal represented by parameter lit
102 * (which was previously propagated by this theory). By default, this
103 * returns the explanation given by the official equality engine of the
104 * Theory, if it exists.
106 virtual TrustNode
explainLit(TNode lit
);
107 //--------------------------------------- conflicts
109 * Raise conflict, called when constants a and b merge. Sends the conflict
110 * on the output channel corresponding to the equality engine's explanation
111 * of (= a b). The proof equality engine (if it exists) will be used as the
114 * Note that this is the preferred method to call on
115 * EqualityEngineNotify::eqNotifyConstantTermMerge.
117 void conflictEqConstantMerge(TNode a
, TNode b
);
119 * Raise conflict conf (of any form), without proofs. This method should
120 * only be called if there is not yet proof support in the given theory.
122 void conflict(TNode conf
);
124 * Raise trusted conflict tconf (of any form) where a proof generator has
125 * been provided in a custom way.
127 void trustedConflict(TrustNode tconf
);
129 * Explain and send conflict from contradictory facts. This method is called
130 * when the proof rule id with premises exp and arguments args concludes
131 * false. This method sends a trusted conflict corresponding to the official
132 * equality engine's explanation of literals in exp, with the proof equality
133 * engine as the proof generator (if it exists).
135 void conflictExp(PfRule id
,
136 const std::vector
<Node
>& exp
,
137 const std::vector
<Node
>& args
);
138 //--------------------------------------- lemmas
140 * Send (trusted) lemma lem with property p on the output channel.
142 * @param tlem The trust node containing the lemma and its proof generator.
143 * @param p The property of the lemma
144 * @param doCache If true, we send the lemma only if it has not already been
145 * cached (see cacheLemma), and add it to the cache during this call.
146 * @return true if the lemma was sent on the output channel.
148 bool trustedLemma(const TrustNode
& tlem
,
149 LemmaProperty p
= LemmaProperty::NONE
,
150 bool doCache
= true);
152 * Send lemma lem with property p on the output channel. Same as above, with
153 * a node instead of a trust node.
155 bool lemma(TNode lem
,
156 LemmaProperty p
= LemmaProperty::NONE
,
157 bool doCache
= true);
159 * Explained lemma. This should be called when
161 * is a valid theory lemma. This method adds a lemma where part of exp
162 * is replaced by its explanation according to the official equality engine
165 * In particular, this method adds a lemma on the output channel of the form
166 * ( ^_{e in exp \ noExplain} EXPLAIN(e) ^ noExplain ) => conc
167 * where EXPLAIN(e) returns the explanation of literal e according to the
168 * official equality engine of the theory. Note that noExplain is the *subset*
169 * of exp that should not be explained.
171 * @param conc The conclusion of the lemma
172 * @param id The proof rule concluding conc
173 * @param exp The set of (all) literals that imply conc
174 * @param noExplain The subset of exp that should not be explained by the
176 * @param args The arguments to the proof step concluding conc
177 * @param p The property of the lemma
178 * @param doCache Whether to check and add the lemma to the cache
179 * @return true if the lemma was sent on the output channel.
181 bool lemmaExp(Node conc
,
183 const std::vector
<Node
>& exp
,
184 const std::vector
<Node
>& noExplain
,
185 const std::vector
<Node
>& args
,
186 LemmaProperty p
= LemmaProperty::NONE
,
187 bool doCache
= true);
189 * Same as above, but where pg can provide a proof of conc from free
190 * assumptions in exp. It is required to do so in the remainder of the user
191 * context when this method returns true.
193 * @param conc The conclusion of the lemma
194 * @param exp The set of (all) literals that imply conc
195 * @param noExplain The subset of exp that should not be explained by the
197 * @param pg If non-null, the proof generator who can provide a proof of conc.
198 * @param p The property of the lemma
199 * @param doCache Whether to check and add the lemma to the cache
200 * @return true if the lemma was sent on the output channel.
202 bool lemmaExp(Node conc
,
203 const std::vector
<Node
>& exp
,
204 const std::vector
<Node
>& noExplain
,
205 ProofGenerator
* pg
= nullptr,
206 LemmaProperty p
= LemmaProperty::NONE
,
207 bool doCache
= true);
209 * Has this inference manager cached and sent the given lemma (in this user
210 * context)? This method can be overridden by the particular manager. If not,
211 * this returns true if lem is in the cache d_lemmasSent maintained by this
212 * class. Notice that the default cache in this base class is not dependent
213 * on the lemma property.
215 virtual bool hasCachedLemma(TNode lem
, LemmaProperty p
);
216 /** The number of lemmas we have sent since the last call to reset */
217 uint32_t numAddedLemmas() const;
218 /** Have we added a lemma since the last call to reset? */
219 bool hasAddedLemma() const;
220 //--------------------------------------- internal facts
222 * Assert internal fact. This is recommended method for asserting "internal"
223 * facts into the equality engine of the theory. In particular, this method
224 * should be used for anything the theory infers that is not sent on the
225 * output channel as a propagation or lemma. This method ensures that the
226 * Theory's preNotifyFact and notifyFact method have been called with
229 * @param atom The atom of the fact to assert
230 * @param pol Its polarity
231 * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid.
233 void assertInternalFact(TNode atom
, bool pol
, TNode exp
);
235 * Assert internal fact, with a proof step justification. Notice that if
236 * proofs are not enabled in this inference manager, then this asserts
237 * a fact to the equality engine in the normal way.
239 * @param atom The atom of the fact to assert
240 * @param pol Its polarity
241 * @param id The proof rule identifier of the proof step
242 * @param exp Its explanation, interpreted as a conjunction
243 * @param args The arguments of the proof step
245 void assertInternalFact(TNode atom
,
248 const std::vector
<Node
>& exp
,
249 const std::vector
<Node
>& args
);
251 * Assert internal fact, with a proof generator justification. Same as above,
252 * but with a proof generator instead of an explicit step.
254 * @param atom The atom of the fact to assert
255 * @param pol Its polarity
256 * @param exp Its explanation, interpreted as a conjunction
257 * @param pg The proof generator for this step. If non-null, pg must be able
258 * to provide a proof concluding (~) atom from free asumptions in exp in
259 * the remainder of the current SAT context.
261 void assertInternalFact(TNode atom
,
263 const std::vector
<Node
>& exp
,
265 /** The number of internal facts we have added since the last call to reset */
266 uint32_t numAddedFacts() const;
267 /** Have we added a internal fact since the last call to reset? */
268 bool hasAddedFact() const;
272 * Process internal fact. This is a common helper method for the
273 * assertInternalFact variants above.
275 void processInternalFact(TNode atom
,
278 const std::vector
<Node
>& exp
,
279 const std::vector
<Node
>& args
,
282 * Explain conflict from constants merging in the equality engine. This
283 * method is called by conflictEqConstantMerge. By default, it returns
284 * the explanation of the official equality engine of the theory, if it
287 virtual TrustNode
explainConflictEqConstantMerge(TNode a
, TNode b
);
289 * Explain formula n (which is possibly a conjunction with no nested
290 * conjunctions), add its explanation to assumptions.
292 void explain(TNode n
, std::vector
<TNode
>& assumptions
);
294 * Explain formula n (which is possibly a conjunction with no nested
295 * conjunctions), return the explanation as a conjunction.
297 Node
mkExplain(TNode n
);
299 * Explain the set of formulas in exp using the official equality engine of
300 * the theory. We ask the equality engine to explain literals in exp
301 * that do not occur in noExplain, and return unchanged those that occur in
302 * noExplain. Note the vector noExplain should be a subset of exp.
304 Node
mkExplainPartial(const std::vector
<Node
>& exp
,
305 const std::vector
<Node
>& noExplain
);
307 * Cache that lemma lem is being sent with property p. Return true if it
308 * did not already exist in the cache maintained by this class. If this
309 * method is not overridden, then we use the d_lemmasSent cache maintained
310 * by this class, which notice is not dependent on lemma property. If
311 * the lemma property should be taken into account, the manager should
312 * override this method to take the lemma property into account as needed.
314 virtual bool cacheLemma(TNode lem
, LemmaProperty p
);
315 /** The theory object */
317 /** Reference to the state of theory */
318 TheoryState
& d_theoryState
;
319 /** Reference to the output channel of the theory */
320 OutputChannel
& d_out
;
321 /** Pointer to equality engine of the theory. */
322 eq::EqualityEngine
* d_ee
;
323 /** A proof equality engine */
324 std::unique_ptr
<eq::ProofEqEngine
> d_pfee
;
325 /** The proof node manager of the theory */
326 ProofNodeManager
* d_pnm
;
328 * The keep set of this class. This set is maintained to ensure that
329 * facts and their explanations are ref-counted. Since facts and their
330 * explanations are SAT-context-dependent, this set is also
331 * SAT-context-dependent.
335 * A cache of all lemmas sent, which is a user-context-dependent set of
336 * nodes. Notice that this cache does not depedent on lemma property.
338 NodeSet d_lemmasSent
;
339 /** The number of lemmas sent since the last call to reset. */
340 uint32_t d_numCurrentLemmas
;
341 /** The number of internal facts added since the last call to reset. */
342 uint32_t d_numCurrentFacts
;
345 } // namespace theory
348 #endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */