Cleaning up some header files

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8437d61b259b238b6478eff6d2bd4d0bff794a27..b2c8b8c1d888110cb4b254aa7137ee924da406ef 100644 (file)
--- 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 a60278ebad4fdd8999cb609131fa59416ff1e9b4..faa80fb841ef291420dbdd43aeb8e6cebf7d6704 100644 (file)
--- 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 0533200fa492ef3b446b1b8f4085d6beaf4f7dd2..a621441e16b43a09028b08a5a9b5c9ecac84dd35 100644 (file)
--- 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 d86a18004ada8ae1f5f0d15797822909205513ba..c88f368d27459fd0849be1f9fc326426ce551566 100644 (file)
--- 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 8a35480cd096e032bab5aedb7bb12428d93ea031..6ed9bb441670e3915a9f623ac40df4a0a6ee61d8 100644 (file)
--- 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 ed7db63cf6f7ddcc657d4134187c8ac47c948593..f7adb2b898009eadd0921af0140bbd7b69cec8fc 100644 (file)
--- 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 2bf0aac31f77730d813cf4921ba948e21625bbc9..4ecba67c2e838e384eb4299ebe657c48ff982ef5 100644 (file)
--- 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 f1fd26ec10ff7cdd4e1fd38d28a1d372c8d637e8..7debc3cf8ffa45744b93b15ed9ccde0528e50148 100644 (file)
--- 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 (file)
index b6c6178..0000000
--- 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 d511e48e74d63c97ed158e6a6f98438fc2e7d278..f061c9c9afceb2d50f2bdc4eb7c0c4d8a3724814 100644 (file)
--- 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 288c3b1d5715972585efb5e9e7b2ccab30e781df..2e1a6d3f4a39da99e34e1aeca24534844cdaf35b 100644 (file)
--- 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 407021b50482d2463dd7120d8add94f812304b2d..06259ddb0893ecb5f311fa47d8094f8e37c78933 100644 (file)
--- 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;