Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGround...

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 02edab533ba3e323b374610d29a93abb4168ee56..ac93114b7f775b11fc40369a86e4839290ef316e 100644 (file)
--- 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 334373642a17d3c0ba396f9b02a6637d1aa1ed0f..bb2956c446faca62407c17644c7b3f748598870c 100644 (file)
--- 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 7b6b9ad86e75a1108adb1b3f88952ad462051a6a..9f77045c483ca8d4d8c146cf415272dc800361cd 100644 (file)
--- 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 665089e4500df4dec0e09b240814869b62fb08df..7ae9d075a065a5ce47f4ef12bef1a22c7efbd0a7 100644 (file)
--- 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 00328e4ab454b6bdcd831fb0a6fcc84c2053f420..6732aa6bd4681d46bab43818ea3269b2d4cb7b20 100644 (file)
--- 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 d14368ca0dad4280c3e6df5a3dd900ed584c8328..427e6c6081e6b085b9f82458d830b0cd43a3f90e 100644 (file)
--- 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 694d46d312ade0f67943fe7ed18191d563e2b1ab..584be1329247c5ebc944c6b5d5520047133447f0 100644 (file)
--- 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 6edb23a2356861a2384bb9a917c0f5e7b88987c3..b2f2cdd532aca875b8bf7c42c8f94edb01b396ec 100644 (file)
--- 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 fb0304045618dc7658827fd6b484c7dc77156ac3..d72e1526e9b2e15393de4d7b09ea0c3631b41277 100644 (file)
--- 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 8580d56725a7e883cdcdd5f7f967d98276223f8b..a666fd381f75159f1d9a32584dbbb702371f50e0 100644 (file)
--- 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 07ace295c7ceaff7fd76f48750c95aee84853fb0..4d884d894b281176bc94937d107982c506f5e892 100644 (file)
--- 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 fc930dc7919a80caa082c5ce7e96f99af4d96520..764cb686684b10b1ce2a041330bd650f13784d1e 100644 (file)
--- 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 7aa4c344182b55fdee3a64ba6d84be1126f1ec24..03f819a5d97f84f1245b8e68f5c97cde88b7bf86 100644 (file)
--- 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 c715312c1e76c1ea277d76b0d8948b7b6193eeaa..a8a84c06f343a3112393816d5bfd1b7a964a1b6c 100644 (file)
--- 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 2b7da63f7165ee203379a8d11b7d3d7eec5d5a1b..08eaf610a35b5a4d73d011c017fba773e2c1d1eb 100644 (file)
--- 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<GetInfoCommand>(out, c) ||
      tryToStream<SetOptionCommand>(out, c) ||
      tryToStream<GetOptionCommand>(out, c) ||
-     tryToStream<DatatypeDeclarationCommand>(out, c) ||
+     tryToStream<DatatypeDeclarationCommand>(out, c, d_variant) ||
      tryToStream<CommentCommand>(out, c, d_variant) ||
      tryToStream<EmptyCommand>(out, c) ||
      tryToStream<EchoCommand>(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<const DeclareTypeCommand*>(c)->getSymbol() << " ";
-
+    if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){  
+      if(d_variant == smt2_6_variant) {
+        out << "(declare-datatypes ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " 0)) (";
+      }else{
+        out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(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<SelectorType>(arg->getType()).getRangeType() << ")";
+    }
+    out << ")";
+  }
+}
+
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Variant v) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
-  out << "(declare-datatypes () (";
-  for(vector<DatatypeType>::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<SelectorType>(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<DatatypeType>::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<DatatypeType>::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<DatatypeType>::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 0354a573844769e4f033d9f44121400911415b46..d73f11b59a5618a5b3d87cf4072f75338776f824 100644 (file)
--- 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 2aaf4356964bb81831c27681ee29c3e8183216b6..306843c81a59dfbe9e43226cecb5fba821083b66 100644 (file)
--- 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 af28269f13f013b344fec4e09a72908046912e57..c23813a514ae1eade1a69b28870a860d9afbb5df 100644 (file)
--- 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 a34689d1edd988e2d47e6ae9e6ea1ddfddcc1dd1..59d12d81f70da7288c56f9a996f4e8c84fe225f6 100644 (file)
--- 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 fed65924b01adde03765eda63acea22ebabc30df..90d6b471633fabf4014fbd869cd6ea4510d0a85b 100644 (file)
--- 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 (file)
index 0000000..07dc016
--- /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 (file)
index 0000000..a132ce8
--- /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 (file)
index 0000000..ae290a5
--- /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 a04e488d8320daa68a7ee80532b20dfd1393327a..5bc46d4f9a5153f58b7d598973543c91b9271c76 100755 (executable)
--- 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