X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=137cb458672901fb8d3603cc7d79537dfe053105;hb=39a2078b0e835d39895a5b6c0862d668ece544f3;hp=f3afc16f46e1047615f089808d648d485623bf34;hpb=95a14ced97592a4116485f94c6ffa806feb62dbc;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index f3afc16f4..137cb4586 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -28,7 +28,8 @@ module type Paramod =
     type bag = t Terms.bag * int
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
-    val paramod : 
+    val paramod :
+      useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 
@@ -184,6 +185,7 @@ module Paramod (B : Orderings.Blob) = struct
      * new'= demod A'' new    *
      * P' = P + new'          *)
     debug "Forward infer step...";
+    debug ("Number of actives : " ^ (string_of_int (List.length (fst actives))));
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
@@ -341,12 +343,12 @@ module Paramod (B : Orderings.Blob) = struct
       debug
         (Printf.sprintf "Number of passives : %d"
            (passive_set_cardinal passives));
-      given_clause ~noinfer
+      given_clause ~useage ~noinfer
         bag maxvar iterno weight_picks max_steps timeout 
         actives passives g_actives g_passives
   ;;
 
-  let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+  let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
     let passives =
       add_passive_clauses ~no_weight:true passive_empty_set passives
@@ -357,7 +359,7 @@ module Paramod (B : Orderings.Blob) = struct
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
-     given_clause ~noinfer:false
+     given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
     with 
     | Sup.Success (bag, _, (i,_,_,_)) ->