summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/Makefile.am2
-rw-r--r--src/parser/input.h11
-rw-r--r--src/parser/parser.h16
-rw-r--r--src/parser/parser_builder.cpp141
-rw-r--r--src/parser/parser_builder.h91
-rw-r--r--src/parser/smt2/Smt2.g13
-rw-r--r--src/parser/smt2/smt2.cpp79
-rw-r--r--src/parser/smt2/smt2.h31
-rw-r--r--src/parser/smt2/smt2_input.cpp7
-rw-r--r--src/parser/smt2/smt2_input.h7
10 files changed, 329 insertions, 69 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 7029c01e5..f95b01b8c 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -48,6 +48,8 @@ libcvc4parser_noinst_la_SOURCES = \
memory_mapped_input_buffer.cpp \
parser.h \
parser.cpp \
+ parser_builder.h \
+ parser_builder.cpp \
parser_options.h \
parser_exception.h
diff --git a/src/parser/input.h b/src/parser/input.h
index 114880bb0..ccae2d84b 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -75,6 +75,7 @@ class Parser;
*/
class CVC4_PUBLIC Input {
friend class Parser; // for parseError, parseCommand, parseExpr
+ friend class ParserBuilder;
/** The input stream. */
InputStream *d_inputStream;
@@ -85,11 +86,6 @@ class CVC4_PUBLIC Input {
Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
Input& operator=(const Input& input) { Unimplemented("operator= for Input."); }
-public:
-
- /** Destructor. Frees the token stream and closes the input. */
- virtual ~Input();
-
/** Create an input for the given file.
*
* @param lang the input language
@@ -116,6 +112,11 @@ public:
static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name)
throw (InputStreamException);
+public:
+
+ /** Destructor. Frees the token stream and closes the input. */
+ virtual ~Input();
+
protected:
/** Create an input.
diff --git a/src/parser/parser.h b/src/parser/parser.h
index c191d9f39..e6e5a2250 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -95,6 +95,7 @@ inline std::string toString(SymbolType type) {
* declarations.
*/
class CVC4_PUBLIC Parser {
+ friend class ParserBuilder;
/** The expression manager */
ExprManager *d_exprManager;
@@ -123,15 +124,20 @@ class CVC4_PUBLIC Parser {
/** Lookup a symbol in the given namespace. */
Expr getSymbol(const std::string& var_name, SymbolType type);
-public:
- /** Create a parser state.
+protected:
+ /** Create a parser state. NOTE: The parser takes "ownership" of the given
+ * input and will delete it on destruction.
*
* @param exprManager the expression manager to use when creating expressions
* @param input the parser input
*/
Parser(ExprManager* exprManager, Input* input, bool strictMode = false);
- virtual ~Parser() { }
+public:
+
+ virtual ~Parser() {
+ delete d_input;
+ }
/** Get the associated <code>ExprManager</code>. */
inline ExprManager* getExprManager() const {
@@ -145,9 +151,9 @@ public:
/** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be
* called before parsing begins. Otherwise, previous declarations will be lost. */
- inline void setDeclarationScope(DeclarationScope declScope) {
+/* inline void setDeclarationScope(DeclarationScope declScope) {
d_declScope = declScope;
- }
+ }*/
/**
* Check if we are done -- either the end of input has been reached, or some
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
new file mode 100644
index 000000000..b2bb15a6a
--- /dev/null
+++ b/src/parser/parser_builder.cpp
@@ -0,0 +1,141 @@
+/********************* */
+/** parser_builder.cpp
+ ** Original author: cconway
+ ** Major contributors: none
+ ** 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.
+ **
+ ** A builder for parsers.
+ **/
+
+#include <string>
+
+#include "parser_builder.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/smt2/smt2.h"
+
+namespace CVC4 {
+
+namespace parser {
+
+/*class FileInputBuilder : public InputBuilder {
+ bool d_useMmap;
+public:
+ FileInputBuilder(InputLanguage lang, const std::string& filename, bool useMmap) :
+ InputBuilder(lang,filename),
+ d_useMmap(useMmap) {
+ }
+ ParserBuilder& useMmap();
+
+ Input& build() {
+ return Input::newFileInput(d_lang,d_name,d_useMmap);
+ }
+};
+
+class StringInputBuilder : public InputBuilder {
+ std::string d_input;
+public:
+ StringInputBuilder(InputLanguage lang, const std::string& input, const std::string& name) :
+ InputBuilder(lang,name),
+ d_input(input) {
+ }
+
+ Input& build() {
+ return Input::newStringInput(lang,input,name);
+ }
+};*/
+
+ParserBuilder::ParserBuilder(InputLanguage lang, const std::string& filename) :
+ d_inputType(FILE_INPUT),
+ d_lang(lang),
+ d_filename(filename),
+ d_exprManager(NULL),
+ d_checksEnabled(true),
+ d_strictMode(false),
+ d_mmap(false) {
+}
+
+Parser *ParserBuilder::build() throw (InputStreamException) {
+ Input *input;
+ switch( d_inputType ) {
+ case FILE_INPUT:
+ input = Input::newFileInput(d_lang,d_filename,d_mmap);
+ break;
+ case STRING_INPUT:
+ input = Input::newStringInput(d_lang,d_stringInput,d_filename);
+ break;
+ }
+ switch(d_lang) {
+ case LANG_SMTLIB_V2:
+ return new Smt2(d_exprManager, input, d_strictMode);
+ default:
+ return new Parser(d_exprManager, input, d_strictMode);
+ }
+}
+
+/*ParserBuilder& ParserBuilder::disableChecks() {
+ d_checksEnabled = false;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::disableMmap() {
+ d_mmap = false;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::disableStrictMode() {
+ d_strictMode = false;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::enableChecks() {
+ d_checksEnabled = true;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::enableMmap() {
+ d_mmap = true;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::enableStrictMode() {
+ d_strictMode = true;
+ return *this;
+}*/
+
+ParserBuilder& ParserBuilder::withChecks(bool flag) {
+ d_checksEnabled = flag;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withMmap(bool flag) {
+ d_mmap = flag;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
+ d_strictMode = flag;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) {
+ d_exprManager = &exprManager;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
+ d_inputType = STRING_INPUT;
+ d_stringInput = input;
+ return *this;
+}
+
+} /* namespace parser */
+
+} /* namespace CVC4 */
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
new file mode 100644
index 000000000..d0b8b7bb2
--- /dev/null
+++ b/src/parser/parser_builder.h
@@ -0,0 +1,91 @@
+/********************* */
+/** parser_builder.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** 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.
+ **
+ ** A builder for parsers.
+ **/
+
+#include "cvc4parser_public.h"
+
+#ifndef __CVC4__PARSER__PARSER_BUILDER_H_
+#define __CVC4__PARSER__PARSER_BUILDER_H_
+
+#include <string>
+
+#include "parser/input.h"
+#include "parser/parser_options.h"
+
+namespace CVC4 {
+
+class ExprManager;
+
+namespace parser {
+/*
+
+class InputBuilder {
+protected:
+ InputLanguage d_lang;
+ std::string d_name;
+public:
+ InputBuilder(InputLanguage lang, const std::string& name) :
+ d_lang(lang),
+ d_name(name) {
+ }
+ virtual Input& build() = 0;
+};
+*/
+
+class Parser;
+
+class CVC4_PUBLIC ParserBuilder {
+ enum InputType {
+ FILE_INPUT,
+ STRING_INPUT
+ };
+
+ /** The input type. */
+ InputType d_inputType;
+
+ /** The input language */
+ InputLanguage d_lang;
+
+ /** The file name (may not exist) */
+ std::string d_filename;
+
+ /** The string input, if any. */
+ std::string d_stringInput;
+
+ /** The expression manager */
+ ExprManager *d_exprManager;
+
+ /** Should semantic checks be enabled during parsing? */
+ bool d_checksEnabled;
+
+ /** Should we parse in strict mode? */
+ bool d_strictMode;
+
+ /** Should we memory-map a file input? */
+ bool d_mmap;
+
+public:
+ ParserBuilder(InputLanguage lang, const std::string& filename);
+ Parser *build() throw (InputStreamException);
+ ParserBuilder& withChecks(bool flag = true);
+ ParserBuilder& withMmap(bool flag = true);
+ ParserBuilder& withStrictMode(bool flag = true);
+ ParserBuilder& withExprManager(ExprManager& exprManager);
+ ParserBuilder& withStringInput(const std::string& input);
+};
+
+} /* namespace parser */
+
+} /* namespace CVC4 */
+#endif /* __CVC4__PARSER__PARSER_BUILDER_H_ */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dec052859..105976628 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -52,14 +52,14 @@ options {
@lexer::postinclude {
#include <stdint.h>
-#include "parser/parser.h"
+#include "parser/smt2/smt2.h"
#include "parser/antlr_input.h"
using namespace CVC4;
using namespace CVC4::parser;
#undef PARSER_STATE
-#define PARSER_STATE ((Parser*)LEXER->super)
+#define PARSER_STATE ((Smt2*)LEXER->super)
}
@parser::includes {
@@ -89,7 +89,7 @@ using namespace CVC4::parser;
/* These need to be macros so they can refer to the PARSER macro, which will be defined
* by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
#undef PARSER_STATE
-#define PARSER_STATE ((Parser*)PARSER->super)
+#define PARSER_STATE ((Smt2*)PARSER->super)
#undef EXPR_MANAGER
#define EXPR_MANAGER PARSER_STATE->getExprManager()
#undef MK_EXPR
@@ -132,11 +132,14 @@ command returns [CVC4::Command* cmd]
SET_LOGIC_TOK SYMBOL
{ name = AntlrInput::tokenText($SYMBOL);
Debug("parser") << "set logic: '" << name << "' " << std::endl;
- Smt2::setLogic(*PARSER_STATE,name);
+ if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) {
+ PARSER_STATE->parseError("Only one set-logic is allowed.");
+ }
+ PARSER_STATE->setLogic(name);
$cmd = new SetBenchmarkLogicCommand(name); }
| SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
{ name = AntlrInput::tokenText($KEYWORD);
- Smt2::setInfo(*PARSER_STATE,name,sexpr);
+ PARSER_STATE->setInfo(name,sexpr);
cmd = new SetInfoCommand(name,sexpr); }
| /* sort declaration */
DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9fd6588bb..d7da84a43 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -39,15 +39,23 @@ Smt2::Logic Smt2::toLogic(const std::string& name) {
return logicMap[name];
}
-void Smt2::addArithmeticOperators(Parser& parser) {
- parser.addOperator(kind::PLUS);
- parser.addOperator(kind::MINUS);
- parser.addOperator(kind::UMINUS);
- parser.addOperator(kind::MULT);
- parser.addOperator(kind::LT);
- parser.addOperator(kind::LEQ);
- parser.addOperator(kind::GT);
- parser.addOperator(kind::GEQ);
+Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) :
+ Parser(exprManager,input,strictMode),
+ d_logicSet(false) {
+ if( !strictModeEnabled() ) {
+ addTheory(Smt2::THEORY_CORE);
+ }
+}
+
+void Smt2::addArithmeticOperators() {
+ addOperator(kind::PLUS);
+ addOperator(kind::MINUS);
+ addOperator(kind::UMINUS);
+ addOperator(kind::MULT);
+ addOperator(kind::LT);
+ addOperator(kind::LEQ);
+ addOperator(kind::GT);
+ addOperator(kind::GEQ);
}
/**
@@ -56,34 +64,34 @@ void Smt2::addArithmeticOperators(Parser& parser) {
* @param parser the CVC4 Parser object
* @param theory the theory to open (e.g., Core, Ints)
*/
-void Smt2::addTheory(Parser& parser, Theory theory) {
+void Smt2::addTheory(Theory theory) {
switch(theory) {
case THEORY_CORE:
- parser.defineType("Bool", parser.getExprManager()->booleanType());
- parser.defineVar("true", parser.getExprManager()->mkConst(true));
- parser.defineVar("false", parser.getExprManager()->mkConst(false));
- parser.addOperator(kind::AND);
- parser.addOperator(kind::EQUAL);
- parser.addOperator(kind::IFF);
- parser.addOperator(kind::IMPLIES);
- parser.addOperator(kind::ITE);
- parser.addOperator(kind::NOT);
- parser.addOperator(kind::OR);
- parser.addOperator(kind::XOR);
+ defineType("Bool", getExprManager()->booleanType());
+ defineVar("true", getExprManager()->mkConst(true));
+ defineVar("false", getExprManager()->mkConst(false));
+ addOperator(kind::AND);
+ addOperator(kind::EQUAL);
+ addOperator(kind::IFF);
+ addOperator(kind::IMPLIES);
+ addOperator(kind::ITE);
+ addOperator(kind::NOT);
+ addOperator(kind::OR);
+ addOperator(kind::XOR);
break;
case THEORY_REALS_INTS:
- parser.defineType("Real", parser.getExprManager()->realType());
+ defineType("Real", getExprManager()->realType());
// falling-through on purpose, to add Ints part of RealsInts
case THEORY_INTS:
- parser.defineType("Int", parser.getExprManager()->integerType());
- addArithmeticOperators(parser);
+ defineType("Int", getExprManager()->integerType());
+ addArithmeticOperators();
break;
case THEORY_REALS:
- parser.defineType("Real", parser.getExprManager()->realType());
- addArithmeticOperators(parser);
+ defineType("Real", getExprManager()->realType());
+ addArithmeticOperators();
break;
default:
@@ -91,23 +99,30 @@ void Smt2::addTheory(Parser& parser, Theory theory) {
}
}
+bool Smt2::logicIsSet() {
+ return d_logicSet;
+}
+
/**
* Sets the logic for the current benchmark. Declares any logic and theory symbols.
*
* @param parser the CVC4 Parser object
* @param name the name of the logic (e.g., QF_UF, AUFLIA)
*/
-void Smt2::setLogic(Parser& parser, const std::string& name) {
+void Smt2::setLogic(const std::string& name) {
+ d_logicSet = true;
+ d_logic = toLogic(name);
+
// Core theory belongs to every logic
- addTheory(parser, THEORY_CORE);
+ addTheory(THEORY_CORE);
- switch(toLogic(name)) {
+ switch(d_logic) {
case QF_UF:
- parser.addOperator(kind::APPLY_UF);
+ addOperator(kind::APPLY_UF);
break;
case QF_LRA:
- addTheory(parser, THEORY_REALS);
+ addTheory(THEORY_REALS);
break;
default:
@@ -115,7 +130,7 @@ void Smt2::setLogic(Parser& parser, const std::string& name) {
}
}
-void Smt2::setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr) {
+void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
// TODO: ???
}
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 715d3199f..0bb3020a3 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -22,6 +22,7 @@
namespace std { using namespace __gnu_cxx; }
#include "util/hash.h"
+#include "parser/parser.h"
namespace CVC4 {
@@ -29,9 +30,8 @@ class SExpr;
namespace parser {
-class Parser;
-
-class Smt2 {
+class Smt2 : public Parser {
+ friend class ParserBuilder;
public:
enum Logic {
@@ -51,14 +51,25 @@ public:
THEORY_REALS_INTS,
};
+private:
+ bool d_logicSet;
+ Logic d_logic;
+
+protected:
+ Smt2(ExprManager* exprManager, Input* input, bool strictMode = false);
+
+public:
/**
* Add theory symbols to the parser state.
*
* @param parser the CVC4 Parser object
* @param theory the theory to open (e.g., Core, Ints)
*/
- static void
- addTheory(Parser& parser, Theory theory);
+ void
+ addTheory(Theory theory);
+
+ bool
+ logicIsSet();
/**
* Sets the logic for the current benchmark. Declares any logic and theory symbols.
@@ -66,17 +77,17 @@ public:
* @param parser the CVC4 Parser object
* @param name the name of the logic (e.g., QF_UF, AUFLIA)
*/
- static void
- setLogic(Parser& parser, const std::string& name);
+ void
+ setLogic(const std::string& name);
- static void
- setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr);
+ void
+ setInfo(const std::string& flag, const SExpr& sexpr);
static Logic toLogic(const std::string& name);
private:
- static void addArithmeticOperators(Parser& parser);
+ void addArithmeticOperators();
static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
};
}/* CVC4::parser namespace */
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 6d7a04800..5150ba010 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -65,12 +65,5 @@ Expr Smt2Input::parseExpr() throw (ParserException) {
return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
-void Smt2Input::setParser(Parser& parser) {
- super::setParser(parser);
- if( !parser.strictModeEnabled() ) {
- Smt2::addTheory(parser,Smt2::THEORY_CORE);
- }
-}
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index c003a76ec..962e2a987 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -32,6 +32,8 @@ class ExprManager;
namespace parser {
+class Smt2;
+
class Smt2Input : public AntlrInput {
typedef AntlrInput super;
@@ -86,11 +88,6 @@ protected:
*/
Expr parseExpr() throw(ParserException);
- /** Set the Parser object for this input. This implementation overrides the super-class
- * implementation to add the core theory symbols to the parser state when strict
- * mode is disabled. */
- virtual void setParser(Parser& parser);
-
};/* class Smt2Input */
}/* CVC4::parser namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback