diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
commit | 3d2b33d66998261f9369cccc098140f64bc8b417 (patch) | |
tree | 9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/expr/pickle_data.h | |
parent | 92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff) |
portfolio merge
Diffstat (limited to 'src/expr/pickle_data.h')
-rw-r--r-- | src/expr/pickle_data.h | 122 |
1 files changed, 122 insertions, 0 deletions
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h new file mode 100644 index 000000000..dab6e56c3 --- /dev/null +++ b/src/expr/pickle_data.h @@ -0,0 +1,122 @@ +/********************* */ +/*! \file pickle_data.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickle" for expressions, CVC4-internal view + ** + ** This is the CVC4-internal view (private data structure) for a + ** "pickle" for expressions. The public-facing view is a "Pickle", + ** which just points to a PickleData. A pickle is a binary + ** serialization of an expression that can be converted back into an + ** expression in the same or another ExprManager. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PICKLE_DATA_H +#define __CVC4__PICKLE_DATA_H + +#include <sstream> +#include <deque> +#include <stack> +#include <exception> + +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/expr_manager.h" +#include "expr/variable_type_map.h" +#include "expr/kind.h" +#include "expr/metakind.h" + +namespace CVC4 { + +class NodeManager; + +namespace expr { +namespace pickle { + +const unsigned NBITS_BLOCK = 32; +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; + +struct BlockHeader { + unsigned d_kind : NBITS_KIND; +};/* struct BlockHeader */ + +struct BlockHeaderOperator { + unsigned d_kind : NBITS_KIND; + unsigned d_nchildren : NBITS_NCHILDREN; + unsigned : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); +};/* struct BlockHeaderOperator */ + +struct BlockHeaderConstant { + unsigned d_kind : NBITS_KIND; + unsigned d_constblocks : NBITS_BLOCK - NBITS_KIND; +};/* struct BlockHeaderConstant */ + +struct BlockHeaderVariable { + unsigned d_kind : NBITS_KIND; + unsigned : NBITS_BLOCK - NBITS_KIND; +};/* struct BlockHeaderVariable */ + +struct BlockBody { + unsigned d_data : NBITS_BLOCK; +};/* struct BlockBody */ + +union Block { + BlockHeader d_header; + BlockHeaderConstant d_headerConstant; + BlockHeaderOperator d_headerOperator; + BlockHeaderVariable d_headerVariable; + + BlockBody d_body; +};/* union Block */ + +class PickleData { + typedef std::deque<Block> BlockDeque; + BlockDeque d_blocks; + +public: + PickleData& operator<<(Block b) { + enqueue(b); + return (*this); + } + + std::string toString() const; + + void enqueue(Block b) { + d_blocks.push_back(b); + } + + Block dequeue() { + Block b = d_blocks.front(); + d_blocks.pop_front(); + return b; + } + + bool empty() const { return d_blocks.empty(); } + uint32_t size() const { return d_blocks.size(); } + + void swap(PickleData& other){ + d_blocks.swap(other.d_blocks); + } + + void writeToStringStream(std::ostringstream& oss) const; +};/* class PickleData */ + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PICKLE_DATA_H */ |