src/expr/node_manager.cpp

   1 /*********************                                                        */
   2 /*! \file node_manager.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: cconway
   6  ** Minor contributors (to current version): acsys, taking, dejan
   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
  13  **
  14  ** \brief Expression manager implementation.
  15  **
  16  ** Expression manager implementation.
  17  **
  18  ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
  19  **/
  20
  21 #include "node_manager.h"
  22
  23 #include "theory/builtin/theory_builtin_type_rules.h"
  24 #include "theory/booleans/theory_bool_type_rules.h"
  25 #include "theory/uf/theory_uf_type_rules.h"
  26 #include "theory/arith/theory_arith_type_rules.h"
  27 #include "theory/arrays/theory_arrays_type_rules.h"
  28 #include "theory/bv/theory_bv_type_rules.h"
  29 #include "theory/datatypes/theory_datatypes_type_rules.h"
  30
  31 #include "util/Assert.h"
  32 #include "util/options.h"
  33 #include "util/stats.h"
  34 #include "util/tls.h"
  35
  36 #include <algorithm>
  37 #include <stack>
  38 #include <ext/hash_set>
  39
  40 using namespace std;
  41 using namespace CVC4::expr;
  42 using __gnu_cxx::hash_set;
  43
  44 namespace CVC4 {
  45
  46 CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL;
  47
  48 /**
  49  * This class sets it reference argument to true and ensures that it gets set
  50  * to false on destruction. This can be used to make sure a flag gets toggled
  51  * in a function even on exceptional exit (e.g., see reclaimZombies()).
  52  */
  53 struct ScopedBool {
  54   bool& d_value;
  55
  56   ScopedBool(bool& value) :
  57     d_value(value) {
  58
  59     Debug("gc") << ">> setting ScopedBool\n";
  60     d_value = true;
  61   }
  62
  63   ~ScopedBool() {
  64     Debug("gc") << "<< clearing ScopedBool\n";
  65     d_value = false;
  66   }
  67 };
  68
  69 /**
  70  * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on
  71  * exceptional exit from NodeManager::reclaimZombies().
  72  */
  73 struct NVReclaim {
  74   NodeValue*& d_deletionField;
  75
  76   NVReclaim(NodeValue*& deletionField) :
  77     d_deletionField(deletionField) {
  78
  79     Debug("gc") << ">> setting NVRECLAIM field\n";
  80   }
  81
  82   ~NVReclaim() {
  83     Debug("gc") << "<< clearing NVRECLAIM field\n";
  84     d_deletionField = NULL;
  85   }
  86 };
  87
  88 NodeManager::NodeManager(context::Context* ctxt,
  89                          ExprManager* exprManager) :
  90   d_optionsAllocated(new Options()),
  91   d_options(d_optionsAllocated),
  92   d_statisticsRegistry(new StatisticsRegistry()),
  93   d_attrManager(ctxt),
  94   d_exprManager(exprManager),
  95   d_nodeUnderDeletion(NULL),
  96   d_inReclaimZombies(false) {
  97   init();
  98 }
  99
 100
 101 NodeManager::NodeManager(context::Context* ctxt,
 102                          ExprManager* exprManager,
 103                          const Options& options) :
 104   d_optionsAllocated(NULL),
 105   d_options(&options),
 106   d_statisticsRegistry(new StatisticsRegistry()),
 107   d_attrManager(ctxt),
 108   d_exprManager(exprManager),
 109   d_nodeUnderDeletion(NULL),
 110   d_inReclaimZombies(false) {
 111   init();
 112 }
 113
 114 inline void NodeManager::init() {
 115   poolInsert( &expr::NodeValue::s_null );
 116
 117   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
 118     Kind k = Kind(i);
 119
 120     if(hasOperator(k)) {
 121       d_operators[i] = mkConst(Kind(k));
 122     }
 123   }
 124 }
 125
 126 NodeManager::~NodeManager() {
 127   // have to ensure "this" is the current NodeManager during
 128   // destruction of operators, because they get GCed.
 129
 130   NodeManagerScope nms(this);
 131
 132   {
 133     ScopedBool dontGC(d_inReclaimZombies);
 134     d_attrManager.deleteAllAttributes();
 135   }
 136
 137   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
 138     d_operators[i] = Node::null();
 139   }
 140
 141   while(!d_zombies.empty()) {
 142     reclaimZombies();
 143   }
 144
 145   poolRemove( &expr::NodeValue::s_null );
 146
 147   if(Debug.isOn("gc:leaks")) {
 148     Debug("gc:leaks") << "still in pool:" << std::endl;
 149     for(NodeValuePool::const_iterator i = d_nodeValuePool.begin(),
 150           iend = d_nodeValuePool.end();
 151         i != iend;
 152         ++i) {
 153       Debug("gc:leaks") << "  " << *i
 154                         << " id=" << (*i)->d_id
 155                         << " rc=" << (*i)->d_rc
 156                         << " " << **i << std::endl;
 157     }
 158     Debug("gc:leaks") << ":end:" << std::endl;
 159   }
 160
 161   delete d_statisticsRegistry;
 162   delete d_optionsAllocated;
 163 }
 164
 165 void NodeManager::reclaimZombies() {
 166   // FIXME multithreading
 167
 168   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
 169
 170   // during reclamation, reclaimZombies() is never supposed to be called
 171   Assert(! d_inReclaimZombies, "NodeManager::reclaimZombies() not re-entrant!");
 172
 173   // whether exit is normal or exceptional, the Reclaim dtor is called
 174   // and ensures that d_inReclaimZombies is set back to false.
 175   ScopedBool r(d_inReclaimZombies);
 176
 177   // We copy the set away and clear the NodeManager's set of zombies.
 178   // This is because reclaimZombie() decrements the RC of the
 179   // NodeValue's children, which may (recursively) reclaim them.
 180   //
 181   // Let's say we're reclaiming zombie NodeValue "A" and its child "B"
 182   // then becomes a zombie (NodeManager::markForDeletion(B) is called).
 183   //
 184   // One way to handle B's zombification would be simply to put it
 185   // into d_zombies.  This is what we do.  However, if we were to
 186   // concurrently process d_zombies in the loop below, such addition
 187   // may be invisible to us (B is leaked) or even invalidate our
 188   // iterator, causing a crash.  So we need to copy the set away.
 189
 190   vector<NodeValue*> zombies;
 191   zombies.reserve(d_zombies.size());
 192   std::remove_copy_if(d_zombies.begin(),
 193                       d_zombies.end(),
 194                       std::back_inserter(zombies),
 195                       NodeValueReferenceCountNonZero());
 196   d_zombies.clear();
 197
 198   for(vector<NodeValue*>::iterator i = zombies.begin();
 199       i != zombies.end();
 200       ++i) {
 201     NodeValue* nv = *i;
 202
 203     // collect ONLY IF still zero
 204     if(nv->d_rc == 0) {
 205       if(Debug.isOn("gc")) {
 206         Debug("gc") << "deleting node value " << nv
 207                     << " [" << nv->d_id << "]: ";
 208         nv->printAst(Debug("gc"));
 209         Debug("gc") << std::endl;
 210       }
 211
 212       // remove from the pool
 213       kind::MetaKind mk = nv->getMetaKind();
 214       if(mk != kind::metakind::VARIABLE) {
 215         poolRemove(nv);
 216       }
 217
 218       // whether exit is normal or exceptional, the NVReclaim dtor is
 219       // called and ensures that d_nodeUnderDeletion is set back to
 220       // NULL.
 221       NVReclaim rc(d_nodeUnderDeletion);
 222       d_nodeUnderDeletion = nv;
 223
 224       // remove attributes
 225       d_attrManager.deleteAllAttributes(nv);
 226
 227       // decr ref counts of children
 228       nv->decrRefCounts();
 229       if(mk == kind::metakind::CONSTANT) {
 230         // Destroy (call the destructor for) the C++ type representing
 231         // the constant in this NodeValue.  This is needed for
 232         // e.g. CVC4::Rational, since it has a gmp internal
 233         // representation that mallocs memory and should be cleaned
 234         // up.  (This won't delete a pointer value if used as a
 235         // constant, but then, you should probably use a smart-pointer
 236         // type for a constant payload.)
 237         kind::metakind::deleteNodeValueConstant(nv);
 238       }
 239       free(nv);
 240     }
 241   }
 242 }/* NodeManager::reclaimZombies() */
 243
 244 TypeNode NodeManager::computeType(TNode n, bool check)
 245   throw (TypeCheckingExceptionPrivate, AssertionException) {
 246   TypeNode typeNode;
 247
 248   // Infer the type
 249   switch(n.getKind()) {
 250   case kind::VARIABLE:
 251     typeNode = getAttribute(n, TypeAttr());
 252     break;
 253   case kind::SKOLEM:
 254     typeNode = getAttribute(n, TypeAttr());
 255     break;
 256   case kind::BUILTIN:
 257     typeNode = builtinOperatorType();
 258     break;
 259   case kind::SORT_TYPE:
 260     typeNode = kindType();
 261     break;
 262   case kind::APPLY:
 263     typeNode = CVC4::theory::builtin::ApplyTypeRule::computeType(this, n, check);
 264     break;
 265   case kind::EQUAL:
 266     typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n, check);
 267     break;
 268   case kind::DISTINCT:
 269     typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n, check);
 270     break;
 271   case kind::TUPLE:
 272     typeNode = CVC4::theory::builtin::TupleTypeRule::computeType(this, n, check);
 273     break;
 274   case kind::CONST_BOOLEAN:
 275     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 276     break;
 277   case kind::NOT:
 278     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 279     break;
 280   case kind::AND:
 281     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 282     break;
 283   case kind::IFF:
 284     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 285     break;
 286   case kind::IMPLIES:
 287     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 288     break;
 289   case kind::OR:
 290     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 291     break;
 292   case kind::XOR:
 293     typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
 294     break;
 295   case kind::ITE:
 296     typeNode = CVC4::theory::boolean::IteTypeRule::computeType(this, n, check);
 297     break;
 298   case kind::APPLY_UF:
 299     typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n, check);
 300     break;
 301   case kind::PLUS:
 302     typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
 303     break;
 304   case kind::MULT:
 305     typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
 306     break;
 307   case kind::MINUS:
 308     typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
 309     break;
 310   case kind::UMINUS:
 311     typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
 312     break;
 313   case kind::DIVISION:
 314     typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
 315     break;
 316   case kind::CONST_RATIONAL:
 317     typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n, check);
 318     break;
 319   case kind::CONST_INTEGER:
 320     typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n, check);
 321     break;
 322   case kind::LT:
 323     typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
 324     break;
 325   case kind::LEQ:
 326     typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
 327     break;
 328   case kind::GT:
 329     typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
 330     break;
 331   case kind::GEQ:
 332     typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check);
 333     break;
 334   case kind::SELECT:
 335     typeNode = CVC4::theory::arrays::ArraySelectTypeRule::computeType(this, n, check);
 336     break;
 337   case kind::STORE:
 338     typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n, check);
 339     break;
 340   case kind::CONST_BITVECTOR:
 341     typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n, check);
 342     break;
 343   case kind::BITVECTOR_AND:
 344     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 345     break;
 346   case kind::BITVECTOR_OR:
 347     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 348     break;
 349   case kind::BITVECTOR_XOR:
 350     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 351     break;
 352   case kind::BITVECTOR_NOT:
 353     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 354     break;
 355   case kind::BITVECTOR_NAND:
 356     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 357     break;
 358   case kind::BITVECTOR_NOR:
 359     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 360     break;
 361   case kind::BITVECTOR_XNOR:
 362     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 363     break;
 364   case kind::BITVECTOR_COMP:
 365     typeNode = CVC4::theory::bv::BitVectorCompRule::computeType(this, n, check);
 366     break;
 367   case kind::BITVECTOR_MULT:
 368     typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
 369     break;
 370   case kind::BITVECTOR_PLUS:
 371     typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
 372     break;
 373   case kind::BITVECTOR_SUB:
 374     typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
 375     break;
 376   case kind::BITVECTOR_NEG:
 377     typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check);
 378     break;
 379   case kind::BITVECTOR_UDIV:
 380     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 381     break;
 382   case kind::BITVECTOR_UREM:
 383     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 384     break;
 385   case kind::BITVECTOR_SDIV:
 386     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 387     break;
 388   case kind::BITVECTOR_SREM:
 389     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 390     break;
 391   case kind::BITVECTOR_SMOD:
 392     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 393     break;
 394   case kind::BITVECTOR_SHL:
 395     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 396     break;
 397   case kind::BITVECTOR_LSHR:
 398     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 399     break;
 400   case kind::BITVECTOR_ASHR:
 401     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 402     break;
 403   case kind::BITVECTOR_ROTATE_LEFT:
 404     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 405     break;
 406   case kind::BITVECTOR_ROTATE_RIGHT:
 407     typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check);
 408     break;
 409   case kind::BITVECTOR_ULT:
 410     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 411     break;
 412   case kind::BITVECTOR_ULE:
 413     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 414     break;
 415   case kind::BITVECTOR_UGT:
 416     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 417     break;
 418   case kind::BITVECTOR_UGE:
 419     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 420     break;
 421   case kind::BITVECTOR_SLT:
 422     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 423     break;
 424   case kind::BITVECTOR_SLE:
 425     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 426     break;
 427   case kind::BITVECTOR_SGT:
 428     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 429     break;
 430   case kind::BITVECTOR_SGE:
 431     typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check);
 432     break;
 433   case kind::BITVECTOR_EXTRACT:
 434     typeNode = CVC4::theory::bv::BitVectorExtractTypeRule::computeType(this, n, check);
 435     break;
 436   case kind::BITVECTOR_CONCAT:
 437     typeNode = CVC4::theory::bv::BitVectorConcatRule::computeType(this, n, check);
 438     break;
 439   case kind::BITVECTOR_REPEAT:
 440     typeNode = CVC4::theory::bv::BitVectorRepeatTypeRule::computeType(this, n, check);
 441     break;
 442   case kind::BITVECTOR_ZERO_EXTEND:
 443     typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
 444     break;
 445   case kind::BITVECTOR_SIGN_EXTEND:
 446     typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
 447     break;
 448   case kind::APPLY_CONSTRUCTOR:
 449     typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check);
 450     break;
 451   case kind::APPLY_SELECTOR:
 452     typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check);
 453     break;
 454   case kind::APPLY_TESTER:
 455     typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
 456     break;
 457   case kind::APPLY_TYPE_ASCRIPTION:
 458     typeNode = CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(this, n, check);
 459     break;
 460   default:
 461     Debug("getType") << "FAILURE" << std::endl;
 462     Unhandled(n.getKind());
 463   }
 464
 465   setAttribute(n, TypeAttr(), typeNode);
 466   setAttribute(n, TypeCheckedAttr(),
 467                check || getAttribute(n, TypeCheckedAttr()));
 468
 469   return typeNode;
 470 }
 471
 472 TypeNode NodeManager::getType(TNode n, bool check)
 473   throw (TypeCheckingExceptionPrivate, AssertionException) {
 474   // Many theories' type checkers call Node::getType() directly.
 475   // This is incorrect, since "this" might not be the caller's
 476   // curent node manager.  Rather than force the individual typecheckers
 477   // not to do this (by policy, which would be imperfect and lead
 478   // to hard-to-find bugs, which it has in the past), we just
 479   // set this node manager to be current for the duration of this
 480   // check.
 481   NodeManagerScope nms(this);
 482
 483   TypeNode typeNode;
 484   bool hasType = getAttribute(n, TypeAttr(), typeNode);
 485   bool needsCheck = check && !getAttribute(n, TypeCheckedAttr());
 486
 487   Debug("getType") << "getting type for " << n << std::endl;
 488
 489   if(needsCheck && !d_options->earlyTypeChecking) {
 490     /* Iterate and compute the children bottom up. This avoids stack
 491        overflows in computeType() when the Node graph is really deep,
 492        which should only affect us when we're type checking lazily. */
 493     stack<TNode> worklist;
 494     worklist.push(n);
 495
 496     while( !worklist.empty() ) {
 497       TNode m = worklist.top();
 498
 499       bool readyToCompute = true;
 500
 501       for( TNode::iterator it = m.begin(), end = m.end();
 502            it != end;
 503            ++it ) {
 504         if( !hasAttribute(*it, TypeAttr())
 505             || (check && !getAttribute(*it, TypeCheckedAttr())) ) {
 506           readyToCompute = false;
 507           worklist.push(*it);
 508         }
 509       }
 510
 511       if( readyToCompute ) {
 512         /* All the children have types, time to compute */
 513         typeNode = computeType(m, check);
 514         worklist.pop();
 515       }
 516     } // end while
 517
 518     /* Last type computed in loop should be the type of n */
 519     Assert( typeNode == getAttribute(n, TypeAttr()) );
 520   } else if( !hasType || needsCheck ) {
 521     /* We can compute the type top-down, without worrying about
 522        deep recursion. */
 523     typeNode = computeType(n, check);
 524   }
 525
 526   /* The type should be have been computed and stored. */
 527   Assert( hasAttribute(n, TypeAttr()) );
 528   /* The check should have happened, if we asked for it. */
 529   Assert( !check || getAttribute(n, TypeCheckedAttr()) );
 530
 531   Debug("getType") << "type of " << n << " is " << typeNode << std::endl;
 532   return typeNode;
 533 }
 534
 535 TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor,
 536                                         TypeNode range) {
 537   std::vector<TypeNode> sorts;
 538   Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
 539   for(Datatype::Constructor::const_iterator i = constructor.begin();
 540       i != constructor.end();
 541       ++i) {
 542     TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
 543     Debug("datatypes") << selectorType << std::endl;
 544     TypeNode sort = selectorType[1];
 545
 546     // should be guaranteed here already, but just in case
 547     Assert(!sort.isFunctionLike());
 548
 549     Debug("datatypes") << "ctor sort: " << sort << std::endl;
 550     sorts.push_back(sort);
 551   }
 552   Debug("datatypes") << "ctor range: " << range << std::endl;
 553   CheckArgument(!range.isFunctionLike(), range,
 554                 "cannot create higher-order function types");
 555   sorts.push_back(range);
 556   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 557 }
 558
 559 }/* CVC4 namespace */