1 /********************* */
2 /*! \file theory_engine.h
4 ** Original author: mdeters
5 ** Major contributors: dejan, taking
6 ** Minor contributors (to current version): cconway
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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
24 #include "expr/node.h"
25 #include "theory/theory.h"
26 #include "theory/theoryof_table.h"
28 #include "prop/prop_engine.h"
29 #include "theory/shared_term_manager.h"
30 #include "theory/builtin/theory_builtin.h"
31 #include "theory/booleans/theory_bool.h"
32 #include "theory/uf/theory_uf.h"
33 #include "theory/uf/tim/theory_uf_tim.h"
34 #include "theory/uf/morgan/theory_uf_morgan.h"
35 #include "theory/arith/theory_arith.h"
36 #include "theory/arrays/theory_arrays.h"
37 #include "theory/bv/theory_bv.h"
39 #include "util/options.h"
40 #include "util/stats.h"
44 // In terms of abstraction, this is below (and provides services to)
48 * This is essentially an abstraction for a collection of theories. A
49 * TheoryEngine provides services to a PropEngine, making various
50 * T-solvers look like a single unit to the propositional part of
55 /** Associated PropEngine engine */
56 prop::PropEngine
* d_propEngine
;
58 /** A table of Kinds to pointers to Theory */
59 theory::TheoryOfTable d_theoryOfTable
;
61 /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
63 /** The "registerTerm()-has-been-called" flag on Nodes */
64 typedef CVC4::expr::CDAttribute
<Registered
, bool> RegisteredAttr
;
67 * An output channel for Theory that passes messages
68 * back to a TheoryEngine.
70 class EngineOutputChannel
: public theory::OutputChannel
{
72 friend class TheoryEngine
;
74 TheoryEngine
* d_engine
;
75 context::Context
* d_context
;
76 context::CDO
<Node
> d_conflictNode
;
77 context::CDO
<Node
> d_explanationNode
;
80 * Literals that are propagated by the theory. Note that these are TNodes.
81 * The theory can only propagate nodes that have an assigned literal in the
82 * sat solver and are hence referenced in the SAT solver.
84 std::vector
<TNode
> d_propagatedLiterals
;
88 EngineOutputChannel(TheoryEngine
* engine
, context::Context
* context
) :
91 d_conflictNode(context
),
92 d_explanationNode(context
){
95 void newFact(TNode n
);
97 void conflict(TNode conflictNode
, bool safe
) throw(theory::Interrupted
, AssertionException
) {
98 Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode
<< ")" << std::endl
;
99 d_conflictNode
= conflictNode
;
100 ++(d_engine
->d_statistics
.d_statConflicts
);
102 throw theory::Interrupted();
106 void propagate(TNode lit
, bool) throw(theory::Interrupted
, AssertionException
) {
107 d_propagatedLiterals
.push_back(lit
);
108 ++(d_engine
->d_statistics
.d_statPropagate
);
111 void lemma(TNode node
, bool) throw(theory::Interrupted
, AssertionException
) {
112 ++(d_engine
->d_statistics
.d_statLemma
);
113 d_engine
->newLemma(node
);
115 void augmentingLemma(TNode node
, bool) throw(theory::Interrupted
, AssertionException
) {
116 ++(d_engine
->d_statistics
.d_statAugLemma
);
117 d_engine
->newAugmentingLemma(node
);
119 void explanation(TNode explanationNode
, bool) throw(theory::Interrupted
, AssertionException
) {
120 d_explanationNode
= explanationNode
;
121 ++(d_engine
->d_statistics
.d_statExplanation
);
127 EngineOutputChannel d_theoryOut
;
129 /** Pointer to Shared Term Manager */
130 SharedTermManager
* d_sharedTermManager
;
132 theory::builtin::TheoryBuiltin
* d_builtin
;
133 theory::booleans::TheoryBool
* d_bool
;
134 theory::uf::TheoryUF
* d_uf
;
135 theory::arith::TheoryArith
* d_arith
;
136 theory::arrays::TheoryArrays
* d_arrays
;
137 theory::bv::TheoryBV
* d_bv
;
140 * Debugging flag to ensure that shutdown() is called before the
146 * Check whether a node is in the pre-rewrite cache or not.
148 static bool inPreRewriteCache(TNode n
, bool topLevel
) throw() {
149 return theory::Theory::inPreRewriteCache(n
, topLevel
);
153 * Get the value of the pre-rewrite cache (or Node::null()) if there is
156 static Node
getPreRewriteCache(TNode n
, bool topLevel
) throw() {
157 return theory::Theory::getPreRewriteCache(n
, topLevel
);
161 * Set the value of the pre-rewrite cache. v cannot be a null Node.
163 static void setPreRewriteCache(TNode n
, bool topLevel
, TNode v
) throw() {
164 return theory::Theory::setPreRewriteCache(n
, topLevel
, v
);
168 * Check whether a node is in the post-rewrite cache or not.
170 static bool inPostRewriteCache(TNode n
, bool topLevel
) throw() {
171 return theory::Theory::inPostRewriteCache(n
, topLevel
);
175 * Get the value of the post-rewrite cache (or Node::null()) if there is
178 static Node
getPostRewriteCache(TNode n
, bool topLevel
) throw() {
179 return theory::Theory::getPostRewriteCache(n
, topLevel
);
183 * Set the value of the post-rewrite cache. v cannot be a null Node.
185 static void setPostRewriteCache(TNode n
, bool topLevel
, TNode v
) throw() {
186 return theory::Theory::setPostRewriteCache(n
, topLevel
, v
);
190 * This is the top rewrite entry point, called during preprocessing.
191 * It dispatches to the proper theories to rewrite the given Node.
193 Node
rewrite(TNode in
, bool topLevel
= true);
196 * Replace ITE forms in a node.
198 Node
removeITEs(TNode t
);
203 * Construct a theory engine.
205 TheoryEngine(context::Context
* ctxt
, const Options
* opts
) :
207 d_theoryOut(this, ctxt
),
208 d_hasShutDown(false),
211 d_sharedTermManager
= new SharedTermManager(this, ctxt
);
213 d_builtin
= new theory::builtin::TheoryBuiltin(0, ctxt
, d_theoryOut
);
214 d_bool
= new theory::booleans::TheoryBool(1, ctxt
, d_theoryOut
);
215 switch(opts
->uf_implementation
) {
217 d_uf
= new theory::uf::tim::TheoryUFTim(2, ctxt
, d_theoryOut
);
219 case Options::MORGAN
:
220 d_uf
= new theory::uf::morgan::TheoryUFMorgan(2, ctxt
, d_theoryOut
);
223 Unhandled(opts
->uf_implementation
);
225 d_arith
= new theory::arith::TheoryArith(3, ctxt
, d_theoryOut
);
226 d_arrays
= new theory::arrays::TheoryArrays(4, ctxt
, d_theoryOut
);
227 d_bv
= new theory::bv::TheoryBV(5, ctxt
, d_theoryOut
);
229 d_sharedTermManager
->registerTheory(d_builtin
);
230 d_sharedTermManager
->registerTheory(d_bool
);
231 d_sharedTermManager
->registerTheory(d_uf
);
232 d_sharedTermManager
->registerTheory(d_arith
);
233 d_sharedTermManager
->registerTheory(d_arrays
);
234 d_sharedTermManager
->registerTheory(d_bv
);
236 d_theoryOfTable
.registerTheory(d_builtin
);
237 d_theoryOfTable
.registerTheory(d_bool
);
238 d_theoryOfTable
.registerTheory(d_uf
);
239 d_theoryOfTable
.registerTheory(d_arith
);
240 d_theoryOfTable
.registerTheory(d_arrays
);
241 d_theoryOfTable
.registerTheory(d_bv
);
245 Assert(d_hasShutDown
);
254 delete d_sharedTermManager
;
257 SharedTermManager
* getSharedTermManager() {
258 return d_sharedTermManager
;
261 void setPropEngine(prop::PropEngine
* propEngine
) {
262 Assert(d_propEngine
== NULL
);
263 d_propEngine
= propEngine
;
267 * This is called at shutdown time by the SmtEngine, just before
268 * destruction. It is important because there are destruction
269 * ordering issues between PropEngine and Theory.
272 // Set this first; if a Theory shutdown() throws an exception,
273 // at least the destruction of the TheoryEngine won't confound
275 d_hasShutDown
= true;
277 d_builtin
->shutdown();
281 d_arrays
->shutdown();
286 * Get the theory associated to a given TypeNode.
288 * @returns the theory owning the type
290 theory::Theory
* theoryOf(TypeNode t
);
293 * Get the theory associated to a given Node.
295 * @returns the theory, or NULL if the TNode is
298 theory::Theory
* theoryOf(TNode n
);
301 * Preprocess a node. This involves theory-specific rewriting, then
302 * calling preRegisterTerm() on what's left over.
303 * @param n the node to preprocess
305 Node
preprocess(TNode n
);
308 * Assert the formula to the apropriate theory.
309 * @param node the assertion
311 inline void assertFact(TNode node
) {
312 Debug("theory") << "TheoryEngine::assertFact(" << node
<< ")" << std::endl
;
313 theory::Theory
* theory
=
314 node
.getKind() == kind::NOT
? theoryOf(node
[0]) : theoryOf(node
);
316 theory
->assertFact(node
);
321 * Check all (currently-active) theories for conflicts.
322 * @param effort the effort level to use
324 inline bool check(theory::Theory::Effort effort
)
326 d_theoryOut
.d_conflictNode
= Node::null();
327 d_theoryOut
.d_propagatedLiterals
.clear();
330 //d_builtin->check(effort);
331 //d_bool->check(effort);
333 d_arith
->check(effort
);
334 d_arrays
->check(effort
);
336 } catch(const theory::Interrupted
&) {
337 Debug("theory") << "TheoryEngine::check() => conflict" << std::endl
;
339 // Return wheather we have a conflict
340 return d_theoryOut
.d_conflictNode
.get().isNull();
343 inline const std::vector
<TNode
>& getPropagatedLiterals() const {
344 return d_theoryOut
.d_propagatedLiterals
;
347 void clearPropagatedLiterals() {
348 d_theoryOut
.d_propagatedLiterals
.clear();
351 inline void newLemma(TNode node
) {
352 d_propEngine
->assertLemma(node
);
355 inline void newAugmentingLemma(TNode node
) {
356 Node preprocessed
= preprocess(node
);
357 d_propEngine
->assertFormula(preprocessed
);
361 * Returns the last conflict (if any).
363 inline Node
getConflict() {
364 return d_theoryOut
.d_conflictNode
;
367 inline void propagate() {
368 d_theoryOut
.d_propagatedLiterals
.clear();
369 // Do the propagation
370 //d_builtin->propagate(theory::Theory::FULL_EFFORT);
371 //d_bool->propagate(theory::Theory::FULL_EFFORT);
372 d_uf
->propagate(theory::Theory::FULL_EFFORT
);
373 d_arith
->propagate(theory::Theory::FULL_EFFORT
);
374 d_arrays
->propagate(theory::Theory::FULL_EFFORT
);
375 //d_bv->propagate(theory::Theory::FULL_EFFORT);
378 inline Node
getExplanation(TNode node
, theory::Theory
* theory
) {
379 theory
->explain(node
);
380 return d_theoryOut
.d_explanationNode
;
383 inline Node
getExplanation(TNode node
){
384 d_theoryOut
.d_explanationNode
= Node::null();
385 theory::Theory
* theory
=
386 node
.getKind() == kind::NOT
? theoryOf(node
[0]) : theoryOf(node
);
387 theory
->explain(node
);
388 return d_theoryOut
.d_explanationNode
;
394 IntStat d_statConflicts
, d_statPropagate
, d_statLemma
, d_statAugLemma
, d_statExplanation
;
396 d_statConflicts("theory::conflicts",0),
397 d_statPropagate("theory::propagate",0),
398 d_statLemma("theory::lemma",0),
399 d_statAugLemma("theory::aug_lemma", 0),
400 d_statExplanation("theory::explanation", 0)
402 StatisticsRegistry::registerStat(&d_statConflicts
);
403 StatisticsRegistry::registerStat(&d_statPropagate
);
404 StatisticsRegistry::registerStat(&d_statLemma
);
405 StatisticsRegistry::registerStat(&d_statAugLemma
);
406 StatisticsRegistry::registerStat(&d_statExplanation
);
410 StatisticsRegistry::unregisterStat(&d_statConflicts
);
411 StatisticsRegistry::unregisterStat(&d_statPropagate
);
412 StatisticsRegistry::unregisterStat(&d_statLemma
);
413 StatisticsRegistry::unregisterStat(&d_statAugLemma
);
414 StatisticsRegistry::unregisterStat(&d_statExplanation
);
417 Statistics d_statistics
;
419 };/* class TheoryEngine */
421 }/* CVC4 namespace */
423 #endif /* __CVC4__THEORY_ENGINE_H */