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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c1c0612b1..8070b4b5d 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -22,7 +22,7 @@ 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
@@ -313,18 +313,19 @@ module Superposition (B : Terms.Blob) =
 	      | (false,acc) ->
 		  let (res,acc) = orphan_murder bag acc i2 in
 		  if res then res,acc else res,i::acc
-;;
+    ;;
 
-    let orphan_murder bag cl =
+    let orphan_murder bag actives cl =
       let (id,_,_,_) = cl in
-      let (res,_) = orphan_murder bag [] id 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 = 
       if is_identity_clause ~unify:false clause then bag,None
-      (* else if orphan_murder bag 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
@@ -338,7 +339,11 @@ module Superposition (B : Terms.Blob) =
 	| 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
@@ -366,7 +371,8 @@ 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
+	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 *
@@ -439,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
+    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 = 
@@ -453,20 +461,17 @@ module Superposition (B : Terms.Blob) =
 	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)
+	| None -> Some (bag,clause)
 	| Some (bag,maxvar,cl,subst) -> 
 	    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) -> 
 	    prerr_endline "Goal subsumed";
-	    raise (Success (bag,maxvar,c))*) 
+	    raise (Success (bag,maxvar,c))
+*) 
     ;;
 
     (* =================== inference ===================== *)
@@ -593,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