From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 12 Jun 2009 12:33:45 +0000 (+0000)
Subject: Added a new keep_simplified function
X-Git-Tag: make_still_working~3879
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7587a7dd68463086e8a6b7c14f10c1dc33f64ba;p=helm.git

Added a new keep_simplified function
---

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 600e204c8..4142a35b6 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -191,6 +191,27 @@ module Superposition (B : Terms.Blob) =
         else Some (bag, clause)
     ;;
 
+    let rec keep_simplified (alist,atable) bag newc = 
+      match newc with
+	| [] -> bag, (alist,atable)
+	| hd::tl -> 
+	    (match simplify atable bag hd with
+	       | None -> keep_simplified (alist,atable) bag tl
+	       | 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) c ->
+			let bag, c1 = demodulate bag c ctable in
+			if (c1 == c) then 
+                          bag, newa, c :: alist, IDX.index_unit_clause atable c
+			else
+			  bag, c :: newa, alist, atable)
+		     (bag,[],[],IDX.DT.empty) alist
+		   in
+		     keep_simplified (alist, atable) bag newa)
+    ;;
+
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag clause = 
       let bag, clause = demodulate bag clause table in