X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUtils.ml;h=7b57e5bb3d2037b98ff681521c3b55d1ecd6a2cc;hb=38ec119c163b0e6f97a9800933d5b71c065332e8;hp=ec76511d97c5c954f9039394a2f008a7146cf4dc;hpb=4ae7d510a430a2a6929f973d36b993d528772d64;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index ec76511d9..7b57e5bb3 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -21,14 +21,9 @@ let rec lexicograph f l1 l2 =
   | _,[] -> 1
 ;;
   
-let mk_id = 
-  let id = ref 0 in
-  fun () -> incr id; !id
-;;
-
-module Utils (B : Terms.Blob) = struct
-  module Subst = FoSubst.Subst(B) ;;
-  module Order = Orderings.Orderings(B) ;;
+module Utils (B : Orderings.Blob) = struct
+  module Subst = FoSubst;; 
+  module Order = B;;
 
   let rec eq_foterm x y =
     x == y ||
@@ -77,15 +72,15 @@ module Utils (B : Terms.Blob) = struct
   let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2
   let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2
     
-  let relocate maxvar varlist =
+  let relocate maxvar varlist subst =
     List.fold_right
       (fun i (maxvar, varlist, s) -> 
          maxvar+1, maxvar::varlist, Subst.build_subst i (Terms.Var maxvar) s)
-      varlist (maxvar+1, [], Subst.id_subst)
+      varlist (maxvar+1, [], subst)
   ;;
 
   let fresh_unit_clause maxvar (id, lit, varlist, proof) =
-    let maxvar, varlist, subst = relocate maxvar varlist in
+    let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in
     let lit = 
       match lit with
       | Terms.Equation (l,r,ty,o) ->
@@ -124,25 +119,24 @@ module Utils (B : Terms.Blob) = struct
       | t -> Terms.Predicate t
     in
     let proof = Terms.Exact proofterm in
-    fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
+    fresh_unit_clause maxvar (0, lit, varlist, proof)
   ;;
 
-  let add_to_bag bag  (_,lit,vl,proof) =
-    let id = mk_id () in
-    let clause = (id, lit, vl, proof) in
-    let bag = Terms.M.add id clause bag in
-    bag, clause 
-   ;;
-    
-  let empty_bag = Terms.M.empty ;;
-
   let mk_passive_clause cl =
     (Order.compute_unit_clause_weight cl, cl)
   ;;
 
-  let compare_passive_clauses (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
+  let mk_passive_goal g =
+    (Order.compute_unit_clause_weight g, g)
+  ;;
+
+  let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
     if w1 = w2 then id1 - id2
     else w1 - w2
   ;;
 
+  let compare_passive_clauses_age (_,(id1,_,_,_)) (_,(id2,_,_,_)) =
+    id1 - id2
+  ;;
+
 end