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, 5 insertions, 0 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 7336dd084..5389f270f 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -34,6 +34,7 @@
 #include "parser/cvc/cvc_input.h"
 #include "parser/smt/smt_input.h"
 #include "parser/smt2/smt2_input.h"
+#include "parser/tptp/tptp_input.h"
 #include "util/output.h"
 #include "util/Assert.h"
 
@@ -201,6 +202,10 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt2Input(inputStream);
     break;
 
+  case LANG_TPTP:
+    input = new TptpInput(inputStream);
+    break;
+
   default:
     Unhandled(lang);
   }