X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=fad0a12d28a7df72ad7acad75eb45abf0d70efbe;hb=0590a3073dae55f31e79c71e3ed2a4d66a851a0d;hp=6a2950b0e3da34514327d96f988bb0599e50d3c9;hpb=3ca99dabf7d136ebd58fa61e7a2d7134c8dc365c;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6a2950b0e..fad0a12d2 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -342,7 +342,6 @@ module Superposition (B : Orderings.Blob) =
       in
        bag, maxvar, res
     ;;
-
     
     let rewrite_eq ~unify l r ty vl table =
       let retrieve = if unify then IDX.DT.retrieve_unifiables
@@ -613,7 +612,10 @@ module Superposition (B : Orderings.Blob) =
       then raise (Success (bag, maxvar, clause))
       else   
         let (id,lit,vl,_) = clause in 
-        if vl = [] then Some (bag,clause)
+        (* this optimization makes sense only if we demodulated, since in 
+	   that case the clause should have been turned into an identity *)
+        if (vl = [] && not(no_demod)) 
+	then Some (bag,clause)
         else
          let l,r,ty = 
            match lit with
@@ -624,15 +626,15 @@ module Superposition (B : Orderings.Blob) =
            table (Some(bag,maxvar,clause,Subst.id_subst)) with
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
-             prerr_endline "Goal subsumed";
-             raise (Success (bag,maxvar,cl))
+             debug (lazy "Goal subsumed");
+             raise (Success (bag,maxvar,cl)))
 (*
-      else match is_subsumed ~unify:true bag maxvar clause table with
+        match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)
         | Some ((bag,maxvar),c) -> 
             prerr_endline "Goal subsumed";
             raise (Success (bag,maxvar,c))
-*) 
+*)
     ;;
 
     let prof_simplify_goal = HExtlib.profile ~enable "simplify_goal";;