diff options
Diffstat (limited to 'src/expr/pickle_data.h')
-rw-r--r-- | src/expr/pickle_data.h | 120 |
1 files changed, 0 insertions, 120 deletions
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h deleted file mode 100644 index 316b6285c..000000000 --- a/src/expr/pickle_data.h +++ /dev/null @@ -1,120 +0,0 @@ -/********************* */ -/*! \file pickle_data.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 = 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; - -struct BlockHeader { - uint64_t d_kind : NBITS_KIND; -};/* struct BlockHeader */ - -struct BlockHeaderOperator { - uint64_t d_kind : NBITS_KIND; - uint64_t d_nchildren : NBITS_NCHILDREN; - uint64_t : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); -};/* struct BlockHeaderOperator */ - -struct BlockHeaderConstant { - uint64_t d_kind : NBITS_KIND; - uint64_t d_constblocks : NBITS_BLOCK - NBITS_KIND; -};/* struct BlockHeaderConstant */ - -struct BlockHeaderVariable { - uint64_t d_kind : NBITS_KIND; - uint64_t : NBITS_BLOCK - NBITS_KIND; -};/* struct BlockHeaderVariable */ - -struct BlockBody { - uint64_t 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 */ |