Remove SMT1 parser. (#3228)

This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).

Fixes #2948 and fixes #1313.

3 files changed, 1 insertions, 15 deletions

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 5fb555d70..fad4e77c5 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -109,7 +109,7 @@ endif()
 #-----------------------------------------------------------------------------#
 # Generate language tokens header files.
 
-foreach(lang Cvc Smt1 Smt2 Tptp)
+foreach(lang Cvc Smt2 Tptp)
   string(TOLOWER ${lang} lang_lc)
   add_custom_command(
     OUTPUT ${lang_lc}_tokens.h
@@ -125,7 +125,6 @@ endforeach()
 add_custom_target(gen-tokens
   DEPENDS
     cvc_tokens.h
-    smt1_tokens.h
     smt2_tokens.h
     tptp_tokens.h
 )
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d0fce8d00..de840cb07 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -165,10 +165,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       unsigned len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
-      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
-      } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
-        opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
         opts.setInputLanguage(language::input::LANG_TPTP);
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index e7cd8691e..f582d20e5 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -69,10 +69,6 @@ static const std::string cvc_commands[] = {
 #include "main/cvc_tokens.h"
 };/* cvc_commands */
 
-static const std::string smt1_commands[] = {
-#include "main/smt1_tokens.h"
-};/* smt1_commands */
-
 static const std::string smt2_commands[] = {
 #include "main/smt2_tokens.h"
 };/* smt2_commands */
@@ -119,11 +115,6 @@ InteractiveShell::InteractiveShell(api::Solver* solver)
       commandsBegin = cvc_commands;
       commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
       break;
-    case output::LANG_SMTLIB_V1:
-      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1";
-      commandsBegin = smt1_commands;
-      commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
-      break;
     case output::LANG_TPTP:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
       commandsBegin = tptp_commands;