X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=96b16bb07b6a66dd674495d750e76075185faae2;hb=68a557b997805b4a96fb2851cb4d2ab2076bba36;hp=84de696df9f088f3c0e7cbc4a244e86952355176;hpb=94ec1bb0fcb0a82bfaaf965aed6993de3a9e658a;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 84de696df..96b16bb07 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -15,7 +15,7 @@ module Superposition (B : Terms.Blob) =
   struct
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
-    module Subst = FoSubst (*.Subst(B)*)
+    module Subst = FoSubst 
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
@@ -92,7 +92,7 @@ module Superposition (B : Terms.Blob) =
           | t -> Terms.Predicate t
         in
         let bag, uc = 
-          Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
+          Terms.add_to_bag (0, literal, vars_of_term t, proof) bag
         in
         Some (bag, uc)
       else
@@ -133,7 +133,6 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table =
-      (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
@@ -303,7 +302,7 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     let rec orphan_murder bag acc i =
-      match Terms.M.find i bag with
+      match Terms.get_from_bag i bag with
 	| (_,_,_,Terms.Exact _),discarded -> (discarded,acc)
 	| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc)
 	| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false ->
@@ -336,8 +335,8 @@ module Superposition (B : Terms.Blob) =
 
     let simplify table maxvar bag clause =
       match simplify table maxvar bag clause with
-	| bag, None -> let (id,_,_,_) = clause in
-	    Terms.M.add id (clause,true) bag, None
+	| bag, None ->
+	    Terms.replace_in_bag (clause,true) bag, None
 	| bag, Some clause -> bag, Some clause
     (*let (id,_,_,_) = clause in
 	    if orphan_murder bag clause then
@@ -574,7 +573,7 @@ module Superposition (B : Terms.Blob) =
       let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
 	(* We need to put fresh_current into the bag so that all *
 	 * variables clauses refer to are known.                 *)
-      let bag, fresh_current = Utils.add_to_bag bag fresh_current in
+      let bag, fresh_current = Terms.add_to_bag fresh_current bag in
 	(* We superpose current with active clauses *)
       let bag, maxvar, additional_new_clauses =
         superposition_with_table bag maxvar fresh_current atable