1) NCicLibrary (which is untrusted) moved after NCicUntrusted.

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 600e204c850b44531e3d97ac90a699203db70542..046799a775149470bd7162252b023e582ffb9e99 100644 (file)
--- 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 =