X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=86a964c1487f36a7f72deb0c8f2608f621ec2aac;hb=dd29593d12cffd332c9d546167215f42a90fa9f7;hp=4b9d29e1c59ee780ebc8631a6869d2ad0ebe3500;hpb=8c678be0b7ee11a60f21b002553cc414f1d18267;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 4b9d29e1c..86a964c14 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -13,7 +13,7 @@
 
 let print s = prerr_endline (Lazy.force s) ;; 
 let noprint s = ();;  
-let debug = print;;
+let debug = noprint;;
 
 let monster = 100;;
     
@@ -202,6 +202,12 @@ module Paramod (B : Orderings.Blob) = struct
     else WeightPassiveSet.min_elt passives_w
   ;;
 
+  let mk_unit_clause bag maxvar (t,ty) =
+    let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in
+    let bag, c = Terms.add_to_bag c bag in
+    (bag, maxvar), c
+  ;;
+
   let mk_clause bag maxvar (t,ty) =
     let (proof,ty) = B.saturate t ty in
     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
@@ -210,9 +216,11 @@ module Paramod (B : Orderings.Blob) = struct
   ;;
   
   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+
   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+
   let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
-    let (bag,maxvar), g = mk_goal (bag,maxvar) t in
+    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
        passive set *)
@@ -268,7 +276,7 @@ module Paramod (B : Orderings.Blob) = struct
 	(List.map Pp.pp_unit_clause actives_l)))
       ^ 
       ("Passives:" ^(String.concat ";\n" 
-        (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+        (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
 	       (IDX.ClauseSet.elements wset))))
   ;;
 
@@ -287,7 +295,7 @@ module Paramod (B : Orderings.Blob) = struct
      * P' = P + new'          *)
     debug (lazy "Forward infer step...");
     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
-    debug (lazy (pp_clauses actives passives));
+    noprint (lazy (pp_clauses actives passives));
     match Sup.keep_simplified current actives bag maxvar
     with
       | _,None -> s
@@ -356,7 +364,7 @@ module Paramod (B : Orderings.Blob) = struct
     let _ = noprint
       (lazy 
 	 ("Passives:" ^(String.concat ";\n" 
-	    (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+	    (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
 	       (IDX.ClauseSet.elements wset))))) in 
     let g_passives = 
       WeightPassiveSet.fold 
@@ -559,14 +567,16 @@ module Paramod (B : Orderings.Blob) = struct
 let demod s goal =
   let bag,maxvar,actives,passives,g_actives,g_passives = s in
   let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+  let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+    if g1 = g then GaveUp else compute_result bag i []
+(*
   if Terms.is_eq_clause g then 
-    let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
-      if g1 = g then GaveUp else compute_result bag i []
-  else GaveUp
+
+  else GaveUp *)
 
 let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
-  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  if is_passive_g_set_empty g_passives then Error "not an equation"
   else
   try 
     goal_narrowing 0 2 None s