+ prerr_endline (" " ^ pp g_passives)
+*)
+;;
+
+module Main(C:LeafComparer) = struct
+ let main goal hypotheses =
+ let module B = MakeBlob(C) in
+ let module Pp = Pp.Pp(B) in
+ let module P = Paramod.Paramod(B) in
+ let bag = Terms.M.empty, 0 in
+ let bag, g_passives = P.mk_goal bag goal in
+ let bag, passives =
+ HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses
+ in
+ start_msg passives g_passives Pp.pp_unit_clause;
+ match
+ P.paramod
+ ~max_steps:max_int bag ~g_passives:[g_passives] ~passives
+ with
+ | [] -> ()
+ | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause
+ ;;
+end
+
+let killall l =
+ List.iter (fun pid -> try Unix.kill pid 9 with _ -> ()) l
+;;
+
+let main () =
+ let childs = ref [] in
+ let _ =
+ Sys.signal 24 (Sys.Signal_handle
+ (fun _ -> fail_msg (); killall !childs; exit 1))
+ in
+ let _ =
+ Sys.signal Sys.sigalrm
+ (Sys.Signal_handle (fun _ -> fail_msg (); killall !childs; exit 1))
+ in
+ Arg.parse [
+ "--tptppath", Arg.String (fun p -> tptppath := p),
+ ("[path] TPTP lib root, default " ^ !tptppath);
+ "--timeout", Arg.Int (fun p -> seconds := p),
+ ("[seconds] timeout, default " ^ string_of_int !seconds);
+ ] (fun x -> problem_file := x) "
+Matitaprover is the first order automatic prover that equips the
+Matita interactive theorem prover (http://matita.cs.unibo.it).
+
+Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1
+
+If --tptppath is given, instead of the problem file you can just give the
+problem name with the .p suffix (e.g. BOO001-1.p)
+
+If --tptppath is not given, included files (i.e. axiom sets) are searched
+in the current directory only.
+
+usage: matitaprover [options] problemfile";
+ let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
+ let goal = match goals with [x] -> x | _ -> assert false in