X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=a1ec9bc14caad983ee84a5f80a8467ef88f65ac4;hb=1c8e230b1d81491b38126900d76201fb84303ced;hp=86a964c1487f36a7f72deb0c8f2608f621ec2aac;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml
index 86a964c14..a1ec9bc14 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
@@ -208,21 +209,22 @@ module Paramod (B : Orderings.Blob) = struct
     (bag, maxvar), c
   ;;
 
-  let mk_clause bag maxvar (t,ty) =
-    let (proof,ty) = B.saturate t ty in
+(*
+  let mk_clause bag maxvar (proof,ty) =
+    let (proof,ty) = B.saturate t ty in 
     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
     let bag, c = Terms.add_to_bag c bag in
     (bag, maxvar), c
-  ;;
+  ;; *)
   
-  let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+  let mk_passive (bag,maxvar) = mk_unit_clause bag maxvar;;
 
-  let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+  let mk_goal (bag,maxvar) = mk_unit_clause bag maxvar;;
 
   let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
     let (bag,maxvar), g = mk_unit_clause bag maxvar t in
     let g_passives = g_passive_empty_set in
-    (* if the goal is not an equation we returns an empty
+    (* if the goal is not an equation we return an empty
        passive set *)
     let g_passives =
       if Terms.is_eq_clause g then add_passive_goal g_passives g
@@ -335,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"