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