src/expr/node_manager.h

   1 /*********************                                                        */
   2 /*! \file node_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Christopher L. Conway, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A manager for Nodes
  13  **
  14  ** A manager for Nodes.
  15  **
  16  ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 /* circular dependency; force node.h first */
  22 //#include "expr/attribute.h"
  23 #include "expr/node.h"
  24 #include "expr/type_node.h"
  25 #include "expr/expr.h"
  26 #include "expr/expr_manager.h"
  27
  28 #ifndef __CVC4__NODE_MANAGER_H
  29 #define __CVC4__NODE_MANAGER_H
  30
  31 #include <vector>
  32 #include <string>
  33 #include <unordered_set>
  34
  35 #include "base/tls.h"
  36 #include "expr/kind.h"
  37 #include "expr/metakind.h"
  38 #include "expr/node_value.h"
  39 #include "options/options.h"
  40
  41 namespace CVC4 {
  42
  43 class StatisticsRegistry;
  44 class ResourceManager;
  45
  46 namespace expr {
  47   namespace attr {
  48     class AttributeUniqueId;
  49     class AttributeManager;
  50   }/* CVC4::expr::attr namespace */
  51
  52   class TypeChecker;
  53 }/* CVC4::expr namespace */
  54
  55 /**
  56  * An interface that an interested party can implement and then subscribe
  57  * to NodeManager events via NodeManager::subscribeEvents(this).
  58  */
  59 class NodeManagerListener {
  60  public:
  61   virtual ~NodeManagerListener() {}
  62   virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {}
  63   virtual void nmNotifyNewSortConstructor(TypeNode tn) {}
  64   virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
  65                                                   uint32_t flags) {}
  66   virtual void nmNotifyNewDatatypes(
  67       const std::vector<DatatypeType>& datatypes) {}
  68   virtual void nmNotifyNewVar(TNode n, uint32_t flags) {}
  69   virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
  70                                  uint32_t flags) {}
  71   /**
  72    * Notify a listener of a Node that's being GCed.  If this function stores a
  73    * reference
  74    * to the Node somewhere, very bad things will happen.
  75    */
  76   virtual void nmNotifyDeleteNode(TNode n) {}
  77 }; /* class NodeManagerListener */
  78
  79 class NodeManager {
  80   template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
  81   friend class NodeManagerScope;
  82   friend class expr::NodeValue;
  83   friend class expr::TypeChecker;
  84
  85   // friends so they can access mkVar() here, which is private
  86   friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
  87   friend Expr ExprManager::mkVar(Type, uint32_t flags);
  88
  89   // friend so it can access NodeManager's d_listeners and notify clients
  90   friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>&, std::set<Type>&);
  91
  92   /** Predicate for use with STL algorithms */
  93   struct NodeValueReferenceCountNonZero {
  94     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
  95   };
  96
  97   typedef std::unordered_set<expr::NodeValue*,
  98                              expr::NodeValuePoolHashFunction,
  99                              expr::NodeValuePoolEq> NodeValuePool;
 100   typedef std::unordered_set<expr::NodeValue*,
 101                              expr::NodeValueIDHashFunction,
 102                              expr::NodeValueIDEquality> NodeValueIDSet;
 103
 104   static CVC4_THREAD_LOCAL NodeManager* s_current;
 105
 106   Options* d_options;
 107   StatisticsRegistry* d_statisticsRegistry;
 108
 109   ResourceManager* d_resourceManager;
 110
 111   /**
 112    * A list of registrations on d_options to that call into d_resourceManager.
 113    * These must be garbage collected before d_options and d_resourceManager.
 114    */
 115   ListenerRegistrationList* d_registrations;
 116
 117   NodeValuePool d_nodeValuePool;
 118
 119   size_t next_id;
 120
 121   expr::attr::AttributeManager* d_attrManager;
 122
 123   /** The associated ExprManager */
 124   ExprManager* d_exprManager;
 125
 126   /**
 127    * The node value we're currently freeing.  This unique node value
 128    * is permitted to have outstanding TNodes to it (in "soft"
 129    * contexts, like as a key in attribute tables), even though
 130    * normally it's an error to have a TNode to a node value with a
 131    * reference count of 0.  Being "under deletion" also enables
 132    * assertions that inc() is not called on it.  (A poorly-behaving
 133    * attribute cleanup function could otherwise create a "Node" that
 134    * points to the node value that is in the process of being deleted,
 135    * springing it back to life.)
 136    */
 137   expr::NodeValue* d_nodeUnderDeletion;
 138
 139   /**
 140    * True iff we are in reclaimZombies().  This avoids unnecessary
 141    * recursion; a NodeValue being deleted might zombify other
 142    * NodeValues, but these shouldn't trigger a (recursive) call to
 143    * reclaimZombies().
 144    */
 145   bool d_inReclaimZombies;
 146
 147   /**
 148    * The set of zombie nodes.  We may want to revisit this design, as
 149    * we might like to delete nodes in least-recently-used order.  But
 150    * we also need to avoid processing a zombie twice.
 151    */
 152   NodeValueIDSet d_zombies;
 153
 154   /**
 155    * NodeValues with maxed out reference counts. These live as long as the
 156    * NodeManager. They have a custom deallocation procedure at the very end.
 157    */
 158   std::vector<expr::NodeValue*> d_maxedOut;
 159
 160   /**
 161    * A set of operator singletons (w.r.t.  to this NodeManager
 162    * instance) for operators.  Conceptually, Nodes with kind, say,
 163    * PLUS, are APPLYs of a PLUS operator to arguments.  This array
 164    * holds the set of operators for these things.  A PLUS operator is
 165    * a Node with kind "BUILTIN", and if you call
 166    * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
 167    */
 168   Node d_operators[kind::LAST_KIND];
 169
 170   /** unique vars per (Kind,Type) */
 171   std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
 172
 173   /**
 174    * A list of subscribers for NodeManager events.
 175    */
 176   std::vector<NodeManagerListener*> d_listeners;
 177
 178   /** A list of datatypes owned by this node manager. */
 179   std::vector<Datatype*> d_ownedDatatypes;
 180
 181   /**
 182    * A map of tuple and record types to their corresponding datatype.
 183    */
 184   class TupleTypeCache {
 185   public:
 186     std::map< TypeNode, TupleTypeCache > d_children;
 187     TypeNode d_data;
 188     TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 );
 189   };
 190   class RecTypeCache {
 191   public:
 192     std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children;
 193     TypeNode d_data;
 194     TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 );
 195   };
 196   TupleTypeCache d_tt_cache;
 197   RecTypeCache d_rt_cache;
 198
 199   /**
 200    * Keep a count of all abstract values produced by this NodeManager.
 201    * Abstract values have a type attribute, so if multiple SmtEngines
 202    * are attached to this NodeManager, we don't want their abstract
 203    * values to overlap.
 204    */
 205   unsigned d_abstractValueCount;
 206
 207   /**
 208    * A counter used to produce unique skolem names.
 209    *
 210    * Note that it is NOT incremented when skolems are created using
 211    * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
 212    * by this node manager.
 213    */
 214   unsigned d_skolemCounter;
 215
 216   /**
 217    * Look up a NodeValue in the pool associated to this NodeManager.
 218    * The NodeValue argument need not be a "completely-constructed"
 219    * NodeValue.  In particular, "non-inlined" constants are permitted
 220    * (see below).
 221    *
 222    * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
 223    * correctly set, and d_children[0..n-1] should be valid (extant)
 224    * NodeValues for lookup.
 225    *
 226    * For CONSTANT metakinds, nv's d_kind should be set correctly.
 227    * Normally a CONSTANT would have d_nchildren == 0 and the constant
 228    * value inlined in the d_children space.  However, here we permit
 229    * "non-inlined" NodeValues to avoid unnecessary copying.  For
 230    * these, d_nchildren == 1, and d_nchildren is a pointer to the
 231    * constant value.
 232    *
 233    * The point of this complex design is to permit efficient lookups
 234    * (without fully constructing a NodeValue).  In the case that the
 235    * argument is not fully constructed, and this function returns
 236    * NULL, the caller should fully construct an equivalent one before
 237    * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
 238    * permitted in the pool!
 239    */
 240   inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
 241
 242   /**
 243    * Insert a NodeValue into the NodeManager's pool.
 244    *
 245    * It is an error to insert a NodeValue already in the pool.
 246    * Enquire first with poolLookup().
 247    */
 248   inline void poolInsert(expr::NodeValue* nv);
 249
 250   /**
 251    * Remove a NodeValue from the NodeManager's pool.
 252    *
 253    * It is an error to request the removal of a NodeValue from the
 254    * pool that is not in the pool.
 255    */
 256   inline void poolRemove(expr::NodeValue* nv);
 257
 258   /**
 259    * Determine if nv is currently being deleted by the NodeManager.
 260    */
 261   inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
 262     return d_nodeUnderDeletion == nv;
 263   }
 264
 265   /**
 266    * Register a NodeValue as a zombie.
 267    */
 268   inline void markForDeletion(expr::NodeValue* nv) {
 269     Assert(nv->d_rc == 0);
 270
 271     // if d_reclaiming is set, make sure we don't call
 272     // reclaimZombies(), because it's already running.
 273     if(Debug.isOn("gc")) {
 274       Debug("gc") << "zombifying node value " << nv
 275                   << " [" << nv->d_id << "]: ";
 276       nv->printAst(Debug("gc"));
 277       Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
 278                   << std::endl;
 279     }
 280     d_zombies.insert(nv);  // FIXME multithreading
 281
 282     if(safeToReclaimZombies()) {
 283       if(d_zombies.size() > 5000) {
 284         reclaimZombies();
 285       }
 286     }
 287   }
 288
 289   /**
 290    * Register a NodeValue as having a maxed out reference count. This NodeValue
 291    * will live as long as its containing NodeManager.
 292    */
 293   inline void markRefCountMaxedOut(expr::NodeValue* nv) {
 294     Assert(nv->HasMaximizedReferenceCount());
 295     if(Debug.isOn("gc")) {
 296       Debug("gc") << "marking node value " << nv
 297                   << " [" << nv->d_id << "]: as maxed out" << std::endl;
 298     }
 299     d_maxedOut.push_back(nv);
 300   }
 301
 302   /**
 303    * Reclaim all zombies.
 304    */
 305   void reclaimZombies();
 306
 307   /**
 308    * It is safe to collect zombies.
 309    */
 310   bool safeToReclaimZombies() const;
 311
 312   /**
 313    * Returns a reverse topological sort of a list of NodeValues. The NodeValues
 314    * must be valid and have ids. The NodeValues are not modified (including ref
 315    * counts).
 316    */
 317   static std::vector<expr::NodeValue*> TopologicalSort(
 318       const std::vector<expr::NodeValue*>& roots);
 319
 320   /**
 321    * This template gives a mechanism to stack-allocate a NodeValue
 322    * with enough space for N children (where N is a compile-time
 323    * constant).  You use it like this:
 324    *
 325    *   NVStorage<4> nvStorage;
 326    *   NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
 327    *
 328    * ...and then you can use nvStack as a NodeValue that you know has
 329    * room for 4 children.
 330    */
 331   template <size_t N>
 332   struct NVStorage {
 333     expr::NodeValue nv;
 334     expr::NodeValue* child[N];
 335   };/* struct NodeManager::NVStorage<N> */
 336
 337   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
 338    *
 339    * It has been decided for now to hold off on implementations of
 340    * these functions, as they may only be needed in CNF conversion,
 341    * where it's pointless to do a lazy isAtomic determination by
 342    * searching through the DAG, and storing it, since the result will
 343    * only be used once.  For more details see the 4/27/2010 CVC4
 344    * developer's meeting notes at:
 345    *
 346    * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
 347    */
 348   // bool containsDecision(TNode); // is "atomic"
 349   // bool properlyContainsDecision(TNode); // all children are atomic
 350
 351   // undefined private copy constructor (disallow copy)
 352   NodeManager(const NodeManager&) CVC4_UNDEFINED;
 353
 354   NodeManager& operator=(const NodeManager&) CVC4_UNDEFINED;
 355
 356   void init();
 357
 358   /**
 359    * Create a variable with the given name and type.  NOTE that no
 360    * lookup is done on the name.  If you mkVar("a", type) and then
 361    * mkVar("a", type) again, you have two variables.  The NodeManager
 362    * version of this is private to avoid internal uses of mkVar() from
 363    * within CVC4.  Such uses should employ mkSkolem() instead.
 364    */
 365   Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 366   Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 367
 368   /** Create a variable with the given type. */
 369   Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 370   Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 371
 372 public:
 373
 374   explicit NodeManager(ExprManager* exprManager);
 375   explicit NodeManager(ExprManager* exprManager, const Options& options);
 376   ~NodeManager();
 377
 378   /** The node manager in the current public-facing CVC4 library context */
 379   static NodeManager* currentNM() { return s_current; }
 380   /** The resource manager associated with the current node manager */
 381   static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
 382
 383   /** Get this node manager's options (const version) */
 384   const Options& getOptions() const {
 385     return *d_options;
 386   }
 387
 388   /** Get this node manager's options (non-const version) */
 389   Options& getOptions() {
 390     return *d_options;
 391   }
 392
 393   /** Get this node manager's resource manager */
 394   ResourceManager* getResourceManager() throw() { return d_resourceManager; }
 395
 396   /** Get this node manager's statistics registry */
 397   StatisticsRegistry* getStatisticsRegistry() const throw() {
 398     return d_statisticsRegistry;
 399   }
 400
 401   /** Subscribe to NodeManager events */
 402   void subscribeEvents(NodeManagerListener* listener) {
 403     Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
 404     d_listeners.push_back(listener);
 405   }
 406
 407   /** Unsubscribe from NodeManager events */
 408   void unsubscribeEvents(NodeManagerListener* listener) {
 409     std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
 410     Assert(elt != d_listeners.end(), "listener not subscribed");
 411     d_listeners.erase(elt);
 412   }
 413
 414   /** register datatype */
 415   unsigned registerDatatype(Datatype* dt);
 416   /** get datatype for index */
 417   const Datatype & getDatatypeForIndex( unsigned index ) const;
 418
 419   /** Get a Kind from an operator expression */
 420   static inline Kind operatorToKind(TNode n);
 421
 422   // general expression-builders
 423
 424   /** Create a node with one child. */
 425   Node mkNode(Kind kind, TNode child1);
 426   Node* mkNodePtr(Kind kind, TNode child1);
 427
 428   /** Create a node with two children. */
 429   Node mkNode(Kind kind, TNode child1, TNode child2);
 430   Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
 431
 432   /** Create a node with three children. */
 433   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 434   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
 435
 436   /** Create a node with four children. */
 437   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 438               TNode child4);
 439   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 440               TNode child4);
 441
 442   /** Create a node with five children. */
 443   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 444               TNode child4, TNode child5);
 445   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 446               TNode child4, TNode child5);
 447
 448   /** Create a node with an arbitrary number of children. */
 449   template <bool ref_count>
 450   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 451   template <bool ref_count>
 452   Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 453
 454   /** Create a node (with no children) by operator. */
 455   Node mkNode(TNode opNode);
 456   Node* mkNodePtr(TNode opNode);
 457
 458   /** Create a node with one child by operator. */
 459   Node mkNode(TNode opNode, TNode child1);
 460   Node* mkNodePtr(TNode opNode, TNode child1);
 461
 462   /** Create a node with two children by operator. */
 463   Node mkNode(TNode opNode, TNode child1, TNode child2);
 464   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
 465
 466   /** Create a node with three children by operator. */
 467   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
 468   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
 469
 470   /** Create a node with four children by operator. */
 471   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
 472               TNode child4);
 473   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
 474               TNode child4);
 475
 476   /** Create a node with five children by operator. */
 477   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
 478               TNode child4, TNode child5);
 479   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
 480               TNode child4, TNode child5);
 481
 482   /** Create a node by applying an operator to the children. */
 483   template <bool ref_count>
 484   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 485   template <bool ref_count>
 486   Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 487
 488   Node mkBoundVar(const std::string& name, const TypeNode& type);
 489   Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
 490
 491   Node mkBoundVar(const TypeNode& type);
 492   Node* mkBoundVarPtr(const TypeNode& type);
 493
 494   /** get the canonical bound variable list for function type tn */
 495   static Node getBoundVarListForFunctionType( TypeNode tn );
 496
 497   /**
 498    * Optional flags used to control behavior of NodeManager::mkSkolem().
 499    * They should be composed with a bitwise OR (e.g.,
 500    * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
 501    * cannot be composed in such a manner.
 502    */
 503   enum SkolemFlags {
 504     SKOLEM_DEFAULT = 0,   /**< default behavior */
 505     SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
 506     SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
 507     SKOLEM_IS_GLOBAL = 4  /**< global vars appear in models even after a pop */
 508   };/* enum SkolemFlags */
 509
 510   /**
 511    * Create a skolem constant with the given name, type, and comment.
 512    *
 513    * @param prefix the name of the new skolem variable is the prefix
 514    * appended with a unique ID.  This way a family of skolem variables
 515    * can be made with unique identifiers, used in dump, tracing, and
 516    * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
 517    * a unique ID appended and use prefix as the name.
 518    *
 519    * @param type the type of the skolem variable to create
 520    *
 521    * @param comment a comment for dumping output; if declarations are
 522    * being dumped, this is included in a comment before the declaration
 523    * and can be quite useful for debugging
 524    *
 525    * @param flags an optional mask of bits from SkolemFlags to control
 526    * mkSkolem() behavior
 527    */
 528   Node mkSkolem(const std::string& prefix, const TypeNode& type,
 529                 const std::string& comment = "", int flags = SKOLEM_DEFAULT);
 530
 531   /** Create a instantiation constant with the given type. */
 532   Node mkInstConstant(const TypeNode& type);
 533
 534   /** Create a boolean term variable. */
 535   Node mkBooleanTermVariable();
 536
 537   /** Make a new abstract value with the given type. */
 538   Node mkAbstractValue(const TypeNode& type);
 539
 540   /** make unique (per Type,Kind) variable. */
 541   Node mkNullaryOperator(const TypeNode& type, Kind k);
 542
 543   /**
 544    * Create a constant of type T.  It will have the appropriate
 545    * CONST_* kind defined for T.
 546    */
 547   template <class T>
 548   Node mkConst(const T&);
 549
 550   template <class T>
 551   TypeNode mkTypeConst(const T&);
 552
 553   template <class NodeClass, class T>
 554   NodeClass mkConstInternal(const T&);
 555
 556   /** Create a node with children. */
 557   TypeNode mkTypeNode(Kind kind, TypeNode child1);
 558   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
 559   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
 560                       TypeNode child3);
 561   TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
 562
 563   /**
 564    * Determine whether Nodes of a particular Kind have operators.
 565    * @returns true if Nodes of Kind k have operators.
 566    */
 567   static inline bool hasOperator(Kind k);
 568
 569   /**
 570    * Get the (singleton) operator of an OPERATOR-kinded kind.  The
 571    * returned node n will have kind BUILTIN, and calling
 572    * n.getConst<CVC4::Kind>() will yield k.
 573    */
 574   inline TNode operatorOf(Kind k) {
 575     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
 576                     "Kind is not an OPERATOR-kinded kind "
 577                     "in NodeManager::operatorOf()" );
 578     return d_operators[k];
 579   }
 580
 581   /**
 582    * Retrieve an attribute for a node.
 583    *
 584    * @param nv the node value
 585    * @param attr an instance of the attribute kind to retrieve.
 586    * @returns the attribute, if set, or a default-constructed
 587    * <code>AttrKind::value_type</code> if not.
 588    */
 589   template <class AttrKind>
 590   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
 591                                                     const AttrKind& attr) const;
 592
 593   /**
 594    * Check whether an attribute is set for a node.
 595    *
 596    * @param nv the node value
 597    * @param attr an instance of the attribute kind to check
 598    * @returns <code>true</code> iff <code>attr</code> is set for
 599    * <code>nv</code>.
 600    */
 601   template <class AttrKind>
 602   inline bool hasAttribute(expr::NodeValue* nv,
 603                            const AttrKind& attr) const;
 604
 605   /**
 606    * Check whether an attribute is set for a node, and, if so,
 607    * retrieve it.
 608    *
 609    * @param nv the node value
 610    * @param attr an instance of the attribute kind to check
 611    * @param value a reference to an object of the attribute's value type.
 612    * <code>value</code> will be set to the value of the attribute, if it is
 613    * set for <code>nv</code>; otherwise, it will be set to the default
 614    * value of the attribute.
 615    * @returns <code>true</code> iff <code>attr</code> is set for
 616    * <code>nv</code>.
 617    */
 618   template <class AttrKind>
 619   inline bool getAttribute(expr::NodeValue* nv,
 620                            const AttrKind& attr,
 621                            typename AttrKind::value_type& value) const;
 622
 623   /**
 624    * Set an attribute for a node.  If the node doesn't have the
 625    * attribute, this function assigns one.  If the node has one, this
 626    * overwrites it.
 627    *
 628    * @param nv the node value
 629    * @param attr an instance of the attribute kind to set
 630    * @param value the value of <code>attr</code> for <code>nv</code>
 631    */
 632   template <class AttrKind>
 633   inline void setAttribute(expr::NodeValue* nv,
 634                            const AttrKind& attr,
 635                            const typename AttrKind::value_type& value);
 636
 637   /**
 638    * Retrieve an attribute for a TNode.
 639    *
 640    * @param n the node
 641    * @param attr an instance of the attribute kind to retrieve.
 642    * @returns the attribute, if set, or a default-constructed
 643    * <code>AttrKind::value_type</code> if not.
 644    */
 645   template <class AttrKind>
 646   inline typename AttrKind::value_type
 647   getAttribute(TNode n, const AttrKind& attr) const;
 648
 649   /**
 650    * Check whether an attribute is set for a TNode.
 651    *
 652    * @param n the node
 653    * @param attr an instance of the attribute kind to check
 654    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 655    */
 656   template <class AttrKind>
 657   inline bool hasAttribute(TNode n,
 658                            const AttrKind& attr) const;
 659
 660   /**
 661    * Check whether an attribute is set for a TNode and, if so, retieve
 662    * it.
 663    *
 664    * @param n the node
 665    * @param attr an instance of the attribute kind to check
 666    * @param value a reference to an object of the attribute's value type.
 667    * <code>value</code> will be set to the value of the attribute, if it is
 668    * set for <code>nv</code>; otherwise, it will be set to the default value of
 669    * the attribute.
 670    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 671    */
 672   template <class AttrKind>
 673   inline bool getAttribute(TNode n,
 674                            const AttrKind& attr,
 675                            typename AttrKind::value_type& value) const;
 676
 677   /**
 678    * Set an attribute for a node.  If the node doesn't have the
 679    * attribute, this function assigns one.  If the node has one, this
 680    * overwrites it.
 681    *
 682    * @param n the node
 683    * @param attr an instance of the attribute kind to set
 684    * @param value the value of <code>attr</code> for <code>n</code>
 685    */
 686   template <class AttrKind>
 687   inline void setAttribute(TNode n,
 688                            const AttrKind& attr,
 689                            const typename AttrKind::value_type& value);
 690
 691   /**
 692    * Retrieve an attribute for a TypeNode.
 693    *
 694    * @param n the type node
 695    * @param attr an instance of the attribute kind to retrieve.
 696    * @returns the attribute, if set, or a default-constructed
 697    * <code>AttrKind::value_type</code> if not.
 698    */
 699   template <class AttrKind>
 700   inline typename AttrKind::value_type
 701   getAttribute(TypeNode n, const AttrKind& attr) const;
 702
 703   /**
 704    * Check whether an attribute is set for a TypeNode.
 705    *
 706    * @param n the type node
 707    * @param attr an instance of the attribute kind to check
 708    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 709    */
 710   template <class AttrKind>
 711   inline bool hasAttribute(TypeNode n,
 712                            const AttrKind& attr) const;
 713
 714   /**
 715    * Check whether an attribute is set for a TypeNode and, if so, retieve
 716    * it.
 717    *
 718    * @param n the type node
 719    * @param attr an instance of the attribute kind to check
 720    * @param value a reference to an object of the attribute's value type.
 721    * <code>value</code> will be set to the value of the attribute, if it is
 722    * set for <code>nv</code>; otherwise, it will be set to the default value of
 723    * the attribute.
 724    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 725    */
 726   template <class AttrKind>
 727   inline bool getAttribute(TypeNode n,
 728                            const AttrKind& attr,
 729                            typename AttrKind::value_type& value) const;
 730
 731   /**
 732    * Set an attribute for a type node.  If the node doesn't have the
 733    * attribute, this function assigns one.  If the type node has one,
 734    * this overwrites it.
 735    *
 736    * @param n the type node
 737    * @param attr an instance of the attribute kind to set
 738    * @param value the value of <code>attr</code> for <code>n</code>
 739    */
 740   template <class AttrKind>
 741   inline void setAttribute(TypeNode n,
 742                            const AttrKind& attr,
 743                            const typename AttrKind::value_type& value);
 744
 745   /** Get the (singleton) type for Booleans. */
 746   inline TypeNode booleanType();
 747
 748   /** Get the (singleton) type for integers. */
 749   inline TypeNode integerType();
 750
 751   /** Get the (singleton) type for reals. */
 752   inline TypeNode realType();
 753
 754   /** Get the (singleton) type for strings. */
 755   inline TypeNode stringType();
 756
 757   /** Get the (singleton) type for RegExp. */
 758   inline TypeNode regExpType();
 759
 760   /** Get the (singleton) type for rounding modes. */
 761   inline TypeNode roundingModeType();
 762
 763   /** Get the bound var list type. */
 764   inline TypeNode boundVarListType();
 765
 766   /** Get the instantiation pattern type. */
 767   inline TypeNode instPatternType();
 768
 769   /** Get the instantiation pattern type. */
 770   inline TypeNode instPatternListType();
 771
 772   /**
 773    * Get the (singleton) type for builtin operators (that is, the type
 774    * of the Node returned from Node::getOperator() when the operator
 775    * is built-in, like EQUAL). */
 776   inline TypeNode builtinOperatorType();
 777
 778   /**
 779    * Make a function type from domain to range.
 780    *
 781    * @param domain the domain type
 782    * @param range the range type
 783    * @returns the functional type domain -> range
 784    */
 785   inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 786
 787   /**
 788    * Make a function type with input types from
 789    * argTypes. <code>argTypes</code> must have at least one element.
 790    *
 791    * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
 792    * @param range the range type
 793    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
 794    */
 795   inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
 796                                  const TypeNode& range);
 797
 798   /**
 799    * Make a function type with input types from
 800    * <code>sorts[0..sorts.size()-2]</code> and result type
 801    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
 802    * at least 2 elements.
 803    */
 804   inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 805
 806   /**
 807    * Make a predicate type with input types from
 808    * <code>sorts</code>. The result with be a function type with range
 809    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
 810    * element.
 811    */
 812   inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 813
 814   /**
 815    * Make a tuple type with types from
 816    * <code>types</code>. <code>types</code> must have at least one
 817    * element.
 818    *
 819    * @param types a vector of types
 820    * @returns the tuple type (types[0], ..., types[n])
 821    */
 822   TypeNode mkTupleType(const std::vector<TypeNode>& types);
 823
 824   /**
 825    * Make a record type with the description from rec.
 826    *
 827    * @param rec a description of the record
 828    * @returns the record type
 829    */
 830   TypeNode mkRecordType(const Record& rec);
 831
 832   /**
 833    * Make a symbolic expression type with types from
 834    * <code>types</code>. <code>types</code> may have any number of
 835    * elements.
 836    *
 837    * @param types a vector of types
 838    * @returns the symbolic expression type (types[0], ..., types[n])
 839    */
 840   inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
 841
 842   /** Make the type of floating-point with <code>exp</code> bit exponent and
 843       <code>sig</code> bit significand */
 844   inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
 845   inline TypeNode mkFloatingPointType(FloatingPointSize fs);
 846
 847   /** Make the type of bitvectors of size <code>size</code> */
 848   inline TypeNode mkBitVectorType(unsigned size);
 849
 850   /** Make the type of arrays with the given parameterization */
 851   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 852
 853   /** Make the type of arrays with the given parameterization */
 854   inline TypeNode mkSetType(TypeNode elementType);
 855
 856   /** Make a type representing a constructor with the given parameterization */
 857   TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
 858
 859   /** Make a type representing a selector with the given parameterization */
 860   inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
 861
 862   /** Make a type representing a tester with given parameterization */
 863   inline TypeNode mkTesterType(TypeNode domain);
 864
 865   /** Make a new (anonymous) sort of arity 0. */
 866   TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
 867
 868   /** Make a new sort with the given name of arity 0. */
 869   TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
 870
 871   /** Make a new sort by parameterizing the given sort constructor. */
 872   TypeNode mkSort(TypeNode constructor,
 873                   const std::vector<TypeNode>& children,
 874                   uint32_t flags = ExprManager::SORT_FLAG_NONE);
 875
 876   /** Make a new sort with the given name and arity. */
 877   TypeNode mkSortConstructor(const std::string& name, size_t arity);
 878
 879   /**
 880    * Get the type for the given node and optionally do type checking.
 881    *
 882    * Initial type computation will be near-constant time if
 883    * type checking is not requested. Results are memoized, so that
 884    * subsequent calls to getType() without type checking will be
 885    * constant time.
 886    *
 887    * Initial type checking is linear in the size of the expression.
 888    * Again, the results are memoized, so that subsequent calls to
 889    * getType(), with or without type checking, will be constant
 890    * time.
 891    *
 892    * NOTE: A TypeCheckingException can be thrown even when type
 893    * checking is not requested. getType() will always return a
 894    * valid and correct type and, thus, an exception will be thrown
 895    * when no valid or correct type can be computed (e.g., if the
 896    * arguments to a bit-vector operation aren't bit-vectors). When
 897    * type checking is not requested, getType() will do the minimum
 898    * amount of checking required to return a valid result.
 899    *
 900    * @param n the Node for which we want a type
 901    * @param check whether we should check the type as we compute it
 902    * (default: false)
 903    */
 904   TypeNode getType(TNode n, bool check = false)
 905     throw(TypeCheckingExceptionPrivate, AssertionException);
 906
 907   /**
 908    * Convert a node to an expression.  Uses the ExprManager
 909    * associated to this NodeManager.
 910    */
 911   inline Expr toExpr(TNode n);
 912
 913   /**
 914    * Convert an expression to a node.
 915    */
 916   static inline Node fromExpr(const Expr& e);
 917
 918   /**
 919    * Convert a node manager to an expression manager.
 920    */
 921   inline ExprManager* toExprManager();
 922
 923   /**
 924    * Convert an expression manager to a node manager.
 925    */
 926   static inline NodeManager* fromExprManager(ExprManager* exprManager);
 927
 928   /**
 929    * Convert a type node to a type.
 930    */
 931   inline Type toType(TypeNode tn);
 932
 933   /**
 934    * Convert a type to a type node.
 935    */
 936   static inline TypeNode fromType(Type t);
 937
 938   /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
 939   void reclaimZombiesUntil(uint32_t k);
 940
 941   /** Reclaims all zombies (if possible).*/
 942   void reclaimAllZombies();
 943
 944   /** Size of the node pool. */
 945   size_t poolSize() const;
 946
 947   /** Deletes a list of attributes from the NM's AttributeManager.*/
 948   void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
 949
 950   /**
 951    * This function gives developers a hook into the NodeManager.
 952    * This can be changed in node_manager.cpp without recompiling most of cvc4.
 953    *
 954    * debugHook is a debugging only function, and should not be present in
 955    * any published code!
 956    */
 957   void debugHook(int debugFlag);
 958 };/* class NodeManager */
 959
 960 /**
 961  * This class changes the "current" thread-global
 962  * <code>NodeManager</code> when it is created and reinstates the
 963  * previous thread-global <code>NodeManager</code> when it is
 964  * destroyed, effectively maintaining a set of nested
 965  * <code>NodeManager</code> scopes.  This is especially useful on
 966  * public-interface calls into the CVC4 library, where CVC4's notion
 967  * of the "current" <code>NodeManager</code> should be set to match
 968  * the calling context.  See, for example, the implementations of
 969  * public calls in the <code>ExprManager</code> and
 970  * <code>SmtEngine</code> classes.
 971  *
 972  * The client must be careful to create and destroy
 973  * <code>NodeManagerScope</code> objects in a well-nested manner (such
 974  * as on the stack). You may create a <code>NodeManagerScope</code>
 975  * with <code>new</code> and destroy it with <code>delete</code>, or
 976  * place it as a data member of an object that is, but if the scope of
 977  * these <code>new</code>/<code>delete</code> pairs isn't properly
 978  * maintained, the incorrect "current" <code>NodeManager</code>
 979  * pointer may be restored after a delete.
 980  */
 981 class NodeManagerScope {
 982   /** The old NodeManager, to be restored on destruction. */
 983   NodeManager* d_oldNodeManager;
 984   Options::OptionsScope d_optionsScope;
 985 public:
 986
 987   NodeManagerScope(NodeManager* nm)
 988       : d_oldNodeManager(NodeManager::s_current)
 989       , d_optionsScope(nm ? nm->d_options : NULL) {
 990     // There are corner cases where nm can be NULL and it's ok.
 991     // For example, if you write { Expr e; }, then when the null
 992     // Expr is destructed, there's no active node manager.
 993     //Assert(nm != NULL);
 994     NodeManager::s_current = nm;
 995     //Options::s_current = nm ? nm->d_options : NULL;
 996     Debug("current") << "node manager scope: "
 997                      << NodeManager::s_current << "\n";
 998   }
 999
1000   ~NodeManagerScope() {
1001     NodeManager::s_current = d_oldNodeManager;
1002     //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
1003     Debug("current") << "node manager scope: "
1004                      << "returning to " << NodeManager::s_current << "\n";
1005   }
1006 };/* class NodeManagerScope */
1007
1008 /** Get the (singleton) type for booleans. */
1009 inline TypeNode NodeManager::booleanType() {
1010   return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
1011 }
1012
1013 /** Get the (singleton) type for integers. */
1014 inline TypeNode NodeManager::integerType() {
1015   return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
1016 }
1017
1018 /** Get the (singleton) type for reals. */
1019 inline TypeNode NodeManager::realType() {
1020   return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
1021 }
1022
1023 /** Get the (singleton) type for strings. */
1024 inline TypeNode NodeManager::stringType() {
1025   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
1026 }
1027
1028 /** Get the (singleton) type for regexps. */
1029 inline TypeNode NodeManager::regExpType() {
1030   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
1031 }
1032
1033 /** Get the (singleton) type for rounding modes. */
1034 inline TypeNode NodeManager::roundingModeType() {
1035   return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
1036 }
1037
1038 /** Get the bound var list type. */
1039 inline TypeNode NodeManager::boundVarListType() {
1040   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
1041 }
1042
1043 /** Get the instantiation pattern type. */
1044 inline TypeNode NodeManager::instPatternType() {
1045   return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
1046 }
1047
1048 /** Get the instantiation pattern type. */
1049 inline TypeNode NodeManager::instPatternListType() {
1050   return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
1051 }
1052
1053 /** Get the (singleton) type for builtin operators. */
1054 inline TypeNode NodeManager::builtinOperatorType() {
1055   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
1056 }
1057
1058 /** Make a function type from domain to range. */
1059 inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
1060   std::vector<TypeNode> sorts;
1061   sorts.push_back(domain);
1062   sorts.push_back(range);
1063   return mkFunctionType(sorts);
1064 }
1065
1066 inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
1067   Assert(argTypes.size() >= 1);
1068   std::vector<TypeNode> sorts(argTypes);
1069   sorts.push_back(range);
1070   return mkFunctionType(sorts);
1071 }
1072
1073 inline TypeNode
1074 NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
1075   Assert(sorts.size() >= 2);
1076   std::vector<TypeNode> sortNodes;
1077   for (unsigned i = 0; i < sorts.size(); ++ i) {
1078     CheckArgument(!sorts[i].isFunctionLike(), sorts,
1079                   "cannot create higher-order function types");
1080     sortNodes.push_back(sorts[i]);
1081   }
1082   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
1083 }
1084
1085 inline TypeNode
1086 NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
1087   Assert(sorts.size() >= 1);
1088   std::vector<TypeNode> sortNodes;
1089   for (unsigned i = 0; i < sorts.size(); ++ i) {
1090     CheckArgument(!sorts[i].isFunctionLike(), sorts,
1091                   "cannot create higher-order function types");
1092     sortNodes.push_back(sorts[i]);
1093   }
1094   sortNodes.push_back(booleanType());
1095   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
1096 }
1097
1098 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
1099   std::vector<TypeNode> typeNodes;
1100   for (unsigned i = 0; i < types.size(); ++ i) {
1101     typeNodes.push_back(types[i]);
1102   }
1103   return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
1104 }
1105
1106 inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
1107   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
1108 }
1109
1110 inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
1111   return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
1112 }
1113
1114 inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
1115   return TypeNode(mkTypeConst<FloatingPointSize>(fs));
1116 }
1117
1118 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
1119                                          TypeNode constituentType) {
1120   CheckArgument(!indexType.isNull(), indexType,
1121                 "unexpected NULL index type");
1122   CheckArgument(!constituentType.isNull(), constituentType,
1123                 "unexpected NULL constituent type");
1124   CheckArgument(!indexType.isFunctionLike(), indexType,
1125                 "cannot index arrays by a function-like type");
1126   CheckArgument(!constituentType.isFunctionLike(), constituentType,
1127                 "cannot store function-like types in arrays");
1128   Debug("arrays") << "making array type " << indexType << " "
1129                   << constituentType << std::endl;
1130   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
1131 }
1132
1133 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
1134   CheckArgument(!elementType.isNull(), elementType,
1135                 "unexpected NULL element type");
1136   // TODO: Confirm meaning of isFunctionLike(). --K
1137   CheckArgument(!elementType.isFunctionLike(), elementType,
1138                 "cannot store function-like types in sets");
1139   Debug("sets") << "making sets type " << elementType << std::endl;
1140   return mkTypeNode(kind::SET_TYPE, elementType);
1141 }
1142
1143 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
1144   CheckArgument(!domain.isFunctionLike(), domain,
1145                 "cannot create higher-order function types");
1146   CheckArgument(!range.isFunctionLike(), range,
1147                 "cannot create higher-order function types");
1148   return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
1149 }
1150
1151 inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
1152   CheckArgument(!domain.isFunctionLike(), domain,
1153                 "cannot create higher-order function types");
1154   return mkTypeNode(kind::TESTER_TYPE, domain );
1155 }
1156
1157 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
1158   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
1159   if(find == d_nodeValuePool.end()) {
1160     return NULL;
1161   } else {
1162     return *find;
1163   }
1164 }
1165
1166 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
1167   Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
1168          "NodeValue already in the pool!");
1169   d_nodeValuePool.insert(nv);// FIXME multithreading
1170 }
1171
1172 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
1173   Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
1174          "NodeValue is not in the pool!");
1175
1176   d_nodeValuePool.erase(nv);// FIXME multithreading
1177 }
1178
1179 inline Expr NodeManager::toExpr(TNode n) {
1180   return Expr(d_exprManager, new Node(n));
1181 }
1182
1183 inline Node NodeManager::fromExpr(const Expr& e) {
1184   return e.getNode();
1185 }
1186
1187 inline ExprManager* NodeManager::toExprManager() {
1188   return d_exprManager;
1189 }
1190
1191 inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
1192   return exprManager->getNodeManager();
1193 }
1194
1195 inline Type NodeManager::toType(TypeNode tn) {
1196   return Type(this, new TypeNode(tn));
1197 }
1198
1199 inline TypeNode NodeManager::fromType(Type t) {
1200   return *Type::getTypeNode(t);
1201 }
1202
1203 }/* CVC4 namespace */
1204
1205 #define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1206 #include "expr/metakind.h"
1207 #undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1208
1209 #include "expr/node_builder.h"
1210
1211 namespace CVC4 {
1212
1213 // general expression-builders
1214
1215 inline bool NodeManager::hasOperator(Kind k) {
1216   switch(kind::MetaKind mk = kind::metaKindOf(k)) {
1217
1218   case kind::metakind::INVALID:
1219   case kind::metakind::VARIABLE:
1220   case kind::metakind::NULLARY_OPERATOR:
1221     return false;
1222
1223   case kind::metakind::OPERATOR:
1224   case kind::metakind::PARAMETERIZED:
1225     return true;
1226
1227   case kind::metakind::CONSTANT:
1228     return false;
1229
1230   default:
1231     Unhandled(mk);
1232   }
1233 }
1234
1235 inline Kind NodeManager::operatorToKind(TNode n) {
1236   return kind::operatorToKind(n.d_nv);
1237 }
1238
1239 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
1240   NodeBuilder<1> nb(this, kind);
1241   nb << child1;
1242   return nb.constructNode();
1243 }
1244
1245 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
1246   NodeBuilder<1> nb(this, kind);
1247   nb << child1;
1248   return nb.constructNodePtr();
1249 }
1250
1251 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
1252   NodeBuilder<2> nb(this, kind);
1253   nb << child1 << child2;
1254   return nb.constructNode();
1255 }
1256
1257 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
1258   NodeBuilder<2> nb(this, kind);
1259   nb << child1 << child2;
1260   return nb.constructNodePtr();
1261 }
1262
1263 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1264                                 TNode child3) {
1265   NodeBuilder<3> nb(this, kind);
1266   nb << child1 << child2 << child3;
1267   return nb.constructNode();
1268 }
1269
1270 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1271                                 TNode child3) {
1272   NodeBuilder<3> nb(this, kind);
1273   nb << child1 << child2 << child3;
1274   return nb.constructNodePtr();
1275 }
1276
1277 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1278                                 TNode child3, TNode child4) {
1279   NodeBuilder<4> nb(this, kind);
1280   nb << child1 << child2 << child3 << child4;
1281   return nb.constructNode();
1282 }
1283
1284 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1285                                 TNode child3, TNode child4) {
1286   NodeBuilder<4> nb(this, kind);
1287   nb << child1 << child2 << child3 << child4;
1288   return nb.constructNodePtr();
1289 }
1290
1291 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1292                                 TNode child3, TNode child4, TNode child5) {
1293   NodeBuilder<5> nb(this, kind);
1294   nb << child1 << child2 << child3 << child4 << child5;
1295   return nb.constructNode();
1296 }
1297
1298 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1299                                     TNode child3, TNode child4, TNode child5) {
1300   NodeBuilder<5> nb(this, kind);
1301   nb << child1 << child2 << child3 << child4 << child5;
1302   return nb.constructNodePtr();
1303 }
1304
1305 // N-ary version
1306 template <bool ref_count>
1307 inline Node NodeManager::mkNode(Kind kind,
1308                                 const std::vector<NodeTemplate<ref_count> >&
1309                                 children) {
1310   NodeBuilder<> nb(this, kind);
1311   nb.append(children);
1312   return nb.constructNode();
1313 }
1314
1315 template <bool ref_count>
1316 inline Node* NodeManager::mkNodePtr(Kind kind,
1317                                 const std::vector<NodeTemplate<ref_count> >&
1318                                 children) {
1319   NodeBuilder<> nb(this, kind);
1320   nb.append(children);
1321   return nb.constructNodePtr();
1322 }
1323
1324 // for operators
1325 inline Node NodeManager::mkNode(TNode opNode) {
1326   NodeBuilder<1> nb(this, operatorToKind(opNode));
1327   if(opNode.getKind() != kind::BUILTIN) {
1328     nb << opNode;
1329   }
1330   return nb.constructNode();
1331 }
1332
1333 inline Node* NodeManager::mkNodePtr(TNode opNode) {
1334   NodeBuilder<1> nb(this, operatorToKind(opNode));
1335   if(opNode.getKind() != kind::BUILTIN) {
1336     nb << opNode;
1337   }
1338   return nb.constructNodePtr();
1339 }
1340
1341 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
1342   NodeBuilder<2> nb(this, operatorToKind(opNode));
1343   if(opNode.getKind() != kind::BUILTIN) {
1344     nb << opNode;
1345   }
1346   nb << child1;
1347   return nb.constructNode();
1348 }
1349
1350 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
1351   NodeBuilder<2> nb(this, operatorToKind(opNode));
1352   if(opNode.getKind() != kind::BUILTIN) {
1353     nb << opNode;
1354   }
1355   nb << child1;
1356   return nb.constructNodePtr();
1357 }
1358
1359 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
1360   NodeBuilder<3> nb(this, operatorToKind(opNode));
1361   if(opNode.getKind() != kind::BUILTIN) {
1362     nb << opNode;
1363   }
1364   nb << child1 << child2;
1365   return nb.constructNode();
1366 }
1367
1368 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
1369   NodeBuilder<3> nb(this, operatorToKind(opNode));
1370   if(opNode.getKind() != kind::BUILTIN) {
1371     nb << opNode;
1372   }
1373   nb << child1 << child2;
1374   return nb.constructNodePtr();
1375 }
1376
1377 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1378                                 TNode child3) {
1379   NodeBuilder<4> nb(this, operatorToKind(opNode));
1380   if(opNode.getKind() != kind::BUILTIN) {
1381     nb << opNode;
1382   }
1383   nb << child1 << child2 << child3;
1384   return nb.constructNode();
1385 }
1386
1387 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1388                                 TNode child3) {
1389   NodeBuilder<4> nb(this, operatorToKind(opNode));
1390   if(opNode.getKind() != kind::BUILTIN) {
1391     nb << opNode;
1392   }
1393   nb << child1 << child2 << child3;
1394   return nb.constructNodePtr();
1395 }
1396
1397 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1398                                 TNode child3, TNode child4) {
1399   NodeBuilder<5> nb(this, operatorToKind(opNode));
1400   if(opNode.getKind() != kind::BUILTIN) {
1401     nb << opNode;
1402   }
1403   nb << child1 << child2 << child3 << child4;
1404   return nb.constructNode();
1405 }
1406
1407 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1408                                 TNode child3, TNode child4) {
1409   NodeBuilder<5> nb(this, operatorToKind(opNode));
1410   if(opNode.getKind() != kind::BUILTIN) {
1411     nb << opNode;
1412   }
1413   nb << child1 << child2 << child3 << child4;
1414   return nb.constructNodePtr();
1415 }
1416
1417 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1418                                 TNode child3, TNode child4, TNode child5) {
1419   NodeBuilder<6> nb(this, operatorToKind(opNode));
1420   if(opNode.getKind() != kind::BUILTIN) {
1421     nb << opNode;
1422   }
1423   nb << child1 << child2 << child3 << child4 << child5;
1424   return nb.constructNode();
1425 }
1426
1427 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1428                                     TNode child3, TNode child4, TNode child5) {
1429   NodeBuilder<6> nb(this, operatorToKind(opNode));
1430   if(opNode.getKind() != kind::BUILTIN) {
1431     nb << opNode;
1432   }
1433   nb << child1 << child2 << child3 << child4 << child5;
1434   return nb.constructNodePtr();
1435 }
1436
1437 // N-ary version for operators
1438 template <bool ref_count>
1439 inline Node NodeManager::mkNode(TNode opNode,
1440                                 const std::vector<NodeTemplate<ref_count> >&
1441                                 children) {
1442   NodeBuilder<> nb(this, operatorToKind(opNode));
1443   if(opNode.getKind() != kind::BUILTIN) {
1444     nb << opNode;
1445   }
1446   nb.append(children);
1447   return nb.constructNode();
1448 }
1449
1450 template <bool ref_count>
1451 inline Node* NodeManager::mkNodePtr(TNode opNode,
1452                                     const std::vector<NodeTemplate<ref_count> >&
1453                                     children) {
1454   NodeBuilder<> nb(this, operatorToKind(opNode));
1455   if(opNode.getKind() != kind::BUILTIN) {
1456     nb << opNode;
1457   }
1458   nb.append(children);
1459   return nb.constructNodePtr();
1460 }
1461
1462
1463 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
1464   return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
1465 }
1466
1467 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1468                                         TypeNode child2) {
1469   return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
1470 }
1471
1472 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1473                                         TypeNode child2, TypeNode child3) {
1474   return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
1475 }
1476
1477 // N-ary version for types
1478 inline TypeNode NodeManager::mkTypeNode(Kind kind,
1479                                         const std::vector<TypeNode>& children) {
1480   return NodeBuilder<>(this, kind).append(children).constructTypeNode();
1481 }
1482
1483 template <class T>
1484 Node NodeManager::mkConst(const T& val) {
1485   return mkConstInternal<Node, T>(val);
1486 }
1487
1488 template <class T>
1489 TypeNode NodeManager::mkTypeConst(const T& val) {
1490   return mkConstInternal<TypeNode, T>(val);
1491 }
1492
1493 template <class NodeClass, class T>
1494 NodeClass NodeManager::mkConstInternal(const T& val) {
1495
1496   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1497   NVStorage<1> nvStorage;
1498   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
1499
1500   nvStack.d_id = 0;
1501   nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
1502   nvStack.d_rc = 0;
1503   nvStack.d_nchildren = 1;
1504
1505 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1506 #pragma GCC diagnostic push
1507 #pragma GCC diagnostic ignored "-Warray-bounds"
1508 #endif
1509
1510   nvStack.d_children[0] =
1511     const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
1512   expr::NodeValue* nv = poolLookup(&nvStack);
1513
1514 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1515 #pragma GCC diagnostic pop
1516 #endif
1517
1518   if(nv != NULL) {
1519     return NodeClass(nv);
1520   }
1521
1522   nv = (expr::NodeValue*)
1523     std::malloc(sizeof(expr::NodeValue) + sizeof(T));
1524   if(nv == NULL) {
1525     throw std::bad_alloc();
1526   }
1527
1528   nv->d_nchildren = 0;
1529   nv->d_kind = kind::metakind::ConstantMap<T>::kind;
1530   nv->d_id = next_id++;// FIXME multithreading
1531   nv->d_rc = 0;
1532
1533   //OwningTheory::mkConst(val);
1534   new (&nv->d_children) T(val);
1535
1536   poolInsert(nv);
1537   if(Debug.isOn("gc")) {
1538     Debug("gc") << "creating node value " << nv
1539                 << " [" << nv->d_id << "]: ";
1540     nv->printAst(Debug("gc"));
1541     Debug("gc") << std::endl;
1542   }
1543
1544   return NodeClass(nv);
1545 }
1546
1547 }/* CVC4 namespace */
1548
1549 #endif /* __CVC4__NODE_MANAGER_H */