diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 11:37:53 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 11:38:09 -0500 |
commit | 966f38dc17ee316fdb069ec2a427c4f79f1f73b2 (patch) | |
tree | 1a1b60435daffa8b59eea589ef04c26b50f8a724 /src/parser | |
parent | 594301e6f2893ebe9baba5083ff084933b1e9da9 (diff) |
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.cpp | 1 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 15 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 1 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 112 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 3 |
6 files changed, 123 insertions, 19 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 6edb23a23..b2f2cdd53 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -249,6 +249,7 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre case LANG_SMTLIB_V2_0: case LANG_SMTLIB_V2_5: + case LANG_SMTLIB_V2_6: input = new Smt2Input(inputStream, lang); break; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index fb0304045..d72e1526e 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1689,17 +1689,22 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } - | NOT_TOK bvNegTerm[f] + | relationTerm[f] + ; + +relationTerm[CVC4::Expr& f] + /* relation terms */ + : NOT_TOK relationTerm[f] { f = MK_EXPR(CVC4::kind::COMPLEMENT, f); } - | TRANSPOSE_TOK bvNegTerm[f] + | TRANSPOSE_TOK relationTerm[f] { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } - | TRANSCLOSURE_TOK bvNegTerm[f] + | TRANSCLOSURE_TOK relationTerm[f] { f = MK_EXPR(CVC4::kind::TCLOSURE, f); } - | TUPLE_TOK LPAREN bvNegTerm[f] RPAREN + | TUPLE_TOK LPAREN relationTerm[f] RPAREN { std::vector<Type> types; std::vector<Expr> args; args.push_back(f); - types.push_back(f.getType()); + types.push_back(f.getType()); DatatypeType t = EXPR_MANAGER->mkTupleType(types); const Datatype& dt = t.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 8580d5672..a666fd381 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -93,6 +93,7 @@ Parser* ParserBuilder::build() break; case language::input::LANG_SMTLIB_V2_0: case language::input::LANG_SMTLIB_V2_5: + case language::input::LANG_SMTLIB_V2_6: parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_SYGUS: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 07ace295c..4d884d894 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1107,6 +1107,10 @@ metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd] sexpr.getRationalValue() == Rational(5, 2)) || sexpr.getValue() == "2.5" ) { PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5); + } else if( (sexpr.isRational() && + sexpr.getRationalValue() == Rational(13, 5)) || + sexpr.getValue() == "2.6" ) { + PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_6); } } PARSER_STATE->setInfo(name.c_str() + 1, sexpr); @@ -1353,7 +1357,9 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd] + | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] + | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | rewriterulesCommand[cmd] @@ -1500,7 +1506,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] ; -datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1516,8 +1522,71 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); - cmd->reset(new DatatypeDeclarationCommand( - PARSER_STATE->mkMutualDatatypeTypes(dts))); + cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); + } + ; + +datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +@declarations { + std::vector<CVC4::Datatype> dts; + std::vector<Type> types; + std::string name; + std::vector<std::string> dnames; + std::vector<unsigned> arities; + std::vector<Type> params; +} + : { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->pushScope(true); } + LPAREN_TOK /* sorts */ + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK + { unsigned arity = AntlrInput::tokenToUnsigned(n); + //Type type; + //if(arity == 0) { + // type = PARSER_STATE->mkSort(name); + //} else { + // type = PARSER_STATE->mkSortConstructor(name, arity); + //} + Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl; + //types.push_back(type); + dnames.push_back(name); + arities.push_back( arity ); + } + )* + RPAREN_TOK + LPAREN_TOK + ( LPAREN_TOK { + params.clear(); + Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl; + if( dts.size()>=dnames.size() ){ + PARSER_STATE->parseError("Too many datatypes defined in this block."); + } + } + ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] + { params.push_back( PARSER_STATE->mkSort(name) ); } + )* + RPAREN_TOK { + if( params.size()!=arities[dts.size()] ){ + PARSER_STATE->parseError("Wrong number of parameters for datatype."); + } + Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; + dts.push_back(Datatype(dnames[dts.size()],params,isCo)); + } + LPAREN_TOK + ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ + RPAREN_TOK { PARSER_STATE->popScope(); } + | { if( 0!=arities[dts.size()] ){ + PARSER_STATE->parseError("No parameters given for datatype."); + } + Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; + dts.push_back(Datatype(dnames[dts.size()],params,isCo)); + } + ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ + ) + RPAREN_TOK + )+ + RPAREN_TOK + { PARSER_STATE->popScope(); + cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); } ; @@ -1890,8 +1959,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | LPAREN_TOK ( /* An indexed function application */ - indexedFunctionName[op] termList[args,expr] RPAREN_TOK - { expr = MK_EXPR(op, args); + indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK + { + if( kind!=kind::NULL_EXPR ){ + expr = MK_EXPR( kind, op, args ); + }else{ + expr = MK_EXPR(op, args); + } PARSER_STATE->checkOperator(expr.getKind(), args.size()); } | /* Array constant (in Z3 syntax) */ @@ -2267,7 +2341,11 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] /** * Matches a bit-vector operator (the ones parametrized by numbers) */ -indexedFunctionName[CVC4::Expr& op] +indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] +@init { + Expr expr; + Expr expr2; +} : LPAREN_TOK INDEX_TOK ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), @@ -2344,6 +2422,13 @@ indexedFunctionName[CVC4::Expr& op] { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); } | FP_TO_SBV_TOK m=INTEGER_LITERAL { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); } + | TESTER_TOK term[expr, expr2] { + if( !expr.getType().isConstructor() ){ + PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor."); + } + op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester(); + kind = CVC4::kind::APPLY_TESTER; + } | badIndexedFunctionName ) RPAREN_TOK @@ -2795,7 +2880,7 @@ GET_ASSERTIONS_TOK : 'get-assertions'; GET_PROOF_TOK : 'get-proof'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; -RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; +RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; ITE_TOK : 'ite'; LET_TOK : 'let'; @@ -2815,8 +2900,13 @@ AS_TOK : 'as'; CONST_TOK : 'const'; // extended commands -DECLARE_DATATYPES_TOK : 'declare-datatypes'; -DECLARE_CODATATYPES_TOK : 'declare-codatatypes'; +DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-datatype'; +DECLARE_DATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-datatypes'; +DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-datatypes'; +DECLARE_CODATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-codatatypes'; +DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-codatatypes'; +PAR_TOK : { PARSER_STATE->v2_6() }?'par'; +TESTER_TOK : { PARSER_STATE->v2_6() }?'is'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; @@ -3039,7 +3129,7 @@ STRING_LITERAL_2_0 * will be part of the token text. Use the str[] parser rule instead. */ STRING_LITERAL_2_5 - : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=> + : { PARSER_STATE->v2_5(false) || PARSER_STATE->sygus() }?=> '"' (~('"') | '""')* '"' ; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fc930dc79..764cb6866 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -108,8 +108,14 @@ public: bool v2_0() const { return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0; } - bool v2_5() const { - return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5; + // 2.6 is a superset of 2.5, use exact=false to query whether smt lib 2.5 or above + bool v2_5( bool exact = true ) const { + return exact ? getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5 : + ( getInput()->getLanguage() >= language::input::LANG_SMTLIB_V2_5 && + getInput()->getLanguage() <= language::input::LANG_SMTLIB_V2 ); + } + bool v2_6() const { + return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6; } bool sygus() const { return getInput()->getLanguage() == language::input::LANG_SYGUS; diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 7aa4c3441..03f819a5d 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -67,7 +67,8 @@ Smt2Input::~Smt2Input() { void Smt2Input::setLanguage(InputLanguage lang) { CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 || - lang == language::input::LANG_SMTLIB_V2_5, lang); + lang == language::input::LANG_SMTLIB_V2_5 || + lang == language::input::LANG_SMTLIB_V2_6, lang); d_lang = lang; } |