Initial support for string standard in smt lib 2.6 (#1848)

2 files changed, 17 insertions, 16 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 4761ba07e..e58c5319a 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -125,22 +125,25 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = smt1_commands;
       commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       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);
-      break;
     case output::LANG_TPTP:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
       commandsBegin = tptp_commands;
       commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
       break;
     default:
-      std::stringstream ss;
-      ss << "internal error: unhandled language " << lang;
-      throw Exception(ss.str());
+      if (language::isOutputLang_smt2(lang))
+      {
+        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
+        commandsBegin = smt2_commands;
+        commandsEnd =
+            smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+      }
+      else
+      {
+        std::stringstream ss;
+        ss << "internal error: unhandled language " << lang;
+        throw Exception(ss.str());
+      }
     }
     d_usingReadline = true;
     int err = ::read_history(d_historyFilename.c_str());
@@ -333,9 +336,8 @@ restart:
     line += "\n";
     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_6) {
+    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+    {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 758d10af8..29d720b90 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -64,9 +64,8 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *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_6) {
+    if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+    {
       *opts.getOut() << "(error \"" << e << "\")" << endl;
     } else {
       *opts.getErr() << "CVC4 Error:" << endl << e << endl;