src/theory/theory_engine.cpp

   1 /*********************                                                        */
   2 /*! \file theory_engine.cpp
   3  ** \verbatim
   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
  13  **
  14  ** \brief The theory engine.
  15  **
  16  ** The theory engine.
  17  **/
  18
  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"
  24
  25 #include <vector>
  26 #include <list>
  27
  28 using namespace std;
  29
  30 using namespace CVC4;
  31 using namespace CVC4::theory;
  32
  33 namespace CVC4 {
  34 namespace theory {
  35
  36 struct PreRegisteredTag {};
  37 typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
  38
  39 struct IteRewriteTag {};
  40 typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
  41
  42 }/* CVC4::theory namespace */
  43
  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
  48     fact = fact[0];
  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);
  52 //     }
  53   }
  54   else if (fact.getKind() == kind::EQUAL) {
  55     // Automatically track all asserted equalities in the shared term manager
  56     d_engine->getSharedTermManager()->addEq(fact);
  57   }
  58   if(! fact.getAttribute(RegisteredAttr())) {
  59     list<TNode> toReg;
  60     toReg.push_back(fact);
  61
  62     Debug("theory") << "Theory::get(): registering new atom" << endl;
  63
  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();
  68         workp != toReg.end();
  69         ++workp) {
  70
  71       TNode n = *workp;
  72       Theory* thParent = d_engine->theoryOf(n);
  73
  74       for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
  75         TNode c = *i;
  76         Theory* thChild = d_engine->theoryOf(c);
  77
  78         if (thParent != thChild) {
  79           d_engine->getSharedTermManager()->addTerm(c, thParent, thChild);
  80         }
  81         if(! c.getAttribute(RegisteredAttr())) {
  82           if(c.getNumChildren() == 0) {
  83             c.setAttribute(RegisteredAttr(), true);
  84             thChild->registerTerm(c);
  85           } else {
  86             toReg.push_back(c);
  87           }
  88         }
  89       }
  90     }
  91
  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();
  97         i != toReg.rend();
  98         ++i) {
  99
 100       TNode n = *i;
 101
 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
 104        * twice. */
 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);
 114       }
 115     }
 116   }
 117 }
 118
 119
 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 (?)
 123
 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>()) {
 128     case BOOLEAN_TYPE:
 129       return d_theoryOfTable[kind::CONST_BOOLEAN];
 130     case INTEGER_TYPE:
 131       return d_theoryOfTable[kind::CONST_INTEGER];
 132     case REAL_TYPE:
 133       return d_theoryOfTable[kind::CONST_RATIONAL];
 134     case KIND_TYPE:
 135     default:
 136       Unhandled(tc);
 137     }
 138   }
 139
 140   return d_theoryOfTable[k];
 141 }
 142
 143
 144 Theory* TheoryEngine::theoryOf(TNode n) {
 145   Kind k = n.getKind();
 146
 147   Assert(k >= 0 && k < kind::LAST_KIND);
 148
 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]);
 154   } else {
 155     // use our Kind-to-Theory mapping
 156     return d_theoryOfTable[k];
 157   }
 158 }
 159
 160 Node TheoryEngine::preprocess(TNode t) {
 161   Node top = rewrite(t);
 162   Debug("rewrite") << "rewrote: " << t << endl << "to     : " << top << endl;
 163
 164   list<TNode> toReg;
 165   toReg.push_back(top);
 166
 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();
 172       ++workp) {
 173
 174     TNode n = *workp;
 175
 176     for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
 177       TNode c = *i;
 178
 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);
 183         } else {
 184           toReg.push_back(c);
 185         }
 186       }
 187     }
 188   }
 189
 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();
 195       i != toReg.rend();
 196       ++i) {
 197
 198     TNode n = *i;
 199
 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
 202      * twice. */
 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);
 208     }
 209   }
 210
 211   return top;
 212 }
 213
 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;
 217
 218   /* The result may be cached already */
 219   Node cachedRewrite;
 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;
 224   }
 225
 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());
 231       Node newAssertion =
 232         nodeManager->mkNode(kind::ITE,
 233                             node[0],
 234                             nodeManager->mkNode(kind::EQUAL, skolem, node[1]),
 235                             nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
 236       nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
 237
 238       Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
 239                    << "->"
 240                    << "["<<newAssertion.getId() << "," << newAssertion << "]"
 241                    << endl;
 242
 243       Node preprocessed = preprocess(newAssertion);
 244       d_propEngine->assertFormula(preprocessed);
 245
 246       return skolem;
 247     }
 248   }
 249   vector<Node> newChildren;
 250   bool somethingChanged = false;
 251   for(TNode::const_iterator it = node.begin(), end = node.end();
 252       it != end;
 253       ++it) {
 254     Node newChild = removeITEs(*it);
 255     somethingChanged |= (newChild != *it);
 256     newChildren.push_back(newChild);
 257   }
 258
 259   if(somethingChanged) {
 260     cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
 261     nodeManager->setAttribute(node, theory::IteRewriteAttr(), cachedRewrite);
 262     return cachedRewrite;
 263   } else {
 264     nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null());
 265     return node;
 266   }
 267 }
 268
 269 namespace theory {
 270 namespace rewrite {
 271
 272 /**
 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.
 276  */
 277 struct RewriteStackElement {
 278   /**
 279    * The node at this rewrite level.  For example (AND (OR x y) z)
 280    * will have, as it's rewriting x, the stack:
 281    *    x
 282    *    (OR x y)
 283    *    (AND (OR x y) z)
 284    */
 285   Node d_node;
 286
 287   /**
 288    * The theory associated to d_node.  Cached here to avoid having to
 289    * look it up again.
 290    */
 291   Theory* d_theory;
 292
 293   /**
 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.
 297    */
 298   bool d_topLevel;
 299
 300   /**
 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.
 308    */
 309   int d_nextChild;
 310
 311   /**
 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.
 319    */
 320   NodeBuilder<> d_builder;
 321
 322   /**
 323    * Construct a fresh stack element.
 324    */
 325   RewriteStackElement(Node n, Theory* thy, bool topLevel) :
 326     d_node(n),
 327     d_theory(thy),
 328     d_topLevel(topLevel),
 329     d_nextChild(0) {
 330   }
 331 };
 332
 333 }/* CVC4::theory::rewrite namespace */
 334 }/* CVC4::theory namespace */
 335
 336 Node TheoryEngine::rewrite(TNode in, bool topLevel) {
 337   using theory::rewrite::RewriteStackElement;
 338
 339   Node noItes = removeITEs(in);
 340   Node out;
 341
 342   Debug("theory-rewrite") << "removeITEs of: " << in << endl
 343                           << "           is: " << noItes << endl;
 344
 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 " : "")
 351                           << "0" << endl;
 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();
 356     bool done;
 357
 358     Debug("theory-rewrite") << "rewriter looking at level " << stack.size()
 359                             << endl
 360                             << "  " << rse.d_node << " " << rse.d_theory
 361                             << "[" << *rse.d_theory << "]"
 362                             << " " << (rse.d_topLevel ? "TOP-LEVEL " : "")
 363                             << rse.d_nextChild << endl;
 364
 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()) {
 370         do {
 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")
 384                                       : " DONE")
 385                                   << endl;
 386           if(rse.d_theory != thy2) {
 387             Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory
 388                                     << " into " << *thy2
 389                                     << ", marking top-level and !done" << endl;
 390             rse.d_theory = thy2;
 391             done = false;
 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;
 395           } else {
 396             done = response.isDone();
 397           }
 398         } while(!done);
 399         setPreRewriteCache(original, wasTopLevel, rse.d_node);
 400       } else {// is in pre-rewrite cache
 401         Debug("theory-rewrite") << "in pre-cache: " << cached << endl;
 402         rse.d_node = cached;
 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;
 408           rse.d_theory = thy2;
 409           rse.d_topLevel = true;
 410         }
 411       }
 412     }
 413
 414     // children
 415     Node original = rse.d_node;
 416     bool wasTopLevel = rse.d_topLevel;
 417     Node cached = getPostRewriteCache(original, wasTopLevel);
 418
 419     if(cached.isNull()) {
 420       unsigned nch = rse.d_nextChild++;
 421
 422       if(nch == 0 &&
 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;
 428         rse.d_builder << op;
 429       }
 430
 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
 438       }
 439
 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()
 445                                 << endl;
 446         rse.d_builder << rse.d_node.getKind();
 447         rse.d_node = Node(rse.d_builder);
 448       }
 449
 450       // post-rewriting
 451       do {
 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")
 467                                     : " DONE")
 468                                 << endl;
 469         if(rse.d_theory != thy2) {
 470           Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory
 471                                   << " into " << *thy2
 472                                   << ", marking top-level and !done" << endl;
 473           rse.d_theory = thy2;
 474           done = false;
 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;
 478         } else {
 479           done = response.isDone();
 480         }
 481         if(response.needsFullRewriting()) {
 482           Debug("theory-rewrite") << "full-rewrite requested for node "
 483                                   << rse.d_node.getId() << ", invoking..."
 484                                   << endl;
 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;
 489           rse.d_node = n;
 490           done = true;
 491         }
 492       } while(!done);
 493
 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"
 505                "Original : %s\n"
 506                "Rewritten: %s\n"
 507                "Again    : %s\n",
 508                original.toString().c_str(),
 509                rse.d_node.toString().c_str(),
 510                rewrittenAgain.toString().c_str());
 511       }
 512       setPostRewriteCache(original, wasTopLevel, rse.d_node);
 513
 514       out = rse.d_node;
 515     } else {
 516       Debug("theory-rewrite") << "in post-cache: " << cached << endl;
 517       out = cached;
 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;
 522         rse.d_theory = thy2;
 523       }
 524     }
 525
 526     stack.pop_back();
 527     if(!stack.empty()) {
 528       Debug("theory-rewrite") << "asserting " << out << " to previous builder "
 529                               << &stack.back().d_builder << endl;
 530       stack.back().d_builder << out;
 531     }
 532   } while(!stack.empty());
 533
 534   Debug("theory-rewrite") << "DONE with theory rewriter." << endl;
 535   Debug("theory-rewrite") << "result is:" << endl << out << endl;
 536
 537   return out;
 538 }/* TheoryEngine::rewrite(TNode in) */
 539
 540 }/* CVC4 namespace */