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

diff --git a/src/util/language.cpp b/src/util/language.cpp
index da54a4783..1792797cf 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -25,6 +25,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB:
   case output::LANG_SMTLIB_V2:
+  case output::LANG_TPTP:
   case output::LANG_CVC4:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
@@ -43,6 +44,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_SMTLIB:
   case input::LANG_SMTLIB_V2:
   case input::LANG_CVC4:
+  case input::LANG_TPTP:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
 
diff --git a/src/util/language.h b/src/util/language.h
index d3405e35b..b84d45d89 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -48,6 +48,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB = 0,
   /** The SMTLIB v2 input language */
   LANG_SMTLIB_V2,
+  /** The TPTP input language */
+  LANG_TPTP,
   /** The CVC4 input language */
   LANG_CVC4,
 
@@ -70,6 +72,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2:
     out << "LANG_SMTLIB_V2";
     break;
+  case LANG_TPTP:
+    out << "LANG_TPTP";
+    break;
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
@@ -100,6 +105,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB = input::LANG_SMTLIB,
   /** The SMTLIB v2 output language */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
+  /** The TPTP output language */
+  LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
   LANG_CVC4 = input::LANG_CVC4,
 
@@ -122,6 +129,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2:
     out << "LANG_SMTLIB_V2";
     break;
+  case LANG_TPTP:
+    out << "LANG_TPTP";
+    break;
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
diff --git a/src/util/language.i b/src/util/language.i
index 28e0eb5ac..ca8e5012a 100644
--- a/src/util/language.i
+++ b/src/util/language.i
@@ -21,12 +21,14 @@ namespace CVC4 {
 %rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO;
 %rename(INPUT_LANG_SMTLIB) CVC4::language::input::LANG_SMTLIB;
 %rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2;
+%rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
 
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
 %rename(OUTPUT_LANG_SMTLIB) CVC4::language::output::LANG_SMTLIB;
 %rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2;
+%rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP;
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
 %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX;
diff --git a/src/util/options.cpp b/src/util/options.cpp
index b9291f59c..c02482e7e 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -312,12 +312,14 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   pl | cvc4      CVC4 presentation language\n\
   smt | smtlib   SMT-LIB format 1.2\n\
   smt2 | smtlib2 SMT-LIB format 2.0\n\
+  tptp           TPTP format (cnf and fof)\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
   auto           match the output language to the input language\n\
   pl | cvc4      CVC4 presentation language\n\
   smt | smtlib   SMT-LIB format 1.2\n\
   smt2 | smtlib2 SMT-LIB format 2.0\n\
+  tptp           TPTP format\n\
   ast            internal format (simple syntax-tree language)\n\
 ";
 
@@ -1633,6 +1635,9 @@ void Options::setOutputLanguage(const char* str) throw(OptionException) {
   } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
     outputLanguage = language::output::LANG_SMTLIB_V2;
     return;
+  } else if(!strcmp(str, "tptp")) {
+    outputLanguage = language::output::LANG_TPTP;
+    return;
   } else if(!strcmp(str, "ast")) {
     outputLanguage = language::output::LANG_AST;
     return;
@@ -1659,6 +1664,9 @@ void Options::setInputLanguage(const char* str) throw(OptionException) {
   } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
     inputLanguage = language::input::LANG_SMTLIB_V2;
     return;
+  } else if(!strcmp(str, "tptp")) {
+    inputLanguage = language::input::LANG_TPTP;
+    return;
   } else if(!strcmp(str, "auto")) {
     inputLanguage = language::input::LANG_AUTO;
     return;