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

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 54dc64aa45bd03d5b982325fc4e0eb608a74d2e8..085a3a0c8f0c9b21d6460b167a64bc9d8c99a4ec 100644 (file)
--- 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 e262fada8c7afaf034307b12540af1ef89e1321f..ace14a10bd4f4ddd1041228ddc51d942720d1bf2 100644 (file)
--- 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 93cebe00ad4148b63df02334b2f6041d04f74acd..a330aa4a96fb221fe03639797e2d8ffd4dfafbbb 100644 (file)
--- 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 3c058c92406676585b36d73b054a83388908ecab..3a5b6f13569b91174b39050a1631453cb398cdb4 100644 (file)
--- 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 64080c275dc9a9fe28a251bbac815efe9eb727e0..0be97b24ac0b8cdff9c774256f1023671fbbdbe7 100644 (file)
--- 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 56ac70c1e28dbb4bbbc27b57c5a68f9567922c62..e9d14c38e0b2e62cbc3035f6dc40cbebdf44f83e 100644 (file)
--- 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 b9c20f27a10509f6ea5dbcf4720d0d375f0e659e..31751b381dd5ce855236899e089dba66348405b6 100644 (file)
--- 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 75d6d8063b88b3ab785707f6458e002e305d5aa2..ae951dbf28204cc09181aad312526f937c1ce413 100644 (file)
--- 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 0cfb674cf549582aaabf33e662b3a6d28b270fd7..21f2d9209093acf3f3245664e97b4c0f2ca705fd 100644 (file)
--- 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 d5929a266258210188a9b75c3d6cb08bb71cd9b1..204f1bcd221c8036e0d88af7e5b388c3d710ec0b 100644 (file)
--- 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 860dfb1a9993345e8ce15da7616967e0dae4734b..4c2cc97e2fafb2bbb08848c3d5f8c12b0a830e2b 100644 (file)
--- 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 26872846e55ca1bee15e9c94d373ff94a314cb71..b272cb692c1a2c13924eefd2d5f017d51003fc4e 100644 (file)
--- 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 */
   }
 };