From cd8b317b498c6c383c7571cd0939ff5044ad8932 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Fri, 4 Jun 2010 17:14:04 +0000 Subject: [PATCH] Enabling RDL/IDL in SMT v1 and adding some simple tests --- src/parser/parser_builder.cpp | 7 +++- src/parser/smt/Makefile.am | 2 + src/parser/smt/Smt.g | 23 ++--------- src/parser/smt2/smt2.cpp | 55 ++++++++------------------- src/parser/smt2/smt2.h | 27 +------------ test/regress/regress0/Makefile.am | 7 +++- test/regress/regress0/simple-lra.smt | 6 +++ test/regress/regress0/simple-lra.smt2 | 6 +++ test/regress/regress0/simple-rdl.smt | 6 +++ test/regress/regress0/simple-rdl.smt2 | 7 ++++ test/regress/regress0/simple-uf.smt2 | 9 +++++ 11 files changed, 69 insertions(+), 86 deletions(-) create mode 100644 test/regress/regress0/simple-lra.smt create mode 100644 test/regress/regress0/simple-lra.smt2 create mode 100644 test/regress/regress0/simple-rdl.smt create mode 100644 test/regress/regress0/simple-rdl.smt2 create mode 100644 test/regress/regress0/simple-uf.smt2 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 -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 Smt2::newLogicMap() { - std::hash_map 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 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 -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 newLogicMap(); }; }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 0b8a60495..66112defc 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -14,13 +14,18 @@ TESTS = \ ite_real_valid.smt \ let.smt \ let2.smt \ - simple2.smt \ simple.smt \ + simple2.smt \ + simple-lra.smt \ + simple-rdl.smt \ simple-uf.smt \ ite.smt2 \ ite2.smt2 \ ite3.smt2 \ ite4.smt2 \ + simple-lra.smt2 \ + simple-rdl.smt2 \ + simple-uf.smt2 \ bug32.cvc \ hole6.cvc \ logops.01.cvc \ diff --git a/test/regress/regress0/simple-lra.smt b/test/regress/regress0/simple-lra.smt new file mode 100644 index 000000000..c80632a96 --- /dev/null +++ b/test/regress/regress0/simple-lra.smt @@ -0,0 +1,6 @@ +(benchmark simple_lra + :logic QF_LRA + :status unsat + :extrafuns ((x Real) (y Real)) + :formula (not (implies (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y)))) +) diff --git a/test/regress/regress0/simple-lra.smt2 b/test/regress/regress0/simple-lra.smt2 new file mode 100644 index 000000000..585c62954 --- /dev/null +++ b/test/regress/regress0/simple-lra.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (not (=> (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y))))) +(check-sat) diff --git a/test/regress/regress0/simple-rdl.smt b/test/regress/regress0/simple-rdl.smt new file mode 100644 index 000000000..080c69f93 --- /dev/null +++ b/test/regress/regress0/simple-rdl.smt @@ -0,0 +1,6 @@ +(benchmark simple_rdl + :logic QF_RDL + :status unsat + :extrafuns ((x Real) (y Real)) + :formula (not (implies (< (- x y) 0) (< x y))) +) diff --git a/test/regress/regress0/simple-rdl.smt2 b/test/regress/regress0/simple-rdl.smt2 new file mode 100644 index 000000000..d2c0a4cde --- /dev/null +++ b/test/regress/regress0/simple-rdl.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_RDL) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (not (=> (< (- x y) 0) (< x y)))) +(check-sat) + diff --git a/test/regress/regress0/simple-uf.smt2 b/test/regress/regress0/simple-uf.smt2 new file mode 100644 index 000000000..ef3b3cf86 --- /dev/null +++ b/test/regress/regress0/simple-uf.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort A 0) +(declare-sort B 0) +(declare-fun x () A) +(declare-fun y () A) +(declare-fun f (A) B) +(assert (not (=> (= x y) (= (f x) (f y))))) +(check-sat) -- 2.30.2