removed support for the old smtlib dialect

ModelWriter · Nov 15, 2017 · 44240ce · 44240ce
1 parent 3f2656e
commit 44240ce
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 9 deletions.
diff --git a/Makefile b/Makefile
@@ -399,8 +399,7 @@ VS_OBJ = Shell/AnswerExtractor.o\
 #         Shell/HalfBoundingRemover.o\
 #         Shell/SubsumptionRemover.o\
 
-PARSE_OBJ = Parse/SMTLIB.o\
-            Parse/SMTLIB2.o\
+PARSE_OBJ = Parse/SMTLIB2.o\
             Parse/TPTP.o
 
 DP_OBJ = DP/ShortConflictMetaDP.o\

diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp
@@ -39,7 +39,6 @@
 #include "Kernel/Problem.hpp"
 #include "Kernel/FormulaUnit.hpp"
 
-#include "Parse/SMTLIB.hpp"
 #include "Parse/SMTLIB2.hpp"
 #include "Parse/TPTP.hpp"
 
@@ -251,13 +250,19 @@ Problem* UIHelper::getInputProblem(const Options& opts)
     }
     break;
   case Options::InputSyntax::SMTLIB:
-    {
-      Parse::SMTLIB parser(opts);
-      parser.parse(*input);
-      units = parser.getFormulas();
-      s_haveConjecture=true;
+    /*  {
+        Parse::SMTLIB parser(opts);
+        parser.parse(*input);
+        units = parser.getFormulas();
+        s_haveConjecture=true;
+      }
+      break; */
+    if (outputAllowed()) {
+      env.beginOutput();
+      addCommentSignForSZS(env.out());
+      env.out() << "Vampire no longer supports the old smtlib format, trying with smtlib2 instead." << endl;
+      env.endOutput();
     }
-    break;
   case Options::InputSyntax::SMTLIB2:
   {
 	  Parse::SMTLIB2 parser(opts);