From: Alberto Griggio <griggio@fbk.eu>
Date: Wed, 22 Jun 2005 17:57:55 +0000 (+0000)
Subject: reverted to previous version, as it worked better...
X-Git-Tag: INDEXING_NO_PROOFS~98
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04fcadbd9e194847138d97a0a9892a475bc21c88;p=helm.git

reverted to previous version, as it worked better...
---

diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml
index 9470e1bde..b5a2d7274 100644
--- a/helm/ocaml/paramodulation/discrimination_tree.ml
+++ b/helm/ocaml/paramodulation/discrimination_tree.ml
@@ -39,10 +39,9 @@ end
 module PosEqSet = Set.Make(OrderedPosEquality);;
 
 
-module DiscriminationTree = Trie.Make(PSMap);;
+(* module DiscriminationTree = Trie.Make(PSMap);; *)
 
 
-(*
 module DiscriminationTree = struct
   type key = path_string
   type t = Node of PosEqSet.t option * (t PSMap.t)
@@ -92,8 +91,8 @@ module DiscriminationTree = struct
     traverse [] t acc
 
 end
-*)
 
+  
 let string_of_discrimination_tree tree =
   let rec to_string level = function
     | DiscriminationTree.Node (value, map) ->
diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index ddec5f9d4..bbd3c4844 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -3,28 +3,24 @@ type retrieval_mode = Matching | Unification;;
 
 
 let print_candidates mode term res =
-(*   match res with *)
-(*   | [] -> () *)
-(*   | _ -> *)
-      let _ =
-        match mode with
-        | Matching ->
-            Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
-        | Unification ->
-            Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
-      in
-      print_endline
-        (String.concat "\n"
-           (List.map
-              (fun (p, e) ->
-                 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
-                   (Inference.string_of_equality e))
-              res));
-      print_endline "|";
+  let _ =
+    match mode with
+    | Matching ->
+        Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
+    | Unification ->
+        Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
+  in
+  print_endline
+    (String.concat "\n"
+       (List.map
+          (fun (p, e) ->
+             Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+               (Inference.string_of_equality e))
+          res));
+  print_endline "|";
 ;;  
 
 
-(*
 let empty_table () =
   Path_indexing.PSTrie.empty
 ;;
@@ -34,20 +30,16 @@ and remove_index = Path_indexing.remove_index
 and in_index = Path_indexing.in_index;;
   
 let get_candidates mode trie term =
-  let res = 
-    let s = 
-      match mode with
-      | Matching -> Path_indexing.retrieve_generalizations trie term
-      | Unification -> Path_indexing.retrieve_unifiables trie term
-    in
-    Path_indexing.PosEqSet.elements s
+  let s = 
+    match mode with
+    | Matching -> Path_indexing.retrieve_generalizations trie term
+    | Unification -> Path_indexing.retrieve_unifiables trie term
   in
-  print_candidates mode term res;
-  res
+  Path_indexing.PosEqSet.elements s
 ;;
-*)
 
 
+(*
 let empty_table () =
   Discrimination_tree.DiscriminationTree.empty
 ;;
@@ -68,6 +60,7 @@ let get_candidates mode tree term =
 (*   print_candidates mode term res; *)
   res
 ;;
+*)
 
 
 let rec find_matches metasenv context ugraph lift_amount term =
@@ -228,10 +221,10 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  let candidates = get_candidates Matching table term in
   match term with
   | C.Meta _ -> None
   | term ->
-      let candidates = get_candidates Matching table term in
       let res =
         find_matches metasenv context ugraph lift_amount term candidates
       in
@@ -361,6 +354,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  let candidates = get_candidates Unification table term in
   let res, lifted_term = 
     match term with
     | C.Meta (i, l) ->
@@ -447,7 +441,6 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   match term with
   | C.Meta _ -> res, lifted_term
   | term ->
-      let candidates = get_candidates Unification table term in
       let r = 
         find_all_matches metasenv context ugraph lift_amount term candidates
       in
diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml
index 95d6de9f5..bc9bc01f1 100644
--- a/helm/ocaml/paramodulation/path_indexing.ml
+++ b/helm/ocaml/paramodulation/path_indexing.ml
@@ -49,6 +49,8 @@ end
 
 module PSMap = Map.Make(OrderedPathStringElement);;
 
+(* module PSTrie = Trie.Make(PathStringElementMap);; *)
+
 module OrderedPosEquality = struct
   type t = Utils.pos * Inference.equality
 
@@ -57,9 +59,6 @@ end
 
 module PosEqSet = Set.Make(OrderedPosEquality);;
 
-module PSTrie = Trie.Make(PSMap);;
-
-(*
 (*
  * Trie: maps over lists.
  * Copyright (C) 2000 Jean-Christophe FILLIATRE
@@ -112,7 +111,6 @@ module PSTrie = struct
     traverse [] t acc
 
 end
-*)
 
 
 let index trie equality =
diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 634df11ff..b77fe955f 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -324,7 +324,7 @@ let prune_passive howmany (active, _) passive =
           let w, s, l = picka w s tl in
           w, s, hd::l
     else
-      0, s, []
+      0, s, l
   in
   let in_age, ns, nl = picka in_age ns nl in
   let _, ps, pl = picka in_age ps pl in
@@ -662,6 +662,7 @@ let backward_simplify env new' ?passive active =
 
 let get_selection_estimate () =
   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
+(*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
   int_of_float (
     ceil ((float_of_int !processed_clauses) *.
             (!time_limit /. !elapsed_time -. 1.)))