diff options
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 67 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 |
2 files changed, 64 insertions, 11 deletions
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<CVC4::Datatype> dts; + Type t; Expr e; + SExpr sexpr; + std::string name; + std::vector<std::string> names; + std::vector<Type> 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<SExpr> 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<SExpr> children; +} + : simpleSymbolicExpr[sexpr] | LPAREN_TOK (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK @@ -611,6 +633,17 @@ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& 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. */ builtinOp[CVC4::Kind& 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<CVC4::Type>& sorts] : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; +nonemptySortList[std::vector<CVC4::Type>& 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; |