Changing the number of bits allocated per field in node values.

12 files changed, 31 insertions, 25 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 54dc64aa4..085a3a0c8 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -267,7 +267,7 @@ bool Expr::operator>(const Expr& e) const {
   return *d_node > *e.d_node;
 }
 
-unsigned Expr::getId() const {
+unsigned long Expr::getId() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->getId();
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index e262fada8..ace14a10b 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -275,7 +275,7 @@ public:
    * @return an identifier uniquely identifying the value this
    * expression holds.
    */
-  unsigned getId() const;
+  unsigned long getId() const;
 
   /**
    * Returns the kind of the expression (AND, PLUS ...).
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 93cebe00a..a330aa4a9 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -136,10 +136,10 @@ namespace kind {
 namespace metakind {
 
 /* these are #defines so their sum can be #if-checked in node_value.h */
-#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 8
-#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 8
-#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 32
-#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 16
+#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20
+#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 10
+#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 40
+#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26
 
 static const unsigned MAX_CHILDREN =
   (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
diff --git a/src/expr/node.h b/src/expr/node.h
index 3c058c924..3a5b6f135 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -466,7 +466,7 @@ public:
    * Returns the unique id of this node
    * @return the ud
    */
-  unsigned getId() const {
+  unsigned long getId() const {
     assertTNodeNotExpired();
     return d_nv->getId();
   }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 64080c275..0be97b24a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -217,7 +217,7 @@ class NodeBuilder {
   /**
    * The number of children allocated in d_nv.
    */
-  uint16_t d_nvMaxChildren;
+  uint32_t d_nvMaxChildren;
 
   template <unsigned N>
   void internalCopy(const NodeBuilder<N>& nb);
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 56ac70c1e..e9d14c38e 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -65,9 +65,9 @@ namespace expr {
 #if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
     __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
     __CVC4__EXPR__NODE_VALUE__NBITS__ID + \
-    __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 64
-#  error NodeValue header bit assignment does not sum to 64 !
-#endif /* sum != 64 */
+    __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96
+#  error NodeValue header bit assignment does not sum to 96 !
+#endif /* sum != 96 */
 
 /**
  * This is a NodeValue.
@@ -92,7 +92,7 @@ class NodeValue {
   // this header fits into one 64-bit word
 
   /** The ID (0 is reserved for the null value) */
-  unsigned d_id        : NBITS_ID;
+  unsigned long d_id        : NBITS_ID;
 
   /** The expression's reference count.  @see cvc4::Node. */
   unsigned d_rc        : NBITS_REFCOUNT;
@@ -255,7 +255,7 @@ public:
     return hash;
   }
 
-  unsigned getId() const { return d_id; }
+  unsigned long getId() const { return d_id; }
   Kind getKind() const { return dKindToKind(d_kind); }
   kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
   unsigned getNumChildren() const {
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h
index b9c20f27a..31751b381 100644
--- a/src/expr/pickle_data.h
+++ b/src/expr/pickle_data.h
@@ -43,7 +43,7 @@ class NodeManager;
 namespace expr {
 namespace pickle {
 
-const unsigned NBITS_BLOCK = 32;
+const unsigned NBITS_BLOCK = 64;
 const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
 const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
 const unsigned NBITS_CONSTBLOCKS = 32;
@@ -55,21 +55,21 @@ struct BlockHeader {
 struct BlockHeaderOperator {
   unsigned d_kind          : NBITS_KIND;
   unsigned d_nchildren     : NBITS_NCHILDREN;
-  unsigned                 : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN);
+  unsigned long            : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN);
 };/* struct BlockHeaderOperator */
 
 struct BlockHeaderConstant {
   unsigned d_kind          : NBITS_KIND;
-  unsigned d_constblocks   : NBITS_BLOCK - NBITS_KIND;
+  unsigned long d_constblocks   : NBITS_BLOCK - NBITS_KIND;
 };/* struct BlockHeaderConstant */
 
 struct BlockHeaderVariable {
   unsigned d_kind          : NBITS_KIND;
-  unsigned                 : NBITS_BLOCK - NBITS_KIND;
+  unsigned long            : NBITS_BLOCK - NBITS_KIND;
 };/* struct BlockHeaderVariable */
 
 struct BlockBody  {
-  unsigned d_data          : NBITS_BLOCK;
+  unsigned long d_data          : NBITS_BLOCK;
 };/* struct BlockBody */
 
 union Block {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 75d6d8063..ae951dbf2 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -239,7 +239,7 @@ public:
    *
    * @return the id
    */
-  inline unsigned getId() const {
+  inline unsigned long getId() const {
     return d_nv->getId();
   }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0cfb674cf..21f2d9209 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -369,7 +369,7 @@ private:
   // trace nodes back to their assertions using CircuitPropagator's BackEdgesMap
   void traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions);
   // remove conjuncts in toRemove from conjunction n; return # of removed conjuncts
-  size_t removeFromConjunction(Node& n, const std::hash_set<unsigned>& toRemove);
+  size_t removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove);
 
   // scrub miplib encodings
   void doMiplibTrick();
@@ -408,6 +408,8 @@ public:
   {
     d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
+
+    Chat() << "NodeValue width" << sizeof(expr::NodeValue) << std::endl;
   }
 
   ~SmtEnginePrivate() {
@@ -2120,7 +2122,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std
   }
 }
 
-size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned>& toRemove) {
+size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) {
   Assert(n.getKind() == kind::AND);
   size_t removals = 0;
   for(Node::iterator j = n.begin(); j != n.end(); ++j) {
@@ -2175,7 +2177,7 @@ void SmtEnginePrivate::doMiplibTrick() {
   Assert(!options::incrementalSolving());
 
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
-  hash_set<unsigned> removeAssertions;
+  hash_set<unsigned long> removeAssertions;
 
   NodeManager* nm = NodeManager::currentNM();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index d5929a266..204f1bcd2 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -105,7 +105,8 @@ public:
 
   void testMkAssociative3() {
     try {
-      unsigned int numVars = d_exprManager->maxArity(AND) + 1;
+      //unsigned int numVars = d_exprManager->maxArity(AND) + 1;
+      unsigned int numVars = (1<<16) + 1;
       std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), numVars);
       Expr n = d_exprManager->mkAssociative(AND,vars);
       checkAssociative(n,AND,numVars);
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 860dfb1a9..4c2cc97e2 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -314,8 +314,9 @@ public:
     std::vector<Node> vars;
     const unsigned int max = metakind::getUpperBoundForKind(AND);
     TypeNode boolType = d_nodeManager->booleanType();
+    Node skolem = d_nodeManager->mkSkolem("i", boolType);
     for( unsigned int i = 0; i <= max; ++i ) {
-      vars.push_back( d_nodeManager->mkSkolem("i", boolType) );
+      vars.push_back( skolem );
     }
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
 #endif
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 26872846e..b272cb692 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -69,8 +69,10 @@ public:
     TS_ASSERT_THROWS_NOTHING(nb.realloc(20000));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(60000));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(65535));
+    TS_ASSERT_THROWS_NOTHING(nb.realloc(65536));
+    TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863));
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.realloc(65536), AssertionException);
+    TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException);
 #endif /* CVC4_ASSERTIONS */
   }
 };