From bd8e9319aab69db90692f72bc52288329879eefc Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 19 Nov 2013 20:57:15 -0500 Subject: [PATCH] Changing the number of bits allocated per field in node values. --- src/expr/expr_template.cpp | 2 +- src/expr/expr_template.h | 2 +- src/expr/metakind_template.h | 8 ++++---- src/expr/node.h | 2 +- src/expr/node_builder.h | 2 +- src/expr/node_value.h | 10 +++++----- src/expr/pickle_data.h | 10 +++++----- src/expr/type_node.h | 2 +- src/smt/smt_engine.cpp | 8 +++++--- test/unit/expr/expr_manager_public.h | 3 ++- test/unit/expr/node_manager_black.h | 3 ++- test/unit/expr/node_manager_white.h | 4 +++- 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 void internalCopy(const NodeBuilder& 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& nodes, std::vector& assertions); // remove conjuncts in toRemove from conjunction n; return # of removed conjuncts - size_t removeFromConjunction(Node& n, const std::hash_set& toRemove); + size_t removeFromConjunction(Node& n, const std::hash_set& 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& nodes, std } } -size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set& toRemove) { +size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set& 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 removeAssertions; + hash_set 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 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 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 */ } }; -- 2.30.2