da161097fc565e91043eab21482ce2ce2b7bd5d7
1 /********************* */
2 /*! \file theory_engine.cpp
4 ** Original author: mdeters
5 ** Major contributors: taking
6 ** Minor contributors (to current version): none
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 "theory/theory_engine.h"
20 #include "expr/node.h"
21 #include "expr/attribute.h"
22 #include "theory/theory.h"
23 #include "expr/node_builder.h"
31 using namespace CVC4::theory
;
36 struct PreRegisteredTag
{};
37 typedef expr::Attribute
<PreRegisteredTag
, bool> PreRegistered
;
39 struct IteRewriteTag
{};
40 typedef expr::Attribute
<IteRewriteTag
, Node
> IteRewriteAttr
;
42 }/* CVC4::theory namespace */
44 void TheoryEngine::EngineOutputChannel::newFact(TNode fact
) {
45 //FIXME: Assert(fact.isLiteral(), "expected literal");
46 if (fact
.getKind() == kind::NOT
) {
47 // No need to register negations - only atoms
49 // FIXME: In future, might want to track disequalities in shared term manager
50 // if (fact.getKind() == kind::EQUAL) {
51 // d_engine->getSharedTermManager()->addDiseq(fact);
54 else if (fact
.getKind() == kind::EQUAL
) {
55 // Automatically track all asserted equalities in the shared term manager
56 d_engine
->getSharedTermManager()->addEq(fact
);
58 if(! fact
.getAttribute(RegisteredAttr())) {
60 toReg
.push_back(fact
);
62 Debug("theory") << "Theory::get(): registering new atom" << endl
;
64 /* Essentially this is doing a breadth-first numbering of
65 * non-registered subterms with children. Any non-registered
66 * leaves are immediately registered. */
67 for(list
<TNode
>::iterator workp
= toReg
.begin();
72 Theory
* thParent
= d_engine
->theoryOf(n
);
74 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
76 Theory
* thChild
= d_engine
->theoryOf(c
);
78 if (thParent
!= thChild
) {
79 d_engine
->getSharedTermManager()->addTerm(c
, thParent
, thChild
);
81 if(! c
.getAttribute(RegisteredAttr())) {
82 if(c
.getNumChildren() == 0) {
83 c
.setAttribute(RegisteredAttr(), true);
84 thChild
->registerTerm(c
);
92 /* Now register the list of terms in reverse order. Between this
93 * and the above registration of leaves, this should ensure that
94 * all subterms in the entire tree were registered in
95 * reverse-topological order. */
96 for(list
<TNode
>::reverse_iterator i
= toReg
.rbegin();
102 /* Note that a shared TNode in the DAG rooted at "fact" could
103 * appear twice on the list, so we have to avoid hitting it
105 // FIXME when ExprSets are online, use one of those to avoid
106 // duplicates in the above?
107 // Actually, that doesn't work because you have to make sure
108 // that the *last* occurrence is the one that gets processed first @CB
109 // This could be a big performance problem though because it requires
110 // traversing a DAG as a tree and that can really blow up @CB
111 if(! n
.getAttribute(RegisteredAttr())) {
112 n
.setAttribute(RegisteredAttr(), true);
113 d_engine
->theoryOf(n
)->registerTerm(n
);
120 Theory
* TheoryEngine::theoryOf(TypeNode t
) {
121 // FIXME: we don't yet have a Type-to-Theory map. When we do,
122 // look up the type of the var and return that Theory (?)
124 // The following JUST hacks around this lack of a table
125 Kind k
= t
.getKind();
126 if(k
== kind::TYPE_CONSTANT
) {
127 switch(TypeConstant tc
= t
.getConst
<TypeConstant
>()) {
129 return d_theoryOfTable
[kind::CONST_BOOLEAN
];
131 return d_theoryOfTable
[kind::CONST_INTEGER
];
133 return d_theoryOfTable
[kind::CONST_RATIONAL
];
140 return d_theoryOfTable
[k
];
144 Theory
* TheoryEngine::theoryOf(TNode n
) {
145 Kind k
= n
.getKind();
147 Assert(k
>= 0 && k
< kind::LAST_KIND
);
149 if(n
.getMetaKind() == kind::metakind::VARIABLE
) {
150 return theoryOf(n
.getType());
151 } else if(k
== kind::EQUAL
) {
152 // equality is special: use LHS
153 return theoryOf(n
[0]);
155 // use our Kind-to-Theory mapping
156 return d_theoryOfTable
[k
];
160 Node
TheoryEngine::preprocess(TNode t
) {
161 Node top
= rewrite(t
);
162 Debug("rewrite") << "rewrote: " << t
<< endl
<< "to : " << top
<< endl
;
165 toReg
.push_back(top
);
167 /* Essentially this is doing a breadth-first numbering of
168 * non-registered subterms with children. Any non-registered
169 * leaves are immediately registered. */
170 for(list
<TNode
>::iterator workp
= toReg
.begin();
171 workp
!= toReg
.end();
176 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
179 if(!c
.getAttribute(theory::PreRegistered())) {// c not yet registered
180 if(c
.getNumChildren() == 0) {
181 c
.setAttribute(theory::PreRegistered(), true);
182 theoryOf(c
)->preRegisterTerm(c
);
190 /* Now register the list of terms in reverse order. Between this
191 * and the above registration of leaves, this should ensure that
192 * all subterms in the entire tree were registered in
193 * reverse-topological order. */
194 for(list
<TNode
>::reverse_iterator i
= toReg
.rbegin();
200 /* Note that a shared TNode in the DAG rooted at "fact" could
201 * appear twice on the list, so we have to avoid hitting it
203 // FIXME when ExprSets are online, use one of those to avoid
204 // duplicates in the above?
205 if(!n
.getAttribute(theory::PreRegistered())) {
206 n
.setAttribute(theory::PreRegistered(), true);
207 theoryOf(n
)->preRegisterTerm(n
);
214 /* Our goal is to tease out any ITE's sitting under a theory operator. */
215 Node
TheoryEngine::removeITEs(TNode node
) {
216 Debug("ite") << "removeITEs(" << node
<< ")" << endl
;
218 /* The result may be cached already */
220 NodeManager
*nodeManager
= NodeManager::currentNM();
221 if(nodeManager
->getAttribute(node
, theory::IteRewriteAttr(), cachedRewrite
)) {
222 Debug("ite") << "removeITEs: in-cache: " << cachedRewrite
<< endl
;
223 return cachedRewrite
.isNull() ? Node(node
) : cachedRewrite
;
226 if(node
.getKind() == kind::ITE
){
227 Assert( node
.getNumChildren() == 3 );
228 TypeNode nodeType
= node
[1].getType();
229 if(!nodeType
.isBoolean()){
230 Node skolem
= nodeManager
->mkVar(node
.getType());
232 nodeManager
->mkNode(kind::ITE
,
234 nodeManager
->mkNode(kind::EQUAL
, skolem
, node
[1]),
235 nodeManager
->mkNode(kind::EQUAL
, skolem
, node
[2]));
236 nodeManager
->setAttribute(node
, theory::IteRewriteAttr(), skolem
);
238 Debug("ite") << "removeITEs([" << node
.getId() << "," << node
<< "])"
240 << "["<<newAssertion
.getId() << "," << newAssertion
<< "]"
243 Node preprocessed
= preprocess(newAssertion
);
244 d_propEngine
->assertFormula(preprocessed
);
249 vector
<Node
> newChildren
;
250 bool somethingChanged
= false;
251 for(TNode::const_iterator it
= node
.begin(), end
= node
.end();
254 Node newChild
= removeITEs(*it
);
255 somethingChanged
|= (newChild
!= *it
);
256 newChildren
.push_back(newChild
);
259 if(somethingChanged
) {
260 cachedRewrite
= nodeManager
->mkNode(node
.getKind(), newChildren
);
261 nodeManager
->setAttribute(node
, theory::IteRewriteAttr(), cachedRewrite
);
262 return cachedRewrite
;
264 nodeManager
->setAttribute(node
, theory::IteRewriteAttr(), Node::null());
273 * TheoryEngine::rewrite() keeps a stack of things that are being pre-
274 * and post-rewritten. Each element of the stack is a
275 * RewriteStackElement.
277 struct RewriteStackElement
{
279 * The node at this rewrite level. For example (AND (OR x y) z)
280 * will have, as it's rewriting x, the stack:
288 * The theory associated to d_node. Cached here to avoid having to
294 * Whether or not this was a top-level rewrite. Note that at theory
295 * boundaries, topLevel is forced to true, so it's not the case that
296 * this is true only at the lowest stack level.
301 * A saved index to the "next child" to pre- and post-rewrite. In
302 * the case when (AND (OR x y) z) is being rewritten, the AND, OR,
303 * and x are pre-rewritten, then (assuming they don't change), x is
304 * post-rewritten, then y is pre- and post-rewritten, then the OR is
305 * post-rewritten, then z is pre-rewritten, then the AND is
306 * post-rewritten. At each stack level, we need to remember the
307 * child index we're currently processing.
312 * A (re)builder for this node. As this node's children are
313 * post-rewritten, in order, they append to this builder. When this
314 * node is post-rewritten, it is reformed from d_builder since the
315 * children may have changed. Note Nodes aren't rebuilt if they
316 * have metakinds CONSTANT (which is illegal) or VARIABLE (which
317 * would create a fresh variable, not what we want)---which is fine,
318 * since those types don't have children anyway.
320 NodeBuilder
<> d_builder
;
323 * Construct a fresh stack element.
325 RewriteStackElement(Node n
, Theory
* thy
, bool topLevel
) :
328 d_topLevel(topLevel
),
333 }/* CVC4::theory::rewrite namespace */
334 }/* CVC4::theory namespace */
336 Node
TheoryEngine::rewrite(TNode in
, bool topLevel
) {
337 using theory::rewrite::RewriteStackElement
;
339 Node noItes
= removeITEs(in
);
342 Debug("theory-rewrite") << "removeITEs of: " << in
<< endl
343 << " is: " << noItes
<< endl
;
345 // descend top-down into the theory rewriters
346 vector
<RewriteStackElement
> stack
;
347 stack
.push_back(RewriteStackElement(noItes
, theoryOf(noItes
), topLevel
));
348 Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl
349 << " " << noItes
<< " " << theoryOf(noItes
)
350 << " " << (topLevel
? "TOP-LEVEL " : "")
352 // This whole thing is essentially recursive, but we avoid actually
353 // doing any recursion.
354 do {// do until the stack is empty..
355 RewriteStackElement
& rse
= stack
.back();
358 Debug("theory-rewrite") << "rewriter looking at level " << stack
.size()
360 << " " << rse
.d_node
<< " " << rse
.d_theory
361 << "[" << *rse
.d_theory
<< "]"
362 << " " << (rse
.d_topLevel
? "TOP-LEVEL " : "")
363 << rse
.d_nextChild
<< endl
;
365 if(rse
.d_nextChild
== 0) {
366 Node original
= rse
.d_node
;
367 bool wasTopLevel
= rse
.d_topLevel
;
368 Node cached
= getPreRewriteCache(original
, wasTopLevel
);
369 if(cached
.isNull()) {
371 Debug("theory-rewrite") << "doing pre-rewrite in " << *rse
.d_theory
372 << " topLevel==" << rse
.d_topLevel
<< endl
;
373 RewriteResponse response
=
374 rse
.d_theory
->preRewrite(rse
.d_node
, rse
.d_topLevel
);
375 rse
.d_node
= response
.getNode();
376 Assert(!rse
.d_node
.isNull(), "node illegally rewritten to null");
377 Theory
* thy2
= theoryOf(rse
.d_node
);
378 Assert(thy2
!= NULL
, "node illegally rewritten to null theory");
379 Debug("theory-rewrite") << "got back " << rse
.d_node
<< " "
380 << thy2
<< "[" << *thy2
<< "]"
381 << (response
.needsMoreRewriting() ?
382 (response
.needsFullRewriting() ?
383 " FULL-REWRITING" : " MORE-REWRITING")
386 if(rse
.d_theory
!= thy2
) {
387 Debug("theory-rewrite") << "pre-rewritten from " << *rse
.d_theory
389 << ", marking top-level and !done" << endl
;
392 // FIXME how to handle the "top-levelness" of a node that's
393 // rewritten from theory T1 into T2, then back to T1 ?
394 rse
.d_topLevel
= true;
396 done
= response
.isDone();
399 setPreRewriteCache(original
, wasTopLevel
, rse
.d_node
);
400 } else {// is in pre-rewrite cache
401 Debug("theory-rewrite") << "in pre-cache: " << cached
<< endl
;
403 Theory
* thy2
= theoryOf(cached
);
404 if(rse
.d_theory
!= thy2
) {
405 Debug("theory-rewrite") << "[cache-]pre-rewritten from "
406 << *rse
.d_theory
<< " into " << *thy2
407 << ", marking top-level" << endl
;
409 rse
.d_topLevel
= true;
415 Node original
= rse
.d_node
;
416 bool wasTopLevel
= rse
.d_topLevel
;
417 Node cached
= getPostRewriteCache(original
, wasTopLevel
);
419 if(cached
.isNull()) {
420 unsigned nch
= rse
.d_nextChild
++;
423 rse
.d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
424 // this is an apply, so we have to push the operator
425 TNode op
= rse
.d_node
.getOperator();
426 Debug("theory-rewrite") << "pushing operator " << op
427 << " of " << rse
.d_node
<< endl
;
431 if(nch
< rse
.d_node
.getNumChildren()) {
432 Debug("theory-rewrite") << "pushing child " << nch
433 << " of " << rse
.d_node
<< endl
;
434 Node c
= rse
.d_node
[nch
];
435 Theory
* t
= theoryOf(c
);
436 stack
.push_back(RewriteStackElement(c
, t
, t
!= rse
.d_theory
));
437 continue;// break out of this node, do its child
440 // incorporate the children's rewrites
441 if(rse
.d_node
.getMetaKind() != kind::metakind::VARIABLE
&&
442 rse
.d_node
.getMetaKind() != kind::metakind::CONSTANT
) {
443 Debug("theory-rewrite") << "builder here is " << &rse
.d_builder
444 << " and it gets " << rse
.d_node
.getKind()
446 rse
.d_builder
<< rse
.d_node
.getKind();
447 rse
.d_node
= Node(rse
.d_builder
);
452 Debug("theory-rewrite") << "doing post-rewrite of "
453 << rse
.d_node
<< endl
454 << " in " << *rse
.d_theory
455 << " topLevel==" << rse
.d_topLevel
<< endl
;
456 RewriteResponse response
=
457 rse
.d_theory
->postRewrite(rse
.d_node
, rse
.d_topLevel
);
458 rse
.d_node
= response
.getNode();
459 Assert(!rse
.d_node
.isNull(), "node illegally rewritten to null");
460 Theory
* thy2
= theoryOf(rse
.d_node
);
461 Assert(thy2
!= NULL
, "node illegally rewritten to null theory");
462 Debug("theory-rewrite") << "got back " << rse
.d_node
<< " "
463 << thy2
<< "[" << *thy2
<< "]"
464 << (response
.needsMoreRewriting() ?
465 (response
.needsFullRewriting() ?
466 " FULL-REWRITING" : " MORE-REWRITING")
469 if(rse
.d_theory
!= thy2
) {
470 Debug("theory-rewrite") << "post-rewritten from " << *rse
.d_theory
472 << ", marking top-level and !done" << endl
;
475 // FIXME how to handle the "top-levelness" of a node that's
476 // rewritten from theory T1 into T2, then back to T1 ?
477 rse
.d_topLevel
= true;
479 done
= response
.isDone();
481 if(response
.needsFullRewriting()) {
482 Debug("theory-rewrite") << "full-rewrite requested for node "
483 << rse
.d_node
.getId() << ", invoking..."
485 Node n
= rewrite(rse
.d_node
, rse
.d_topLevel
);
486 Debug("theory-rewrite") << "full-rewrite finished for node "
487 << rse
.d_node
.getId() << ", got node "
488 << n
<< " output." << endl
;
494 /* If extra-checking is on, do _another_ rewrite before putting
495 * in the cache to make sure they are the same. This is
496 * especially necessary if a theory post-rewrites something into
497 * a term of another theory. */
498 if(Debug
.isOn("extra-checking") &&
499 !Debug
.isOn("$extra-checking:inside-rewrite")) {
500 ScopedDebug
d("$extra-checking:inside-rewrite");
501 Node rewrittenAgain
= rewrite(rse
.d_node
, rse
.d_topLevel
);
502 Assert(rewrittenAgain
== rse
.d_node
,
503 "\nExtra-checking assumption failed, "
504 "node is not completely rewritten.\n\n"
508 original
.toString().c_str(),
509 rse
.d_node
.toString().c_str(),
510 rewrittenAgain
.toString().c_str());
512 setPostRewriteCache(original
, wasTopLevel
, rse
.d_node
);
516 Debug("theory-rewrite") << "in post-cache: " << cached
<< endl
;
518 Theory
* thy2
= theoryOf(cached
);
519 if(rse
.d_theory
!= thy2
) {
520 Debug("theory-rewrite") << "[cache-]post-rewritten from "
521 << *rse
.d_theory
<< " into " << *thy2
<< endl
;
528 Debug("theory-rewrite") << "asserting " << out
<< " to previous builder "
529 << &stack
.back().d_builder
<< endl
;
530 stack
.back().d_builder
<< out
;
532 } while(!stack
.empty());
534 Debug("theory-rewrite") << "DONE with theory rewriter." << endl
;
535 Debug("theory-rewrite") << "result is:" << endl
<< out
<< endl
;
538 }/* TheoryEngine::rewrite(TNode in) */
540 }/* CVC4 namespace */