From a358ed3b520919acbb72fb9bcd2974ee4165f495 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 12 May 2010 20:29:24 +0000 Subject: Adding ParserBuilder, reducing visibility of Parser and Input constructors Adding Smt2 subclass of Parser Checking for multiple calls to set-logic in SMT v2 --- src/parser/smt2/Smt2.g | 13 ++++--- src/parser/smt2/smt2.cpp | 79 +++++++++++++++++++++++++----------------- src/parser/smt2/smt2.h | 31 +++++++++++------ src/parser/smt2/smt2_input.cpp | 7 ---- src/parser/smt2/smt2_input.h | 7 ++-- 5 files changed, 78 insertions(+), 59 deletions(-) (limited to 'src/parser/smt2') 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 -#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 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 */ -- cgit v1.2.3