First version of deep_subsumption.

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 8e77936c8f964bc721b64170a3326ce1db3e3890..e931423b96b9d011965f13e8b1487e54c9c8c52b 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -178,13 +178,12 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause ~unify = function
+    let is_identity_clause = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
+      | _, Terms.Equation (l,r,_,_), vl, proof ->
          (try ignore(Unif.unification vl [] l r); true
          with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Predicate _, _, _ -> assert false       
-      | _ -> false
     ;;
 
     let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =
@@ -195,7 +194,6 @@ module Superposition (B : Terms.Blob) =
       | None -> None
     ;;
 
-
     let fold_build_new_clause bag maxvar id rule filter res =
       let (bag, maxvar), res =
        HExtlib.filter_map_acc 
@@ -249,20 +247,53 @@ module Superposition (B : Terms.Blob) =
                  build_new_clause bag maxvar (fun _ -> true)
                    Terms.Superposition id_t subst [] id id2 [2] dir 
     ;;
+    (* id refers to a clause proving contextl l = contextr r *)
 
-(*
-    let rec deeply_subsumed ~unify bag maxvar (id, lit, vl, _) table =
-      match lit with
-      | Terms.Predicate _ -> assert false
-      | Terms.Equation (l,r,ty,_) -> 
-       (match is_subsumed ~unify bag maxvar (id, lit, vl, _) table with
-        | Some((bag,maxvar),c) -> Some((bag,maxvar),c)
-        | None -> 
-            match l,r with ->
-              Var i, _ -> 
+    let rec deep_eq ~unify l r ty pos contextl contextr table acc =
+      match acc with 
+      | None -> None
+      | Some(bag,maxvar,[],subst) -> assert false
+      | Some(bag,maxvar,(id,_,vl,_)::clauses,subst) -> 
+         let l = Subst.apply_subst subst l in 
+         let r = Subst.apply_subst subst r in 
+           try 
+             let subst1,vl1 = Unif.unification vl [] l r in
+               Some(bag,maxvar,clauses,Subst.concat subst1 subst)
+           with FoUnif.UnificationFailure _ -> 
+             match rewrite_eq ~unify l r ty vl table with
+              | Some (id2, dir, subst1) ->
+                 let id_t = 
+                   Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r] in
+                   (match 
+                     build_new_clause bag maxvar (fun _ -> true)
+                       Terms.Superposition id_t subst1 [] id id2 (2::pos) dir 
+                   with
+                   | Some ((bag, maxvar), c) -> 
+                       Some(bag,maxvar,c::clauses,Subst.concat subst1 subst)
+                   | None -> assert false)
+             | None ->
+                 match l,r with 
+                 | Terms.Node (a::la), Terms.Node (b::lb) when 
+                     a = b && List.length la = List.length lb ->
+                      let acc,_,_,_ =
+                       List.fold_left2 
+                         (fun (acc,pre,postl,postr) a b -> 
+                             let newcl = 
+                             fun x -> contextl(Terms.Node (pre@(x::postl))) in
+                             let newcr = 
+                             fun x -> contextr(Terms.Node (pre@(x::postr))) in
+                             let newpos = List.length pre::pos in
+                             let footail l =
+                               if l = [] then [] else List.tl l in
+                               (deep_eq ~unify a b ty 
+                                newpos newcl newcr table acc,pre@[b],
+                                 footail postl, footail postr))
+                         (acc,[a],List.tl la,List.tl lb) la lb
+                     in acc
+                  | Terms.Var _, _
+                  | _, Terms.Var _ -> assert false
+                  | _,_ -> None
     ;;
-*)       
-
 
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
@@ -373,15 +404,32 @@ module Superposition (B : Terms.Blob) =
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag g_actives clause = 
       let bag, clause = demodulate bag clause table in
-      if (is_identity_clause ~unify:true clause)
+      if (is_identity_clause clause)
       then raise (Success (bag, maxvar, clause))
+(*
+      else   
+       let (id,lit,vl,_) = clause in 
+       let l,r,ty = 
+         match lit with
+           | Terms.Equation(l,r,ty,_) -> l,r,ty
+           | _ -> assert false 
+       in
+       match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) 
+         table (Some(bag,maxvar,[clause],Subst.id_subst)) with
+       | None -> 
+           if List.exists (are_alpha_eq clause) g_actives then None
+           else Some (bag, clause)
+       | Some (bag,maxvar,cl,subst) -> 
+           debug "Goal subsumed";
+           raise (Success (bag,maxvar,List.hd cl))
+*)
       else match is_subsumed ~unify:true bag maxvar clause table with
        | None -> 
            if List.exists (are_alpha_eq clause) g_actives then None
            else Some (bag, clause)
        | Some ((bag,maxvar),c) -> 
            debug "Goal subsumed";
-           raise (Success (bag,maxvar,c))
+           raise (Success (bag,maxvar,c)) 
     ;;
 
     (* =================== inference ===================== *)