Changed the type of compute-equality_weight that now takes also

in input the ordering

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 83dc1b180126d71f4ffce95640ee6dc92adf540f..bbc60562089780ec0c0956bca1ba768e8676b71a 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -589,9 +589,10 @@ let rec demodulation_equality ?from newmeta env table sign target =
   (* first, we simplify *)
   let right = U.guarded_simpl context right in
   let left = U.guarded_simpl context left in
-  let w = Utils.compute_equality_weight eq_ty left right in
   let order = !Utils.compare_terms left right in
-  let target = w, proof, (eq_ty, left, right, order), metas, args in
+  let stat = (eq_ty, left, right, order) in 
+  let w = Utils.compute_equality_weight stat in
+  let target = w, proof, stat, metas, args in
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -691,11 +692,12 @@ let rec demodulation_equality ?from newmeta env table sign target =
     in
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
+    let stat = (eq_ty, left, right, ordering) in
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
-      let w = Utils.compute_equality_weight eq_ty left right in
-      (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in
+      let w = Utils.compute_equality_weight stat in
+      (w, newproof, stat,newmenv,args) in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
@@ -945,12 +947,13 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
     let neworder = !Utils.compare_terms left right in
+    let stat = (eq_ty, left, right, neworder) in
     let newmenv = (* Inference.filter s *) menv in  
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
-    let w = Utils.compute_equality_weight eq_ty left right in
-    (w, newproof, (eq_ty, left, right, neworder), newmenv, []) 
+    let w = Utils.compute_equality_weight stat in
+    (w, newproof, stat, newmenv, []) 
 
   in
   !maxmeta, List.map build_new expansions
@@ -1028,9 +1031,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let neworder = !Utils.compare_terms left right in
       let newmenv = (* Inference.filter s *) m in
       let newargs = args @ args' in
+      let stat = (eq_ty, left, right, neworder) in
       let eq' =
-        let w = Utils.compute_equality_weight eq_ty left right in
-        (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
+        let w = Utils.compute_equality_weight stat in
+        (w, newproof, stat, newmenv, newargs) in
       if Utils.debug_metas then 
        ignore (check_target context eq' "buildnew3");
       let newm, eq' = Inference.fix_metas !maxmeta eq' in

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index fdaf68018ee5971516f1be9700ae497cf6bafe4c..07d95ef866aa0ba5c88e6d94e3b8bbebcaafa52c 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -698,9 +698,10 @@ let find_equalities context proof =
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
-                    let w = compute_equality_weight ty t1 t2 in
+                    let stat = (ty,t1,t2,o) in
+                    let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+                    let e = (w, proof, stat, newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -710,8 +711,9 @@ let find_equalities context proof =
               let t1 = S.lift index t1 in
               let t2 = S.lift index t2 in
               let o = !Utils.compare_terms t1 t2 in
-              let w = compute_equality_weight ty t1 t2 in
-              let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
+              let stat = (ty,t1,t2,o) in
+              let w = compute_equality_weight stat in
+              let e = (w, BasicProof (C.Rel index), stat, [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -846,17 +848,19 @@ let find_library_equalities dbd context status maxmeta =
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
-                    let w = compute_equality_weight ty t1 t2 in
+                    let stat = (ty,t1,t2,o) in
+                    let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+                    let e = (w, proof, stat, newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
               when iseq uri && not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
-              let w = compute_equality_weight ty t1 t2 in
-              let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+              let stat = (ty,t1,t2,o) in
+              let w = compute_equality_weight stat in
+              let e = (w, BasicProof term, stat, [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1115,8 +1119,9 @@ let equality_of_term proof term =
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
       let o = !Utils.compare_terms t1 t2 in
-      let w = compute_equality_weight ty t1 t2 in
-      let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
+      let stat = (ty,t1,t2,o) in
+      let w = compute_equality_weight stat in
+      let e = (w, BasicProof proof, stat, [], []) in
       e
   | _ ->
       raise TermIsNotAnEquality

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 9bc9d2464421e136230468ea7cc09b23addc3916..654195c06360bd16ee0d274a3d5425bc1723774b 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -70,7 +70,7 @@ let maximal_retained_equality = ref None;;
 
 (* equality-selection related globals *)
 let use_fullred = ref true;;
-let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *)
+let weight_age_ratio = ref 5 (* 5 *);; (* settable by the user *)
 let weight_age_counter = ref !weight_age_ratio ;;
 let symbols_ratio = ref 0 (* 3 *);;
 let symbols_counter = ref 0;;
@@ -260,10 +260,10 @@ let rec select env goals passive (active, _) =
     )
   | _ ->
       symbols_counter := !symbols_ratio;
-      (* let set_selection set = EqualitySet.min_elt set in *)
-      let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in 
+      let set_selection set = EqualitySet.min_elt set in 
+      (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *)
       if EqualitySet.is_empty neg_set then
-        let current = set_selection pos_list in
+        let current = set_selection pos_set in
         let passive =
           (neg_list, neg_set),
           (remove current pos_list, EqualitySet.remove current pos_set),
@@ -271,7 +271,7 @@ let rec select env goals passive (active, _) =
         in
         (Positive, current), passive
       else
-        let current = set_selection neg_list in
+        let current = set_selection neg_set in
         let passive =
           (remove current neg_list, EqualitySet.remove current neg_set),
           (pos_list, pos_set),

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 84de8800e7c8de566ff7e93cd0d7bec23c0fea9d..babf684bf97ea27a42c4623603960565fee5d4be 100644 (file)
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -292,17 +292,18 @@ end
 
 module IntSet = Set.Make(OrderedInt)
 
-let compute_equality_weight ty left right =
+let compute_equality_weight (ty,left,right,o) =
   let metasw = ref 0 in
   let weight_of t =
     let w, m = (weight_of_term 
                  ~consider_metas:true ~count_metas_occurrences:false t) in
-    metasw := !metasw + (2 * (List.length m)) ;
+    metasw := !metasw + (1 * (List.length m)) ;
     w
   in
   (* Warning: the following let cannot be expanded since it forces the
      right evaluation order!!!! *)
-  let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+  let w = (weight_of ty) + (weight_of left) + (weight_of right) in 
+  (* let w = weight_of (Cic.Appl [ty;left;right]) in *)
   w + !metasw
 ;;
 

diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli
index 9dc6501d796d296d4797d67704b924f5778da45a..bef03b1415538e577a197d1843c509a8d1f23be9 100644 (file)
--- a/components/tactics/paramodulation/utils.mli
+++ b/components/tactics/paramodulation/utils.mli
@@ -81,7 +81,7 @@ type pos = Left | Right
 
 val string_of_pos: pos -> string
 
-val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
+val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int
 
 val debug_print: string Lazy.t -> unit