From f4969cca302fe640fed334cf9cbf8e032b468ae6 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 26 Oct 2010 18:17:13 +0000 Subject: [PATCH] Cleaning up some header files --- src/main/interactive_shell.cpp | 15 +++++++++++ src/main/interactive_shell.h | 19 +++++-------- src/parser/Makefile.am | 1 - src/parser/antlr_input.h | 10 +++---- src/parser/input.h | 2 +- src/parser/parser.h | 7 +++-- src/parser/parser_builder.cpp | 10 ++++--- src/parser/parser_builder.h | 4 +-- src/parser/parser_options.h | 36 ------------------------- test/unit/Makefile.am | 8 +++--- test/unit/parser/parser_black.h | 2 +- test/unit/parser/parser_builder_black.h | 2 +- 12 files changed, 44 insertions(+), 72 deletions(-) delete mode 100644 src/parser/parser_options.h 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 #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 = ""; +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 #include -#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 #include -#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 #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 #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 - -#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 filebuf_gnu; -- 2.30.2