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.)

3 files changed, 41 insertions, 13 deletions

diff --git a/src/util/language.cpp b/src/util/language.cpp
index f19f20c03..ca611f729 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -22,7 +22,8 @@ namespace language {
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB_V1:
-  case output::LANG_SMTLIB_V2:
+  case output::LANG_SMTLIB_V2_0:
+  case output::LANG_SMTLIB_V2_5:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
@@ -41,7 +42,8 @@ InputLanguage toInputLanguage(OutputLanguage language) {
 OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
   case input::LANG_SMTLIB_V1:
-  case input::LANG_SMTLIB_V2:
+  case input::LANG_SMTLIB_V2_0:
+  case input::LANG_SMTLIB_V2_5:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
@@ -75,8 +77,12 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_SMTLIB_V1;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
-            language == "LANG_SMTLIB_V2") {
-    return output::LANG_SMTLIB_V2;
+            language == "smtlib2.0" || language == "smt2.0" ||
+            language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") {
+    return output::LANG_SMTLIB_V2_0;
+  } else if(language == "smtlib2.5" || language == "smt2.5" ||
+            language == "LANG_SMTLIB_V2_5") {
+    return output::LANG_SMTLIB_V2_5;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
@@ -101,8 +107,12 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_SMTLIB_V1;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
-            language == "LANG_SMTLIB_V2") {
-    return input::LANG_SMTLIB_V2;
+            language == "smtlib2.0" || language == "smt2.0" ||
+            language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") {
+    return input::LANG_SMTLIB_V2_0;
+  } else if(language == "smtlib2.5" || language == "smt2.5" ||
+            language == "LANG_SMTLIB_V2_5") {
+    return input::LANG_SMTLIB_V2_5;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
diff --git a/src/util/language.h b/src/util/language.h
index be962bf3e..abde0b509 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -45,8 +45,12 @@ enum CVC4_PUBLIC Language {
 
   /** The SMTLIB v1 input language */
   LANG_SMTLIB_V1 = 0,
-  /** The SMTLIB v2 input language */
-  LANG_SMTLIB_V2,
+  /** The SMTLIB v2.0 input language */
+  LANG_SMTLIB_V2_0,
+  /** The SMTLIB v2.5 input language */
+  LANG_SMTLIB_V2_5,
+  /** Backward-compatibility for enumeration naming */
+  LANG_SMTLIB_V2 = LANG_SMTLIB_V2_5,
   /** The TPTP input language */
   LANG_TPTP,
   /** The CVC4 input language */
@@ -70,8 +74,11 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V1:
     out << "LANG_SMTLIB_V1";
     break;
-  case LANG_SMTLIB_V2:
-    out << "LANG_SMTLIB_V2";
+  case LANG_SMTLIB_V2_0:
+    out << "LANG_SMTLIB_V2_0";
+    break;
+  case LANG_SMTLIB_V2_5:
+    out << "LANG_SMTLIB_V2_5";
     break;
   case LANG_TPTP:
     out << "LANG_TPTP";
@@ -107,7 +114,11 @@ enum CVC4_PUBLIC Language {
 
   /** The SMTLIB v1 output language */
   LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1,
-  /** The SMTLIB v2 output language */
+  /** The SMTLIB v2.0 output 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,
+  /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
   /** The TPTP output language */
   LANG_TPTP = input::LANG_TPTP,
@@ -134,8 +145,11 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V1:
     out << "LANG_SMTLIB_V1";
     break;
-  case LANG_SMTLIB_V2:
-    out << "LANG_SMTLIB_V2";
+  case LANG_SMTLIB_V2_0:
+    out << "LANG_SMTLIB_V2_0";
+    break;
+  case LANG_SMTLIB_V2_5:
+    out << "LANG_SMTLIB_V2_5";
     break;
   case LANG_TPTP:
     out << "LANG_TPTP";
diff --git a/src/util/language.i b/src/util/language.i
index 4cbe01df3..3ffc518ac 100644
--- a/src/util/language.i
+++ b/src/util/language.i
@@ -21,6 +21,8 @@ namespace CVC4 {
 %rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO;
 %rename(INPUT_LANG_SMTLIB_V1) CVC4::language::input::LANG_SMTLIB_V1;
 %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_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
@@ -29,6 +31,8 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
 %rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1;
 %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_TPTP) CVC4::language::output::LANG_TPTP;
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;