Ported demodulation on clauses

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

diff --git a/helm/software/components/ng_paramodulation/clauses.ml b/helm/software/components/ng_paramodulation/clauses.ml
index 895d3865e792e295522e16ef4d71a0b6bc3ed085..5955fcae1d21a63e9c88be8213c64f7d9fe2de5a 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.ml
+++ b/helm/software/components/ng_paramodulation/clauses.ml
@@ -20,6 +20,7 @@ module type Blob =
 module Clauses (B : Orderings.Blob) = struct
   module Order = B;;
   module Utils = FoUtils.Utils(B)
+  module Unif = FoUnif.FoUnif(B)
 
   let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
   let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
@@ -81,4 +82,21 @@ module Clauses (B : Orderings.Blob) = struct
     id1 - id2
   ;;
 
+  let are_alpha_eq_cl cl1 cl2 =
+    let (_,nlit1,plit1,_,_) = cl1 in
+    let (_,nlit2,plit2,_,_) = cl2 in
+    let alpha_eq (lit1,_) (lit2,_) =
+       let get_term lit =
+       match lit with
+          | Terms.Predicate _ -> assert false
+          | Terms.Equation (l,r,ty,_) ->
+              Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+       in
+       try ignore(Unif.alpha_eq (get_term lit1) (get_term lit2)) ; true
+       with FoUnif.UnificationFailure _ -> false
+    in
+       try (List.for_all2 alpha_eq nlit1 nlit2 && List.for_all2 alpha_eq plit1 plit2)
+       with Invalid_argument _ -> false
+    ;;
+
 end