Dependency coq.moo.opt added to target tests.opt

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 10d76faa1295522168ceae334cb12b5cd0689f48..eb4a35d6c443f823e2b94438b4c4f13f6cc17549 100644 (file)
--- 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;;
 
@@ -55,6 +57,7 @@ let symbols_counter = ref 0;;
 
 (* non-recursive Knuth-Bendix term ordering by default *)
 Utils.compare_terms := Utils.nonrec_kbo;; 
+(* Utils.compare_terms := Utils.ao;; *)
 
 (* statistics... *)
 let derived_clauses = ref 0;;
@@ -141,7 +144,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 +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),
@@ -230,7 +232,7 @@ let make_passive neg pos =
 
 
 let make_active () =
-  [], Indexing.empty_table () 
+  [], Indexing.empty
 ;;
 
 
@@ -363,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  
 ;;
@@ -397,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
@@ -654,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 (
@@ -691,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
@@ -705,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
@@ -1842,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
@@ -2019,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
@@ -2214,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
@@ -2300,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
@@ -2359,15 +2361,18 @@ let main_demod_equalities dbd term metasenv ugraph =
       match rp with
       | (n, _), (p, _), _ ->
           EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
-      | _ -> assert false
     in
     let active =
       let l = List.map snd (fst ra) in
       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
     in
     Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
-      (String.concat "\n" (List.map (string_of_equality ~env) active))
-      (String.concat "\n" (List.map (string_of_equality ~env) passive));
+(*       (String.concat "\n" (List.map (string_of_equality ~env) active)) *)
+      (String.concat "\n"
+         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active))
+(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
+      (String.concat "\n"
+         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
     print_newline ();
   with e ->
     debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))