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 600e204c850b44531e3d97ac90a699203db70542..4142a35b67205f1cc19638931420260b74a2fd7f 100644 (file)
--- 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