new tptp-provers interface now present in Makefile.in and why.conf.

The printer exists but is not yet usable.

Makefile.in

@@ -106,7 +106,7 @@ LIB_TRANSFORM = simplify_recursive_definition inlining \
 		eliminate_definition eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if
 
-LIB_PRINTER = print_real alt_ergo why3 smt coq
+LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
 
 LIBMODULES = src/config \
 	      $(addprefix src/util/, $(LIB_UTIL)) \

src/printer/tptp.ml

@@ -73,13 +73,10 @@ let rec print_term drv fmt t = match t.t_node with
           | _ -> fprintf fmt "@[(%a %a)@]"
 	      print_ident ls.ls_name (print_list space (print_term drv)) tl
         end end
-  | Tlet (t1, tb) ->
-      let v, t2 = t_open_bound tb in
-      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
-        (print_term drv) t1 (print_term drv) t2;
-      forget_var v
+  | Tlet (t1, tb) -> unsupportedTerm t
+      "tptp : you must eliminate let"
   | Tif (f1,t1,t2) ->
-      fprintf fmt "@[(ite %a@ %a@ %a)@]"
+      fprintf fmt "@[itef(%a@, %a@, %a)@]"
         (print_fmla drv) f1 (print_term drv) t1 (print_term drv) t2
   | Tcase _ -> unsupportedTerm t
       "tptp : you must eliminate match"

why.conf

@@ -22,3 +22,7 @@ name = "Z3"
 command = "why-cpulimit %t z3 -smt %f 2>&1"
 driver = "drivers/z3.drv"
 
+[prover spass]
+name = "spass"
+command = "SPASS -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
+driver = "drivers/tptp.drv"