From 546e74b52ee86a69cb735c699098dbf64274cf54 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 2 Dec 2009 09:45:42 +0000 Subject: [PATCH] Added a boolean test function to discriminate equations from predicates --- helm/software/components/ng_paramodulation/terms.ml | 5 +++++ helm/software/components/ng_paramodulation/terms.mli | 1 + 2 files changed, 6 insertions(+) diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 3947107ea..61b027d72 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -46,6 +46,11 @@ 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 diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 0146dba2c..03bdddb89 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -52,6 +52,7 @@ type 'a unit_clause = type 'a passive_clause = int * 'a unit_clause (* weight * equation *) +val is_eq_clause : 'a unit_clause -> bool val vars_of_term : 'a foterm -> int list module M : Map.S with type key = int -- 2.39.2