Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)

7 files changed, 93 insertions, 38 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 220916a1a..94ca46257 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -141,6 +141,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
      tryToStream<ResetCommand>(out, c) ||
+     tryToStream<ResetAssertionsCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
@@ -229,6 +230,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() {
   out << "Reset()";
 }
 
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() {
+  out << "ResetAssertions()";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "Quit()";
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 48f1aadec..f8df9d906 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -860,6 +860,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
      tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
      tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
      tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
      tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
      tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
@@ -1051,6 +1052,10 @@ static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) th
   out << "RESET;";
 }
 
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c, bool cvc3Mode) throw() {
+  out << "RESET ASSERTIONS;";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
   //out << "EXIT;";
 }
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index dd2e180e1..a8e2534dc 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -40,7 +40,10 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   case LANG_SMTLIB_V1: // TODO the printer
     return new printer::smt1::Smt1Printer();
 
-  case LANG_SMTLIB_V2:
+  case LANG_SMTLIB_V2_0:
+    return new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant);
+
+  case LANG_SMTLIB_V2_5:
     return new printer::smt2::Smt2Printer();
 
   case LANG_TPTP:
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index 474fe58dc..05714fbce 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -33,24 +33,24 @@ namespace smt1 {
 
 void Smt1Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types, size_t dag) const throw() {
-  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const Command* c,
                            int toDepth, bool types, size_t dag) const throw() {
-  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
-  s->toStream(out, language::output::LANG_SMTLIB_V2);
+  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
 }
 
 void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5dc5cb7ee..88bcce5ae 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -125,7 +125,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, language::output::LANG_SMTLIB_V2);
+      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
     }
 
     return;
@@ -192,6 +192,27 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::CONST_STRING: {
+      const String& s = n.getConst<String>();
+      out << '"';
+      for(size_t i = 0; i < s.size(); ++i) {
+        char c = String::convertUnsignedIntToChar(s[i]);
+        if(c == '"') {
+          if(d_variant == z3str_variant || d_variant == smt2_0_variant) {
+            out << "\\\"";
+          } else {
+            out << "\"\"";
+          }
+        } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) {
+          out << "\\\\";
+        } else {
+          out << c;
+        }
+      }
+      out << '"';
+      break;
+    }
+
     case kind::STORE_ALL: {
       ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
       out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")";
@@ -483,7 +504,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       out << (*i).getType();
       // The following code do stange things
       // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-      //                         false, language::output::LANG_SMTLIB_V2);
+      //                         false, language::output::LANG_SMTLIB_V2_5);
       out << ')';
       if(++i != iend) {
         out << ' ';
@@ -699,6 +720,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
      tryToStream<ResetCommand>(out, c) ||
+     tryToStream<ResetAssertionsCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
@@ -714,16 +736,16 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<GetProofCommand>(out, c) ||
      tryToStream<GetUnsatCoreCommand>(out, c) ||
-     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
-     tryToStream<SetInfoCommand>(out, c) ||
+     tryToStream<SetInfoCommand>(out, c, d_variant) ||
      tryToStream<GetInfoCommand>(out, c) ||
      tryToStream<SetOptionCommand>(out, c) ||
      tryToStream<GetOptionCommand>(out, c) ||
      tryToStream<DatatypeDeclarationCommand>(out, c) ||
-     tryToStream<CommentCommand>(out, c) ||
+     tryToStream<CommentCommand>(out, c, d_variant) ||
      tryToStream<EmptyCommand>(out, c) ||
-     tryToStream<EchoCommand>(out, c)) {
+     tryToStream<EchoCommand>(out, c, d_variant)) {
     return;
   }
 
@@ -733,7 +755,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
 }/* Smt2Printer::toStream(Command*) */
 
 static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
 }
 
 // SMT-LIB quoting for symbols
@@ -753,7 +775,7 @@ static std::string quoteSymbol(std::string s) {
 
 static std::string quoteSymbol(TNode n) {
   std::stringstream ss;
-  ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+  ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
   return quoteSymbol(ss.str());
 }
 
@@ -766,13 +788,13 @@ void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw()
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw();
 
 void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
 
-  if(tryToStream<CommandSuccess>(out, s) ||
-     tryToStream<CommandFailure>(out, s) ||
-     tryToStream<CommandUnsupported>(out, s)) {
+  if(tryToStream<CommandSuccess>(out, s, d_variant) ||
+     tryToStream<CommandFailure>(out, s, d_variant) ||
+     tryToStream<CommandUnsupported>(out, s, d_variant)) {
     return;
   }
 
@@ -944,6 +966,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() {
   out << "(reset)";
 }
 
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() {
+  out << "(reset-assertions)";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "(exit)";
 }
@@ -1065,8 +1091,12 @@ static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() {
   out << "(get-unsat-core)";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
-  out << "(set-info :status " << c->getStatus() << ")";
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Variant v) throw() {
+  if(v == z3str_variant || v == smt2_0_variant) {
+    out << "(set-info :status " << c->getStatus() << ")";
+  } else {
+    out << "(meta-info :status " << c->getStatus() << ")";
+  }
 }
 
 static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) throw() {
@@ -1078,8 +1108,12 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Varia
   }
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
-  out << "(set-info :" << c->getFlag() << " ";
+static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) throw() {
+  if(v == z3str_variant || v == smt2_0_variant) {
+    out << "(set-info :" << c->getFlag() << " ";
+  } else {
+    out << "(meta-info :" << c->getFlag() << " ";
+  }
   toStream(out, c->getSExpr());
   out << ")";
 }
@@ -1126,11 +1160,11 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
   out << "))";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() {
   string s = c->getComment();
   size_t pos = 0;
   while((pos = s.find_first_of('"', pos)) != string::npos) {
-    s.replace(pos, 1, "\\\"");
+    s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(set-info :notes \"" << s << "\")";
@@ -1139,8 +1173,15 @@ static void toStream(std::ostream& out, const CommentCommand* c) throw() {
 static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 }
 
-static void toStream(std::ostream& out, const EchoCommand* c) throw() {
-  out << "(echo \"" << c->getOutput() << "\")";
+static void toStream(std::ostream& out, const EchoCommand* c, Variant v) throw() {
+  std::string s = c->getOutput();
+  // escape all double-quotes
+  size_t pos = 0;
+  while((pos = s.find('"', pos)) != string::npos) {
+    s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+    pos += 2;
+  }
+  out << "(echo \"" << s << "\")";
 }
 
 template <class T>
@@ -1161,13 +1202,13 @@ static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw()
   return false;
 }
 
-static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) throw() {
   if(Command::printsuccess::getPrintSuccess(out)) {
     out << "success" << endl;
   }
 }
 
-static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() {
 #ifdef CVC4_COMPETITION_MODE
   // if in competition mode, lie and say we're ok
   // (we have nothing to lose by saying success, and everything to lose
@@ -1178,21 +1219,21 @@ static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
 #endif /* CVC4_COMPETITION_MODE */
 }
 
-static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+static void toStream(std::ostream& out, const CommandFailure* s, Variant v) throw() {
   string message = s->getMessage();
   // escape all double-quotes
   size_t pos = 0;
   while((pos = message.find('"', pos)) != string::npos) {
-    message = message.replace(pos, 1, "\\\"");
+    message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(error \"" << message << "\")" << endl;
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() {
   if(typeid(*s) == typeid(T)) {
-    toStream(out, dynamic_cast<const T*>(s));
+    toStream(out, dynamic_cast<const T*>(s), v);
     return true;
   }
   return false;
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index dbbc67fc2..4455a053c 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -29,7 +29,8 @@ namespace smt2 {
 
 enum Variant {
   no_variant,
-  z3str_variant
+  smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
+  z3str_variant // old-style 2.0 and also z3str syntax
 };/* enum Variant */
 
 class Smt2Printer : public CVC4::Printer {
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index cce48ae47..3c46a5849 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -33,26 +33,26 @@ namespace tptp {
 
 void TptpPrinter::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types, size_t dag) const throw() {
-  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const Command* c,
                            int toDepth, bool types, size_t dag) const throw() {
-  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
-  s->toStream(out, language::output::LANG_SMTLIB_V2);
+  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
   out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
-    this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2, out, m, m.getCommand(i));
+    this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i));
   }
   out << "% SZS output end FiniteModel for " << m.getInputName() << endl;
 }