X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fclauses.ml;h=f8724601cfc1e236ddc1b71d2d351ad3b0e999d2;hb=0842258ce37ce992a0d52c813a9a5cb4c3f2bb52;hp=5955fcae1d21a63e9c88be8213c64f7d9fe2de5a;hpb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/clauses.ml b/helm/software/components/ng_paramodulation/clauses.ml
index 5955fcae1..f8724601c 100644
--- a/helm/software/components/ng_paramodulation/clauses.ml
+++ b/helm/software/components/ng_paramodulation/clauses.ml
@@ -25,8 +25,8 @@ module Clauses (B : Orderings.Blob) = struct
   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
@@ -99,4 +99,14 @@ module Clauses (B : Orderings.Blob) = struct
        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