Now iterating superposition

[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..f8724601cfc1e236ddc1b71d2d351ad3b0e999d2 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.ml
+++ b/helm/software/components/ng_paramodulation/clauses.ml
@@ -20,12 +20,13 @@ 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
     
-  let fresh_clause maxvar (id, nlit, plit, varlist, proof) =
-    let maxvar, varlist, subst = Utils.relocate maxvar varlist FoSubst.id_subst in
+  let fresh_clause maxvar ?(subst=FoSubst.id_subst) (id, nlit, plit, varlist, proof) =
+    let maxvar, varlist, subst = Utils.relocate maxvar varlist subst in
     let apply_subst_on_lit = function
       | Terms.Equation (l,r,ty,o) ->
           let l = FoSubst.apply_subst subst l in
@@ -81,4 +82,31 @@ 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
+    ;;
+
+  let vars_of_clause (id,nlit,plit,_,pr) = 
+    let vars_of_lit acc lit =
+      match lit with
+       | (Terms.Predicate t,_) -> Terms.vars_of_term ~start_acc:acc t
+       | (Terms.Equation (l,r,ty,o),_) ->
+            Terms.vars_of_term ~start_acc:(Terms.vars_of_term ~start_acc:acc l) r
+    in
+    List.fold_left vars_of_lit [] (nlit@plit)
+;;
+
 end