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 64cc35bd4e3a41e8331bb0ec071bbb9e5f30826f..6b98ed5be24667a5c6be75049bab6f71ff0de53e 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -18,6 +18,7 @@ module Superposition (B : Terms.Blob) =
     module Subst = FoSubst.Subst(B)
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
+    module Pp = Pp.Pp(B)
 
     let all_positions pos ctx t f =
       let rec aux pos ctx = function
@@ -41,7 +42,7 @@ module Superposition (B : Terms.Blob) =
     let superposition_right table varlist subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
       HExtlib.filter_map
-        (fun (dir, (id,lit,vl,_)) ->
+        (fun (dir, (id,lit,vl,_ (*as uc*))) ->
            match lit with
            | Terms.Predicate _ -> assert false
            | Terms.Equation (l,r,_,o) ->
@@ -59,7 +60,10 @@ module Superposition (B : Terms.Blob) =
                    if o <> Terms.Lt && o <> Terms.Eq then  
                      Some (context newside, subst, varlist, id, pos, dir)
                    else 
-                     None
+                     ((*prerr_endline ("Filtering: " ^ 
+                        Pp.pp_foterm side ^ " =(< || =)" ^ 
+                        Pp.pp_foterm newside ^ " coming from " ^ 
+                        Pp.pp_unit_clause uc );*)None)
                  else
                    Some (context newside, subst, varlist, id, pos, dir)
                with FoUnif.UnificationFailure _ -> None)
@@ -84,7 +88,7 @@ module Superposition (B : Terms.Blob) =
         in
         Some (bag, maxvar, uc)
       else
-        None
+        ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
     ;;
 
     let fold_build_new_clause bag maxvar id filter res =
@@ -126,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