Cleaning up some header files

12 files changed, 44 insertions, 72 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8437d61b2..b2c8b8c1d 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -17,17 +17,32 @@
 #include <iostream>
 
 #include "interactive_shell.h"
+
 #include "expr/command.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "util/options.h"
 
 using namespace std;
 
 namespace CVC4 {
 
+using namespace parser;
+
 const string InteractiveShell::INPUT_FILENAME = "<shell>";
 
+InteractiveShell::InteractiveShell(ExprManager& exprManager,
+                                   const Options& options) : 
+   d_in(*options.in),
+   d_out(*options.out),
+   d_language(options.inputLanguage) {
+   ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
+   /* Create parser with bogus input. */
+   d_parser = parserBuilder.withStringInput("").build();
+}
+
+
 Command* InteractiveShell::readCommand() {
   /* Don't do anything if the input is closed. */
   if( d_in.eof() ) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index a60278eba..faa80fb84 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -20,34 +20,29 @@
 #include <iostream>
 #include <string>
 
-#include "parser/parser_builder.h"
 #include "util/language.h"
-#include "util/options.h"
 
 namespace CVC4 {
 
   class Command;
+  class ExprManager;
+  class Options;
 
-  using namespace parser;
+  namespace parser {
+    class Parser;
+  }
 
 class CVC4_PUBLIC InteractiveShell {
   std::istream& d_in;
   std::ostream& d_out;
-  Parser* d_parser;
+  parser::Parser* d_parser;
   const InputLanguage d_language;
 
   static const std::string INPUT_FILENAME;
 
 public:
   InteractiveShell(ExprManager& exprManager,
-                  const Options& options) : 
-    d_in(*options.in),
-    d_out(*options.out),
-    d_language(options.inputLanguage) {
-    ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
-    /* Create parser with bogus input. */
-    d_parser = parserBuilder.withStringInput("").build();
-  }
+                   const Options& options);
 
   /** Read a command from the interactive shell. This will read as
       many lines as necessary to parse a well-formed command. */
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 0533200fa..a621441e1 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -53,7 +53,6 @@ libcvc4parser_la_SOURCES = \
 	parser.cpp \
 	parser_builder.h \
 	parser_builder.cpp \
-	parser_options.h \
 	parser_exception.h
 
 libcvc4parser_noinst_la_SOURCES = \
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index d86a18004..c88f368d2 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -28,12 +28,10 @@
 #include <string>
 #include <vector>
 
-#include "parser/input.h"
-#include "parser/parser_options.h"
-#include "parser/parser_exception.h"
-#include "parser/bounded_token_buffer.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "bounded_token_buffer.h"
+#include "parser_exception.h"
+#include "input.h"
+
 #include "util/Assert.h"
 #include "util/bitvector.h"
 #include "util/integer.h"
diff --git a/src/parser/input.h b/src/parser/input.h
index 8a35480cd..6ed9bb441 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -29,8 +29,8 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/parser_exception.h"
-#include "parser/parser_options.h"
 #include "util/Assert.h"
+#include "util/language.h"
 
 namespace CVC4 {
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index ed7db63cf..f7adb2b89 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -27,24 +27,23 @@
 
 #include "input.h"
 #include "parser_exception.h"
-#include "parser_options.h"
 #include "expr/declaration_scope.h"
-#include "expr/expr.h"
 #include "expr/kind.h"
-#include "util/Assert.h"
 
 namespace CVC4 {
 
 // Forward declarations
 class BooleanType;
+class Expr;
 class ExprManager;
 class Command;
 class FunctionType;
-class KindType;
 class Type;
 
 namespace parser {
 
+class Input;
+
 /** Types of check for the symols */
 enum DeclarationCheck {
   /** Enforce that the symbol has been declared */
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 2bf0aac31..4ecba67c2 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -19,11 +19,13 @@
 #include <string>
 
 #include "parser_builder.h"
+#include "input.h"
+#include "parser.h"
+#include "smt/smt.h"
+#include "smt2/smt2.h"
+
 #include "expr/expr_manager.h"
-#include "parser/input.h"
-#include "parser/parser.h"
-#include "parser/smt/smt.h"
-#include "parser/smt2/smt2.h"
+#include "util/options.h"
 
 namespace CVC4 {
 
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index f1fd26ec1..7debc3cf8 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -24,13 +24,13 @@
 #include <string>
 
 #include "input.h"
-#include "parser_options.h"
 
-#include "util/options.h"
+#include "util/language.h"
 
 namespace CVC4 {
 
 class ExprManager;
+class Options;
 
 namespace parser {
 
diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h
deleted file mode 100644
index b6c61786b..000000000
--- a/src/parser/parser_options.h
+++ /dev/null
@@ -1,36 +0,0 @@
-/*********************                                                        */
-/*! \file parser_options.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add file-specific comments here ]].
- **
- ** [[ Add file-specific comments here ]]
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PARSER__PARSER_OPTIONS_H
-#define __CVC4__PARSER__PARSER_OPTIONS_H
-
-#include <iostream>
-
-#include "util/language.h"
-
-namespace CVC4 {
-namespace parser {
-
-// content moved to util/language.h
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__PARSER_OPTIONS_H */
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index d511e48e7..f061c9c9a 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -74,13 +74,13 @@ AM_LDFLAGS_WHITE =
 AM_LDFLAGS_BLACK =
 AM_LDFLAGS_PUBLIC =
 AM_LIBADD_WHITE = \
+	@abs_top_builddir@/src/main/libmain.a \
 	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
-	@abs_top_builddir@/src/libcvc4_noinst.la \
-	@abs_top_builddir@/src/main/libmain.a
+	@abs_top_builddir@/src/libcvc4_noinst.la
 AM_LIBADD_BLACK = \
+	@abs_top_builddir@/src/main/libmain.a \
 	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
-	@abs_top_builddir@/src/libcvc4_noinst.la \
-	@abs_top_builddir@/src/main/libmain.a
+	@abs_top_builddir@/src/libcvc4_noinst.la
 AM_LIBADD_PUBLIC = \
 	@abs_top_builddir@/src/parser/libcvc4parser.la \
 	@abs_top_builddir@/src/libcvc4.la
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 288c3b1d5..2e1a6d3f4 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -25,10 +25,10 @@
 #include "expr/expr_manager.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "parser/parser_options.h"
 #include "parser/smt2/smt2.h"
 #include "expr/command.h"
 #include "util/output.h"
+#include "util/language.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 407021b50..06259ddb0 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -28,7 +28,7 @@
 #include "expr/command.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "parser/parser_options.h"
+#include "util/language.h"
 
 typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;