Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertib...

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 48811239bf08a30caaca026a3c97929be3e4e590..1f64314c9df48197d718debd7b937b0de1d3cc6c 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -19,27 +19,22 @@ 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.clause
-    val mk_goal : bag -> input * input -> bag * t Terms.clause
     val paramod :
       useage:bool ->
       max_steps:int ->
+      print_problem:bool ->
       ?timeout:float ->
-      bag -> 
-      g_passives:t Terms.clause list -> 
-      passives:t Terms.clause list -> szsontology
+      t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) -> 
+      (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) 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 
@@ -48,21 +43,22 @@ module Paramod (B : Orderings.Blob) = struct
   exception Stop of szsontology
   type bag = B.t Terms.bag * int
   module Pp = Pp.Pp (B) 
-  module FU = FoUnif.Founif(B) 
+  module FU = FoUnif.FoUnif(B) 
   module IDX = Index.Index(B) 
   module Sup = Superposition.Superposition(B) 
   module Utils = FoUtils.Utils(B) 
   module Order = B
+  module Clauses = Clauses.Clauses(B)
   module WeightOrderedPassives =
       struct
         type t = B.t Terms.passive_clause
-        let compare = Utils.compare_passive_clauses_weight
+        let compare = Clauses.compare_passive_clauses_weight
       end
 
   module AgeOrderedPassives =
       struct
         type t = B.t Terms.passive_clause
-        let compare = Utils.compare_passive_clauses_age
+        let compare = Clauses.compare_passive_clauses_age
       end
   
   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
@@ -70,13 +66,13 @@ module Paramod (B : Orderings.Blob) = struct
 
   let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
     let cl = if no_weight then (0,cl)
-    else Utils.mk_passive_clause cl in
+    else Clauses.mk_passive_clause cl in
     WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   ;;
 
   let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
     let g = if no_weight then (0,g)
-    else Utils.mk_passive_goal g in
+    else Clauses.mk_passive_goal g in
     WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
   ;;
 
@@ -125,16 +121,6 @@ module Paramod (B : Orderings.Blob) = struct
     else WeightPassiveSet.min_elt passives_w
   ;;
 
-  let mk_clause bag maxvar (t,ty) =
-    let (proof,ty) = B.saturate t ty in
-    let c, maxvar = Utils.mk_clause maxvar [] [ty] proof in
-    let bag, c = Terms.add_to_bag c bag in
-    (bag, maxvar), c
-  ;;
-  
-  let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
-  let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
-
   (* TODO : global age over facts and goals (without comparing weights) *)
   let select ~use_age passives g_passives =
     if is_passive_set_empty passives then begin
@@ -347,16 +333,32 @@ module Paramod (B : Orderings.Blob) = struct
         actives passives g_actives g_passives
   ;;
 
-  let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+  let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses =
     let initial_timestamp = Unix.gettimeofday () in
+    let bag = Terms.empty_bag in
+    let maxvar = 0 in
+    let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
+      let c,maxvar = Clauses.mk_clause maxvar nlit plit t in
+      let bag,c = Terms.add_to_bag c bag in
+      (bag,maxvar,c::l)
+    in
+    let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
+    let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+    let goal = match goals with | [g] -> g | _ -> assert false in
     let passives =
-      add_passive_clauses ~no_weight:true passive_empty_set passives
+      add_passive_clauses ~no_weight:true passive_empty_set hypotheses
     in
     let g_passives =
-      add_passive_goals ~no_weight:true passive_empty_set g_passives
+      add_passive_goal ~no_weight:true passive_empty_set goal
     in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
+    if print_problem then begin
+       prerr_endline "Facts:";
+       List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses;
+       prerr_endline "Goal:";
+       prerr_endline (" " ^ Pp.pp_clause goal);
+    end;
     try 
      given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives