From 72aa8b2087285826b14fc39a389632f0317c51b6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 13 Jul 2009 08:56:24 +0000 Subject: [PATCH] matitaprover is now flexible enough to allow the computation of statistics on the clauses and then choose an ordering to be used for the proof search --- .../binaries/matitaprover/matitaprover.ml | 67 +++++++++++++------ .../components/ng_paramodulation/paramod.ml | 22 ++++++ .../components/ng_paramodulation/paramod.mli | 21 +++--- 3 files changed, 81 insertions(+), 29 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 1c837f18d..f516552bc 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -79,6 +79,8 @@ module MakeBlob(C:LeafComparer) : Terms.Blob ;; let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord = + (* TODO: do some sort of poor man lock (open + OEXCL) so that + * just one thread at a time prints the proof *) print_endline ("% SZS status Unsatisfiable for " ^ Filename.basename !problem_file); print_endline ("% SZS output start CNFRefutation for " ^ @@ -110,24 +112,16 @@ let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) oname let report_error s = prerr_endline (string_of_int (Unix.getpid())^": "^s);; -module Main(C:Orderings.Blob with type t = leaf) = struct - let main goal hypotheses = - let module B = C in - let module Pp = Pp.Pp(B) in - let module P = Paramod.Paramod(B) in - let bag = Terms.empty_bag, 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 C.name; +module Main(P : Paramod.Paramod with type t = leaf) = struct + + let run bag g_passives passives pp_unit_clause name = match P.paramod ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with | P.Error s -> report_error s; 3 | P.Unsatisfiable ((bag,_,l)::_) -> - success_msg bag l Pp.pp_unit_clause C.name; 0 + success_msg bag l pp_unit_clause name; 0 | P.Unsatisfiable ([]) -> report_error "Unsatisfiable but no solution output"; 3 | P.GaveUp -> 2 @@ -135,6 +129,43 @@ module Main(C:Orderings.Blob with type t = leaf) = struct ;; end +let worker order goal hypotheses = + let module C = + struct type t = leaf let cmp (a,_) (b,_) = Pervasives.compare a b end + in + let module B = MakeBlob(C) in + let module Pp = Pp.Pp(B) in + let module O = Orderings.NRKBO(B) in (* just for processing the clauses *) + let module P = Paramod.Paramod(O) in + let bag = Terms.empty_bag, 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 + (* TODO: do stats analysys there and generate a new + * C and then B + * TODO: rebuild clauses, since the ordering has to + * change after the stats are computed *) + let module C = C in + let module B = MakeBlob(C) in + match order with + | `NRKBO -> + let module O = Orderings.NRKBO(B) in + let module Main = Main(Paramod.Paramod(O)) in + start_msg passives g_passives Pp.pp_unit_clause O.name; + Main.run bag g_passives passives Pp.pp_unit_clause O.name + | `KBO -> + let module O = Orderings.KBO(B) in + let module Main = Main(Paramod.Paramod(O)) in + start_msg passives g_passives Pp.pp_unit_clause O.name; + Main.run bag g_passives passives Pp.pp_unit_clause O.name + | `LPO -> + let module O = Orderings.LPO(B) in + let module Main = Main(Paramod.Paramod(O)) in + start_msg passives g_passives Pp.pp_unit_clause O.name; + Main.run bag g_passives passives Pp.pp_unit_clause O.name +;; + let print_status p = let print_endline s = prerr_endline (string_of_int p ^ ": " ^ s) in function @@ -197,17 +228,11 @@ usage: matitaprover [options] problemfile"; let pid = Unix.fork () in if pid = 0 then (exit (f ())) else pid) [ - (fun () -> - let module M = Main(Orderings.NRKBO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in - M.main goal hypotheses) + (fun () -> worker `NRKBO goal hypotheses) ; - (fun () -> - let module M = Main(Orderings.KBO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in - M.main goal hypotheses) + (fun () -> worker `KBO goal hypotheses) ; - (fun () -> - let module M = Main(Orderings.LPO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in - M.main goal hypotheses) + (fun () -> worker `LPO goal hypotheses) ]; let rec aux () = if List.length !childs = 0 then diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 1cdb9eb5c..f3afc16f4 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -16,7 +16,29 @@ let debug _ = ();; let monster = 100;; +module type Paramod = + sig + type t + type input + type szsontology = + | Unsatisfiable of (t Terms.bag * int * int list) list + | GaveUp + | Error of string + | Timeout of int * t Terms.bag + type bag = t Terms.bag * int + val mk_passive : bag -> input * input -> bag * t Terms.unit_clause + val mk_goal : bag -> input * input -> bag * t Terms.unit_clause + val paramod : + max_steps:int -> + ?timeout:float -> + bag -> + g_passives:t Terms.unit_clause list -> + passives:t Terms.unit_clause list -> szsontology + end + module Paramod (B : Orderings.Blob) = struct + type t = B.t + type input = B.input type szsontology = | Unsatisfiable of (B.t Terms.bag * int * int list) list | GaveUp diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 13fe56fc5..e133036af 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -11,20 +11,25 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -module Paramod ( B : Orderings.Blob ) : +module type Paramod = sig + type t + type input type szsontology = - | Unsatisfiable of (B.t Terms.bag * int * int list) list + | Unsatisfiable of (t Terms.bag * int * int list) list | GaveUp | Error of string - | Timeout of int * B.t Terms.bag - type bag = B.t Terms.bag * int - val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause - val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause + | Timeout of int * t Terms.bag + type bag = t Terms.bag * int + val mk_passive : bag -> input * input -> bag * t Terms.unit_clause + val mk_goal : bag -> input * input -> bag * t Terms.unit_clause val paramod : max_steps:int -> ?timeout:float -> bag -> - g_passives:B.t Terms.unit_clause list -> - passives:B.t Terms.unit_clause list -> szsontology + g_passives:t Terms.unit_clause list -> + passives:t Terms.unit_clause list -> szsontology end + +module Paramod ( B : Orderings.Blob ) : Paramod +with type t = B.t and type input = B.input -- 2.39.2