Moving sexpr.{cpp,h,i} from expr/ back into util/.

12 files changed, 24 insertions, 28 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 24c4d8112..9ae394b97 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -28,7 +28,6 @@
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/predicate.h"
-#include "expr/sexpr.h"
 #include "options/base_options.h"
 #include "options/expr_options.h"
 #include "options/parser_options.h"
@@ -41,9 +40,9 @@
 #include "util/hash.h"
 #include "util/integer.h"
 #include "util/rational.h"
+#include "util/sexpr.h"
 #include "util/subrange_bound.h"
 
-
 using namespace std;
 
 // Matches base/cvc4_assert.h's PrettyCheckArgument.
diff --git a/src/cvc4.i b/src/cvc4.i
index e81276f23..601c9a878 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -52,12 +52,12 @@ using namespace CVC4;
 #include "base/modal_exception.h"
 #include "expr/datatype.h"
 #include "expr/expr.h"
-#include "expr/sexpr.h"
 #include "expr/type.h"
 #include "options/option_exception.h"
 #include "smt_util/command.h"
-#include "util/integer.h"
 #include "util/bitvector.h"
+#include "util/integer.h"
+#include "util/sexpr.h"
 #include "util/unsafe_interrupt_exception.h"
 
 #ifdef SWIGJAVA
@@ -306,25 +306,24 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 // At the moment, the header includes seem to need to follow a special order.
 // I don't know why. I am following the build order 
 %include "base/exception.i"
-%include "util/unsafe_interrupt_exception.i"
-%include "util/integer.i"
-%include "util/rational.i"
-%include "options/language.i"
-%include "util/configuration.i"
-%include "util/bool.i"
-%include "util/cardinality.i"
 %include "base/modal_exception.i"
-%include "expr/sexpr.i"
-
-%include "util/bitvector.i"
 
+%include "options/language.i"
 
+%include "util/bitvector.i"
+%include "util/bool.i"
+%include "util/cardinality.i"
+%include "util/configuration.i"
 %include "util/hash.i"
+%include "util/integer.i"
 %include "util/proof.i"
+%include "util/rational.i"
 %include "util/regexp.i"
 %include "util/result.i"
+%include "util/sexpr.i"
 %include "util/subrange_bound.i"
 %include "util/tuple.i"
+%include "util/unsafe_interrupt_exception.i"
 //%include "util/floatingpoint.i"
 
 %include "expr/uninterpreted_constant.i"
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index d4964f56a..5c046c282 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -54,8 +54,6 @@ libexpr_la_SOURCES = \
 	pickler.h \
 	resource_manager.cpp \
 	resource_manager.h \
-	sexpr.cpp \
-	sexpr.h \
 	symbol_table.cpp \
 	symbol_table.h \
 	type.cpp \
@@ -109,7 +107,6 @@ EXTRA_DIST = \
 	kind.i \
 	expr.i \
 	resource_manager.i \
-	sexpr.i \
 	record.i \
 	predicate.i \
 	variable_type_map.i \
diff --git a/src/expr/statistics.h b/src/expr/statistics.h
index 425404692..a0b6ed083 100644
--- a/src/expr/statistics.h
+++ b/src/expr/statistics.h
@@ -20,14 +20,14 @@
 #ifndef __CVC4__STATISTICS_H
 #define __CVC4__STATISTICS_H
 
-#include "expr/sexpr.h"
-
 #include <iterator>
 #include <ostream>
 #include <set>
 #include <string>
 #include <utility>
 
+#include "util/sexpr.h"
+
 namespace CVC4 {
 
 class Stat;
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 48787f70a..ca9aff65d 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -23,10 +23,10 @@
 #include <string>
 
 #include "expr/node.h"
-#include "expr/sexpr.h"
 #include "options/language.h"
 #include "smt_util/command.h"
 #include "smt_util/model.h"
+#include "util/sexpr.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3f049e392..531b499ac 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,7 +28,6 @@
 #include "context/cdlist_forward.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "expr/sexpr.h"
 #include "expr/statistics.h"
 #include "options/options.h"
 #include "proof/unsat_core.h"
@@ -38,6 +37,7 @@
 #include "util/hash.h"
 #include "util/proof.h"
 #include "util/result.h"
+#include "util/sexpr.h"
 #include "util/unsafe_interrupt_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp
index 5917d71da..8cc8a421c 100644
--- a/src/smt_util/command.cpp
+++ b/src/smt_util/command.cpp
@@ -27,7 +27,6 @@
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/node.h"
-#include "expr/sexpr.h"
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
@@ -35,6 +34,7 @@
 #include "smt/smt_engine_scope.h"
 #include "smt_util/dump.h"
 #include "smt_util/model.h"
+#include "util/sexpr.h"
 
 using namespace std;
 
diff --git a/src/smt_util/command.h b/src/smt_util/command.h
index c9b968722..d8f9789f5 100644
--- a/src/smt_util/command.h
+++ b/src/smt_util/command.h
@@ -30,12 +30,12 @@
 
 #include "expr/datatype.h"
 #include "expr/expr.h"
-#include "expr/sexpr.h"
 #include "expr/type.h"
 #include "expr/variable_type_map.h"
 #include "proof/unsat_core.h"
 #include "util/proof.h"
 #include "util/result.h"
+#include "util/sexpr.h"
 
 namespace CVC4 {
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b06666ae3..d086e3068 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -45,6 +45,8 @@ libutil_la_SOURCES = \
 	regexp.h \
 	result.cpp \
 	result.h \
+	sexpr.cpp \
+	sexpr.h \
 	smt2_quote_string.cpp \
 	smt2_quote_string.h \
 	subrange_bound.cpp \
@@ -92,6 +94,7 @@ EXTRA_DIST = \
 	rational_gmp_imp.h \
 	regexp.i \
 	result.i \
+	sexpr.i \
 	subrange_bound.i \
 	tuple.i \
 	unsafe_interrupt_exception.i
diff --git a/src/expr/sexpr.cpp b/src/util/sexpr.cpp
index 69741859f..eb53e34c2 100644
--- a/src/expr/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -22,18 +22,16 @@
  ** handled in the SExpr class and the libexpr library.
  **/
 
-#include "expr/sexpr.h"
+#include "util/sexpr.h"
 
 #include <iostream>
 #include <sstream>
 #include <vector>
 
 #include "base/cvc4_assert.h"
-#include "expr/expr.h"
 #include "options/set_language.h"
 #include "util/smt2_quote_string.h"
 
-
 namespace CVC4 {
 
 const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
diff --git a/src/expr/sexpr.h b/src/util/sexpr.h
index 40fd9dd56..40fd9dd56 100644
--- a/src/expr/sexpr.h
+++ b/src/util/sexpr.h
diff --git a/src/expr/sexpr.i b/src/util/sexpr.i
index f6229782e..4c89c5019 100644
--- a/src/expr/sexpr.i
+++ b/src/util/sexpr.i
@@ -1,5 +1,5 @@
 %{
-#include "expr/sexpr.h"
+#include "util/sexpr.h"
 %}
 
 %ignore CVC4::operator<<(std::ostream&, const SExpr&);
@@ -18,4 +18,4 @@
 %rename(equals) CVC4::SExpr::operator==(const SExpr&) const;
 %ignore CVC4::SExpr::operator!=(const SExpr&) const;
 
-%include "expr/sexpr.h"
+%include "util/sexpr.h"