1 files changed, 0 insertions, 116 deletions
diff --git a/src/util/dump.h b/src/util/dump.h
deleted file mode 100644
index 2cf5877d4..000000000
--- a/src/util/dump.h
+++ /dev/null
@@ -1,116 +0,0 @@
-/*********************                                                        */
-/*! \file dump.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__DUMP_H
-#define __CVC4__DUMP_H
-
-#include "expr/command.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC CVC4dumpstream {
-
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-  std::ostream* d_os;
-#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
-
-#ifdef CVC4_PORTFOLIO
-  CommandSequence* d_commands;
-#endif /* CVC4_PORTFOLIO */
-
-public:
-  CVC4dumpstream() throw()
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
-    : d_os(NULL), d_commands(NULL)
-#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-    : d_os(NULL)
-#elif defined(CVC4_PORTFOLIO)
-    : d_commands(NULL)
-#endif /* CVC4_PORTFOLIO */
-  { }
-
-  CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
-    : d_os(&os), d_commands(&commands)
-#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-    : d_os(&os)
-#elif defined(CVC4_PORTFOLIO)
-    : d_commands(&commands)
-#endif /* CVC4_PORTFOLIO */
-  { }
-
-  CVC4dumpstream& operator<<(const Command& c) {
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-    if(d_os != NULL) {
-      (*d_os) << c << std::endl;
-    }
-#endif
-#if defined(CVC4_PORTFOLIO)
-    if(d_commands != NULL) {
-      d_commands->addCommand(c.clone());
-    }
-#endif
-    return *this;
-  }
-};/* class CVC4dumpstream */
-
-/** The dump class */
-class CVC4_PUBLIC DumpC {
-  std::set<std::string> d_tags;
-  CommandSequence d_commands;
-
-public:
-  CVC4dumpstream operator()(const char* tag) {
-    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
-      return CVC4dumpstream(getStream(), d_commands);
-    } else {
-      return CVC4dumpstream();
-    }
-  }
-  CVC4dumpstream operator()(std::string tag) {
-    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
-      return CVC4dumpstream(getStream(), d_commands);
-    } else {
-      return CVC4dumpstream();
-    }
-  }
-
-  void clear() { d_commands.clear(); }
-  const CommandSequence& getCommands() const { return d_commands; }
-
-  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
-  bool on (std::string tag) { d_tags.insert(tag); return true; }
-  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
-  bool off(std::string tag) { d_tags.erase (tag); return false; }
-  bool off()                { d_tags.clear(); return false; }
-
-  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
-  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
-
-  std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; }
-  std::ostream& getStream() { return DumpOut.getStream(); }
-};/* class DumpC */
-
-/** The dump singleton */
-extern DumpC DumpChannel CVC4_PUBLIC;
-
-#define Dump ::CVC4::DumpChannel
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__DUMP_H */