X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=6ec6048de9147191b13cfd96b14b5e763df8c255;hb=88efee4c688d660d2205c5933d302770acb5b407;hp=6a2950b0e3da34514327d96f988bb0599e50d3c9;hpb=946065280df015323ce624769fd0c4261f8b4209;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6a2950b0e..6ec6048de 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -20,7 +20,11 @@ module Superposition (B : Orderings.Blob) =
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
     
-    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+    exception Success of 
+      B.t Terms.bag 
+      * int 
+      * B.t Terms.unit_clause
+      * B.t Terms.substitution
 
     (* let debug s = prerr_endline (Lazy.force s);; *)
     let debug _ = ();; 
@@ -243,10 +247,12 @@ module Superposition (B : Orderings.Blob) =
                      ((*prerr_endline ("Filtering: " ^ 
                         Pp.pp_foterm side ^ " =(< || =)" ^ 
                         Pp.pp_foterm newside ^ " coming from " ^ 
-                        Pp.pp_unit_clause uc );*)None)
+                        Pp.pp_unit_clause uc );*)
+		       debug (lazy "not applied");None)
                  else
                    Some (newside, subst, id, dir)
-               with FoUnif.UnificationFailure _ -> None)
+               with FoUnif.UnificationFailure _ -> 
+                 debug (lazy "not applied"); None)
         (IDX.ClauseSet.elements cands)
     ;;
 
@@ -264,7 +270,7 @@ module Superposition (B : Orderings.Blob) =
     ;;
       
     let rec demodulate bag (id, literal, vl, pr) table =
-      debug (lazy "demodulate...");
+      debug (lazy ("demodulate " ^ (string_of_int id)));
        match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
@@ -311,15 +317,21 @@ module Superposition (B : Orderings.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause ~unify = function
+    let is_identity_clause = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
-          (try ignore(Unif.unification (* vl *) [] l r); true
-          with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Equation (_,_,_,_), _, _ -> false
       | _, Terms.Predicate _, _, _ -> assert false          
     ;;
 
+    let is_identity_goal = function
+      | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some []
+      | _, Terms.Equation (l,r,_,_), vl, proof ->
+          (try Some (Unif.unification (* vl *) [] l r)
+           with FoUnif.UnificationFailure _ -> None)
+      | _, Terms.Equation (_,_,_,_), _, _ -> None
+      | _, Terms.Predicate _, _, _ -> assert false          
+    ;;
+
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
       let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
       (Subst.apply_subst subst t)) subst in
@@ -342,7 +354,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
@@ -476,10 +487,10 @@ module Superposition (B : Orderings.Blob) =
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause =
       debug (lazy "simplify...");
-      if is_identity_clause ~unify:false clause then bag,None
+      if is_identity_clause clause then bag,None
       (* else if orphan_murder bag actives clause then bag,None *)
       else let bag, clause = demodulate bag clause table in
-      if is_identity_clause ~unify:false clause then bag,None
+      if is_identity_clause clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
           | None -> bag, Some clause
@@ -609,11 +620,14 @@ module Superposition (B : Orderings.Blob) =
         if no_demod then bag, clause else demodulate bag clause table 
       in
       if List.exists (are_alpha_eq clause) g_actives then None
-      else if (is_identity_clause ~unify:true clause)
-      then raise (Success (bag, maxvar, clause))
-      else   
+      else match (is_identity_goal clause) with
+	| Some subst -> raise (Success (bag,maxvar,clause,subst))
+	| None ->
         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 +638,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,subst))
 (*
-      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";;
@@ -738,6 +752,10 @@ module Superposition (B : Orderings.Blob) =
              bag, maxvar, newc @ acc)
           (bag, maxvar, []) alist
       in
+        debug
+	(lazy 
+	 ("New clauses :" ^ (String.concat ";\n" 
+	    (List.map Pp.pp_unit_clause new_clauses)))); 
         debug (lazy "First superpositions");
         (* We add current to active clauses so that it can be *
          * superposed with itself                             *)