X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=8070b4b5db69a2334ccc1e536009ae38895136ea;hb=a232a59672817abd3d6ec07db0b20d8b3fe5ad3b;hp=e931423b96b9d011965f13e8b1487e54c9c8c52b;hpb=b1deec2fe384585cf41368cdea782db9e33825f7;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index e931423b9..8070b4b5d 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -22,9 +22,8 @@ module Superposition (B : Terms.Blob) =
     
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
-    let debug s =
-       () (* prerr_endline s *)
-    ;;
+    let debug s = prerr_endline s;;
+    let debug _ = ();;
 
     let rec list_first f = function
       | [] -> None
@@ -178,11 +177,12 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause = function
+    let is_identity_clause ~unify = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof ->
+      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
 	  (try ignore(Unif.unification vl [] l r); true
 	  with FoUnif.UnificationFailure _ -> false)
+      | _, Terms.Equation (_,_,_,_), _, _ -> false
       | _, Terms.Predicate _, _, _ -> assert false	  
     ;;
 
@@ -252,24 +252,33 @@ module Superposition (B : Terms.Blob) =
     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) -> 
+      | Some(bag,maxvar,(id,lit,vl,p),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)
+              let lit = 
+                match lit with Terms.Predicate _ -> assert false
+                  | Terms.Equation (l,r,ty,o) -> 
+                     Terms.Equation (FoSubst.apply_subst subst1 l,
+                       FoSubst.apply_subst subst1 r, ty, o)
+	      in
+		Some(bag,maxvar,(id,lit,vl1,p),Subst.concat subst1 subst)
 	    with FoUnif.UnificationFailure _ -> 
 	      match rewrite_eq ~unify l r ty vl table with
               | Some (id2, dir, subst1) ->
+		  let newsubst = Subst.concat subst1 subst in
 		  let id_t = 
-		    Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r] in
+                    FoSubst.apply_subst newsubst
+		      (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 
+			Terms.Superposition id_t 
+			  subst1 [] id id2 (pos@[2]) dir 
 		    with
 		    | Some ((bag, maxvar), c) -> 
-			Some(bag,maxvar,c::clauses,Subst.concat subst1 subst)
+			Some(bag,maxvar,c,newsubst)
 		    | None -> assert false)
 	      | None ->
 		  match l,r with 
@@ -290,14 +299,34 @@ module Superposition (B : Terms.Blob) =
                                  footail postl, footail postr))
 			  (acc,[a],List.tl la,List.tl lb) la lb
 		      in acc
-                  | Terms.Var _, _
-                  | _, Terms.Var _ -> assert false
                   | _,_ -> None
     ;;
 
+    let rec orphan_murder bag acc i =
+      match Terms.M.find i bag with
+	| (_,_,_,Terms.Exact _),discarded -> (discarded,acc)
+	| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc)
+	| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false ->
+            if (List.mem i acc) then (false,acc)
+            else match orphan_murder bag acc i1 with
+	      | (true,acc) -> (true,acc)
+	      | (false,acc) ->
+		  let (res,acc) = orphan_murder bag acc i2 in
+		  if res then res,acc else res,i::acc
+    ;;
+
+    let orphan_murder bag actives cl =
+      let (id,_,_,_) = cl in
+      let actives = List.map (fun (i,_,_,_) -> i) actives in
+      let (res,_) = orphan_murder bag actives id in
+	if res then debug "Orphan murdered"; res
+    ;;
+
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
-      let bag, clause = demodulate bag clause table in
+      if is_identity_clause ~unify:false clause then bag,None
+      (* else if orphan_murder bag actives clause then bag,None *)
+      else let bag, clause = demodulate bag clause table in
       if is_identity_clause ~unify:false clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
@@ -305,21 +334,33 @@ module Superposition (B : Terms.Blob) =
 	  | Some _ -> bag, None
     ;;
 
+    let simplify table maxvar bag clause =
+      match simplify table maxvar bag clause with
+	| bag, None -> let (id,_,_,_) = clause in
+	    Terms.M.add id (clause,true) bag, None
+	| bag, Some clause -> bag, Some clause
+    (*let (id,_,_,_) = clause in
+	    if orphan_murder bag clause then
+	      Terms.M.add id (clause,true) bag, Some clause
+	    else bag, Some clause*)
+    ;;
+
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
-	| bag,None -> None (* new_clause has been discarded *)
+	| bag,None -> bag,None (* new_clause has been discarded *)
 	| bag,(Some clause) ->
 	    let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 	    let bag, alist, atable = 
 	      List.fold_left 
-		(fun (bag, alist, atable as acc) c ->
+		(fun (bag, alist, atable) c ->
 		   match simplify ctable maxvar bag c with
-		     |bag,None -> acc (* an active clause as been discarded *)
+		     |bag,None -> (bag,alist,atable)
+			(* an active clause as been discarded *)
 		     |bag,Some c1 ->
 			bag, c :: alist, IDX.index_unit_clause atable c)
 		(bag,[],IDX.DT.empty) alist
 	    in
-	      Some (clause, bag, (alist,atable))
+	      bag, Some (clause, (alist,atable))
     ;;
 
     let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause =
@@ -330,17 +371,19 @@ module Superposition (B : Terms.Blob) =
 	(* Simplification of new_clause with :      *
 	 * - actives and cl if new_clause is not cl *
 	 * - only actives otherwise                 *)
-	match simplify atable1 maxvar bag new_clause with
-	  | bag,None -> (Some cl, None) (* new_clause has been discarded *)
+	match
+	  simplify atable1 maxvar bag new_clause with
+	  | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
 	  | bag,Some clause ->
 	      (* Simplification of each active clause with clause *
 	       * which is the simplified form of new_clause       *)
               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 	      let bag, newa, alist, atable = 
 		List.fold_left 
-		  (fun (bag, newa, alist, atable as acc) c ->
+		  (fun (bag, newa, alist, atable) c ->
 		     match simplify ctable maxvar bag c with
-		       |bag,None -> acc (* an active clause as been discarded *)
+		       |bag,None -> (bag, newa, alist, atable)
+			  (* an active clause as been discarded *)
 		       |bag,Some c1 ->
 			    if (c1 == c) then 
 			      bag, newa, c :: alist,
@@ -350,37 +393,37 @@ module Superposition (B : Terms.Blob) =
 		  (bag,[],[],IDX.DT.empty) alist
 	      in
 		if new_cl then
-		  (Some cl, Some (clause, (alist,atable), newa, bag))
+		  bag, (Some cl, Some (clause, (alist,atable), newa))
 		else
 		  (* if new_clause is not cl, we simplify cl with clause *)
 		  match simplify ctable maxvar bag cl with
 		    | bag,None ->
 			(* cl has been discarded *)
-			(None, Some (clause, (alist,atable), newa, bag))
+			bag,(None, Some (clause, (alist,atable), newa))
 		    | bag,Some cl1 ->
-			(Some cl1, Some (clause, (alist,atable), newa, bag))
+			bag,(Some cl1, Some (clause, (alist,atable), newa))
     ;;
 
     let keep_simplified cl (alist,atable) bag maxvar =
       let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc =
 	if new_cl then
 	  match simplification_step ~new_cl cl (alist,atable) bag maxvar cl with
-	    | (None, _) -> assert false
-	    | (Some _, None) -> None
-	    | (Some _, Some (clause, (alist,atable), newa, bag)) ->
+	    | _,(None, _) -> assert false
+	    | bag,(Some _, None) -> bag,None
+	    | bag,(Some _, Some (clause, (alist,atable), newa)) ->
 		keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
 		  bag (newa@newc)
 	else
 	  match newc with
-	    | [] -> Some (cl, bag, (alist,atable))
+	    | [] -> bag, Some (cl, (alist,atable))
 	    | hd::tl ->
 		match simplification_step ~new_cl cl
 		  (alist,atable) bag maxvar hd with
-		  | (None,None) -> assert false
-		  | (Some _,None) ->
+		  | _,(None,None) -> assert false
+		  | bag,(Some _,None) ->
 		      keep_simplified_aux ~new_cl cl (alist,atable) bag tl
-		  | (None, Some _) -> None
-		  | (Some cl1, Some (clause, (alist,atable), newa, bag)) ->
+		  | bag,(None, Some _) -> bag,None
+		  | bag,(Some cl1, Some (clause, (alist,atable), newa)) ->
 		      let alist,atable =
 			(clause::alist, IDX.index_unit_clause atable clause)
 		      in
@@ -402,11 +445,13 @@ 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 clause)
+    let simplify_goal ~no_demod maxvar table bag g_actives clause = 
+      let bag, clause = 
+	if no_demod then bag, clause else demodulate bag clause table 
+      in
+      if List.exists (are_alpha_eq clause) g_actives then None else
+      if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
-(*
       else   
 	let (id,lit,vl,_) = clause in 
 	let l,r,ty = 
@@ -415,21 +460,18 @@ module Superposition (B : Terms.Blob) =
 	    | _ -> 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)
+	  table (Some(bag,maxvar,clause,Subst.id_subst)) with
+	| None -> Some (bag,clause)
 	| Some (bag,maxvar,cl,subst) -> 
-	    debug "Goal subsumed";
-	    raise (Success (bag,maxvar,List.hd cl))
-*)
+	    prerr_endline "Goal subsumed";
+	    raise (Success (bag,maxvar,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)
+	| None -> Some (bag, clause)
 	| Some ((bag,maxvar),c) -> 
-	    debug "Goal subsumed";
-	    raise (Success (bag,maxvar,c)) 
+	    prerr_endline "Goal subsumed";
+	    raise (Success (bag,maxvar,c))
+*) 
     ;;
 
     (* =================== inference ===================== *)
@@ -556,7 +598,7 @@ module Superposition (B : Terms.Blob) =
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g -> 
-	    match simplify_goal maxvar atable bag [] g with
+	    match simplify_goal ~no_demod:false maxvar atable bag [] g with
 	      | None -> assert false
 	      | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals