From bbe7741f3bbaacb93f2876c018dace82f5e929b8 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Wed, 29 Jun 2005 15:08:20 +0000
Subject: [PATCH] various updates, removed proofs for now because they are the
 real bottleneck!!

---
 helm/ocaml/paramodulation/Makefile         |   1 -
 helm/ocaml/paramodulation/indexing.ml      | 228 +++++++++++-----
 helm/ocaml/paramodulation/inference.ml     | 290 +++++++++++++++++++--
 helm/ocaml/paramodulation/inference.mli    |   5 +
 helm/ocaml/paramodulation/saturation.ml    | 171 +++++++-----
 helm/ocaml/paramodulation/test_indexing.ml |  31 ++-
 helm/ocaml/paramodulation/utils.ml         |   4 +-
 helm/ocaml/paramodulation/utils.mli        |   2 +-
 8 files changed, 578 insertions(+), 154 deletions(-)

diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile
index 9d30e7020..a34ec0c2b 100644
--- a/helm/ocaml/paramodulation/Makefile
+++ b/helm/ocaml/paramodulation/Makefile
@@ -31,7 +31,6 @@ INTERFACE_FILES = \
 
 DEPOBJS = \
 	$(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
-	trie.ml \
 	path_indexing.ml \
 	discrimination_tree.ml \
 	test_indexing.ml \
diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 0193b781b..5a8960101 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -24,6 +24,52 @@ let print_candidates mode term res =
 let indexing_retrieval_time = ref 0.;;
 
 
+(* let my_apply_subst subst term = *)
+(*   let module C = Cic in *)
+(*   let lookup lift_amount meta = *)
+(*     match meta with *)
+(*     | C.Meta (i, _) -> ( *)
+(*         try *)
+(*           let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
+(*           (\* CicSubstitution.lift lift_amount  *\)t *)
+(*         with Not_found -> meta *)
+(*       ) *)
+(*     | _ -> assert false *)
+(*   in *)
+(*   let rec apply_aux lift_amount =  function *)
+(*     | C.Meta (i, l) as t -> lookup lift_amount t *)
+(*     | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
+(*     | C.Prod (nn, s, t) -> *)
+(*         C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
+(*     | C.Lambda (nn, s, t) -> *)
+(*         C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
+(*     | t -> t *)
+(*   in *)
+(*   apply_aux 0 term *)
+(* ;; *)
+
+
+(* let apply_subst subst term = *)
+(*   Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
+(*     (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
+(*   let res = my_apply_subst subst term in *)
+(* (\*   let res = CicMetaSubst.apply_subst subst term in *\) *)
+(*   Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
+(*   print_endline "|"; *)
+(*   res *)
+(* ;; *)
+
+(* let apply_subst = my_apply_subst *)
+let apply_subst = CicMetaSubst.apply_subst
+
+
+let apply_subst =
+  let profile = CicUtil.profile "apply_subst" in
+  (fun s a -> profile (apply_subst s) a)
+;;
+
+
+(*
 let empty_table () =
   Path_indexing.PSTrie.empty
 ;;
@@ -48,9 +94,9 @@ let get_candidates mode trie term =
   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
   res
 ;;
+*)
 
 
-(*
 let empty_table () =
   Discrimination_tree.DiscriminationTree.empty
 ;;
@@ -60,6 +106,7 @@ and remove_index = Discrimination_tree.remove_index
 and in_index = Discrimination_tree.in_index;;
 
 let get_candidates mode tree term =
+  let t1 = Unix.gettimeofday () in
   let res =
     let s = 
       match mode with
@@ -69,9 +116,17 @@ let get_candidates mode tree term =
     Discrimination_tree.PosEqSet.elements s
   in
 (*   print_candidates mode term res; *)
+  let t2 = Unix.gettimeofday () in
+  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
   res
 ;;
-*)
+
+
+(* let get_candidates = *)
+(*   let profile = CicUtil.profile "Indexing.get_candidates" in *)
+(*   (fun mode tree term -> profile (get_candidates mode tree) term) *)
+(* ;; *)
+
 
 let match_unif_time_ok = ref 0.;;
 let match_unif_time_no = ref 0.;;
@@ -120,8 +175,8 @@ let rec find_matches metasenv context ugraph lift_amount term =
           let res = try do_match c other eq_URI with e -> None in
           match res with
           | Some (_, s, _, _, _) ->
-              let c' = M.apply_subst s c
-              and other' = M.apply_subst s other in
+              let c' = (* M. *)apply_subst s c
+              and other' = (* M. *)apply_subst s other in
               let order = cmp c' other' in
               let names = U.names_of_context context in
               if order = U.Gt then
@@ -133,7 +188,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
 ;;
 
 
-let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
+let rec find_all_matches ?(unif_fun=Inference.unification)
     metasenv context ugraph lift_amount term =
   let module C = Cic in
   let module U = Utils in
@@ -181,8 +236,8 @@ let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
             let res = do_match c other eq_URI in
             match res with
             | _, s, _, _, _ ->
-                let c' = M.apply_subst s c
-                and other' = M.apply_subst s other in
+                let c' = (* M. *)apply_subst s c
+                and other' = (* M. *)apply_subst s other in
                 let order = cmp c' other' in
                 let names = U.names_of_context context in
                 if order <> U.Lt && order <> U.Le then
@@ -198,7 +253,7 @@ let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
 
 
 let subsumption env table target =
-  let _, (ty, tl, tr, _), tmetas, _ = target in
+  let _, (ty, left, right, _), tmetas, _ = target in
   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =
@@ -214,50 +269,47 @@ let subsumption env table target =
            true)
       subst'
   in
-  let subsaux left right =
-    let leftc = get_candidates Matching table left in
-    let leftr =
-      find_all_matches ~unif_fun:Inference.matching
-        metasenv context ugraph 0 left leftc
-    in
-    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' =
-          let t1 = Unix.gettimeofday () in
-          try
-            let r = 
-              Inference.matching metasenv context what other ugraph in
-            let t2 = Unix.gettimeofday () in
-            match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-            r
-          with e ->
-            let t2 = Unix.gettimeofday () in
-            match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-            raise e
-        in
-        samesubst subst subst'
-      with e ->
-        false
-    in
-    let r = List.exists (ok right) leftr in
-    if r then
-      true
-    else
-      let rightc = get_candidates Matching table right in
-      let rightr =
+  let leftr =
+    match left with
+    | Cic.Meta _ -> []
+    | _ ->
+        let leftc = get_candidates Matching table left in
         find_all_matches ~unif_fun:Inference.matching
-          metasenv context ugraph 0 right rightc
+          metasenv context ugraph 0 left leftc
+  in
+  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' =
+        let t1 = Unix.gettimeofday () in
+        try
+          let r = 
+            Inference.matching metasenv context what other ugraph in
+          let t2 = Unix.gettimeofday () in
+          match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+          r
+        with e ->
+          let t2 = Unix.gettimeofday () in
+          match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+          raise e
       in
-      List.exists (ok left) rightr
+      samesubst subst subst'
+    with e ->
+      false
   in
-  let res =  subsaux tl tr in
-  if res then (
-    Printf.printf "subsumption!:\ntarget: %s\n"
-      (Inference.string_of_equality ~env target);
-    print_newline ();
-  );
-  res
+  let r = List.exists (ok right) leftr in
+  if r then
+    true
+  else
+    let rightr =
+      match right with
+      | Cic.Meta _ -> []
+      | _ ->
+          let rightc = get_candidates Matching table right in
+          find_all_matches ~unif_fun:Inference.matching
+            metasenv context ugraph 0 right rightc
+    in
+    List.exists (ok left) rightr
 ;;
 
 
@@ -323,6 +375,8 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
 ;;
 
 
+let build_newtarget_time = ref 0.;;
+
 let rec demodulation newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -332,10 +386,12 @@ let rec demodulation newmeta env table target =
   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 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 = (* 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] @
@@ -343,8 +399,9 @@ let rec demodulation newmeta env table target =
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo,
-      M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                                   proof; other; proof'])
+      C.Implicit None
+(*       (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
+(*                                    proof; other; proof']) *)
     in
     let left, right = if is_left then newterm, right else left, newterm in
     let m =
@@ -357,8 +414,16 @@ let rec demodulation newmeta env table target =
         args
     in
     let ordering = !Utils.compare_terms left right in
+
+    let time2 = Unix.gettimeofday () in
+    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
+    
     newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
   in
+(*   let build_newtarget = *)
+(*     let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
+(*     (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
@@ -372,9 +437,9 @@ let rec demodulation newmeta env table target =
         (Inference.meta_convertibility_eq target newtarget) then
           newmeta, newtarget
       else
-        if subsumption env table newtarget then
-          newmeta, build_identity newtarget
-        else
+(*         if subsumption env table newtarget then *)
+(*           newmeta, build_identity newtarget *)
+(*         else *)
           demodulation newmeta env table newtarget
   | None ->
       let res = demodulate_term metasenv' context ugraph table 0 right in
@@ -385,9 +450,9 @@ let rec demodulation newmeta env table target =
             (Inference.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else
-            if subsumption env table newtarget then
-              newmeta, build_identity newtarget
-            else
+(*             if subsumption env table newtarget then *)
+(*               newmeta, build_identity newtarget *)
+(*             else *)
               demodulation newmeta env table newtarget
       | None ->
           newmeta, target
@@ -506,10 +571,12 @@ let superposition_left (metasenv, context, ugraph) table target =
     betaexpand_term metasenv context ugraph table 0 term
   in
   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 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' = (* M. *)apply_subst s (S.subst other bo) in
       let bo'' =
         C.Appl (
           [C.MutInd (HL.Logic.eq_URI, 0, []);
@@ -519,15 +586,24 @@ let superposition_left (metasenv, context, ugraph) table target =
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo',
-      M.apply_subst s
-        (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                 proof; other; proof'])
+      C.Implicit None
+(*       (\* M. *\)apply_subst s *)
+(*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
+(*                  proof; other; proof']) *)
     in
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
     let neworder = !Utils.compare_terms left right in
+
+    let time2 = Unix.gettimeofday () in
+    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
+    
     (newproof, (eq_ty, left, right, neworder), [], [])
   in
+(*   let build_new = *)
+(*     let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
+(*     (fun e -> profile build_new e) *)
+(*   in *)
   List.map build_new expansions
 ;;
 
@@ -550,7 +626,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         let res l r =
           List.filter
             (fun (_, subst, _, _, _) ->
-               let subst = M.apply_subst subst in
+               let subst = (* M. *)apply_subst subst in
                let o = !Utils.compare_terms (subst l) (subst r) in
                o <> U.Lt && o <> U.Le)
             (fst (betaexpand_term metasenv' context ugraph table 0 l))
@@ -558,10 +634,13 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         (res left right), (res right left)
   in
   let build_new ordering (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 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' = (* 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] @
@@ -570,14 +649,15 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo',
-      M.apply_subst s
-        (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                 eqproof; other; proof'])
+      C.Implicit None
+(*       (\* M. *\)apply_subst s *)
+(*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
+(*                  eqproof; other; proof']) *)
     in
     let newmeta, newequality = 
       let left, right =
-        if ordering = U.Gt then newgoal, M.apply_subst s right
-        else M.apply_subst s left, newgoal in
+        if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
+        else (* M. *)apply_subst s left, newgoal in
       let neworder = !Utils.compare_terms left right 
       and newmenv = newmetas @ menv'
       and newargs = args @ args' in
@@ -587,8 +667,18 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       newm, eq'
     in
     maxmeta := newmeta;
+
+    let time2 = Unix.gettimeofday () in
+    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
+    
     newequality
   in
+
+(*   let build_new = *)
+(*     let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
+(*     (fun o e -> profile (build_new o) e) *)
+(*   in *)
+  
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
   let ok = function
diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index e79d78e84..d8ff4a7d9 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -294,29 +294,285 @@ let rec restore_subst (* context *) subst =
 ;;
 
 
-exception MatchingFailure;;
+let rec check_irl start = function
+  | [] -> true
+  | None::tl -> check_irl (start+1) tl
+  | (Some (Cic.Rel x))::tl ->
+      if x = start then check_irl (start+1) tl else false
+  | _ -> false
+;;
 
-let matching metasenv context t1 t2 ugraph =
-  try
-    let subst, metasenv, ugraph =
-      CicUnification.fo_unif metasenv context t1 t2 ugraph
+let rec is_simple_term = function
+  | Cic.Appl ((Cic.Meta _)::_) -> false
+  | Cic.Appl l -> List.for_all is_simple_term l
+  | Cic.Meta (i, l) -> check_irl 1 l
+  | Cic.Rel _ -> true
+  | _ -> false
+;;
+
+
+let lookup_subst meta subst =
+  match meta with
+  | Cic.Meta (i, _) -> (
+      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+      with Not_found -> meta
+    )
+  | _ -> assert false
+;;
+
+
+let unification_simple metasenv context t1 t2 ugraph =
+  let module C = Cic in
+  let module M = CicMetaSubst in
+  let module U = CicUnification in
+  let lookup = lookup_subst in
+  let rec occurs_check subst what where =
+    (*       Printf.printf "occurs_check %s %s" *)
+    (*         (CicPp.ppterm what) (CicPp.ppterm where); *)
+    (*       print_newline (); *)
+    match where with
+    | t when what = t -> true
+    | C.Appl l -> List.exists (occurs_check subst what) l
+    | C.Meta _ ->
+        let t = lookup where subst in
+        if t <> where then occurs_check subst what t else false
+    | _ -> false
+  in
+  let rec unif subst menv s t =
+(*     Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
+(*       (print_subst subst); *)
+(*     print_newline (); *)
+    let s = match s with C.Meta _ -> lookup s subst | _ -> s
+    and t = match t with C.Meta _ -> lookup t subst | _ -> t
     in
-    let t' = CicMetaSubst.apply_subst subst t1 in
-    if not (meta_convertibility t1 t') then
-      raise MatchingFailure
+    (*       Printf.printf "after apply_subst: %s %s\n%s" *)
+    (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
+    (*       print_newline (); *)
+    match s, t with
+    | s, t when s = t -> subst, menv
+    | C.Meta (i, _), C.Meta (j, _) when i > j ->
+        unif subst menv t s
+    | C.Meta _, t when occurs_check subst s t ->
+        raise (U.UnificationFailure "Inference.unification.unif")
+(*     | C.Meta (i, l), C.Meta (j, l') -> *)
+(*         let _, _, ty = CicUtil.lookup_meta i menv in *)
+(*         let _, _, ty' = CicUtil.lookup_meta j menv in *)
+(*         let binding1 = lookup s subst in *)
+(*         let binding2 = lookup t subst in *)
+(*         let subst, menv =  *)
+(*           if binding1 != s then *)
+(*             if binding2 != t then *)
+(*               unif subst menv binding1 binding2 *)
+(*             else *)
+(*               if binding1 = t then *)
+(*                 subst, menv *)
+(*               else *)
+(*                 ((j, (context, binding1, ty'))::subst, *)
+(*                  List.filter (fun (m, _, _) -> j <> m) menv) *)
+(*           else *)
+(*             if binding2 != t then *)
+(*               if s = binding2 then *)
+(*                 subst, menv *)
+(*               else *)
+(*                 ((i, (context, binding2, ty))::subst, *)
+(*                  List.filter (fun (m, _, _) -> i <> m) menv) *)
+(*             else *)
+(*               ((i, (context, t, ty))::subst, *)
+(*                List.filter (fun (m, _, _) -> i <> m) menv) *)
+(*         in *)
+(*         subst, menv *)
+        
+    | C.Meta (i, l), t ->
+        let _, _, ty = CicUtil.lookup_meta i menv in
+        let subst =
+          if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+          else subst
+        in
+        let menv = List.filter (fun (m, _, _) -> i <> m) menv in
+        subst, menv
+    | _, C.Meta _ -> unif subst menv t s
+    | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
+        raise (U.UnificationFailure "Inference.unification.unif")
+    | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
+        try
+          List.fold_left2
+            (fun (subst', menv) s t -> unif subst' menv s t)
+            (subst, menv) tls tlt
+        with e ->
+          raise (U.UnificationFailure "Inference.unification.unif")
+      )
+    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+  in
+  let subst, menv = unif [] metasenv t1 t2 in
+  (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
+  (*     print_newline (); *)
+(*   let rec fix_term = function *)
+(*     | (C.Meta (i, l) as t) -> *)
+(*         lookup t subst *)
+(*     | C.Appl l -> C.Appl (List.map fix_term l) *)
+(*     | t -> t *)
+(*   in *)
+(*   let rec fix_subst = function *)
+(*     | [] -> [] *)
+(*     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
+(*   in *)
+(*   List.rev (fix_subst subst), menv, ugraph *)
+  List.rev subst, menv, ugraph
+;;
+
+
+let unification metasenv context t1 t2 ugraph =
+(*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+  let subst, menv, ug =
+    if not (is_simple_term t1) || not (is_simple_term t2) then
+      CicUnification.fo_unif metasenv context t1 t2 ugraph
     else
-      let metas = metas_of_term t1 in
-      let fix_subst = function
-        | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-            (j, (c, Cic.Meta (i, lc), ty))
-        | s -> s
+      unification_simple metasenv context t1 t2 ugraph
+  in
+  let rec fix_term = function
+    | (Cic.Meta (i, l) as t) ->
+        let t' = lookup_subst t subst in
+        if t <> t' then fix_term t' else t
+    | Cic.Appl l -> Cic.Appl (List.map fix_term l)
+    | t -> t
+  in
+  let rec fix_subst = function
+    | [] -> []
+    | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
+  in
+(*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
+(*   print_endline "|"; *)
+  (* fix_subst *) subst, menv, ug
+;;
+
+(* let unification = CicUnification.fo_unif;; *)
+
+exception MatchingFailure;;
+
+
+let matching_simple metasenv context t1 t2 ugraph =
+  let module C = Cic in
+  let module M = CicMetaSubst in
+  let module U = CicUnification in
+  let lookup meta subst =
+    match meta with
+    | C.Meta (i, _) -> (
+        try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+        with Not_found -> meta
+      )
+    | _ -> assert false
+  in
+  let rec do_match subst menv s t =
+(*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
+(*       (print_subst subst); *)
+(*     print_newline (); *)
+(*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
+(*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
+    (*       Printf.printf "after apply_subst: %s %s\n%s" *)
+    (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
+    (*       print_newline (); *)
+    match s, t with
+    | s, t when s = t -> subst, menv
+(*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
+(*         do_match subst menv t s *)
+(*     | C.Meta _, t when occurs_check subst s t -> *)
+(*         raise MatchingFailure *)
+(*     | s, C.Meta _ when occurs_check subst t s -> *)
+(*         raise MatchingFailure *)
+    | s, C.Meta (i, l) ->
+        let filter_menv i menv =
+          List.filter (fun (m, _, _) -> i <> m) menv
+        in
+        let subst, menv =
+          let value = lookup t subst in
+          match value with
+(*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
+(*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
+          | value when value = t ->
+              let _, _, ty = CicUtil.lookup_meta i menv in
+              (i, (context, s, ty))::subst, filter_menv i menv
+          | value when value <> s ->
+              raise MatchingFailure
+          | value -> do_match subst menv s value
+        in
+        subst, menv
+(*           else if value <> s then *)
+(*             raise MatchingFailure *)
+(*           else subst *)
+(*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
+(*           else subst *)
+(*         in *)
+(*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
+(*         subst, menv *)
+(*     | _, C.Meta _ -> do_match subst menv t s *)
+(*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
+(*         raise MatchingFailure *)
+    | C.Appl ls, C.Appl lt -> (
+        try
+          List.fold_left2
+            (fun (subst, menv) s t -> do_match subst menv s t)
+            (subst, menv) ls lt
+        with e ->
+(*           print_endline (Printexc.to_string e); *)
+(*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
+(*           print_newline ();           *)
+          raise MatchingFailure
+      )
+    | _, _ ->
+(*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
+(*         print_newline (); *)
+        raise MatchingFailure
+  in
+  let subst, menv = do_match [] metasenv t1 t2 in
+  (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
+  (*     print_newline (); *)
+  subst, menv, ugraph
+;;
+
+
+let matching metasenv context t1 t2 ugraph =
+(*   if (is_simple_term t1) && (is_simple_term t2) then *)
+(*     let subst, menv, ug = *)
+(*       matching_simple metasenv context t1 t2 ugraph in *)
+(* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
+(* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
+(* (\*     print_newline (); *\) *)
+(*     subst, menv, ug *)
+(*   else *)
+    try
+      let subst, metasenv, ugraph =
+        (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
+        unification metasenv context t1 t2 ugraph
       in
-      let subst = List.map fix_subst subst in
-      subst, metasenv, ugraph
-  with e ->
-    raise MatchingFailure
+      let t' = CicMetaSubst.apply_subst subst t1 in
+      if not (meta_convertibility t1 t') then
+        raise MatchingFailure
+      else
+        let metas = metas_of_term t1 in
+        let fix_subst = function
+          | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+              (j, (c, Cic.Meta (i, lc), ty))
+          | s -> s
+        in
+        let subst = List.map fix_subst subst in
+
+(*         Printf.printf "matching %s %s:\n%s\n" *)
+(*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
+(*         print_newline (); *)
+
+        subst, metasenv, ugraph
+    with e ->
+(*       Printf.printf "failed to match %s %s\n" *)
+(*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+      raise MatchingFailure
 ;;
 
+(* let matching = *)
+(*   let profile = CicUtil.profile "Inference.matching" in *)
+(*   (fun metasenv context t1 t2 ugraph -> *)
+(*      profile (matching metasenv context t1 t2) ugraph) *)
+(* ;; *)
+
 
 let beta_expand ?(metas_ok=true) ?(match_only=false)
     what type_of_what where context metasenv ugraph = 
diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 5ced528bb..42fc39bf3 100644
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -18,7 +18,12 @@ val matching:
   CicUniv.universe_graph ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
+val unification:
+  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  CicUniv.universe_graph ->
+  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
+    
 (**
    Performs the beta expansion of the term "where" w.r.t. "what",
    i.e. returns the list of all the terms t s.t. "(t what) = where".
diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index a1414de79..d8019cae8 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -5,15 +5,17 @@ open Utils;;
 (* profiling statistics... *)
 let infer_time = ref 0.;;
 let forward_simpl_time = ref 0.;;
+let forward_simpl_new_time = ref 0.;;
 let backward_simpl_time = ref 0.;;
+let passive_maintainance_time = ref 0.;;
 
 (* limited-resource-strategy related globals *)
 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
 let start_time = ref 0.;; (* time at which the execution started *)
 let elapsed_time = ref 0.;;
-let maximal_weight = ref None;;
-(* let maximal_retained_equality = ref None;; *)
+(* let maximal_weight = ref None;; *)
+let maximal_retained_equality = ref None;;
 
 (* equality-selection related globals *)
 let use_fullred = ref false;;
@@ -63,8 +65,13 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
 
 
 let weight_of_equality (_, (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 meta_number = ref 0 in
+  let weight_of t =
+    let weight, ml =  weight_of_term t in
+    meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
+    weight
+  in
+  (weight_of ty) + (weight_of left) + (weight_of right), meta_number
 ;;
 
 
@@ -77,13 +84,15 @@ module OrderedEquality = struct
     | false ->
         let _, (ty, left, right, _), _, _ = eq1
         and _, (ty', left', right', _), _, _ = eq2 in
+(*         let w1, m1 = weight_of_equality eq1 *)
+(*         and w2, m2 = weight_of_equality 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
-(*         let w1 = weight_of_equality eq1 *)
-(*         and w2 = weight_of_equality eq2 in *)
         match Pervasives.compare w1 w2 with
         | 0 -> Pervasives.compare eq1 eq2
+(*             let res = Pervasives.compare m1 m2 in *)
+(*             if res = 0 then Pervasives.compare eq1 eq2 else res *)
         | res -> res
 end
 
@@ -141,6 +150,10 @@ let select env passive (active, _) =
             in
             let c = others + (abs (common - card)) in
             if c < i then (c, equality)
+(*             else if c = i then *)
+(*               match OrderedEquality.compare equality e with *)
+(*               | -1 -> (c, equality) *)
+(*               | res -> (i, e) *)
             else (i, e)
           in
           let e1 = EqualitySet.min_elt pos_set in
@@ -347,8 +360,8 @@ let prune_passive howmany (active, _) passive =
   let in_age, ns, nl = picka in_age ns nl in
   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_weight := Some (weight_of_equality (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 ())
@@ -390,11 +403,11 @@ 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_weight *)!maximal_retained_equality with
   | None -> new_neg, new_pos
-  | Some w (* eq *) ->
+  | Some (* w *) eq ->
       let new_pos =
-        List.filter (fun e -> (weight_of_equality e) <= w (* OrderedEquality.compare e eq <= 0 *)) new_pos in
+        List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
       new_neg, new_pos
 ;;
 
@@ -432,6 +445,17 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 (*         else find_duplicate sign current tl *)
 (*     | _::tl -> find_duplicate sign current tl *)
 (*   in *)
+
+(*   let res =  *)
+(*     if sign = Positive then *)
+(*       Indexing.subsumption env active_table current *)
+(*     else *)
+(*       false *)
+(*   in *)
+(*   if res then *)
+(*     None *)
+(*   else *)
+  
   let demodulate table current = 
     let newmeta, newcurrent =
       Indexing.demodulation !maxmeta env table current in
@@ -552,14 +576,14 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   in
   let new_pos = EqualitySet.elements new_pos_set in
 
-(*   let subs = *)
-(*     match passive_table with *)
-(*     | None -> *)
-(*         (fun e -> not (Indexing.subsumption env active_table e)) *)
-(*     | Some passive_table -> *)
-(*         (fun e -> not ((Indexing.subsumption env active_table e) || *)
-(*                          (Indexing.subsumption env passive_table e))) *)
-(*   in *)
+  let subs =
+    match passive_table with
+    | None ->
+        (fun e -> not (Indexing.subsumption env active_table e))
+    | Some passive_table ->
+        (fun e -> not ((Indexing.subsumption env active_table e) ||
+                         (Indexing.subsumption env passive_table e)))
+  in
 
   let t1 = Unix.gettimeofday () in
 
@@ -595,13 +619,8 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
 ;;
 
 
-let backward_simplify_active env (new_neg, new_pos) active =
+let backward_simplify_active env new_pos new_table active =
   let active_list, active_table = active in
-  let new_pos, new_table =
-    List.fold_left
-      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
-      ([], Indexing.empty_table ()) new_pos
-  in
   let active_list, newa = 
     List.fold_right
       (fun (s, equality) (res, newn) ->
@@ -640,12 +659,7 @@ let backward_simplify_active env (new_neg, new_pos) active =
 ;;
 
 
-let backward_simplify_passive env (new_neg, new_pos) passive =
-  let new_pos, new_table =
-    List.fold_left
-      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
-      ([], Indexing.empty_table ()) new_pos
-  in
+let backward_simplify_passive env new_pos new_table passive =
   let (nl, ns), (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
     match forward_simplify env (sign, equality) (new_pos, new_table) with
@@ -670,13 +684,18 @@ let backward_simplify_passive env (new_neg, new_pos) passive =
 
 
 let backward_simplify env new' ?passive active =
-  let active, newa = backward_simplify_active env new' active in
+  let new_pos, new_table =
+    List.fold_left
+      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
+      ([], Indexing.empty_table ()) (snd new')
+  in    
+  let active, newa = backward_simplify_active env new_pos new_table active in
   match passive with
   | None ->
       active, (make_passive [] []), newa, None
   | Some passive ->
       let passive, newp =
-        backward_simplify_passive env new' passive in
+        backward_simplify_passive env new_pos new_table passive in
       active, passive, newa, newp
 ;;
 
@@ -686,11 +705,13 @@ let get_selection_estimate () =
 (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
   int_of_float (
     ceil ((float_of_int !processed_clauses) *.
-            ((!time_limit *. 2.) /. !elapsed_time -. 1.)))
+            ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 ;;
 
   
 let rec given_clause env passive active =
+  let time1 = Unix.gettimeofday () in
+
   let selection_estimate = get_selection_estimate () in
   let kept = size_of_passive passive in
   let passive =
@@ -708,13 +729,20 @@ let rec given_clause env passive active =
       passive
   in
 
+  let time2 = Unix.gettimeofday () in
+  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+
   kept_clauses := (size_of_passive passive) + (size_of_active active);
     
   match passive_is_empty passive with
   | true -> Failure
   | false ->
       let (sign, current), passive = select env passive active in
-      match forward_simplify env (sign, current) ~passive active with
+      let time1 = Unix.gettimeofday () in
+      let res = forward_simplify env (sign, current) ~passive active in
+      let time2 = Unix.gettimeofday () in
+      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+      match res with
       | None ->
           given_clause env passive active
       | Some (sign, current) ->
@@ -743,7 +771,7 @@ let rec given_clause env passive active =
               let new' = forward_simplify_new env new' (* ~passive *) active in
               let t2 = Unix.gettimeofday () in
               let _ =
-                forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
+                forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
               in
               let active =
                 match sign with
@@ -818,6 +846,8 @@ let rec given_clause env passive active =
 
 
 let rec given_clause_fullred env passive active =
+  let time1 = Unix.gettimeofday () in
+  
   let selection_estimate = get_selection_estimate () in
   let kept = size_of_passive passive in
   let passive =
@@ -834,12 +864,21 @@ let rec given_clause_fullred env passive active =
     ) else
       passive
   in
+
+  let time2 = Unix.gettimeofday () in
+  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
     
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
+
   match passive_is_empty passive with
   | true -> Failure
   | false ->
       let (sign, current), passive = select env passive active in
-      match forward_simplify env (sign, current) ~passive active with
+      let time1 = Unix.gettimeofday () in
+      let res = forward_simplify env (sign, current) ~passive active in
+      let time2 = Unix.gettimeofday () in
+      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+      match res with
       | None ->
           given_clause_fullred env passive active
       | Some (sign, current) ->
@@ -872,7 +911,7 @@ let rec given_clause_fullred env passive active =
               let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' ~passive active in
               let t2 = Unix.gettimeofday () in
-              forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
+              forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
               let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained =
                 backward_simplify env new' ~passive active in
@@ -894,27 +933,27 @@ let rec given_clause_fullred env passive active =
             if k < (kept - 1) then
               processed_clauses := !processed_clauses + (kept - 1 - k);
             
-            let _ =
-              Printf.printf "active:\n%s\n"
-                (String.concat "\n"
-                   ((List.map
-                       (fun (s, e) -> (string_of_sign s) ^ " " ^
-                          (string_of_equality ~env e)) (fst active))));
-              print_newline ();
-            in
-            let _ =
-              match new' with
-              | neg, pos ->
-                  Printf.printf "new':\n%s\n"
-                    (String.concat "\n"
-                       ((List.map
-                           (fun e -> "Negative " ^
-                              (string_of_equality ~env e)) neg) @
-                          (List.map
-                             (fun e -> "Positive " ^
-                                (string_of_equality ~env e)) pos)));
-                  print_newline ();
-            in
+(*             let _ = *)
+(*               Printf.printf "active:\n%s\n" *)
+(*                 (String.concat "\n" *)
+(*                    ((List.map *)
+(*                        (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
+(*                           (string_of_equality ~env e)) (fst active)))); *)
+(*               print_newline (); *)
+(*             in *)
+(*             let _ = *)
+(*               match new' with *)
+(*               | neg, pos -> *)
+(*                   Printf.printf "new':\n%s\n" *)
+(*                     (String.concat "\n" *)
+(*                        ((List.map *)
+(*                            (fun e -> "Negative " ^ *)
+(*                               (string_of_equality ~env e)) neg) @ *)
+(*                           (List.map *)
+(*                              (fun e -> "Positive " ^ *)
+(*                                 (string_of_equality ~env e)) pos))); *)
+(*                   print_newline (); *)
+(*             in *)
             match contains_empty env new' with
             | false, _ -> 
                 let passive = add_to_passive passive new' in
@@ -998,14 +1037,20 @@ let main () =
           Printf.printf "Success, but no proof?!?\n\n"
     in
     Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+                     "forward_simpl_new_time: %.9f\n" ^^
                      "backward_simpl_time: %.9f\n")
-      !infer_time !forward_simpl_time !backward_simpl_time;
-    Printf.printf "successful unification/matching time: %.9f\n"
+      !infer_time !forward_simpl_time !forward_simpl_new_time
+      !backward_simpl_time;
+    Printf.printf "passive_maintainance_time: %.9f\n"
+      !passive_maintainance_time;
+    Printf.printf "    successful unification/matching time: %.9f\n"
       !Indexing.match_unif_time_ok;
-    Printf.printf "failed unification/matching time: %.9f\n"
+    Printf.printf "    failed unification/matching time: %.9f\n"
       !Indexing.match_unif_time_no;
-    Printf.printf "indexing retrieval time: %.9f\n"
+    Printf.printf "    indexing retrieval time: %.9f\n"
       !Indexing.indexing_retrieval_time;
+    Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
+      !Indexing.build_newtarget_time;
     Printf.printf "derived %d clauses, kept %d clauses.\n"
       !derived_clauses !kept_clauses;
   with exc ->
diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
index 2ef07a17c..0324f9e56 100644
--- a/helm/ocaml/paramodulation/test_indexing.ml
+++ b/helm/ocaml/paramodulation/test_indexing.ml
@@ -140,8 +140,37 @@ let discrimination_tree_test () =
 ;;
 
 
+let test_subst () =
+  let module C = Cic in
+  let module M = CicMetaSubst in
+  let term = C.Appl [
+    C.Rel 1;
+    C.Appl [C.Rel 11;
+            C.Meta (43, []);
+            C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
+    C.Appl [C.Rel 11;
+            C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
+            C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
+  ] in
+  let subst1 = [
+    (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16));
+    (10, ([], C.Rel 12, C.Rel 16));
+    (12, ([], C.Meta (41, []), C.Rel 16))
+  ]
+  and subst2 = [
+    (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16));
+    (10, ([], C.Rel 12, C.Rel 16));
+    (12, ([], C.Meta (41, []), C.Rel 16))
+  ] in
+  let t1 = M.apply_subst subst1 term
+  and t2 = M.apply_subst subst2 term in
+  Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
+;;
+
+
 (* differing ();; *)
 (* next_after ();; *)
-discrimination_tree_test ();;
+(* discrimination_tree_test ();; *)
 (* path_indexing_test ();; *)
+test_subst ();;
 
diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index f2c475799..52d99327e 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -7,8 +7,8 @@ let print_metasenv metasenv =
 ;;
 
 
-let print_subst subst =
-  String.concat "\n"
+let print_subst ?(prefix="\n") subst =
+  String.concat prefix
     (List.map
        (fun (i, (c, t, ty)) ->
           Printf.sprintf "?%d -> %s : %s" i
diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 71f2fc1b5..612f07cf0 100644
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -5,7 +5,7 @@ type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
 
 val print_metasenv: Cic.metasenv -> string
 
-val print_subst: Cic.substitution -> string
+val print_subst: ?prefix:string -> Cic.substitution -> string
 
 val string_of_weight: weight -> string
 
-- 
2.39.2