New translation work, support Z3-str-style string constraints.

2 files changed, 66 insertions, 1 deletions

diff --git a/src/util/language.cpp b/src/util/language.cpp
index 9cac3dd3f..c5c9828df 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -25,6 +25,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_SMTLIB_V2:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
+  case output::LANG_Z3STR:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
 
@@ -41,8 +42,9 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
   case input::LANG_SMTLIB_V1:
   case input::LANG_SMTLIB_V2:
-  case input::LANG_CVC4:
   case input::LANG_TPTP:
+  case input::LANG_CVC4:
+  case input::LANG_Z3STR:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
 
@@ -61,5 +63,55 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   }/* switch(language) */
 }/* toOutputLanguage() */
 
+OutputLanguage toOutputLanguage(std::string language) {
+  if(language == "cvc4" || language == "pl" ||
+     language == "presentation" || language == "native" ||
+     language == "LANG_CVC4") {
+    return output::LANG_CVC4;
+  } else if(language == "smtlib1" || language == "smt1" ||
+            language == "LANG_SMTLIB_V1") {
+    return output::LANG_SMTLIB_V1;
+  } else if(language == "smtlib" || language == "smt" ||
+            language == "smtlib2" || language == "smt2" ||
+            language == "LANG_SMTLIB_V2") {
+    return output::LANG_SMTLIB_V2;
+  } else if(language == "tptp" || language == "LANG_TPTP") {
+    return output::LANG_TPTP;
+  } else if(language == "z3str" || language == "z3-str" ||
+            language == "LANG_Z3STR") {
+    return output::LANG_Z3STR;
+  } else if(language == "ast" || language == "LANG_AST") {
+    return output::LANG_AST;
+  } else if(language == "auto" || language == "LANG_AUTO") {
+    return output::LANG_AUTO;
+  }
+
+  throw OptionException(std::string("unknown output language `" + language + "'"));
+}/* toOutputLanguage() */
+
+InputLanguage toInputLanguage(std::string language) {
+  if(language == "cvc4" || language == "pl" ||
+     language == "presentation" || language == "native" ||
+     language == "LANG_CVC4") {
+    return input::LANG_CVC4;
+  } else if(language == "smtlib1" || language == "smt1" ||
+            language == "LANG_SMTLIB_V1") {
+    return input::LANG_SMTLIB_V1;
+  } else if(language == "smtlib" || language == "smt" ||
+            language == "smtlib2" || language == "smt2" ||
+            language == "LANG_SMTLIB_V2") {
+    return input::LANG_SMTLIB_V2;
+  } else if(language == "tptp" || language == "LANG_TPTP") {
+    return input::LANG_TPTP;
+  } else if(language == "z3str" || language == "z3-str" ||
+            language == "LANG_Z3STR") {
+    return input::LANG_Z3STR;
+  } else if(language == "auto" || language == "LANG_AUTO") {
+    return input::LANG_AUTO;
+  }
+
+  throw OptionException(std::string("unknown input language " + language + "'"));
+}/* toInputLanguage() */
+
 }/* CVC4::language namespace */
 }/* CVC4 namespace */
diff --git a/src/util/language.h b/src/util/language.h
index b83b3d093..c79c4d9aa 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -23,6 +23,7 @@
 #include <string>
 
 #include "util/exception.h"
+#include "options/option_exception.h"
 
 namespace CVC4 {
 namespace language {
@@ -50,6 +51,8 @@ enum CVC4_PUBLIC Language {
   LANG_TPTP,
   /** The CVC4 input language */
   LANG_CVC4,
+  /** The Z3-str input language */
+  LANG_Z3STR,
 
   // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
@@ -76,6 +79,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
+  case LANG_Z3STR:
+    out << "LANG_Z3STR";
+    break;
   default:
     out << "undefined_input_language";
   }
@@ -107,6 +113,8 @@ enum CVC4_PUBLIC Language {
   LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
   LANG_CVC4 = input::LANG_CVC4,
+  /** The Z3-str output language */
+  LANG_Z3STR = input::LANG_Z3STR,
 
   // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -133,6 +141,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
+  case LANG_Z3STR:
+    out << "LANG_Z3STR";
+    break;
   case LANG_AST:
     out << "LANG_AST";
     break;
@@ -153,6 +164,8 @@ namespace language {
 
 InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
 OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
+InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC;
+OutputLanguage toOutputLanguage(std::string language) CVC4_PUBLIC;
 
 }/* CVC4::language namespace */
 }/* CVC4 namespace */