diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/parser_builder.cpp | 7 | ||||
-rw-r--r-- | src/parser/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 23 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 55 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 27 |
5 files changed, 29 insertions, 85 deletions
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index a9b3c461d..4e4b0309f 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -19,6 +19,7 @@ #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" +#include "parser/smt/smt.h" #include "parser/smt2/smt2.h" namespace CVC4 { @@ -64,7 +65,7 @@ ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filena } Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { - Input *input; + Input *input = NULL; switch( d_inputType ) { case FILE_INPUT: input = Input::newFileInput(d_lang,d_filename,d_mmap); @@ -77,8 +78,12 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { case STRING_INPUT: input = Input::newStringInput(d_lang,d_stringInput,d_filename); break; + default: + Unreachable(); } switch(d_lang) { + case LANG_SMTLIB: + return new Smt(&d_exprManager, input, d_strictMode); case LANG_SMTLIB_V2: return new Smt2(&d_exprManager, input, d_strictMode); default: diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 792527816..731676644 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -24,6 +24,8 @@ ANTLR_STUFF = \ libparsersmt_la_SOURCES = \ Smt.g \ + smt.h \ + smt.cpp \ smt_input.h \ smt_input.cpp \ $(ANTLR_STUFF) diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 9c609d0d4..c11f350a6 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -64,6 +64,7 @@ namespace CVC4 { #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" +#include "parser/smt/smt.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -75,7 +76,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 ((Smt*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -83,24 +84,6 @@ using namespace CVC4::parser; #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst -/** - * Sets the logic for the current benchmark. Declares any logic 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) { - if( name == "QF_UF" ) { - parser->mkSort("U"); - } else if(name == "QF_LRA"){ - parser->defineType("Real", parser->getExprManager()->realType()); - } else if(name == "QF_BV"){ - } else { - // NOTE: Theory types go here - Unhandled(name); - } -} } @@ -155,7 +138,7 @@ benchAttribute returns [CVC4::Command* smt_command] Expr expr; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { setLogic(PARSER_STATE,name); + { PARSER_STATE->setLogic(name); smt_command = new SetBenchmarkLogicCommand(name); } | ASSUMPTION_TOK annotatedFormula[expr] { smt_command = new AssertCommand(expr); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index f6089382c..5cf902260 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -13,36 +13,13 @@ ** Definitions of SMT2 constants. **/ -#include <ext/hash_map> -namespace std { -using namespace __gnu_cxx; -} - #include "parser/parser.h" +#include "parser/smt/smt.h" #include "parser/smt2/smt2.h" namespace CVC4 { namespace parser { -std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> Smt2::newLogicMap() { - std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap; - logicMap["QF_AX"] = QF_AX; - logicMap["QF_BV"] = QF_BV; - logicMap["QF_IDL"] = QF_IDL; - logicMap["QF_LIA"] = QF_LIA; - logicMap["QF_LRA"] = QF_LRA; - logicMap["QF_NIA"] = QF_NIA; - logicMap["QF_RDL"] = QF_RDL; - logicMap["QF_UF"] = QF_UF; - logicMap["QF_UFIDL"] = QF_UFIDL; - return logicMap; -} - -Smt2::Logic Smt2::toLogic(const std::string& name) { - static std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); - return logicMap[name]; -} - Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) : Parser(exprManager,input,strictMode), d_logicSet(false) { @@ -115,38 +92,38 @@ bool Smt2::logicIsSet() { */ void Smt2::setLogic(const std::string& name) { d_logicSet = true; - d_logic = toLogic(name); + d_logic = Smt::toLogic(name); // Core theory belongs to every logic addTheory(THEORY_CORE); switch(d_logic) { - case QF_IDL: - case QF_LIA: - case QF_NIA: + case Smt::QF_IDL: + case Smt::QF_LIA: + case Smt::QF_NIA: addTheory(THEORY_INTS); break; - case QF_LRA: - case QF_RDL: + case Smt::QF_LRA: + case Smt::QF_RDL: addTheory(THEORY_REALS); break; - case QF_UFIDL: + case Smt::QF_UFIDL: addTheory(THEORY_INTS); // falling-through on purpose, to add UF part of UFIDL - case QF_UF: + case Smt::QF_UF: addOperator(kind::APPLY_UF); break; - case AUFLIA: - case AUFLIRA: - case AUFNIRA: - case QF_AUFBV: - case QF_AUFLIA: - case QF_AX: - case QF_BV: + case Smt::AUFLIA: + case Smt::AUFLIRA: + case Smt::AUFNIRA: + case Smt::QF_AUFBV: + case Smt::QF_AUFLIA: + case Smt::QF_AX: + case Smt::QF_BV: Unhandled(name); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5eae90fa3..0e057db68 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -18,11 +18,8 @@ #ifndef __CVC4__PARSER__SMT2_H #define __CVC4__PARSER__SMT2_H -#include <ext/hash_map> -namespace std { using namespace __gnu_cxx; } - -#include "util/hash.h" #include "parser/parser.h" +#include "parser/smt/smt.h" namespace CVC4 { @@ -34,23 +31,6 @@ class Smt2 : public Parser { friend class ParserBuilder; public: - enum Logic { - AUFLIA, - AUFLIRA, - AUFNIRA, - QF_AUFBV, - QF_AUFLIA, - QF_AX, - QF_BV, - QF_IDL, - QF_LIA, - QF_LRA, - QF_NIA, - QF_RDL, - QF_UF, - QF_UFIDL - }; - enum Theory { THEORY_ARRAYS, THEORY_BITVECTORS, @@ -62,7 +42,7 @@ public: private: bool d_logicSet; - Logic d_logic; + Smt::Logic d_logic; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false); @@ -92,12 +72,9 @@ public: void setInfo(const std::string& flag, const SExpr& sexpr); - static Logic toLogic(const std::string& name); - private: void addArithmeticOperators(); - static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap(); }; }/* CVC4::parser namespace */ }/* CVC4 namespace */ |