X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=51bd67286f0dc498886df771a0ae18cd2f91a8a8;hb=2701c980f48541dd5e8317b5a5661b439ced8b29;hp=d85c5627a4e4b4e97d1a9e667253dac41cd7aecb;hpb=65e1aa022da79a3a880f5c2d5d0d512b80e50635;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index d85c5627a..51bd67286 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let debug s = prerr_endline s ;;
+(* let debug s = prerr_endline s ;;*)
 let debug _ = ();;
     
 module Paramod (B : Terms.Blob) = struct
@@ -49,8 +49,10 @@ module Paramod (B : Terms.Blob) = struct
       passives_w,passives_a
   ;;
 
-  let add_passive_clauses (passives_w,passives_a) new_clauses =
-    let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
+  let add_passive_clauses ?(no_weight=false)
+      (passives_w,passives_a) new_clauses =
+    let new_clauses_w,new_clauses_a =
+      List.fold_left (add_passive_clause ~no_weight)
       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
       (WeightPassiveSet.union new_clauses_w passives_w,
@@ -172,22 +174,22 @@ module Paramod (B : Terms.Blob) = struct
 
     let use_age = iterno mod 10 = 0 in
 
-    let rec aux_select passives g_passives =
+    let rec aux_select bag passives g_passives =
       let backward,current,passives,g_passives =
 	select ~use_age:false passives g_passives
       in
 	if backward then
 	 match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
-	    | None -> aux_select passives g_passives
-	    | Some x -> let bag,g_current = x in
+	    | None -> aux_select bag passives g_passives
+	    | Some (bag,g_current) ->
 		backward_infer_step bag maxvar actives passives
 	          g_actives g_passives g_current
 	else
 	  (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
           match Sup.keep_simplified current actives bag maxvar with
 	(*  match Sup.one_pass_simplification current actives bag maxvar with*)
-	      | None -> aux_select passives g_passives
-	      | Some x -> let (current, bag, actives) = x in
+	      | bag,None -> aux_select bag passives g_passives
+	      | bag,Some (current,actives) ->
 		  forward_infer_step bag maxvar actives passives
 		                     g_actives g_passives current
     in
@@ -198,7 +200,7 @@ module Paramod (B : Terms.Blob) = struct
 	  (fst actives)); *)
 
     let bag,maxvar,actives,passives,g_actives,g_passives =      
-      aux_select passives g_passives
+      aux_select bag passives g_passives
     in
       debug
 	(Printf.sprintf "Number of active goals : %d"
@@ -218,8 +220,12 @@ module Paramod (B : Terms.Blob) = struct
 
   let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
-    let passives = add_passive_clauses passive_empty_set passives in
-    let g_passives = add_passive_clauses passive_empty_set g_passives in
+    let passives =
+      add_passive_clauses ~no_weight:true passive_empty_set passives
+    in
+    let g_passives =
+      add_passive_clauses ~no_weight:true passive_empty_set g_passives
+    in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try