From: ajreynol Date: Thu, 16 Mar 2017 16:37:53 +0000 (-0500) Subject: Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGround... X-Git-Tag: cvc5-1.0.0~5888 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=966f38dc17ee316fdb069ec2a427c4f79f1f73b2;p=cvc5.git 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. --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 02edab533..ac93114b7 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -395,6 +395,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); ExprManagerScope ems(d_self); + Debug("datatypes") << "mkGroundTerm of type " << t << std::endl; // is this already in the cache ? std::map< Type, Expr >::iterator it = d_ground_term.find( t ); @@ -437,8 +438,8 @@ Expr getSubtermWithType( Expr e, Type t, bool isTop ){ } Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { - if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){ - processing.push_back( d_self ); + if( std::find( processing.begin(), processing.end(), t )==processing.end() ){ + processing.push_back( t ); for( unsigned r=0; r<2; r++ ){ for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { //do nullary constructors first @@ -462,7 +463,7 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons } processing.pop_back(); }else{ - Debug("datatypes") << "...already processing " << t << std::endl; + Debug("datatypes") << "...already processing " << t << " " << d_self << std::endl; } return Expr(); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 334373642..bb2956c44 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -127,6 +127,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, break; case output::LANG_SMTLIB_V2_0: case output::LANG_SMTLIB_V2_5: + case output::LANG_SMTLIB_V2_6: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); @@ -332,7 +333,8 @@ restart: goto restart; } catch(ParserException& pe) { if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 || - d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5) { + d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5 || + d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_6) { d_out << "(error \"" << pe << "\")" << endl; } else { d_out << pe << endl; diff --git a/src/main/main.cpp b/src/main/main.cpp index 7b6b9ad86..9f77045c4 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -65,7 +65,8 @@ int main(int argc, char* argv[]) { *opts.getOut() << "unknown" << endl; #endif if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 || - opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5) { + opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5 || + opts.getOutputLanguage() == output::LANG_SMTLIB_V2_6) { *opts.getOut() << "(error \"" << e << "\")" << endl; } else { *opts.getErr() << "CVC4 Error:" << endl << e << endl; diff --git a/src/options/language.cpp b/src/options/language.cpp index 665089e45..7ae9d075a 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -24,6 +24,7 @@ InputLanguage toInputLanguage(OutputLanguage language) { case output::LANG_SMTLIB_V1: case output::LANG_SMTLIB_V2_0: case output::LANG_SMTLIB_V2_5: + case output::LANG_SMTLIB_V2_6: case output::LANG_TPTP: case output::LANG_CVC4: case output::LANG_Z3STR: @@ -45,6 +46,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) { case input::LANG_SMTLIB_V1: case input::LANG_SMTLIB_V2_0: case input::LANG_SMTLIB_V2_5: + case input::LANG_SMTLIB_V2_6: case input::LANG_TPTP: case input::LANG_CVC4: case input::LANG_Z3STR: @@ -85,6 +87,9 @@ OutputLanguage toOutputLanguage(std::string language) { } else if(language == "smtlib2.5" || language == "smt2.5" || language == "LANG_SMTLIB_V2_5") { return output::LANG_SMTLIB_V2_5; + } else if(language == "smtlib2.6" || language == "smt2.6" || + language == "LANG_SMTLIB_V2_6") { + return output::LANG_SMTLIB_V2_6; } else if(language == "tptp" || language == "LANG_TPTP") { return output::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || @@ -117,6 +122,9 @@ InputLanguage toInputLanguage(std::string language) { } else if(language == "smtlib2.5" || language == "smt2.5" || language == "LANG_SMTLIB_V2_5") { return input::LANG_SMTLIB_V2_5; + } else if(language == "smtlib2.6" || language == "smt2.6" || + language == "LANG_SMTLIB_V2_6") { + return input::LANG_SMTLIB_V2_6; } else if(language == "tptp" || language == "LANG_TPTP") { return input::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || diff --git a/src/options/language.h b/src/options/language.h index 00328e4ab..6732aa6bd 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -49,8 +49,10 @@ enum CVC4_PUBLIC Language { LANG_SMTLIB_V2_0, /** The SMTLIB v2.5 input language */ LANG_SMTLIB_V2_5, + /** The SMTLIB v2.6 input language */ + LANG_SMTLIB_V2_6, /** Backward-compatibility for enumeration naming */ - LANG_SMTLIB_V2 = LANG_SMTLIB_V2_5, + LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6, /** The TPTP input language */ LANG_TPTP, /** The CVC4 input language */ @@ -82,6 +84,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_SMTLIB_V2_5: out << "LANG_SMTLIB_V2_5"; break; + case LANG_SMTLIB_V2_6: + out << "LANG_SMTLIB_V2_6"; + break; case LANG_TPTP: out << "LANG_TPTP"; break; @@ -123,6 +128,8 @@ enum CVC4_PUBLIC Language { LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0, /** The SMTLIB v2.5 output language */ LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5, + /** The SMTLIB v2.6 output language */ + LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6, /** Backward-compatibility for enumeration naming */ LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, /** The TPTP output language */ diff --git a/src/options/language.i b/src/options/language.i index d14368ca0..427e6c608 100644 --- a/src/options/language.i +++ b/src/options/language.i @@ -23,6 +23,7 @@ namespace CVC4 { %rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2; %rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0; %rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5; +%rename(INPUT_LANG_SMTLIB_V2_6) CVC4::language::input::LANG_SMTLIB_V2_6; %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP; %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; @@ -34,6 +35,7 @@ namespace CVC4 { %rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2; %rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0; %rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5; +%rename(OUTPUT_LANG_SMTLIB_V2_6) CVC4::language::output::LANG_SMTLIB_V2_6; %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP; %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 694d46d31..584be1329 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -434,6 +434,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt | smtlib | smt2 |\n\ smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6\n\ tptp TPTP format (cnf and fof)\n\ sygus SyGuS format\n\ \n\ @@ -445,6 +446,7 @@ Languages currently supported as arguments to the --output-lang option:\n\ smt | smtlib | smt2 |\n\ smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6\n\ tptp TPTP format\n\ z3str SMT-LIB 2.0 with Z3-str string constraints\n\ ast internal format (simple syntax trees)\n\ 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 types; std::vector 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* 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* 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* cmd] ; -datatypesDefCommand[bool isCo, CVC4::PtrCloser* cmd] +datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser* cmd] @declarations { std::vector dts; std::string name; @@ -1516,8 +1522,71 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser* 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* cmd] +@declarations { + std::vector dts; + std::vector types; + std::string name; + std::vector dnames; + std::vector arities; + std::vector 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; } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index c715312c1..a8a84c06f 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -43,6 +43,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { case LANG_SMTLIB_V2_5: return new printer::smt2::Smt2Printer(); + + case LANG_SMTLIB_V2_6: + return new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant); case LANG_TPTP: return new printer::tptp::TptpPrinter(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2b7da63f7..08eaf610a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -671,11 +671,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, tmp.replace(pos, 8, "::"); } out << tmp; - }else if( n.getKind()==kind::APPLY_TESTER ){ + }else if( n.getKind()==kind::APPLY_TESTER ){ unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - out << "is-"; - toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + if( d_variant==smt2_6_variant ){ + out << "(_ is "; + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + out << ")"; + }else{ + out << "is-"; + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + } }else{ toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); } @@ -1018,7 +1024,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || - tryToStream(out, c) || + tryToStream(out, c, d_variant) || tryToStream(out, c, d_variant) || tryToStream(out, c) || tryToStream(out, c, d_variant)) { @@ -1102,9 +1108,12 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps; std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn ); - if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){ - out << "(declare-datatypes () ((" << dynamic_cast(c)->getSymbol() << " "; - + if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){ + if(d_variant == smt2_6_variant) { + out << "(declare-datatypes ((" << dynamic_cast(c)->getSymbol() << " 0)) ("; + }else{ + out << "(declare-datatypes () ((" << dynamic_cast(c)->getSymbol() << " "; + } for( size_t i=0, N = tn_iterator->second.size(); i < N; i++ ){ out << "(" << (*tn_iterator).second[i] << ")"; } @@ -1457,32 +1466,60 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "(get-option :" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { +static void toStream(std::ostream& out, const Datatype & d) { + for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); + ctor != ctor_end; ++ctor){ + if( ctor!=d.begin() ) out << " "; + out << "(" << maybeQuoteSymbol(ctor->getName()); + + for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); + arg != arg_end; ++arg){ + out << " (" << arg->getSelector() << " " + << static_cast(arg->getType()).getRangeType() << ")"; + } + out << ")"; + } +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Variant v) throw() { const vector& datatypes = c->getDatatypes(); - out << "(declare-datatypes () ("; - for(vector::const_iterator i = datatypes.begin(), - i_end = datatypes.end(); - i != i_end; - ++i) { - - const Datatype & d = i->getDatatype(); - - out << "(" << maybeQuoteSymbol(d.getName()) << " "; - for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); - ctor != ctor_end; ++ctor){ - if( ctor!=d.begin() ) out << " "; - out << "(" << maybeQuoteSymbol(ctor->getName()); - - for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); - arg != arg_end; ++arg){ - out << " (" << arg->getSelector() << " " - << static_cast(arg->getType()).getRangeType() << ")"; - } - out << ")"; + out << "(declare-"; + Assert( !datatypes.empty() ); + if( datatypes[0].getDatatype().isCodatatype() ){ + out << "co"; + } + out << "datatypes"; + if(v == smt2_6_variant) { + out << " ("; + for(vector::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; ++i) { + const Datatype & d = i->getDatatype(); + out << "(" << maybeQuoteSymbol(d.getName()); + out << " " << d.getNumParameters() << ")"; } - out << ")" << endl; + out << ") "; + for(vector::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; ++i) { + const Datatype & d = i->getDatatype(); + out << "("; + toStream( out, d ); + out << ")" << endl; + } + }else{ + out << " () ("; + for(vector::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; ++i) { + const Datatype & d = i->getDatatype(); + out << "(" << maybeQuoteSymbol(d.getName()) << " "; + toStream( out, d ); + out << ")" << endl; + } + out << ")"; } - out << "))"; + out << ")"; } static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 0354a5738..d73f11b59 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -30,6 +30,7 @@ namespace smt2 { enum Variant { no_variant, smt2_0_variant, // old-style 2.0 syntax, when it makes a difference + smt2_6_variant, // new-style 2.6 syntax, when it makes a difference z3str_variant, // old-style 2.0 and also z3str syntax sygus_variant // variant for sygus };/* enum Variant */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2aaf43569..306843c81 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2057,7 +2057,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.0" ) { // supported SMT-LIB version if(!options::outputLanguage.wasSetByUser() && - options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) { + ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) { options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0); *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0); } @@ -2071,6 +2071,15 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5); } return; + } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) || + value.getValue() == "2.6" ) { + // supported SMT-LIB version + if(!options::outputLanguage.wasSetByUser() && + options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { + options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6); + *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6); + } + return; } Warning() << "Warning: unsupported smt-lib-version: " << value << endl; throw UnrecognizedOptionException(); diff --git a/src/util/result.cpp b/src/util/result.cpp index af28269f1..c23813a51 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -351,6 +351,7 @@ void Result::toStream(std::ostream& out, OutputLanguage language) const { switch (language) { case language::output::LANG_SMTLIB_V2_0: case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SMTLIB_V2_6: case language::output::LANG_SYGUS: case language::output::LANG_Z3STR: toStreamSmt2(out); diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index a34689d1e..59d12d81f 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -272,6 +272,7 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) { case language::output::LANG_SMTLIB_V1: case language::output::LANG_SMTLIB_V2_0: case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SMTLIB_V2_6: case language::output::LANG_SYGUS: case language::output::LANG_TPTP: case language::output::LANG_Z3STR: diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index fed65924b..90d6b4716 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -74,7 +74,10 @@ TESTS = \ dt-param-card4-bool-sat.smt2 \ bug604.smt2 \ bug597-rbt.smt2 \ - example-dailler-min.smt2 + example-dailler-min.smt2 \ + dt-2.6.smt2 \ + dt-sel-2.6.smt2 \ + dt-param-2.6.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/dt-2.6.smt2 b/test/regress/regress0/datatypes/dt-2.6.smt2 new file mode 100644 index 000000000..07dc0169e --- /dev/null +++ b/test/regress/regress0/datatypes/dt-2.6.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --lang=smt2.6 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((IntList 0)) ( +((empty) (insert ( head Int ) ( tail IntList ) )) +)) + +(declare-fun x () IntList) +(declare-fun y () IntList) +(declare-fun z () IntList) + +(assert (distinct x y z)) + +(check-sat) diff --git a/test/regress/regress0/datatypes/dt-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-param-2.6.smt2 new file mode 100644 index 000000000..a132ce8fc --- /dev/null +++ b/test/regress/regress0/datatypes/dt-param-2.6.smt2 @@ -0,0 +1,37 @@ +; COMMAND-LINE: --lang=smt2.6 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ( ( Tree 1) ( TreeList 1) ) ( +(par ( X ) ( ( node ( value X ) ( children ( TreeList X )) ))) +(par ( Y ) ( ( empty ) ( insert ( head ( Tree Y )) ( tail ( TreeList Y ))) )) +)) + + +(declare-fun x () (Tree Int)) +(declare-fun y () (Tree Int)) +(declare-fun z () (Tree Int)) + + +(assert (distinct x y z)) +(assert (= (value x) 5)) +(assert ((_ is insert) (children y))) +(assert (= (value (head (children y))) 7)) + +(declare-sort U 0) +(declare-fun a () (Tree U)) +(declare-fun b () (Tree U)) +(declare-fun c () (Tree U)) + +(assert (distinct a b c)) + +(assert ((_ is insert) (children a))) + + +(declare-fun d () (Tree (Tree Int))) +(declare-fun e () (Tree (Tree Int))) +(declare-fun f () (Tree (Tree Int))) + +(assert (distinct d e f)) + +(check-sat) diff --git a/test/regress/regress0/datatypes/dt-sel-2.6.smt2 b/test/regress/regress0/datatypes/dt-sel-2.6.smt2 new file mode 100644 index 000000000..ae290a5ba --- /dev/null +++ b/test/regress/regress0/datatypes/dt-sel-2.6.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --lang=smt2.6 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((IntList 0)) ( +((empty) (insert ( head Int ) ( tail IntList ) )) +)) + +(declare-fun x () IntList) +(declare-fun y () IntList) +(declare-fun z () IntList) + +(assert (distinct x y z)) + +(assert (not ((_ is insert) x))) +(assert (not ((_ is insert) y))) + +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index a04e488d8..5bc46d4f9 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -212,7 +212,7 @@ else error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p or *.sy" fi -command_line="${command_line:+$command_line }--lang=$lang" +command_line="--lang=$lang ${command_line:+$command_line }" gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX