snapshot

[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..fe4b578b6c0afc80c91c394c448ebaa3f0677766 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 =