parallel

[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 84de696df9f088f3c0e7cbc4a244e86952355176..96b16bb07b6a66dd674495d750e76075185faae2 100644 (file)
--- 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