From e61d023695578ebf09d487480e6e7cac3a2dd2ee Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Fri, 1 Jul 2005 19:08:05 +0000
Subject: [PATCH] fixed bug in proof generation, new weight function to sort
 equalities, which gives a huge speedup

---
 .../paramodulation/discrimination_tree.ml     |   6 +-
 helm/ocaml/paramodulation/indexing.ml         | 113 ++++++++++++------
 helm/ocaml/paramodulation/inference.ml        |  75 +++++-------
 helm/ocaml/paramodulation/inference.mli       |  13 +-
 helm/ocaml/paramodulation/path_indexing.ml    |   6 +-
 helm/ocaml/paramodulation/saturation.ml       |  39 +++---
 helm/ocaml/paramodulation/utils.ml            |  11 +-
 7 files changed, 138 insertions(+), 125 deletions(-)

diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml
index 443c5c63b..254a42332 100644
--- a/helm/ocaml/paramodulation/discrimination_tree.ml
+++ b/helm/ocaml/paramodulation/discrimination_tree.ml
@@ -126,7 +126,7 @@ let string_of_discrimination_tree tree =
 
 
 let index tree equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_string_of_term l
   and psr = path_string_of_term r in
   let index pos tree ps =
@@ -146,7 +146,7 @@ let index tree equality =
 
 
 let remove_index tree equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_string_of_term l
   and psr = path_string_of_term r in
   let remove_index pos tree ps =
@@ -170,7 +170,7 @@ let remove_index tree equality =
 
 
 let in_index tree equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_string_of_term l
   and psr = path_string_of_term r in
   let meta_convertibility = Inference.meta_convertibility_eq equality in
diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index c50d809ac..bd9091e4c 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -143,7 +143,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
   function
     | [] -> None
     | candidate::tl ->
-        let pos, (proof, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
         let do_match c other eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -200,7 +200,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   function
     | [] -> []
     | candidate::tl ->
-        let pos, (proof, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
         let do_match c other eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -277,7 +277,7 @@ let subsumption env table target =
         find_all_matches ~unif_fun:Inference.matching
           metasenv context ugraph 0 left leftc
   in
-  let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) =
+  let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
     try
       let other = if pos = Utils.Left then r else l in
       let subst', menv', ug' =
@@ -377,27 +377,41 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
 
 let build_newtarget_time = ref 0.;;
 
+
+let demod_counter = ref 1;;
+
 let rec demodulation newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let metasenv, context, ugraph = env in
-  let proof, (eq_ty, left, right, order), metas, args = target in
+  let _, proof, (eq_ty, left, right, order), metas, args = target in
   let metasenv' = metasenv @ metas in
   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
     let time1 = Unix.gettimeofday () in
     
-    let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
       let bo = (* M. *)apply_subst subst (S.subst other t) in
-      let bo'' =
-        C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
-                 S.lift 1 eq_ty] @
-                 if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
+      let t' =
+        let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
+        incr demod_counter;
+        let l, r = if is_left then bo, right else left, bo in
+        (name, ty, eq_ty, l, r)
       in
-      let t' = C.Lambda (C.Anonymous, ty, bo'') in
+(*       let bo'' = *)
+(*         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []); *)
+(*                  S.lift 1 eq_ty] @ *)
+(*                  if is_left then [S.lift 1 bo; S.lift 1 right] *)
+(*                  else [S.lift 1 left; S.lift 1 bo]) *)
+(*       in *)
+(*       let t' = *)
+(*         let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *)
+(*         incr demod_counter; *)
+(*         C.Lambda (name, ty, bo'') *)
+(*       in *)
       bo,
       Inference.ProofBlock (subst, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
@@ -420,9 +434,8 @@ let rec demodulation newmeta env table target =
 
     let res =
       let w = Utils.compute_equality_weight eq_ty left right in
-      (w, (eq_ty, left, right, ordering), newmetasenv, newargs)
+      (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
     in
-    Inference.store_proof res newproof;
     newmeta, res
   in
 (*   let build_newtarget = *)
@@ -430,11 +443,11 @@ let rec demodulation newmeta env table target =
 (*     (fun a b -> profile (build_newtarget a) b) *)
 (*   in *)
   let res = demodulate_term metasenv' context ugraph table 0 left in
-  let build_identity (p, (t, l, r, o), m, a) =
-    match o with
-    | Utils.Gt -> (p, (t, r, r, Utils.Eq), m, a)
-    | _ -> (p, (t, l, l, Utils.Eq), m, a)
-  in
+(*   let build_identity (w, p, (t, l, r, o), m, a) = *)
+(*     match o with *)
+(*     | Utils.Gt -> (w, p, (t, r, r, Utils.Eq), m, a) *)
+(*     | _ -> (w, p, (t, l, l, Utils.Eq), m, a) *)
+(*   in *)
   match res with
   | Some t ->
       let newmeta, newtarget = build_newtarget true t in
@@ -563,6 +576,8 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
 ;;
 
 
+let sup_l_counter = ref 1;;
+
 let superposition_left (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -570,7 +585,7 @@ let superposition_left (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let proof, (eq_ty, left, right, ordering), _, _ = target in
+  let _, proof, (eq_ty, left, right, ordering), _, _ = target in
   let expansions, _ =
     let term = if ordering = U.Gt then left else right in
     betaexpand_term metasenv context ugraph table 0 term
@@ -578,18 +593,28 @@ let superposition_left (metasenv, context, ugraph) table target =
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
     let time1 = Unix.gettimeofday () in
     
-    let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' = (* M. *)apply_subst s (S.subst other bo) in
-      let bo'' =
-        C.Appl (
-          [C.MutInd (HL.Logic.eq_URI, 0, []);
-           S.lift 1 eq_ty] @
-            if ordering = U.Gt then [bo'; S.lift 1 right]
-            else [S.lift 1 left; bo'])
+      let t' =
+        let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
+        incr sup_l_counter;
+        let l, r = if ordering = U.Gt then bo', right else left, bo' in
+        (name, ty, eq_ty, l, r)
       in
-      let t' = C.Lambda (C.Anonymous, ty, bo'') in
+(*       let bo'' = *)
+(*         C.Appl ( *)
+(*           [C.MutInd (HL.Logic.eq_URI, 0, []); *)
+(*            S.lift 1 eq_ty] @ *)
+(*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
+(*             else [S.lift 1 left; S.lift 1 bo']) *)
+(*       in *)
+(*       let t' = *)
+(*         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
+(*         incr sup_l_counter; *)
+(*         C.Lambda (name, ty, bo'') *)
+(*       in *)
       bo',
       Inference.ProofBlock (s, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst s *)
@@ -605,9 +630,8 @@ let superposition_left (metasenv, context, ugraph) table target =
 
     let res =
       let w = Utils.compute_equality_weight eq_ty left right in
-      (w, (eq_ty, left, right, neworder), [], [])
+      (w, newproof, (eq_ty, left, right, neworder), [], [])
     in
-    Inference.store_proof res newproof;
     res
   in
 (*   let build_new = *)
@@ -618,6 +642,8 @@ let superposition_left (metasenv, context, ugraph) table target =
 ;;
 
 
+let sup_r_counter = ref 1;;
+
 let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -625,7 +651,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
+  let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
   let metasenv' = metasenv @ newmetas in
   let maxmeta = ref newmeta in
   let res1, res2 =
@@ -647,17 +673,27 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 
     let time1 = Unix.gettimeofday () in
     
-    let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' = (* M. *)apply_subst s (S.subst other bo) in
-      let bo'' =
-        C.Appl (
-          [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
-            if ordering = U.Gt then [bo'; S.lift 1 right]
-            else [S.lift 1 left; bo'])
+      let t' =
+        let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
+        incr sup_r_counter;
+        let l, r = if ordering = U.Gt then bo', right else left, bo' in
+        (name, ty, eq_ty, l, r)
       in
-      let t' = C.Lambda (C.Anonymous, ty, bo'') in
+(*       let bo'' = *)
+(*         C.Appl ( *)
+(*           [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ *)
+(*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
+(*             else [S.lift 1 left; S.lift 1 bo']) *)
+(*       in *)
+(*       let t' = *)
+(*         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in *)
+(*         incr sup_r_counter; *)
+(*         C.Lambda (name, ty, bo'') *)
+(*       in *)
       bo',
       Inference.ProofBlock (s, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst s *)
@@ -673,7 +709,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       and newargs = args @ args' in
       let eq' =
         let w = Utils.compute_equality_weight eq_ty left right in
-        (w, (eq_ty, left, right, neworder), newmenv, newargs)
+        (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
       and env = (metasenv, context, ugraph) in
       let newm, eq' = Inference.fix_metas !maxmeta eq' in
       newm, eq'
@@ -683,7 +719,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
-    Inference.store_proof newequality newproof;
     newequality
   in
 
@@ -695,7 +730,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
   let ok = function
-    | _, (_, left, right, _), _, _ ->
+    | _, _, (_, left, right, _), _, _ ->
         not (fst (CR.are_convertible context left right ugraph))
   in
   (!maxmeta,
diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index f5233d03d..fad86a854 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -3,20 +3,21 @@ open Utils;;
 
 type equality =
     int  *               (* weight *)
+    proof * 
     (Cic.term *          (* type *)
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
     Cic.metasenv *       (* environment for metas *)
     Cic.term list        (* arguments *)
-;;
-
 
-type proof =
+and proof =
   | BasicProof of Cic.term
   | ProofBlock of
-      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
-        equality
+      Cic.substitution * UriManager.uri *
+        (* name, ty, eq_ty, left, right *)
+        (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * 
+        (Utils.pos * equality) * equality
   | NoProof
 ;;
 
@@ -25,40 +26,25 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | _, (ty, left, right, o), _, _ ->
-            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+        | w, _, (ty, left, right, o), _, _ ->
+            Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
     )
   | Some (_, context, _) -> (
       let names = names_of_context context in
       function
-        | _, (ty, left, right, o), _, _ ->
-            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+        | w, _, (ty, left, right, o), _, _ ->
+            Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
               (CicPp.pp left names) (string_of_comparison o)
               (CicPp.pp right names)
     )
 ;;
 
 
-let prooftable = Hashtbl.create 2001;;
-
-let store_proof equality proof =
-  if not (Hashtbl.mem prooftable equality) then
-    Hashtbl.add prooftable equality proof
-;;
-
-
-let delete_proof equality =
-(*   Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
-(*   print_newline (); *)
-  Hashtbl.remove prooftable equality
-;;
-
-
 let rec build_term_proof equality =
 (*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
 (*   print_newline (); *)
-  let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
+  let _, proof, _, _, _ = equality in
   match proof with
   | NoProof ->
       Printf.fprintf stderr "WARNING: no proof for %s\n"
@@ -66,12 +52,18 @@ let rec build_term_proof equality =
       Cic.Implicit None
   | BasicProof term -> term
   | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+      let name, ty, eq_ty, left, right = t' in
+      let bo =
+        Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+                  eq_ty; left; right]
+      in
+      let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in
 (*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
 (*         (string_of_equality eq) (string_of_equality eq'); *)
 (*       print_newline (); *)
       let proof' = build_term_proof eq in
       let eqproof = build_term_proof eq' in
-      let _, (ty, what, other, _), menv', args' = eq in
+      let _, _, (ty, what, other, _), menv', args' = eq in
       let what, other = if pos = Utils.Left then what, other else other, what in
       CicMetaSubst.apply_subst subst
         (Cic.Appl [Cic.Const (eq_URI, []); ty;
@@ -220,8 +212,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, (ty, left, right, _), _, _ = eq1
-  and _, (ty', left', right', _), _, _ = eq2 in
+  let _, _, (ty, left, right, _), _, _ = eq1
+  and _, _, (ty', left', right', _), _, _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -1027,8 +1019,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
-                    let e = (w, (ty, t1, t2, o), newmetas, args) in
-                    store_proof e (BasicProof p);
+                    let proof = BasicProof p in
+                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -1037,8 +1029,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
               and 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, (ty, t1, t2, o), [], []) in
-              store_proof e (BasicProof (C.Rel index));
+              let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -1056,7 +1047,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 ;;
 
 
-let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
   let table = Hashtbl.create (List.length args) in
   let newargs, _ =
     List.fold_right
@@ -1092,7 +1083,7 @@ let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
   (newmeta + (List.length newargs) + 1,
-   (weight, (ty, left, right, o), menv', newargs))
+   (w, p, (ty, left, right, o), menv', newargs))
 ;;
 
 
@@ -1102,8 +1093,7 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
       let o = !Utils.compare_terms t1 t2 in
       let w = compute_equality_weight ty t1 t2 in
-      let e = (w, (ty, t1, t2, o), [], []) in
-      store_proof e (BasicProof proof);
+      let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
       e
 (*       (proof, (ty, t1, t2, o), [], []) *)
   | _ ->
@@ -1320,16 +1310,9 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
 
 
 let is_identity ((_, context, ugraph) as env) = function
-  | ((_, (ty, left, right, _), _, _) as equality) ->
-      let res =
-        (left = right ||
-            (fst (CicReduction.are_convertible context left right ugraph)))
-      in
-(*       if res then ( *)
-(*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(*         print_newline (); *)
-(*       ); *)
-      res
+  | ((_, _, (ty, left, right, _), _, _) as equality) ->
+      (left = right ||
+          (fst (CicReduction.are_convertible context left right ugraph)))
 ;;
 
 
diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index aa2b9231d..0ce2e40a6 100644
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -1,5 +1,6 @@
 type equality =
     int *                (* weight *)
+    proof * 
     (Cic.term *          (* type *)
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
@@ -7,11 +8,13 @@ type equality =
     Cic.metasenv *       (* environment for metas *)
     Cic.term list        (* arguments *)
 
-type proof =
+and proof =
   | BasicProof of Cic.term
   | ProofBlock of
-      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
-        equality
+      Cic.substitution * UriManager.uri *
+        (* name, ty, eq_ty, left, right *)
+        (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * 
+        (Utils.pos * equality) * equality
   | NoProof
 
 
@@ -96,8 +99,4 @@ val extract_differing_subterms:
   Cic.term -> Cic.term -> (Cic.term * Cic.term) option
 
 
-val store_proof: equality -> proof -> unit
-
-val delete_proof: equality -> unit
-
 val build_term_proof: equality -> Cic.term
diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml
index 9212f0ac8..72120c7f7 100644
--- a/helm/ocaml/paramodulation/path_indexing.ml
+++ b/helm/ocaml/paramodulation/path_indexing.ml
@@ -117,7 +117,7 @@ end
 
 
 let index trie equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_strings_of_term 0 l
   and psr = path_strings_of_term 0 r in
   let index pos trie ps =
@@ -138,7 +138,7 @@ let index trie equality =
       
 
 let remove_index trie equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_strings_of_term 0 l
   and psr = path_strings_of_term 0 r in
   let remove_index pos trie ps =
@@ -164,7 +164,7 @@ let remove_index trie equality =
 
 
 let in_index trie equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_strings_of_term 0 l
   and psr = path_strings_of_term 0 r in
   let meta_convertibility = Inference.meta_convertibility_eq equality in
diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 877e5929a..c933aec0b 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -44,7 +44,7 @@ let symbols_of_equality (_, (_, left, right), _, _) =
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -71,8 +71,8 @@ module OrderedEquality = struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let w1, (ty, left, right, _), _, a = eq1
-        and w2, (ty', left', right', _), _, a' = eq2 in
+        let w1, _, (ty, left, right, _), _, a = eq1
+        and w2, _, (ty', left', right', _), _, a' = eq2 in
 (*         let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
 (*         let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
 (*         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
@@ -414,7 +414,7 @@ let contains_empty env (negative, positive) =
   try
     let found =
       List.find
-        (fun (proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -459,7 +459,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
     maxmeta := newmeta;
     if is_identity env newcurrent then
       if sign = Negative then Some (sign, newcurrent)
-      else (Inference.delete_proof newcurrent; None)
+      else None
     else
       Some (sign, newcurrent)
   in
@@ -483,13 +483,12 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
       if ok then res else None
   | Some (Positive, c) ->
       if Indexing.in_index active_table c then
-        (Inference.delete_proof c; None)
+        None
       else
         match passive_table with
         | None -> res
         | Some passive_table ->
-            if Indexing.in_index passive_table c then
-              (Inference.delete_proof c; None)
+            if Indexing.in_index passive_table c then None
             else res
 
 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
@@ -572,12 +571,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
     List.fold_left
       (fun s e ->
          if not (Inference.is_identity env e) then
-           if EqualitySet.mem e s then
-             (Inference.delete_proof e; s)
-           else
-             EqualitySet.add e s
-         else
-           (Inference.delete_proof e; s))
+           if EqualitySet.mem e s then s
+           else EqualitySet.add e s
+         else s)
       EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
@@ -609,16 +605,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let is_duplicate =
     match passive_table with
     | None ->
-        (fun e ->
-           let ok = not (Indexing.in_index active_table e) in
-           if not ok then Inference.delete_proof e;
-           ok)
+        (fun e -> not (Indexing.in_index active_table e))
     | Some passive_table ->
         (fun e ->
-           let ok = not ((Indexing.in_index active_table e) ||
-                           (Indexing.in_index passive_table e)) in
-           if not ok then Inference.delete_proof e;
-           ok)
+           not ((Indexing.in_index active_table e) ||
+                  (Indexing.in_index passive_table e)))
   in
   new_neg, List.filter is_duplicate new_pos
 
@@ -655,7 +646,6 @@ let backward_simplify_active env new_pos new_table active =
          if List.mem (s, eq) res then
            res, tbl
          else if (is_identity env eq) || (find eq res) then (
-           Inference.delete_proof eq;
            res, tbl
          ) (* else if (find eq res) then *)
 (*            res, tbl *)
@@ -665,7 +655,6 @@ let backward_simplify_active env new_pos new_table active =
     List.fold_right
       (fun (s, eq) (n, p) ->
          if (s <> Negative) && (is_identity env eq) then (
-           Inference.delete_proof eq;
            (n, p)
          ) else
            if s = Negative then eq::n, p
@@ -1017,7 +1006,7 @@ let main () =
   let env = (metasenv, context, ugraph) in
   try
     let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+    let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = make_active () in
     let passive = make_passive [term_equality] equalities in
     Printf.printf "\ncurrent goal: %s\n"
diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 42703045d..d6454f202 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -84,8 +84,15 @@ let weight_of_term ?(consider_metas=true) term =
 
 
 let compute_equality_weight ty left right =
-  let weight_of t = fst (weight_of_term ~consider_metas:false t) in
-  (weight_of ty) + (weight_of left) + (weight_of right)
+  let metasw = ref 0 in
+  let weight_of t =
+    let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
+(*     let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
+(*     metasw := !metasw + mw; *)
+    metasw := !metasw + (2 * (List.length m));
+    w
+  in
+  (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
 ;;
 
 
-- 
2.39.2