changed default parameter values...

diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml
index a2a4e1f079e6957bd3074d82ac7813175d07e631..6f1ea3f2b7011017b61a7f3b02241efaae6d9c13 100644 (file)
--- a/helm/ocaml/paramodulation/saturate_main.ml
+++ b/helm/ocaml/paramodulation/saturate_main.ml
@@ -17,7 +17,7 @@ let get_from_user ~(dbd:Mysql.dbd) =
 
 let _ =
   let module S = Saturation in
-  let set_ratio v = S.weight_age_ratio := (v+1); S.weight_age_counter := (v+1)
+  let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v
   and set_sel v = S.symbols_ratio := v; S.symbols_counter := v;
   and set_conf f = configuration_file := f
   and set_ordering o =

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 515060aacdf5d4125c6207e6d640a08d0fdf1427..6d5ecee159a8ba72f0d39b4351af16a044d837eb 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -23,9 +23,9 @@ let maximal_retained_equality = ref None;;
 
 (* equality-selection related globals *)
 let use_fullred = ref true;;
-let weight_age_ratio = ref (* 5 *) 3;; (* settable by the user *)
+let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *)
 let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref (* 0 *) 2;;
+let symbols_ratio = ref (* 0 *) 3;;
 let symbols_counter = ref 0;;
 
 (* non-recursive Knuth-Bendix term ordering by default *)
@@ -282,8 +282,12 @@ 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 
+  let round v =
+    let t = ceil v in 
+    int_of_float (if t -. v < 0.5 then t else v)
+  in
+  let in_weight = round (howmany *. ratio /. (ratio +. 1.))
+  and in_age = round (howmany /. (ratio +. 1.)) in 
   debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
   let symbols, card =
     match active with
@@ -365,7 +369,7 @@ let prune_passive howmany (active, _) passive =
   let _, ps, pl = picka in_age ps pl in
   if not (EqualitySet.is_empty ps) then
 (*     maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
-    maximal_retained_equality := Some (EqualitySet.max_elt ps);
+    maximal_retained_equality := Some (EqualitySet.max_elt ps); 
   let tbl =
     EqualitySet.fold
       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
@@ -412,11 +416,52 @@ let infer env sign current (active_list, active_table) =
   in
   derived_clauses := !derived_clauses + (List.length new_neg) +
     (List.length new_pos);
-  match (* !maximal_weight *)!maximal_retained_equality with
+  match !maximal_retained_equality with
   | None -> new_neg, new_pos
-  | Some (* w *) eq ->
-      let new_pos =
-        List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
+  | Some eq ->
+      (* if we have a maximal_retained_equality, we can discard all equalities
+         "greater" than it, as they will never be reached...  An equality is
+         greater than maximal_retained_equality if it is bigger
+         wrt. OrderedEquality.compare and it is less similar than
+         maximal_retained_equality to the current goal *)
+      let symbols, card =
+        match active_list 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 new_pos = 
+        match symbols with
+        | None ->
+            List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
+        | Some symbols ->
+            let filterfun e =
+              if OrderedEquality.compare e eq <= 0 then
+                true
+              else
+                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 initial =
+                  let common, others =
+                    TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
+                  others + (abs (common - card))
+                in
+                let common, others =
+                  TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
+                let c = others + (abs (common - card)) in
+                if c < initial then true else false 
+            in
+            List.filter filterfun new_pos
+      in
       new_neg, new_pos
 ;;
 
@@ -447,7 +492,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   in
   let all = if pl = [] then active_list else active_list @ pl in
 
-(*   let rec find_duplicate sign current = function *)
+  (*   let rec find_duplicate sign current = function *)
 (*     | [] -> false *)
 (*     | (s, eq)::tl when s = sign -> *)
 (*         if meta_convertibility_eq current eq then true *)