diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-04 17:14:04 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-04 17:14:04 +0000 |
commit | cd8b317b498c6c383c7571cd0939ff5044ad8932 (patch) | |
tree | 0913cd2f5c4ba6361513fb7f2e8405f4a2fa6028 /src/parser/smt | |
parent | f780dd882fc343cef668d5cd9eed8f515d0e70ed (diff) |
Enabling RDL/IDL in SMT v1 and adding some simple tests
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 23 |
2 files changed, 5 insertions, 20 deletions
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); } |