From b1deec2fe384585cf41368cdea782db9e33825f7 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 25 Jun 2009 15:55:14 +0000
Subject: [PATCH] First version of deep_subsumption.

---
 .../ng_paramodulation/superposition.ml        | 84 +++++++++++++++----
 1 file changed, 66 insertions(+), 18 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 8e77936c8..e931423b9 100644
--- 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 ===================== *)
-- 
2.39.2