diff options
author | Tim King <taking@cs.nyu.edu> | 2013-11-19 20:57:15 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-11-20 15:37:18 -0500 |
commit | bd8e9319aab69db90692f72bc52288329879eefc (patch) | |
tree | 7bfee530c06836827378fd5b9bd1f47bb4f1eea1 /src | |
parent | f806a8eedf01753116c225b4c1a5e29543fda370 (diff) |
Changing the number of bits allocated per field in node values.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_template.h | 2 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 8 | ||||
-rw-r--r-- | src/expr/node.h | 2 | ||||
-rw-r--r-- | src/expr/node_builder.h | 2 | ||||
-rw-r--r-- | src/expr/node_value.h | 10 | ||||
-rw-r--r-- | src/expr/pickle_data.h | 10 | ||||
-rw-r--r-- | src/expr/type_node.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 8 |
9 files changed, 24 insertions, 22 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)); |