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/expr/pickle_data.h | |
| parent | f806a8eedf01753116c225b4c1a5e29543fda370 (diff) | |
Changing the number of bits allocated per field in node values.
Diffstat (limited to 'src/expr/pickle_data.h')
| -rw-r--r-- | src/expr/pickle_data.h | 10 |
1 files changed, 5 insertions, 5 deletions
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 { |