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 */