X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=83845673b3142cf1805323034983fc316bf957c1;hb=4f3b04e9966484011328d5b0eb358da4416e29b0;hp=33f802f7f036caf9152d65de93a4c3cabce55842;hpb=d0d2ebcf0ad48c38dcd69142f5e080e987fc5536;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml
index 33f802f7f..83845673b 100644
--- a/matitaB/components/ng_paramodulation/paramod.ml
+++ b/matitaB/components/ng_paramodulation/paramod.ml
@@ -30,6 +30,7 @@ module type Paramod =
     type bag = t Terms.bag * int
     type state
     val empty_state : state
+    val size_of_state : state -> int*int
     val bag_of_state : state -> bag
     val replace_bag: state -> bag -> state
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
@@ -336,6 +337,8 @@ module Paramod (B : Orderings.Blob) = struct
     add_passive_goals g_passives new_goals
   ;;
 
+  let size_of_state (_,_,(a,_),p,_,_) = List.length a, passive_set_cardinal p;;
+
   let debug_status (_,_,actives,passives,g_actives,g_passives) =
     lazy
       ((Printf.sprintf "Number of active goals : %d\n"