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)

12 files changed, 174 insertions, 3 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index a1d960079..5eda230c3 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -85,6 +85,19 @@ CVC_TESTS = \
 	wiki.21.cvc \
 	simplification_bug3.cvc
 
+# Regression tests for TPTP inputs
+TPTP_TESTS = \
+	tptp_parser.p \
+	tptp_parser2.p \
+	tptp_parser3.p \
+	tptp_parser4.p \
+	tptp_parser5.p \
+	tptp_parser6.p \
+	tptp_parser7.p \
+	tptp_parser8.p \
+	tptp_parser9.p \
+	tptp_parser10.p
+
 # Regression tests derived from bug reports
 BUG_TESTS = \
 	bug32.cvc \
@@ -104,7 +117,7 @@ BUG_TESTS = \
 	bug310.cvc \
 	bug339.smt2
 
-TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect
diff --git a/test/regress/regress0/tptp_parser.p b/test/regress/regress0/tptp_parser.p
new file mode 100644
index 000000000..0be0adbbf
--- /dev/null
+++ b/test/regress/regress0/tptp_parser.p
@@ -0,0 +1,17 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+/*
+cnf(query_1,axiom,
+    $false | $false /* | $false).
+*/
+
+cnf(query_1,axiom,
+    $false | $false | $false).
+
+cnf(query_1,negated_conjecture, ~
+    $false | $false | $false).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser10.p b/test/regress/regress0/tptp_parser10.p
new file mode 100644
index 000000000..90db619e7
--- /dev/null
+++ b/test/regress/regress0/tptp_parser10.p
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+fof(query_1,axiom, ![A,B]: (A != B => e(A) != e(B)) ).
+
+fof(query_1,conjecture, e(1.6) != e(1) ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser2.p b/test/regress/regress0/tptp_parser2.p
new file mode 100644
index 000000000..83a5f7b83
--- /dev/null
+++ b/test/regress/regress0/tptp_parser2.p
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, a | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~a | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser3.p b/test/regress/regress0/tptp_parser3.p
new file mode 100644
index 000000000..3677e6ffe
--- /dev/null
+++ b/test/regress/regress0/tptp_parser3.p
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( a, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(a, d) | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser4.p b/test/regress/regress0/tptp_parser4.p
new file mode 100644
index 000000000..6c5bd29da
--- /dev/null
+++ b/test/regress/regress0/tptp_parser4.p
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+% EXIT: 20
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, d) | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp_parser5.p
new file mode 100644
index 000000000..faacfdccc
--- /dev/null
+++ b/test/regress/regress0/tptp_parser5.p
@@ -0,0 +1,16 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, e) | ~ 'c' ).
+
+cnf(query_1,axiom, e != d ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp_parser6.p
new file mode 100644
index 000000000..0684a6a3d
--- /dev/null
+++ b/test/regress/regress0/tptp_parser6.p
@@ -0,0 +1,16 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | cnf ).
+
+cnf(query_1,axiom, cnf | c ).
+
+cnf(query_1,axiom, ~p(A, axiom) | ~ 'c' ).
+
+cnf(query_1,axiom, axiom != d ).
+
+cnf(query_1,negated_conjecture, ~ cnf ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp_parser7.p
new file mode 100644
index 000000000..ec90157e7
--- /dev/null
+++ b/test/regress/regress0/tptp_parser7.p
@@ -0,0 +1,16 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, axiom) ).
+
+cnf(query_1,axiom, axiom != d ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp_parser8.p
new file mode 100644
index 000000000..3bfd8efb6
--- /dev/null
+++ b/test/regress/regress0/tptp_parser8.p
@@ -0,0 +1,11 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+include('tptp_parser7.p').
+
+cnf(query_1,axiom, include('A') | b ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp_parser9.p
new file mode 100644
index 000000000..dab8065b5
--- /dev/null
+++ b/test/regress/regress0/tptp_parser9.p
@@ -0,0 +1,14 @@
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
+
+%--------------------------------------------------------------------------
+
+fof(query_1,axiom, include(1) ).
+
+fof(query_1,axiom, ![E]: e(E,1.6) ).
+
+fof(query_1,axiom, ![A,E]: ~e(A,3.0E3) ).
+
+fof(query_1,conjecture, ![E]: e(E,2.6) ).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 587d3cdda..5ed43d1a0 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -13,7 +13,7 @@
 prog=`basename "$0"`
 
 if [ $# -lt 2 -o $# -gt 3 ]; then
-  echo "usage: $prog [ --proof | --dump ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
+  echo "usage: $prog [ --proof | --dump ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ]" >&2
   exit 1
 fi
 
@@ -149,8 +149,24 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
     error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
   fi
   command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
+  proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1;
+  lang=tptp
+  expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
+  expected_output=$(grep '^% EXPECT: ' "$benchmark")
+  expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
+  if [ -z "$expected_output" -a -z "$expected_error" ]; then
+    error "cannot determine expected output of \`$benchmark': " \
+          "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
+  fi
+  expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,')
+  expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
+  if [ -z "$expected_exit_status" ]; then
+    error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
+  fi
+  command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
 else
-  error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
+  error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p"
 fi
 
 command_line="${command_line:+$command_line }--lang=$lang"