From f4969cca302fe640fed334cf9cbf8e032b468ae6 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 26 Oct 2010 18:17:13 +0000 Subject: 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 ------------------------------------ 9 files changed, 38 insertions(+), 66 deletions(-) delete mode 100644 src/parser/parser_options.h (limited to 'src') 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 */ -- cgit v1.2.3