Moved ID management inside the bag

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index d3e6000b77781dd88758678eb7d63364f83c7740..96b16bb07b6a66dd674495d750e76075185faae2 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -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
@@ -302,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 ->
@@ -335,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
@@ -573,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