From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 Dec 2009 15:47:38 +0000 (+0000)
Subject: Minor fixing for last chance
X-Git-Tag: make_still_working~3179
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0590a3073dae55f31e79c71e3ed2a4d66a851a0d;p=helm.git

Minor fixing for last chance
---

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";;