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

1 files changed, 53 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 */