X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=eb4a35d6c443f823e2b94438b4c4f13f6cc17549;hb=f7aedf0ebd0fb55d3587db4f0753521927dcbb69;hp=2e7f1f21a82c8ff0a2117314872d6a18a1e9c96d;hpb=b52f57d8573a909a486d52a7317e017f56d07199;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 2e7f1f21a..eb4a35d6c 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Inference;;
 open Utils;;
 
@@ -54,8 +56,8 @@ let symbols_ratio = ref (* 0 *) 3;;
 let symbols_counter = ref 0;;
 
 (* non-recursive Knuth-Bendix term ordering by default *)
-(* Utils.compare_terms := Utils.nonrec_kbo;; *)
-Utils.compare_terms := Utils.ao;;
+Utils.compare_terms := Utils.nonrec_kbo;; 
+(* Utils.compare_terms := Utils.ao;; *)
 
 (* statistics... *)
 let derived_clauses = ref 0;;
@@ -221,8 +223,7 @@ let make_passive neg pos =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
   in
   let table =
-      List.fold_left (fun tbl e -> Indexing.index tbl e)
-        (Indexing.empty_table ()) pos
+      List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos
   in
   (neg, set_of neg),
   (pos, set_of pos),
@@ -231,7 +232,7 @@ let make_passive neg pos =
 
 
 let make_active () =
-  [], Indexing.empty_table () 
+  [], Indexing.empty
 ;;
 
 
@@ -364,7 +365,7 @@ let prune_passive howmany (active, _) passive =
     maximal_retained_equality := Some (EqualitySet.max_elt ps); 
   let tbl =
     EqualitySet.fold
-      (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+      (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
   in
   (nl, ns), (pl, ps), tbl  
 ;;
@@ -398,7 +399,7 @@ let infer env sign current (active_list, active_table) =
               let neg, pos = infer_positive table tl in
               neg, res @ pos
         in
-        let curr_table = Indexing.index (Indexing.empty_table ()) current in
+        let curr_table = Indexing.index Indexing.empty current in
         let neg, pos = infer_positive curr_table active_list in
         neg, res @ pos
   in
@@ -655,7 +656,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
          ) 
          else
            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
-      active_list ([], Indexing.empty_table ()),
+      active_list ([], Indexing.empty),
     List.fold_right
       (fun (s, eq) (n, p) ->
          if (s <> Negative) && (is_identity env eq) then (
@@ -692,7 +693,7 @@ let backward_simplify_passive env new_pos new_table min_weight passive =
   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
   let passive_table =
     List.fold_left
-      (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
+      (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
   in
   match newn, newp with
   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
@@ -706,7 +707,7 @@ let backward_simplify env new' ?passive active =
       (fun (l, t, w) e ->
          let ew, _, _, _, _ = e in
          (Positive, e)::l, Indexing.index t e, min ew w)
-      ([], Indexing.empty_table (), 1000000) (snd new')
+      ([], Indexing.empty, 1000000) (snd new')
   in
   let active, newa =
     backward_simplify_active env new_pos new_table min_weight active in
@@ -1843,7 +1844,7 @@ let main dbd full term metasenv ugraph =
         let tbl =
           List.fold_left
             (fun t (_, e) -> Indexing.index t e)
-            (Indexing.empty_table ()) active
+             Indexing.empty active
         in
         let res = forward_simplify env e (active, tbl) in
         match others with
@@ -2020,7 +2021,7 @@ let saturate
         let tbl =
           List.fold_left
             (fun t (_, e) -> Indexing.index t e)
-            (Indexing.empty_table ()) active
+             Indexing.empty active
         in
         let res = forward_simplify env e (active, tbl) in
         match others with
@@ -2215,7 +2216,7 @@ let retrieve_and_print dbd term metasenv ugraph =
           let tbl =
             List.fold_left
               (fun t (_, e) -> Indexing.index t e)
-              (Indexing.empty_table ()) active
+              Indexing.empty active
           in
           let res = forward_simplify env (Positive, e) (active, tbl) in
             match others with
@@ -2301,7 +2302,7 @@ let main_demod_equalities dbd term metasenv ugraph =
         let tbl =
           List.fold_left
             (fun t (_, e) -> Indexing.index t e)
-            (Indexing.empty_table ()) active
+            Indexing.empty active
         in
         let res = forward_simplify env e (active, tbl) in
         match others with