From: Alberto Griggio <griggio@fbk.eu>
Date: Sun, 19 Jun 2005 12:42:08 +0000 (+0000)
Subject: limited-resource-strategy implementation (now working!)
X-Git-Tag: INDEXING_NO_PROOFS~112
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad4ab0b27cf44913b82c32f9405a7c87719d77ef;p=helm.git

limited-resource-strategy implementation (now working!)
---

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index aebb04775..c45124338 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -107,18 +107,18 @@ let select env passive (active, _) =
       | (Negative, e)::_ ->
           let symbols = symbols_of_equality e in
           let card = cardinality symbols in
+          let foldfun k v (r1, r2) = 
+            if TermMap.mem k symbols then
+              let c = TermMap.find k symbols in
+              let c1 = abs (c - v) in
+              let c2 = v - c1 in
+              r1 + c2, r2 + c1
+            else
+              r1, r2 + v
+          in
           let f equality (i, e) =
             let common, others =
-              TermMap.fold
-                (fun k v (r1, r2) ->
-                   if TermMap.mem k symbols then
-                     let c = TermMap.find k symbols in
-                     let c1 = abs (c - v) in
-                     let c2 = v - c1 in
-                     r1 + c2, r2 + c1
-                   else
-                     r1, r2 + v)
-                (symbols_of_equality equality) (0, 0)
+              TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
             in
             let c = others + (abs (common - card)) in
             if c < i then (c, equality)
@@ -127,16 +127,7 @@ let select env passive (active, _) =
           let e1 = EqualitySet.min_elt pos_set in
           let initial =
             let common, others = 
-              TermMap.fold
-                (fun k v (r1, r2) ->
-                   if TermMap.mem k symbols then
-                     let c = TermMap.find k symbols in
-                     let c1 = abs (c - v) in
-                     let c2 = v - (abs (c - v)) in
-                     r1 + c1, r2 + c2
-                   else
-                     r1, r2 + v)
-                (symbols_of_equality e1) (0, 0)
+              TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
             in
             (others + (abs (common - card))), e1
           in
@@ -220,26 +211,87 @@ let size_of_passive ((_, ns), (_, ps), _) =
 ;;
 
 
-let prune_passive (((nl, ns), (pl, ps), tbl) as passive) =
-  let f =
-    int_of_float ((!time_limit -. !elapsed_time) /.
-                    (!elapsed_time *. (float_of_int !weight_age_ratio)))
+let prune_passive howmany (active, _) passive =
+  let (nl, ns), (pl, ps), tbl = passive in
+  let howmany = float_of_int howmany
+  and ratio = float_of_int !weight_age_ratio in
+  let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
+  and in_age = int_of_float (howmany /. (ratio +. 1.)) in 
+  Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
+(*   let rec pickw w s = *)
+(*     if w > 0 then  *)
+(*       try *)
+(*         let e = EqualitySet.min_elt s in *)
+(*         let w, s' = pickw (w-1) (EqualitySet.remove e s) in *)
+(*         w, EqualitySet.add e s' *)
+(*       with Not_found -> *)
+(*         w, s *)
+(*     else *)
+(*       0, EqualitySet.empty *)
+(*   in *)
+  let symbols, card =
+    match active with
+    | (Negative, e)::_ ->
+        let symbols = symbols_of_equality e in
+        let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
+        Some symbols, card
+    | _ -> None, 0
   in
-  let in_weight = !processed_clauses * !weight_age_ratio * f
-  and in_age = !processed_clauses * f in
-  let rec pickw w s =
-    if w > 0 then 
-      try
-        let e = EqualitySet.min_elt s in
-        let w, s' = pickw (w-1) (EqualitySet.remove e s) in
-        w, EqualitySet.add e s'
-      with Not_found ->
-        w, s
+  let counter = ref !symbols_ratio in
+  let rec pickw w ns ps =
+    if w > 0 then
+      if not (EqualitySet.is_empty ns) then
+        let e = EqualitySet.min_elt ns in
+        let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
+        EqualitySet.add e ns', ps
+      else if !counter > 0 then
+        let _ =
+          counter := !counter - 1;
+          if !counter = 0 then counter := !symbols_ratio
+        in
+        match symbols with
+        | None ->
+            let e = EqualitySet.min_elt ps in
+            let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+            ns, EqualitySet.add e ps'
+        | Some symbols ->
+            let foldfun k v (r1, r2) =
+              if TermMap.mem k symbols then
+                let c = TermMap.find k symbols in
+                let c1 = abs (c - v) in
+                let c2 = v - c1 in
+                r1 + c2, r2 + c1
+              else
+                r1, r2 + v
+            in
+            let f equality (i, e) =
+              let common, others =
+                TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+              in
+              let c = others + (abs (common - card)) in
+              if c < i then (c, equality)
+              else (i, e)
+            in
+            let e1 = EqualitySet.min_elt ps in
+            let initial =
+              let common, others = 
+                TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+              in
+              (others + (abs (common - card))), e1
+            in
+            let _, e = EqualitySet.fold f ps initial in
+            let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+            ns, EqualitySet.add e ps'
+      else
+        let e = EqualitySet.min_elt ps in
+        let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+        ns, EqualitySet.add e ps'        
     else
-      0, EqualitySet.empty
+      EqualitySet.empty, EqualitySet.empty
   in
-  let in_weight, ns = pickw in_weight ns in
-  let _, ps = pickw in_weight ps in
+(*   let in_weight, ns = pickw in_weight ns in *)
+(*   let _, ps = pickw in_weight ps in *)
+  let ns, ps = pickw in_weight ns ps in
   let rec picka w s l =
     if w > 0 then
       match l with
@@ -567,13 +619,17 @@ let rec given_clause env passive active =
   let selection_estimate = get_selection_estimate () in
   let kept = size_of_passive passive in
   let passive =
-    if !time_limit = 0. then
+    if !time_limit = 0. || !processed_clauses = 0 then
       passive
-    else if !elapsed_time > !time_limit then
+    else if !elapsed_time > !time_limit then (
+      Printf.printf "Time limit (%.2f) reached: %.2f\n"
+        !time_limit !elapsed_time;
       make_passive [] []
-    else if kept > selection_estimate then
-      prune_passive passive
-    else
+    ) else if kept > selection_estimate then (
+      Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
+                       "selection_estimate: %d)\n") kept selection_estimate;
+      prune_passive selection_estimate active passive
+    ) else
       passive
   in
     
@@ -685,6 +741,23 @@ let rec given_clause env passive active =
 
 
 let rec given_clause_fullred env passive active =
+  let selection_estimate = get_selection_estimate () in
+  let kept = size_of_passive passive in
+  let passive =
+    if !time_limit = 0. || !processed_clauses = 0 then
+      passive
+    else if !elapsed_time > !time_limit then (
+      Printf.printf "Time limit (%.2f) reached: %.2f\n"
+        !time_limit !elapsed_time;
+      make_passive [] []
+    ) else if kept > selection_estimate then (
+      Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
+                       "selection_estimate: %d)\n") kept selection_estimate;
+      prune_passive selection_estimate active passive
+    ) else
+      passive
+  in
+    
   match passive_is_empty passive with
   | true -> Failure
   | false ->
@@ -739,6 +812,11 @@ let rec given_clause_fullred env passive active =
                   simplify (nn @ n @ rn, np @ p @ rp) active passive
             in
             let active, passive, new' = simplify new' active passive in
+
+            let k = size_of_passive passive in
+            if k < (kept - 1) then
+              processed_clauses := !processed_clauses + (kept - 1 - k);
+            
             let _ =
               Printf.printf "active:\n%s\n"
                 (String.concat "\n"
@@ -834,10 +912,10 @@ let main () =
         Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
                          "backward_simpl_time: %.9f\n")
           !infer_time !forward_simpl_time !backward_simpl_time;
-        Printf.printf ("forward_simpl_details:\n  build_all: %.9f\n" ^^
-                         "  demodulate: %.9f\n  subsumption: %.9f\n")
-          fs_time_info.build_all fs_time_info.demodulate
-          fs_time_info.subsumption;
+(*         Printf.printf ("forward_simpl_details:\n  build_all: %.9f\n" ^^ *)
+(*                          "  demodulate: %.9f\n  subsumption: %.9f\n") *)
+(*           fs_time_info.build_all fs_time_info.demodulate *)
+(*           fs_time_info.subsumption; *)
     | Success (None, env) ->
         Printf.printf "Success, but no proof?!?\n\n"
   with exc ->