From 45a138c326da72890bf889a3670aad503ef4aa1e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 1 Mar 2012 14:48:04 +0000 Subject: Partial merge from kind-backend branch, including Minisat and CNF work to support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too! --- src/parser/smt2/Smt2.g | 67 ++++++++++++++++++++++++++++++++++++++++-------- src/parser/smt2/smt2.cpp | 8 ++++++ 2 files changed, 64 insertions(+), 11 deletions(-) (limited to 'src/parser/smt2') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 791e550b9..926ce1718 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -67,7 +67,6 @@ options { #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" -#include "parser/antlr_tracing.h" using namespace CVC4; using namespace CVC4::parser; @@ -79,6 +78,7 @@ using namespace CVC4::parser; @parser::includes { #include "expr/command.h" #include "parser/parser.h" +#include "parser/antlr_tracing.h" namespace CVC4 { class Expr; @@ -358,7 +358,12 @@ command returns [CVC4::Command* cmd = NULL] extendedCommand[CVC4::Command*& cmd] @declarations { std::vector dts; + Type t; Expr e; + SExpr sexpr; + std::string name; + std::vector names; + std::vector sorts; } /* Z3's extended SMT-LIBv2 set of commands syntax */ : DECLARE_DATATYPES_TOK @@ -368,33 +373,43 @@ extendedCommand[CVC4::Command*& cmd] { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } - | DECLARE_SORTS_TOK | DECLARE_FUNS_TOK + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] nonemptySortList[sorts] RPAREN_TOK )+ + RPAREN_TOK | DECLARE_PREDS_TOK - | DEFINE_TOK + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortList[sorts] RPAREN_TOK )+ + RPAREN_TOK + | DEFINE_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e] | DEFINE_SORTS_TOK - | DECLARE_CONST_TOK - + LPAREN_TOK + ( LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK | + symbol[name,CHECK_UNDECLARED,SYM_SORT] symbol[name,CHECK_NONE,SYM_SORT] ) RPAREN_TOK RPAREN_TOK )+ + RPAREN_TOK + | DECLARE_CONST_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] + | SIMPLIFY_TOK term[e] { cmd = new SimplifyCommand(e); } | ECHO_TOK - ( STRING_LITERAL - { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; } + ( simpleSymbolicExpr[sexpr] + { Message() << sexpr << std::endl; } | { Message() << std::endl; } ) + { cmd = new EmptyCommand; } ; -symbolicExpr[CVC4::SExpr& sexpr] +simpleSymbolicExpr[CVC4::SExpr& sexpr] @declarations { - std::vector children; CVC4::Kind k; + std::string s; } : INTEGER_LITERAL { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } | DECIMAL_LITERAL { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } - | STRING_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } + | str[s] + { sexpr = SExpr(s); } | SYMBOL { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } | builtinOp[k] @@ -404,6 +419,13 @@ symbolicExpr[CVC4::SExpr& sexpr] } | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } + ; + +symbolicExpr[CVC4::SExpr& sexpr] +@declarations { + std::vector children; +} + : simpleSymbolicExpr[sexpr] | LPAREN_TOK (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK @@ -610,6 +632,17 @@ termList[std::vector& formulas, CVC4::Expr& expr] : ( term[expr] { formulas.push_back(expr); } )+ ; +/** + * Matches a string, and strips off the quotes. + */ +str[std::string& s] + : STRING_LITERAL + { s = AntlrInput::tokenText($STRING_LITERAL); + /* strip off the quotes */ + s = s.substr(1, s.size() - 2); + } + ; + /** * Matches a builtin operator symbol and sets kind to its associated Expr kind. */ @@ -637,6 +670,8 @@ builtinOp[CVC4::Kind& kind] | MINUS_TOK { $kind = CVC4::kind::MINUS; } | STAR_TOK { $kind = CVC4::kind::MULT; } | DIV_TOK { $kind = CVC4::kind::DIVISION; } + | INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; } + | INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; } | SELECT_TOK { $kind = CVC4::kind::SELECT; } | STORE_TOK { $kind = CVC4::kind::STORE; } @@ -705,6 +740,13 @@ sortList[std::vector& sorts] : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; +nonemptySortList[std::vector& sorts] +@declarations { + Type t; +} + : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+ + ; + /** * Matches a sequence of (variable,sort) symbol pairs and fills them * into the given vector. @@ -937,6 +979,9 @@ STORE_TOK : 'store'; // TILDE_TOK : '~'; XOR_TOK : 'xor'; +INTS_DIV_TOK : 'div'; +INTS_MOD_TOK : 'mod'; + CONCAT_TOK : 'concat'; BVNOT_TOK : 'bvnot'; BVAND_TOK : 'bvand'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7d6f27aa5..39eaf5b95 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -127,6 +127,7 @@ void Smt2::setLogic(const std::string& name) { case Smt::QF_UFIDL: case Smt::QF_UFLIA: + case Smt::QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addOperator(kind::APPLY_UF); break; @@ -137,6 +138,13 @@ void Smt2::setLogic(const std::string& name) { addOperator(kind::APPLY_UF); break; + case Smt::QF_UFLIRA:// nonstandard logic + case Smt::QF_UFNIRA:// nonstandard logic + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + break; + case Smt::QF_BV: addTheory(THEORY_BITVECTORS); break; -- cgit v1.2.3