TPTP: add parser for cnf and fof

 - include directive works
 - no keyword : 'fof', 'cnf', ... can be used for symbols name
 - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
 - same thing for string

But:
 - string not distinct by projection to real, not sure if the current state of string theory make them distinct
 - filtering in include is not done
 - the result is not printed in the TPTP way (currently SMT2 way)

4 files changed, 18 insertions, 1 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index e6aa6b423..594751358 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -53,7 +53,8 @@ BUILT_SOURCES = \
 TOKENS_FILES = \
 	cvc_tokens.h \
 	smt_tokens.h \
-	smt2_tokens.h
+	smt2_tokens.h \
+	tptp_tokens.h
 
 cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
@@ -61,6 +62,8 @@ smt_tokens.h: @srcdir@/../parser/smt/Smt.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
 smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
+tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g
+	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
 
 clean-local:
 	rm -f $(BUILT_SOURCES)
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index 742cba8d2..44457841d 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -182,6 +182,9 @@ int runCvc4(int argc, char* argv[], Options& options) {
         options.inputLanguage = language::input::LANG_SMTLIB_V2;
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
         options.inputLanguage = language::input::LANG_SMTLIB;
+      } else if((len >= 2 && !strcmp(".p", filename + len - 2))
+                || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
+        options.inputLanguage = language::input::LANG_TPTP;
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
         options.inputLanguage = language::input::LANG_CVC4;
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 7972cd94d..a8da88173 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -261,6 +261,9 @@ int runCvc4(int argc, char *argv[], Options& options) {
         options.inputLanguage = language::input::LANG_SMTLIB_V2;
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
         options.inputLanguage = language::input::LANG_SMTLIB;
+      } else if((len >= 2 && !strcmp(".p", filename + len - 2))
+                || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
+        options.inputLanguage = language::input::LANG_TPTP;
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
         options.inputLanguage = language::input::LANG_CVC4;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index d8e7df2f2..03a3a0ae3 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -72,6 +72,10 @@ static const char* const smt2_commands[] = {
 #include "main/smt2_tokens.h"
 };/* smt2_commands */
 
+static const char* const tptp_commands[] = {
+#include "main/tptp_tokens.h"
+};/* tptp_commands */
+
 static const char* const* commandsBegin;
 static const char* const* commandsEnd;
 
@@ -110,6 +114,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
       commandsBegin = smt2_commands;
       commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+    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: Unhandled(lang);
     }