X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=046799a775149470bd7162252b023e582ffb9e99;hb=134d8273511016e9b6de3423d301a080046f3948;hp=600e204c850b44531e3d97ac90a699203db70542;hpb=3a4481e963c6b6e78ad1dce05d75bea992ceaaed;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 600e204c8..046799a77 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -191,6 +191,67 @@ module Superposition (B : Terms.Blob) =
         else Some (bag, clause)
     ;;
 
+    let simplification_step ~new_cl cl (alist,atable) bag new_clause =
+      let atable1 =
+	if new_cl then atable else
+	IDX.index_unit_clause atable cl
+      in
+	match simplify atable1 bag new_clause with
+	  | None -> (Some cl, None)
+	  | Some (bag, 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 ->
+		     match simplify ctable bag c with
+		       |None -> acc
+		       |Some (bag, c1) ->
+			    if (c1 == c) then 
+			      bag, newa, c :: alist,
+			    IDX.index_unit_clause atable c
+			    else
+			      bag, c1 :: newa, alist, atable)		  
+		  (bag,[],[],IDX.DT.empty) alist
+	      in
+		if new_cl then
+		  (Some cl, Some (clause, (alist,atable), newa, bag))
+		else
+		  match simplify ctable bag cl with
+		    | None ->
+			(None, Some (clause, (alist,atable), newa, bag))
+		    | Some (bag,cl1) ->
+			(Some cl1, Some (clause, (alist,atable), newa, bag))
+    ;;
+
+    let keep_simplified cl (alist,atable) bag =
+      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 cl with
+	    | (None, _) -> assert false
+	    | (Some _, None) -> None
+	    | (Some _, Some (clause, (alist,atable), newa, bag)) ->
+		keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
+		  bag (newa@newc)
+	else
+	  match newc with
+	    | [] -> Some (cl, bag, (alist,atable))
+	    | hd::tl ->
+		match simplification_step ~new_cl cl
+		  (alist,atable) bag hd with
+		  | (None,None) -> assert false
+		  | (Some _,None) ->
+		      keep_simplified_aux ~new_cl cl (alist,atable) bag tl
+		  | (None, Some _) -> None
+		  | (Some cl1, Some (clause, (alist,atable), newa, bag)) ->
+		      let alist,atable =
+			(clause::alist, IDX.index_unit_clause atable clause)
+		      in
+			keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
+			  bag (newa@tl)
+      in
+	keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
+    ;;			
+	  
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag clause = 
       let bag, clause = demodulate bag clause table in
@@ -285,14 +346,16 @@ module Superposition (B : Terms.Blob) =
     (* the current equation is normal w.r.t. demodulation with atable
      * (and is not the identity) *)
     let infer_right bag maxvar current (alist,atable) = 
-      (* We demodulate actives clause with current *)
+      (* We demodulate actives clause with current until all *
+       * active clauses are reduced w.r.t each other         *)
+      (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
-      let bag, (alist, atable) = 
+      (* let bag, (alist, atable) = 
         let bag, alist = 
           HExtlib.filter_map_acc (simplify ctable) bag alist
         in
         bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
-      in
+      in*)
 	debug "Simplified active clauses with fact";
       (* We superpose active clauses with current *)
       let bag, maxvar, new_clauses =