X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=bef39f7b22f91b63b87f5936b0c6c5b52aebf14f;hb=a423d321a98c6f31dab56505fe7acf0110df38e8;hp=9e533d8d635bd1c707706eec04107b37afb70e1b;hpb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 9e533d8d6..bef39f7b2 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -54,7 +54,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.nonrec_kbo;; *)
+Utils.compare_terms := Utils.ao;;
 
 (* statistics... *)
 let derived_clauses = ref 0;;
@@ -141,7 +142,7 @@ let select env goals passive (active, _) =
           (* Negatives aren't indexed, no need to remove them... *)
           (Negative, hd),
           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
-      | [], hd::tl ->
+      | [], (hd:EqualitySet.elt)::tl ->
           let passive_table =
             Indexing.remove_index passive_table hd
           in
@@ -220,8 +221,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),
@@ -230,7 +230,7 @@ let make_passive neg pos =
 
 
 let make_active () =
-  [], Indexing.empty_table () 
+  [], Indexing.empty
 ;;
 
 
@@ -363,7 +363,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  
 ;;
@@ -397,7 +397,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
@@ -654,7 +654,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 (
@@ -691,7 +691,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
@@ -705,7 +705,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
@@ -1842,7 +1842,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
@@ -2019,7 +2019,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
@@ -2214,7 +2214,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
@@ -2300,7 +2300,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