#include "cvc4autoconfig.h"
#include "main.h"
#include "usage.h"
-#include "parser/input.h"
#include "parser/parser.h"
+#include "parser/parser_builder.h"
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "expr/command.h"
}
}
- // Create the parser
- Input* input;
-
/* TODO: Hack ANTLR3 to support input from streams */
-// if(inputFromStdin) {
- // parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
-// } else {
- input = Input::newFileInput(options.lang, argv[firstArgIndex],
- options.memoryMap);
-// }
- Parser parser(&exprMgr, input);
-
- if(!options.semanticChecks || Configuration::isMuzzledBuild()) {
- parser.disableChecks();
- }
+ ParserBuilder parserBuilder(options.lang, argv[firstArgIndex]);
- if( options.strictParsing ) {
- parser.enableStrictMode();
- }
+ Parser *parser =
+ parserBuilder.withExprManager(exprMgr)
+ .withMmap(options.memoryMap)
+ .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() )
+ .withStrictMode( options.strictParsing )
+ .build();
// Parse and execute commands until we are done
Command* cmd;
- while((cmd = parser.nextCommand())) {
+ while((cmd = parser->nextCommand())) {
if( !options.parseOnly ) {
doCommand(smt, cmd);
}
}
// Remove the parser
- delete input;
+ delete parser;
switch(lastResult.asSatisfiabilityResult().isSAT()) {
memory_mapped_input_buffer.cpp \
parser.h \
parser.cpp \
+ parser_builder.h \
+ parser_builder.cpp \
parser_options.h \
parser_exception.h
*/
class CVC4_PUBLIC Input {
friend class Parser; // for parseError, parseCommand, parseExpr
+ friend class ParserBuilder;
/** The input stream. */
InputStream *d_inputStream;
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
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.
* declarations.
*/
class CVC4_PUBLIC Parser {
+ friend class ParserBuilder;
/** The expression manager */
ExprManager *d_exprManager;
/** 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 {
/** 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
--- /dev/null
+/********************* */
+/** 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 */
--- /dev/null
+/********************* */
+/** 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_ */
@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 {
/* 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
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
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);
}
/**
* @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:
}
}
+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:
}
}
-void Smt2::setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr) {
+void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
// TODO: ???
}
namespace std { using namespace __gnu_cxx; }
#include "util/hash.h"
+#include "parser/parser.h"
namespace CVC4 {
namespace parser {
-class Parser;
-
-class Smt2 {
+class Smt2 : public Parser {
+ friend class ParserBuilder;
public:
enum Logic {
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.
* @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 */
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 */
namespace parser {
+class Smt2;
+
class Smt2Input : public AntlrInput {
typedef AntlrInput super;
*/
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 */
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "parser/input.h"
#include "parser/parser.h"
+#include "parser/parser_builder.h"
#include "parser/smt2/smt2.h"
#include "expr/command.h"
#include "util/output.h"
// Debug.on("parser-extra");
// cerr << "Testing good input: <<" << goodInput << ">>" << endl;
// istringstream stream(goodInputs[i]);
- Input* input = Input::newStringInput(d_lang, goodInput, "test");
- Parser parser(d_exprManager, input);
- TS_ASSERT( !parser.done() );
+ ParserBuilder parserBuilder(d_lang,"test");
+ Parser *parser =
+ parserBuilder.withStringInput(goodInput)
+ .withExprManager(*d_exprManager)
+ .build();
+ TS_ASSERT( !parser->done() );
Command* cmd;
- while((cmd = parser.nextCommand()) != NULL) {
+ while((cmd = parser->nextCommand()) != NULL) {
Debug("parser") << "Parsed command: " << (*cmd) << endl;
}
- TS_ASSERT( parser.done() );
- delete input;
- Debug.off("parser");
+ TS_ASSERT( parser->done() );
+ delete parser;
+// Debug.off("parser");
// Debug.off("parser-extra");
} catch (Exception& e) {
cout << "\nGood input failed:\n" << goodInput << endl
void tryBadInput(const string badInput, bool strictMode = false) {
// cerr << "Testing bad input: '" << badInput << "'\n";
// Debug.on("parser");
- Input* input = Input::newStringInput(d_lang, badInput, "test");
- Parser parser(d_exprManager, input, strictMode);
+ ParserBuilder parserBuilder(d_lang,"test");
+ Parser *parser =
+ parserBuilder.withStringInput(badInput)
+ .withExprManager(*d_exprManager)
+ .withStrictMode(strictMode)
+ .build();
TS_ASSERT_THROWS
- ( while(parser.nextCommand());
+ ( while(parser->nextCommand());
cout << "\nBad input succeeded:\n" << badInput << endl;,
const ParserException& );
// Debug.off("parser");
- delete input;
+ delete parser;
}
void tryGoodExpr(const string goodExpr) {
// cerr << "Testing good expr: '" << goodExpr << "'\n";
// Debug.on("parser");
// istringstream stream(context + goodBooleanExprs[i]);
- Input* input = Input::newStringInput(d_lang,
- goodExpr, "test");
- Parser parser(d_exprManager, input);
- TS_ASSERT( !parser.done() );
- setupContext(parser);
- TS_ASSERT( !parser.done() );
- Expr e = parser.nextExpression();
+ ParserBuilder parserBuilder(d_lang,"test");
+ Parser *parser =
+ parserBuilder.withStringInput(goodExpr)
+ .withExprManager(*d_exprManager)
+ .build();
+ TS_ASSERT( !parser->done() );
+ setupContext(*parser);
+ TS_ASSERT( !parser->done() );
+ Expr e = parser->nextExpression();
TS_ASSERT( !e.isNull() );
- e = parser.nextExpression();
- TS_ASSERT( parser.done() );
+ e = parser->nextExpression();
+ TS_ASSERT( parser->done() );
TS_ASSERT( e.isNull() );
- delete input;
+ delete parser;
} catch (Exception& e) {
cout << endl
<< "Good expr failed." << endl
// Debug.on("parser");
// Debug.on("parser-extra");
// cout << "Testing bad expr: '" << badExpr << "'\n";
- Input* input = Input::newStringInput(d_lang, badExpr, "test");
- Parser parser(d_exprManager, input, strictMode);
- setupContext(parser);
- TS_ASSERT( !parser.done() );
+ ParserBuilder parserBuilder(d_lang,"test");
+ Parser *parser =
+ parserBuilder.withStringInput(badExpr)
+ .withExprManager(*d_exprManager)
+ .withStrictMode(strictMode)
+ .build();
+ setupContext(*parser);
+ TS_ASSERT( !parser->done() );
TS_ASSERT_THROWS
- ( Expr e = parser.nextExpression();
+ ( Expr e = parser->nextExpression();
cout << endl
<< "Bad expr succeeded." << endl
<< "Input: <<" << badExpr << ">>" << endl
<< "Output: <<" << e << ">>" << endl;,
const ParserException& );
- delete input;
+ delete parser;
// Debug.off("parser");
}
public:
Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
- void setupContext(Parser& parser) {
- Smt2::addTheory(parser,Smt2::THEORY_CORE);
+ void setupContext(Smt2& parser) {
+ parser.addTheory(Smt2::THEORY_CORE);
super::setupContext(parser);
}
projects / cvc5.git / commitdiff