1 /********************* */
2 /*! \file theory_engine.h
4 ** Original author: mdeters
5 ** Major contributors: taking, dejan
6 ** Minor contributors (to current version): cconway, barrett
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief The theory engine.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY_ENGINE_H
22 #define __CVC4__THEORY_ENGINE_H
26 #include "expr/node.h"
27 #include "prop/prop_engine.h"
28 #include "theory/shared_term_manager.h"
29 #include "theory/theory.h"
30 #include "theory/rewriter.h"
31 #include "theory/valuation.h"
32 #include "util/options.h"
33 #include "util/stats.h"
37 // In terms of abstraction, this is below (and provides services to)
41 * This is essentially an abstraction for a collection of theories. A
42 * TheoryEngine provides services to a PropEngine, making various
43 * T-solvers look like a single unit to the propositional part of
48 /** Associated PropEngine engine */
49 prop::PropEngine
* d_propEngine
;
52 context::Context
* d_context
;
54 /** A table of from theory ifs to theory pointers */
55 theory::Theory
* d_theoryTable
[theory::THEORY_LAST
];
58 * An output channel for Theory that passes messages
59 * back to a TheoryEngine.
61 class EngineOutputChannel
: public theory::OutputChannel
{
63 friend class TheoryEngine
;
65 TheoryEngine
* d_engine
;
66 context::Context
* d_context
;
67 context::CDO
<Node
> d_conflictNode
;
68 context::CDO
<Node
> d_explanationNode
;
71 * Literals that are propagated by the theory. Note that these are TNodes.
72 * The theory can only propagate nodes that have an assigned literal in the
73 * sat solver and are hence referenced in the SAT solver.
75 std::vector
<TNode
> d_propagatedLiterals
;
77 /** Time spent in newFact() (largely spent doing term registration) */
78 KEEP_STATISTIC(TimerStat
,
80 "theory::newFactTimer");
84 EngineOutputChannel(TheoryEngine
* engine
, context::Context
* context
) :
87 d_conflictNode(context
),
88 d_explanationNode(context
) {
91 void newFact(TNode n
);
93 void conflict(TNode conflictNode
, bool safe
)
94 throw(theory::Interrupted
, AssertionException
) {
95 Debug("theory") << "EngineOutputChannel::conflict("
96 << conflictNode
<< ")" << std::endl
;
97 d_conflictNode
= conflictNode
;
98 ++(d_engine
->d_statistics
.d_statConflicts
);
100 throw theory::Interrupted();
104 void propagate(TNode lit
, bool)
105 throw(theory::Interrupted
, AssertionException
) {
106 Debug("theory") << "EngineOutputChannel::propagate("
107 << lit
<< ")" << std::endl
;
108 d_propagatedLiterals
.push_back(lit
);
109 ++(d_engine
->d_statistics
.d_statPropagate
);
112 void lemma(TNode node
, bool)
113 throw(theory::Interrupted
, AssertionException
) {
114 Debug("theory") << "EngineOutputChannel::lemma("
115 << node
<< ")" << std::endl
;
116 ++(d_engine
->d_statistics
.d_statLemma
);
117 d_engine
->newLemma(node
);
120 void explanation(TNode explanationNode
, bool)
121 throw(theory::Interrupted
, AssertionException
) {
122 Debug("theory") << "EngineOutputChannel::explanation("
123 << explanationNode
<< ")" << std::endl
;
124 d_explanationNode
= explanationNode
;
125 ++(d_engine
->d_statistics
.d_statExplanation
);
129 throw(theory::Interrupted
, AssertionException
) {
130 d_engine
->d_incomplete
= true;
132 };/* class EngineOutputChannel */
134 EngineOutputChannel d_theoryOut
;
136 /** Pointer to Shared Term Manager */
137 SharedTermManager
* d_sharedTermManager
;
140 * Whether or not theory registration is on. May not be safe to
141 * turn off with some theories.
143 bool d_theoryRegistration
;
146 * Debugging flag to ensure that shutdown() is called before the
152 * True if a theory has notified us of incompleteness (at this
153 * context level or below).
155 context::CDO
<bool> d_incomplete
;
158 * Replace ITE forms in a node.
160 Node
removeITEs(TNode t
);
165 * Construct a theory engine.
167 TheoryEngine(context::Context
* ctxt
);
170 * Destroy a theory engine.
175 * Adds a theory. Only one theory per theoryId can be present, so if there is another theory it will be deleted.
177 template <class TheoryClass
>
179 TheoryClass
* theory
= new TheoryClass(d_context
, d_theoryOut
, theory::Valuation(this));
180 d_theoryTable
[theory
->getId()] = theory
;
181 d_sharedTermManager
->registerTheory(static_cast<TheoryClass
*>(theory
));
184 SharedTermManager
* getSharedTermManager() {
185 return d_sharedTermManager
;
188 void setPropEngine(prop::PropEngine
* propEngine
) {
189 Assert(d_propEngine
== NULL
);
190 d_propEngine
= propEngine
;
194 * Get a pointer to the underlying propositional engine.
196 prop::PropEngine
* getPropEngine() const {
201 * Return whether or not we are incomplete (in the current context).
203 bool isIncomplete() {
208 * This is called at shutdown time by the SmtEngine, just before
209 * destruction. It is important because there are destruction
210 * ordering issues between PropEngine and Theory.
213 // Set this first; if a Theory shutdown() throws an exception,
214 // at least the destruction of the TheoryEngine won't confound
216 d_hasShutDown
= true;
218 // Shutdown all the theories
219 for(unsigned theoryId
= 0; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
220 if(d_theoryTable
[theoryId
]) {
221 d_theoryTable
[theoryId
]->shutdown();
225 theory::Rewriter::shutdown();
229 * Get the theory associated to a given Node.
231 * @returns the theory, or NULL if the TNode is
234 inline theory::Theory
* theoryOf(TNode node
) {
235 return d_theoryTable
[theory::Theory::theoryOf(node
)];
239 * Get the theory associated to a given Node.
241 * @returns the theory, or NULL if the TNode is
244 inline theory::Theory
* theoryOf(const TypeNode
& typeNode
) {
245 return d_theoryTable
[theory::Theory::theoryOf(typeNode
)];
249 * Preprocess a node. This involves theory-specific rewriting, then
250 * calling preRegisterTerm() on what's left over.
251 * @param n the node to preprocess
253 Node
preprocess(TNode n
);
254 void preRegister(TNode preprocessed
);
257 * Assert the formula to the appropriate theory.
258 * @param node the assertion
260 inline void assertFact(TNode node
) {
261 Debug("theory") << "TheoryEngine::assertFact(" << node
<< ")" << std::endl
;
263 // Mark it as asserted in this context
265 // [MGD] removed for now, this appears to have a nontrivial
266 // performance penalty
267 // node.setAttribute(theory::Asserted(), true);
270 TNode atom
= node
.getKind() == kind::NOT
? node
[0] : node
;
272 // Again, equality is a special case
273 if (atom
.getKind() == kind::EQUAL
) {
274 theory::TheoryId theoryLHS
= theory::Theory::theoryOf(atom
[0]);
275 Debug("theory") << "asserting " << node
<< " to " << theoryLHS
<< std::endl
;
276 d_theoryTable
[theoryLHS
]->assertFact(node
);
277 // theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]);
278 // if (theoryLHS != theoryRHS) {
279 // Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl;
280 // d_theoryTable[theoryRHS]->assertFact(node);
282 // theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType());
283 // if (typeTheory!= theoryLHS && typeTheory != theoryRHS) {
284 // Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl;
285 // d_theoryTable[typeTheory]->assertFact(node);
288 theory::Theory
* theory
= theoryOf(atom
);
289 Debug("theory") << "asserting " << node
<< " to " << theory
->getId() << std::endl
;
290 theory
->assertFact(node
);
295 * Check all (currently-active) theories for conflicts.
296 * @param effort the effort level to use
298 bool check(theory::Theory::Effort effort
);
301 * Calls staticLearning() on all active theories, accumulating their
302 * combined contributions in the "learned" builder.
304 void staticLearning(TNode in
, NodeBuilder
<>& learned
);
307 * Calls presolve() on all active theories and returns true
308 * if one of the theories discovers a conflict.
313 * Calls notifyRestart() on all active theories.
315 void notifyRestart();
317 inline const std::vector
<TNode
>& getPropagatedLiterals() const {
318 return d_theoryOut
.d_propagatedLiterals
;
321 void clearPropagatedLiterals() {
322 d_theoryOut
.d_propagatedLiterals
.clear();
325 inline void newLemma(TNode node
) {
326 d_propEngine
->assertLemma(preprocess(node
));
330 * Returns the last conflict (if any).
332 inline Node
getConflict() {
333 return d_theoryOut
.d_conflictNode
;
338 inline Node
getExplanation(TNode node
, theory::Theory
* theory
) {
339 theory
->explain(node
);
340 return d_theoryOut
.d_explanationNode
;
343 inline Node
getExplanation(TNode node
) {
344 d_theoryOut
.d_explanationNode
= Node::null();
345 TNode atom
= node
.getKind() == kind::NOT
? node
[0] : node
;
346 if (atom
.getKind() == kind::EQUAL
) {
347 theoryOf(atom
[0])->explain(node
);
349 theoryOf(atom
)->explain(node
);
351 Assert(!d_theoryOut
.d_explanationNode
.get().isNull());
352 return d_theoryOut
.d_explanationNode
;
355 Node
getValue(TNode node
);
360 IntStat d_statConflicts
, d_statPropagate
, d_statLemma
, d_statAugLemma
, d_statExplanation
;
362 d_statConflicts("theory::conflicts", 0),
363 d_statPropagate("theory::propagate", 0),
364 d_statLemma("theory::lemma", 0),
365 d_statAugLemma("theory::aug_lemma", 0),
366 d_statExplanation("theory::explanation", 0)
368 StatisticsRegistry::registerStat(&d_statConflicts
);
369 StatisticsRegistry::registerStat(&d_statPropagate
);
370 StatisticsRegistry::registerStat(&d_statLemma
);
371 StatisticsRegistry::registerStat(&d_statAugLemma
);
372 StatisticsRegistry::registerStat(&d_statExplanation
);
376 StatisticsRegistry::unregisterStat(&d_statConflicts
);
377 StatisticsRegistry::unregisterStat(&d_statPropagate
);
378 StatisticsRegistry::unregisterStat(&d_statLemma
);
379 StatisticsRegistry::unregisterStat(&d_statAugLemma
);
380 StatisticsRegistry::unregisterStat(&d_statExplanation
);
383 Statistics d_statistics
;
385 };/* class TheoryEngine */
387 }/* CVC4 namespace */
389 #endif /* __CVC4__THEORY_ENGINE_H */