Remove portfolio (#3236)

8 files changed, 0 insertions, 812 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 300af8e8c..cae23054c 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -33,10 +33,6 @@ libcvc4_add_sources(
   node_trie.h
   node_value.cpp
   node_value.h
-  pickle_data.cpp
-  pickle_data.h
-  pickler.cpp
-  pickler.h
   symbol_table.cpp
   symbol_table.h
   term_canonize.cpp
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 17affaef0..a4efa7286 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -44,12 +44,6 @@ class IntStat;
 struct ExprManagerMapCollection;
 class ResourceManager;
 
-namespace expr {
-  namespace pickle {
-    class Pickler;
-  }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
 class CVC4_PUBLIC ExprManager {
 private:
   /** The internal node manager */
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index a32590050..458255c06 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -64,12 +64,6 @@ namespace api {
 class Solver;
 }
 
-namespace expr {
-  namespace pickle {
-    class Pickler;
-  }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
 namespace prop {
   class TheoryProxy;
 }/* CVC4::prop namespace */
@@ -218,7 +212,6 @@ class CVC4_PUBLIC Expr {
   friend class TypeCheckingException;
   friend class api::Solver;
   friend class expr::ExportPrivate;
-  friend class expr::pickle::Pickler;
   friend class prop::TheoryProxy;
   friend class smt::SmtEnginePrivate;
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
diff --git a/src/expr/node.h b/src/expr/node.h
index 768d7b948..f0ee7a56c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -52,12 +52,6 @@ namespace CVC4 {
 class TypeNode;
 class NodeManager;
 
-namespace expr {
-  namespace pickle {
-    class PicklerPrivate;
-  }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
 template <bool ref_count>
 class NodeTemplate;
 
@@ -182,7 +176,6 @@ class NodeTemplate {
    */
   friend class expr::NodeValue;
 
-  friend class expr::pickle::PicklerPrivate;
   friend class expr::ExportPrivate;
 
   /** A convenient null-valued encapsulated pointer */
diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp
deleted file mode 100644
index fd3b69d26..000000000
--- a/src/expr/pickle_data.cpp
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                                        */
-/*! \file pickle_data.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** 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 <iostream>
-#include <sstream>
-#include <string>
-
-#include "base/cvc4_assert.h"
-#include "expr/pickle_data.h"
-#include "expr/expr.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "expr/expr_manager_scope.h"
-#include "expr/variable_type_map.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
-
-namespace CVC4 {
-namespace expr {
-namespace pickle {
-
-void PickleData::writeToStringStream(std::ostringstream& oss) const {
-  BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end();
-  for(; i != end; ++i) {
-    Block b = *i;
-    Assert(sizeof(b) * 8 == NBITS_BLOCK);
-    oss << b.d_body.d_data << " ";
-  }
-}
-
-std::string PickleData::toString() const {
-  std::ostringstream oss;
-  oss.flags(std::ios::oct | std::ios::showbase);
-  writeToStringStream(oss);
-  return oss.str();
-}
-
-}/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
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 */
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
deleted file mode 100644
index 42198d676..000000000
--- a/src/expr/pickler.cpp
+++ /dev/null
@@ -1,481 +0,0 @@
-/*********************                                                        */
-/*! \file pickler.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Kshitij Bansal, Tim King
- ** 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 "pickler" for expressions
- **
- ** This is a "pickler" for expressions.  It produces a binary
- ** serialization of an expression that can be converted back
- ** into an expression in the same or another ExprManager.
- **/
-
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-#include "expr/pickler.h"
-#include "expr/pickle_data.h"
-#include "expr/expr.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "expr/expr_manager_scope.h"
-#include "expr/variable_type_map.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
-
-namespace CVC4 {
-namespace expr {
-namespace pickle {
-
-class PicklerPrivate {
-public:
-  typedef std::stack<Node> NodeStack;
-  NodeStack d_stack;
-
-  PickleData d_current;
-
-  Pickler& d_pickler;
-
-  NodeManager* const d_nm;
-
-  PicklerPrivate(Pickler& pickler, ExprManager* em) :
-    d_pickler(pickler),
-    d_nm(NodeManager::fromExprManager(em)) {
-  }
-
-  bool atDefaultState(){
-    return d_stack.empty() && d_current.empty();
-  }
-
-  /* Helper functions for toPickle */
-  void toCaseNode(TNode n);
-  void toCaseVariable(TNode n);
-  void toCaseConstant(TNode n);
-  void toCaseOperator(TNode n);
-  void toCaseString(Kind k, const std::string& s);
-
-  /* Helper functions for toPickle */
-  Node fromCaseOperator(Kind k, uint32_t nchildren);
-  Node fromCaseConstant(Kind k, uint32_t nblocks);
-  std::string fromCaseString(uint32_t nblocks);
-  Node fromCaseVariable(Kind k);
-
-};/* class PicklerPrivate */
-
-static Block mkBlockBody4Chars(char a, char b, char c, char d) {
-  Block newBody;
-  newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d;
-  return newBody;
-}
-
-static char getCharBlockBody(BlockBody body, int i) {
-  Assert(0 <= i && i <= 3);
-
-  switch(i) {
-  case 0: return (body.d_data & 0xff000000) >> 24;
-  case 1: return (body.d_data & 0x00ff0000) >> 16;
-  case 2: return (body.d_data & 0x0000ff00) >> 8;
-  case 3: return (body.d_data & 0x000000ff);
-  default:
-    Unreachable();
-  }
-  return '\0';
-}
-
-static Block mkBlockBody(unsigned data) {
-  Block newBody;
-  newBody.d_body.d_data = data;
-  return newBody;
-}
-
-static Block mkOperatorHeader(Kind k, unsigned numChildren) {
-  Block newHeader;
-  newHeader.d_headerOperator.d_kind = k;
-  newHeader.d_headerOperator.d_nchildren = numChildren;
-  return newHeader;
-}
-
-static Block mkVariableHeader(Kind k) {
-  Block newHeader;
-  newHeader.d_header.d_kind = k;
-  return newHeader;
-}
-
-static Block mkConstantHeader(Kind k, unsigned numBlocks) {
-  Block newHeader;
-  newHeader.d_headerConstant.d_kind = k;
-  newHeader.d_headerConstant.d_constblocks = numBlocks;
-  return newHeader;
-}
-
-Pickler::Pickler(ExprManager* em) :
-  d_private(new PicklerPrivate(*this, em)) {
-}
-
-Pickler::~Pickler() {
-  delete d_private;
-}
-
-void Pickler::toPickle(Expr e, Pickle& p)
-{
-  Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
-  Assert(d_private->atDefaultState());
-
-  try{
-    d_private->d_current.swap(*p.d_data);
-    d_private->toCaseNode(e.getTNode());
-    d_private->d_current.swap(*p.d_data);
-  }catch(PicklingException& pe){
-    d_private->d_current = PickleData();
-    Assert(d_private->atDefaultState());
-    throw pe;
-  }
-
-  Assert(d_private->atDefaultState());
-}
-
-void PicklerPrivate::toCaseNode(TNode n)
-{
-  Debug("pickler") << "toCaseNode: " << n << std::endl;
-  Kind k = n.getKind();
-  kind::MetaKind m = metaKindOf(k);
-  switch(m) {
-  case kind::metakind::CONSTANT:
-    toCaseConstant(n);
-    break;
-  case kind::metakind::VARIABLE:
-    toCaseVariable(n);
-    break;
-  case kind::metakind::OPERATOR:
-  case kind::metakind::PARAMETERIZED:
-    toCaseOperator(n);
-    break;
-  default:
-    Unhandled(m);
-  }
-}
-
-void PicklerPrivate::toCaseOperator(TNode n)
-{
-  Kind k = n.getKind();
-  kind::MetaKind m = metaKindOf(k);
-  Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR);
-  if(m == kind::metakind::PARAMETERIZED) {
-    toCaseNode(n.getOperator());
-  }
-  for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
-    toCaseNode(*i);
-  }
-  d_current << mkOperatorHeader(k, n.getNumChildren());
-}
-
-void PicklerPrivate::toCaseVariable(TNode n)
-{
-  Kind k = n.getKind();
-  Assert(metaKindOf(k) == kind::metakind::VARIABLE);
-
-  const NodeValue* nv = n.d_nv;
-  uint64_t asInt = reinterpret_cast<uint64_t>(nv);
-  uint64_t mapped = d_pickler.variableToMap(asInt);
-
-  uint32_t firstHalf = mapped >> 32;
-  uint32_t secondHalf = mapped & 0xffffffff;
-
-  d_current << mkVariableHeader(k);
-  d_current << mkBlockBody(firstHalf);
-  d_current << mkBlockBody(secondHalf);
-}
-
-
-void PicklerPrivate::toCaseConstant(TNode n) {
-  Kind k = n.getKind();
-  Assert(metaKindOf(k) == kind::metakind::CONSTANT);
-  switch(k) {
-  case kind::CONST_BOOLEAN:
-    d_current << mkConstantHeader(k, 1);
-    d_current << mkBlockBody(n.getConst<bool>());
-    break;
-  case kind::CONST_RATIONAL: {
-    std::string asString;
-    Assert(k == kind::CONST_RATIONAL);
-    const Rational& q = n.getConst<Rational>();
-    asString = q.toString(16);
-    toCaseString(k, asString);
-    break;
-  }
-  case kind::BITVECTOR_EXTRACT_OP: {
-    BitVectorExtract bve = n.getConst<BitVectorExtract>();
-    d_current << mkConstantHeader(k, 2);
-    d_current << mkBlockBody(bve.high);
-    d_current << mkBlockBody(bve.low);
-    break;
-  }
-  case kind::CONST_BITVECTOR: {
-    // irritating: we incorporate the size of the string in with the
-    // size of this constant, so it appears as one big constant and
-    // doesn't confuse anybody
-    BitVector bv = n.getConst<BitVector>();
-    std::string asString = bv.getValue().toString(16);
-    d_current << mkConstantHeader(k, 2 + asString.size());
-    d_current << mkBlockBody(bv.getSize());
-    toCaseString(k, asString);
-    break;
-  }
-  case  kind::BITVECTOR_SIGN_EXTEND_OP: {
-    BitVectorSignExtend bvse = n.getConst<BitVectorSignExtend>();
-    d_current << mkConstantHeader(k, 1);
-    d_current << mkBlockBody(bvse.signExtendAmount);
-    break;
-  }
-  default:
-    Unhandled(k);
-  }
-}
-
-void PicklerPrivate::toCaseString(Kind k, const std::string& s) {
-  d_current << mkConstantHeader(k, s.size());
-
-  unsigned size = s.size();
-  unsigned i;
-  for(i = 0; i + 4 <= size; i += 4) {
-    d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]);
-  }
-  switch(size % 4) {
-  case 0: break;
-  case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break;
-  case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break;
-  case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break;
-  default:
-    Unreachable();
-  }
-
-}
-
-void Pickler::debugPickleTest(Expr e) {
-
-  //ExprManager *em = e.getExprManager();
-  //Expr e1 = mkVar("x", makeType());
-  //return ;
-
-  Pickler pickler(e.getExprManager());
-
-  Pickle p;
-  pickler.toPickle(e, p);
-
-  uint32_t size = p.d_data->size();
-  std::string str = p.d_data->toString();
-
-  Expr from = pickler.fromPickle(p);
-  ExprManagerScope ems(e);
-
-  Debug("pickle") << "before: " << e << std::endl;
-  Debug("pickle") << "after: " << from.getNode() << std::endl;
-  Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl;
-
-  Assert(p.d_data->empty());
-  Assert(e == from);
-}
-
-Expr Pickler::fromPickle(Pickle& p) {
-  Assert(d_private->atDefaultState());
-
-  d_private->d_current.swap(*p.d_data);
-
-  while(!d_private->d_current.empty()) {
-    Block front = d_private->d_current.dequeue();
-
-    Kind k = (Kind)front.d_header.d_kind;
-    kind::MetaKind m = metaKindOf(k);
-
-    Node result = Node::null();
-    switch(m) {
-    case kind::metakind::VARIABLE:
-      result = d_private->fromCaseVariable(k);
-      break;
-    case kind::metakind::CONSTANT:
-      result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks);
-      break;
-    case kind::metakind::OPERATOR:
-    case kind::metakind::PARAMETERIZED:
-      result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren);
-      break;
-    default:
-      Unhandled(m);
-    }
-    Assert(result != Node::null());
-    d_private->d_stack.push(result);
-  }
-
-  Assert(d_private->d_current.empty());
-  Assert(d_private->d_stack.size() == 1);
-  Node res = d_private->d_stack.top();
-  d_private->d_stack.pop();
-
-  Assert(d_private->atDefaultState());
-
-  return d_private->d_nm->toExpr(res);
-}
-
-Node PicklerPrivate::fromCaseVariable(Kind k) {
-  Assert(metaKindOf(k) == kind::metakind::VARIABLE);
-
-  Block firstHalf = d_current.dequeue();
-  Block secondHalf = d_current.dequeue();
-
-  uint64_t asInt = firstHalf.d_body.d_data;
-  asInt = asInt << 32;
-  asInt = asInt | (secondHalf.d_body.d_data);
-
-  uint64_t mapped = d_pickler.variableFromMap(asInt);
-
-  NodeValue* nv = reinterpret_cast<NodeValue*>(mapped);
-  Node fromNodeValue(nv);
-
-  Assert(fromNodeValue.getKind() == k);
-
-  return fromNodeValue;
-}
-
-Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) {
-  switch(k) {
-  case kind::CONST_BOOLEAN: {
-    Assert(constblocks == 1);
-    Block val = d_current.dequeue();
-
-    bool b= val.d_body.d_data;
-    return d_nm->mkConst<bool>(b);
-  }
-  case kind::CONST_RATIONAL: {
-    std::string s = fromCaseString(constblocks);
-    Rational q(s, 16);
-    return d_nm->mkConst<Rational>(q);
-  }
-  case kind::BITVECTOR_EXTRACT_OP: {
-    Block high = d_current.dequeue();
-    Block low = d_current.dequeue();
-    BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data);
-    return d_nm->mkConst<BitVectorExtract>(bve);
-  }
-  case kind::CONST_BITVECTOR: {
-    unsigned size = d_current.dequeue().d_body.d_data;
-    Block header CVC4_UNUSED = d_current.dequeue();
-    Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR);
-    Assert(header.d_headerConstant.d_constblocks == constblocks - 2);
-    Integer value(fromCaseString(constblocks - 2));
-    BitVector bv(size, value);
-    return d_nm->mkConst(bv);
-  }
-  case  kind::BITVECTOR_SIGN_EXTEND_OP: {
-    Block signExtendAmount = d_current.dequeue();
-    BitVectorSignExtend bvse(signExtendAmount.d_body.d_data);
-    return d_nm->mkConst<BitVectorSignExtend>(bvse);
-  }
-  default:
-    Unhandled(k);
-  }
-}
-
-std::string PicklerPrivate::fromCaseString(uint32_t size) {
-  std::stringstream ss;
-  unsigned i;
-  for(i = 0; i + 4 <= size; i += 4) {
-    Block front = d_current.dequeue();
-    BlockBody body = front.d_body;
-
-    ss << getCharBlockBody(body,0)
-       << getCharBlockBody(body,1)
-       << getCharBlockBody(body,2)
-       << getCharBlockBody(body,3);
-  }
-  Assert(i == size - (size%4) );
-  if(size % 4 != 0) {
-    Block front = d_current.dequeue();
-    BlockBody body = front.d_body;
-    switch(size % 4) {
-    case 1:
-      ss << getCharBlockBody(body,0);
-      break;
-    case 2:
-      ss << getCharBlockBody(body,0)
-         << getCharBlockBody(body,1);
-      break;
-    case 3:
-      ss << getCharBlockBody(body,0)
-         << getCharBlockBody(body,1)
-         << getCharBlockBody(body,2);
-      break;
-    default:
-      Unreachable();
-    }
-  }
-  return ss.str();
-}
-
-Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) {
-  kind::MetaKind m = metaKindOf(k);
-  bool parameterized = (m == kind::metakind::PARAMETERIZED);
-  uint32_t npops = nchildren + (parameterized? 1 : 0);
-
-  NodeStack aux;
-  while(npops > 0) {
-    Assert(!d_stack.empty());
-    Node top = d_stack.top();
-    aux.push(top);
-    d_stack.pop();
-    --npops;
-  }
-
-  NodeBuilder<> nb(d_nm, k);
-  while(!aux.empty()) {
-    Node top = aux.top();
-    nb << top;
-    aux.pop();
-  }
-
-  return nb;
-}
-
-Pickle::Pickle() {
-  d_data = new PickleData();
-}
-
-// Just copying the pointer isn't right, we have to copy the
-// underlying data.  Otherwise user-level Pickles will delete the data
-// twice! (once in each thread)
-Pickle::Pickle(const Pickle& p) {
-  d_data = new PickleData(*p.d_data);
-}
-
-Pickle& Pickle::operator = (const Pickle& other) {
-  if (this != &other) {
-    delete d_data;
-    d_data = new PickleData(*other.d_data);
-  }
-  return *this;
-}
-
-
-Pickle::~Pickle() {
-  delete d_data;
-}
-
-uint64_t MapPickler::variableFromMap(uint64_t x) const 
-{
-  VarMap::const_iterator i = d_fromMap.find(x);
-  Assert(i != d_fromMap.end());
-  return i->second;
-}
-
-}/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
deleted file mode 100644
index 02abdf18d..000000000
--- a/src/expr/pickler.h
+++ /dev/null
@@ -1,129 +0,0 @@
-/*********************                                                        */
-/*! \file pickler.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Clark Barrett
- ** 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 "pickler" for expressions
- **
- ** This is a "pickler" for expressions.  It produces a binary
- ** serialization of an expression that can be converted back
- ** into an expression in the same or another ExprManager.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__PICKLER_H
-#define CVC4__PICKLER_H
-
-#include "expr/variable_type_map.h"
-#include "expr/expr.h"
-#include "base/exception.h"
-
-#include <exception>
-#include <stack>
-
-namespace CVC4 {
-
-class ExprManager;
-
-namespace expr {
-namespace pickle {
-
-class Pickler;
-class PicklerPrivate;
-
-class PickleData;// CVC4-internal representation
-
-class CVC4_PUBLIC Pickle {
-  PickleData* d_data;
-  friend class Pickler;
-  friend class PicklerPrivate;
-public:
-  Pickle();
-  Pickle(const Pickle& p);
-  ~Pickle();
-  Pickle& operator=(const Pickle& other);
-};/* class Pickle */
-
-class CVC4_PUBLIC PicklingException : public Exception {
-public:
-  PicklingException() :
-    Exception("Pickling failed") {
-  }
-};/* class PicklingException */
-
-class CVC4_PUBLIC Pickler {
-  PicklerPrivate* d_private;
-
-  friend class PicklerPrivate;
-
-protected:
- virtual uint64_t variableToMap(uint64_t x) const { return x; }
- virtual uint64_t variableFromMap(uint64_t x) const { return x; }
-public:
-  Pickler(ExprManager* em);
-  virtual ~Pickler();
-
-  /**
-   * Constructs a new Pickle of the node n.
-   * n must be a node allocated in the node manager specified at initialization
-   * time. The new pickle has variables mapped using the VariableIDMap provided
-   * at initialization.
-   * TODO: Fix comment
-   *
-   * @return the pickle, which should be dispose()'d when you're done with it
-   */
-  void toPickle(Expr e, Pickle& p);
-
-  /**
-   * Constructs a node from a Pickle.
-   * This destroys the contents of the Pickle.
-   * The node is created in the NodeManager getNM();
-   * TODO: Fix comment
-   */
-  Expr fromPickle(Pickle& p);
-
-  static void debugPickleTest(Expr e);
-
-};/* class Pickler */
-
-class CVC4_PUBLIC MapPickler : public Pickler {
-private:
-  const VarMap& d_toMap;
-  const VarMap& d_fromMap;
-
-public:
-  MapPickler(ExprManager* em, const VarMap& to, const VarMap& from):
-    Pickler(em),
-    d_toMap(to),
-    d_fromMap(from) {
-  }
-
-protected:
- uint64_t variableToMap(uint64_t x) const override
- {
-   VarMap::const_iterator i = d_toMap.find(x);
-   if (i != d_toMap.end())
-   {
-     return i->second;
-   }
-   else
-   {
-     throw PicklingException();
-   }
-  }
-
-  uint64_t variableFromMap(uint64_t x) const override;
-};/* class MapPickler */
-
-}/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__PICKLER_H */