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)

1 files changed, 8 insertions, 0 deletions

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);
     }