1 module OT = struct type t = string let compare = Pervasives.compare end
2 module HC = Map.Make(OT)
4 type leaf = int * string
6 let cache = ref HC.empty
12 cache := HC.add s (!num,s) !cache;
21 let problem_file = ref "no-file-given" in
22 let tptppath = ref "./" in
24 "--tptppath", Arg.String (fun p -> tptppath := p), "[path] TPTP lib root"
25 ] (fun x -> problem_file := x) "matitaprover [problemfile]";
26 let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
27 let goal = match goals with [x] -> x | _ -> assert false in
28 let module B : Terms.Blob with type t = leaf and type input = Ast.term = struct
31 let compare (a,_) (b,_) = Pervasives.compare a b
35 let rec embed m = function
36 | Ast.Variable name ->
37 (try m, List.assoc name m
39 let t = Terms.Var ~-(List.length m) in
41 | Ast.Constant name -> m, Terms.Leaf (hash name)
42 | Ast.Function (name,args) ->
45 (fun x _ m -> embed m x) m args
47 m, Terms.Node (Terms.Leaf (hash name):: args)
50 let vars, ty = embed [] ty in
51 let _, bo = embed vars bo in
52 let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
55 let embed t = snd(embed [] t);;
59 let module P = Paramod.Paramod(B) in
60 let module Pp = Pp.Pp(B) in
61 let bag = Terms.M.empty, 0 in
62 let bag, g_passives = P.mk_goal bag goal in
64 HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses
66 prerr_endline "Order";
67 HC.iter (fun _ (w,x) -> prerr_endline (" " ^ x ^ " is " ^ string_of_int w)) !cache;
68 prerr_endline "Facts";
69 List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives;
71 prerr_endline (" " ^ Pp.pp_unit_clause g_passives);
72 ignore(P.paramod bag ~g_passives:[g_passives] ~passives);