From b68e52f889215ce2c21c3d771f59b2d2057d53c1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jul 2009 10:03:44 +0000 Subject: [PATCH] more profilers --- .../components/ng_paramodulation/superposition.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index f86d4d36e..f69de41f5 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -128,6 +128,7 @@ module Superposition (B : Orderings.Blob) = let prof_demod_u = HExtlib.profile ~enable "demod.unify";; let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";; let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";; + let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";; let demod table varlist subterm = let cands = @@ -145,8 +146,14 @@ module Superposition (B : Orderings.Blob) = prof_demod_u.HExtlib.profile (Unif.unification (varlist@vl) varlist subterm) side in - let side = Subst.apply_subst subst side in - let newside = Subst.apply_subst subst newside in + let side = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) side + in + let newside = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) newside + in if o = Terms.Incomparable then let o = prof_demod_o.HExtlib.profile -- 2.39.2