From d1459372b7d5f766cd20fb5546ce82bfbb5726b5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 18 Jul 2012 17:34:12 +0000
Subject: [PATCH] removing output operator for SExprTypes, which is never used
 (and SExprTypes is not public-facing)---this fixes the language bindings,
 which fixes the broken debian build overnight

---
 src/util/sexpr.cpp | 24 ------------------------
 src/util/sexpr.h   |  3 ---
 2 files changed, 27 deletions(-)

diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index ff6ff6872..f90426fab 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -26,30 +26,6 @@
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, SExpr::SExprTypes type) {
-  switch(type) {
-  case SExpr::SEXPR_STRING:
-    out << "SEXPR_STRING";
-    break;
-  case SExpr::SEXPR_KEYWORD:
-    out << "SEXPR_KEYWORD";
-    break;
-  case SExpr::SEXPR_INTEGER:
-    out << "SEXPR_INTEGER";
-    break;
-  case SExpr::SEXPR_RATIONAL:
-    out << "SEXPR_RATIONAL";
-    break;
-  case SExpr::SEXPR_NOT_ATOM:
-    out << "SEXPR_NOT_ATOM";
-    break;
-  default:
-    Unimplemented();
-    break;
-  }
-  return out;
-}
-
 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
   Printer::getPrinter(Expr::setlanguage::getLanguage(out))->toStream(out, sexpr);
   return out;
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index a49da4b48..9db9a34ce 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -43,7 +43,6 @@ class CVC4_PUBLIC SExpr {
     SEXPR_RATIONAL,
     SEXPR_NOT_ATOM
   } d_sexprType;
-  friend std::ostream& operator<<(std::ostream&, SExprTypes);
 
   /** The value of an atomic integer-valued S-expression. */
   CVC4::Integer d_integerValue;
@@ -154,8 +153,6 @@ public:
 
 };/* class SExpr */
 
-std::ostream& operator<<(std::ostream& out, SExpr::SExprTypes type) CVC4_PUBLIC;
-
 inline bool SExpr::isAtom() const {
   return d_sexprType != SEXPR_NOT_ATOM;
 }
-- 
2.30.2