X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=ffca04b96c7ff7b2c84f2cdde3953ed97b787df2;hb=eca915d2656084f1e58149a476a2d305758b00f9;hp=554028fa75b857c3c10ccadf73d6d5cf825404a7;hpb=cb1b4380e7133a0a7a0f22c667afbb6abd0de410;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 554028fa7..ffca04b96 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -120,7 +120,7 @@ module Superposition (B : Terms.Blob) =
                    let newside = Subst.apply_subst subst newside in
                    let o = Order.compare_terms newside side in
                    (* Riazanov, pp. 45 (ii) *)
-                   if o = Terms.Lt then  
+                   if o = Terms.Lt then
                      Some (context newside, subst, varlist, id, pos, dir)
                    else 
                      ((*prerr_endline ("Filtering: " ^ 
@@ -133,20 +133,25 @@ module Superposition (B : Terms.Blob) =
         (IDX.ClauseSet.elements cands)
     ;;
 
-    (* XXX: possible optimization, if the literal has a "side" already
-     * in normal form we should not traverse it again *)
-    let demodulate_once bag (id, literal, vl, pr) table =
+    let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table =
       (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
-        match first_position [2]
-	  (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l
-	  (demod table vl)
-	with
+	let left_position = if jump_to_right then None else
+	  first_position [2]
+	    (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l
+	    (demod table vl)
+	in
+        match left_position with
 	  | Some (newt, subst, varlist, id2, pos, dir) ->
-	      build_clause bag (fun _ -> true) Terms.Demodulation 
-		newt subst varlist id id2 pos dir
+	      begin
+		match build_clause bag (fun _ -> true) Terms.Demodulation 
+		  newt subst varlist id id2 pos dir
+		with
+		  | None -> assert false
+		  | Some x -> Some (x,false)
+	      end
 	  | None ->
 	      match first_position
 		[3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r
@@ -154,14 +159,22 @@ module Superposition (B : Terms.Blob) =
 	      with
 		| None -> None
 		| Some (newt, subst, varlist, id2, pos, dir) ->
-		    build_clause bag (fun _ -> true) Terms.Demodulation 
-		      newt subst varlist id id2 pos dir
+		    match build_clause bag (fun _ -> true)
+		      Terms.Demodulation newt subst varlist id id2 pos dir
+		    with
+			| None -> assert false
+			| Some x -> Some (x,true)
     ;;
 
-    let rec demodulate bag clause table =
-      match demodulate_once bag clause table with
+    let rec demodulate ~jump_to_right bag clause table =
+      match demodulate_once ~jump_to_right bag clause table with
       | None -> bag, clause
-      | Some (bag, clause) -> demodulate bag clause table
+      | Some ((bag, clause),r) -> demodulate ~jump_to_right:r
+	  bag clause table
+    ;;
+
+    let demodulate bag clause table = demodulate ~jump_to_right:false
+      bag clause table
     ;;
 
     (* move away *)
@@ -319,15 +332,28 @@ module Superposition (B : Terms.Blob) =
 			  bag (newa@tl)
       in
 	keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
-    ;;			
-	  
+    ;;
+
+    let are_alpha_eq cl1 cl2 =
+      let get_term (_,lit,_,_) =
+	match lit with
+	  | Terms.Predicate _ -> assert false
+	  | Terms.Equation (l,r,ty,_) ->
+	      Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+      in
+	try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
+	with FoUnif.UnificationFailure _ -> false
+;;
+
     (* this is like simplify but raises Success *)
-    let simplify_goal maxvar table bag clause = 
+    let simplify_goal maxvar table bag g_actives clause = 
       let bag, clause = demodulate bag clause table in
       if (is_identity_clause clause)
       then raise (Success (bag, maxvar, clause))
       else match is_subsumed ~unify:true bag maxvar clause table with
-	| None -> bag, clause
+	| 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))
@@ -438,6 +464,8 @@ module Superposition (B : Terms.Blob) =
       in
 	debug "Another superposition";
       let new_clauses = new_clauses @ additional_new_clauses in
+	debug (Printf.sprintf "Demodulating %d clauses"
+		 (List.length new_clauses));
       let bag, new_clauses = 
         HExtlib.filter_map_acc (simplify atable maxvar) bag new_clauses
       in
@@ -451,15 +479,16 @@ module Superposition (B : Terms.Blob) =
         superposition_with_table bag maxvar goal atable 
       in
 	debug "Superposed goal with active clauses";
-	(* We demodulate the goal with active clauses *)
+	(* We simplify the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g -> 
-            let bag, g = demodulate bag g atable in
-            bag, g :: acc) 
+	    match simplify_goal maxvar atable bag [] g with
+	      | None -> assert false
+	      | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals
       in
-	debug "Demodulated goal with active clauses";
+	debug "Simplified new goals with active clauses";
       bag, maxvar, List.rev new_goals
     ;;