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

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index cde063584..5229400b5 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -39,6 +39,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   case LANG_SMTLIB_V2:
     return new printer::smt2::Smt2Printer();
 
+  case LANG_TPTP: //TODO the printer
+    return new printer::smt2::Smt2Printer();
+
   case LANG_CVC4:
     return new printer::cvc::CvcPrinter();