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 8024dbba02e085fb8e730ab21a9cfc2ecc6a8368..1f64314c9df48197d718debd7b937b0de1d3cc6c 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -43,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)
@@ -65,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
   ;;
 
@@ -337,7 +338,7 @@ module Paramod (B : Orderings.Blob) = struct
     let bag = Terms.empty_bag in
     let maxvar = 0 in
     let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
-      let c,maxvar = Utils.mk_clause maxvar nlit plit t in
+      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