X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.ml;h=61b027d72d690cd564291ac813cb70f0324ca4e2;hb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;hp=169d19b80b68a52d0eb062162464e451a96a5757;hpb=772def9075b7b62870ebf4cecec6bcd37a549b1d;p=helm.git diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 169d19b80..61b027d72 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -18,7 +18,7 @@ type 'a foterm = type 'a substitution = (int * 'a foterm) list -type comparison = Lt | Eq | Gt | Incomparable +type comparison = Lt | Eq | Gt | Incomparable | Invertible type rule = Superposition | Demodulation type direction = Left2Right | Right2Left | Nodir @@ -46,6 +46,19 @@ type 'a unit_clause = type 'a passive_clause = int * 'a unit_clause (* weight * equation *) +let is_eq_clause (_,l,_,_) = + match l with + | Equation _ -> true + | Predicate _ -> false +;; + +let vars_of_term t = + let rec aux acc = function + | Leaf _ -> acc + | Var i -> if (List.mem i acc) then acc else i::acc + | Node l -> List.fold_left aux acc l + in aux [] t +;; module OT = struct