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 5955fcae1d21a63e9c88be8213c64f7d9fe2de5a..f8724601cfc1e236ddc1b71d2d351ad3b0e999d2 100644 (file)
--- 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