diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/language.h | 31 | ||||
-rw-r--r-- | src/parser/parser.h | 15 | ||||
-rw-r--r-- | src/parser/parser_state.h | 2 | ||||
-rw-r--r-- | src/parser/pl.ypp | 4 | ||||
-rw-r--r-- | src/parser/smtlib.ypp | 4 |
5 files changed, 42 insertions, 14 deletions
diff --git a/src/parser/language.h b/src/parser/language.h new file mode 100644 index 000000000..7ea6547cd --- /dev/null +++ b/src/parser/language.h @@ -0,0 +1,31 @@ +/********************* -*- C++ -*- */ +/** language.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Input languages. + **/ + +#ifndef __CVC4__PARSER__LANGUAGE_H +#define __CVC4__PARSER__LANGUAGE_H + +#include "util/exception.h" +#include "parser/language.h" + +namespace CVC4 { +namespace parser { + +enum Language { + AUTO = 0, + PL, + SMTLIB, +};/* enum Language */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__LANGUAGE_H */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 36b8c34eb..73565b8c4 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,13 +13,13 @@ #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H -#include "core/exception.h" -#include "core/lang.h" +#include "util/exception.h" +#include "parser/language.h" +#include "util/command.h" namespace CVC4 { namespace parser { - class ValidityChecker; class Expr; // Internal parser state and other data @@ -33,16 +33,11 @@ namespace parser { void deleteParser(); public: // Constructors - Parser(ValidityChecker* vc, InputLanguage lang, - // The 'interactive' flag is ignored when fileName != "" - bool interactive = true, - const std::string& fileName = ""); - Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is, - bool interactive = false); + Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false); // Destructor ~Parser(); // Read the next command. - Expr next(); + CVC4::Command* next(); // Check if we are done (end of input has been reached) bool done() const; // The same check can be done by using the class Parser's value as diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 4eda5eb38..1d013a0b4 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -19,7 +19,7 @@ #include <iostream> #include <sstream> -#include "cvc4_expr.h" +#include "expr/expr.h" #include "expr/expr_manager.h" #include "util/exception.h" diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index e7d752419..b59c7c69e 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -13,10 +13,10 @@ %{ -#include "cvc4.h" -#include "cvc4_expr.h" +#include "smt/smt_engine.h" #include "parser/parser_exception.h" #include "parser/parser_state.h" +#include "expr/expr.h" #include "expr/expr_builder.h" #include "expr/expr_manager.h" #include "util/command.h" diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 692a9cda5..e616b3a65 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,10 +11,12 @@ ** commands in SMT-LIB language. **/ -#include "cvc4.h" +#include "smt/smt_engine.h" #include "parser/parser_exception.h" #include "parser/parser_state.h" +#include <vector> + // Exported shared data namespace CVC4 { extern ParserState* parserState; |