almost complete superposition right step

[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 fe4b578b6c0afc80c91c394c448ebaa3f0677766..6b98ed5be24667a5c6be75049bab6f71ff0de53e 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -130,6 +130,29 @@ module Superposition (B : Terms.Blob) =
                l (superposition_right table vl)))
       | _ -> assert false
     ;;
+
+    (* the current equation is normal w.r.t. demodulation with atable
+     * (and is not the identity) *)
+    let superposition_right bag maxvar current (alist,atable) = 
+      let ctable = IDX.index_unit_clause IDX.DT.empty current in
+      let bag, maxvar, new_clauses =
+        List.fold_left 
+          (fun (bag, maxvar, acc) active ->
+             let bag, maxvar, newc = 
+               superposition_right_with_table bag maxvar active ctable 
+             in
+             bag, maxvar, newc @ acc)
+          (bag, maxvar, []) alist
+      in
+      let alist, atable = 
+        current :: alist, IDX.index_unit_clause atable current
+      in
+      let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
+      let bag, maxvar, additional_new_clauses =
+        superposition_right_with_table bag maxvar fresh_current atable 
+      in
+      bag, maxvar, (alist, atable), new_clauses @ additional_new_clauses
+    ;;
           
   end