X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=47119d4770e25beab157df62540aa120c0d1533e;hb=2041f4fefe300f77338f6aea598f025f84db1bbc;hp=0dbac61c3be98ac41ab5f212727a5f8a3be946e2;hpb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 0dbac61c3..47119d477 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -14,15 +14,16 @@
 module Superposition (B : Orderings.Blob) = 
   struct
     module IDX = Index.Index(B)
-    module Unif = FoUnif.Founif(B)
+    module Unif = FoUnif.FoUnif(B)
     module Subst = FoSubst 
     module Order = B
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
+    module Clauses = Clauses.Clauses(B)
     
     exception Success of B.t Terms.bag * int * B.t Terms.clause
 
-    let debug s = prerr_endline s;;
+    let debug s = prerr_endline (Lazy.force s);;
     let debug _ = ();;
     let enable = true;;
 
@@ -194,6 +195,7 @@ module Superposition (B : Orderings.Blob) =
 
     let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table =
      match nlit,plit with
+     |[literal,_], []
      |[],[literal,_] ->
       (match literal with
       | Terms.Predicate t -> assert false
@@ -259,8 +261,7 @@ module Superposition (B : Orderings.Blob) =
       | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
           (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
-      | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false
-      | _ -> assert false
+      | _ -> false
     ;;
 
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
@@ -410,7 +411,7 @@ module Superposition (B : Orderings.Blob) =
       let (id,_,_,_,_) = cl in
       let actives = List.map (fun (i,_,_,_,_) -> i) actives in
       let (res,_) = orphan_murder bag actives id in
-        if res then debug "Orphan murdered"; res
+        if res then debug (lazy "Orphan murdered"); res
     ;;
     let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";;
     let orphan_murder bag actives x =
@@ -588,6 +589,7 @@ module Superposition (B : Orderings.Blob) =
     (* this is OK for both the sup_left and sup_right inference steps *)
     let superposition table varlist subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
+      debug (lazy (string_of_int (IDX.ClauseSet.cardinal cands) ^ " candidates found"));
       HExtlib.filter_map
         (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) ->
            match nlit,plit with
@@ -669,7 +671,7 @@ module Superposition (B : Orderings.Blob) =
         in
         bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist)
       in*)
-        debug "Simplified active clauses with fact";
+        debug (lazy "Simplified active clauses with fact");
       (* We superpose active clauses with current *)
       let bag, maxvar, new_clauses =
         List.fold_left 
@@ -680,14 +682,14 @@ module Superposition (B : Orderings.Blob) =
              bag, maxvar, newc @ acc)
           (bag, maxvar, []) alist
       in
-        debug "First superpositions";
+        debug (lazy "First superpositions");
         (* We add current to active clauses so that it can be *
          * superposed with itself                             *)
       let alist, atable = 
         current :: alist, IDX.index_clause atable current
       in
-        debug "Indexed";
-      let fresh_current, maxvar = Utils.fresh_clause maxvar current in
+        debug (lazy "Indexed");
+      let fresh_current, maxvar = Clauses.fresh_clause maxvar current in
         (* We need to put fresh_current into the bag so that all *
          * variables clauses refer to are known.                 *)
       let bag, fresh_current = Terms.add_to_bag fresh_current bag in
@@ -695,14 +697,14 @@ module Superposition (B : Orderings.Blob) =
       let bag, maxvar, additional_new_clauses =
         superposition_with_table bag maxvar fresh_current atable 
       in
-        debug "Another superposition";
+        debug (lazy "Another superposition");
       let new_clauses = new_clauses @ additional_new_clauses in
         debug (lazy (Printf.sprintf "Demodulating %d clauses"
                  (List.length new_clauses)));
       let bag, new_clauses = 
         HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
       in
-        debug "Demodulated new clauses";
+        debug (lazy "Demodulated new clauses");
       bag, maxvar, (alist, atable), new_clauses
     ;;
 
@@ -718,7 +720,7 @@ module Superposition (B : Orderings.Blob) =
       let bag, maxvar, new_goals =        
         superposition_with_table bag maxvar goal atable 
       in
-        debug "Superposed goal with active clauses";
+        debug (lazy "Superposed goal with active clauses");
         (* We simplify the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left
@@ -728,7 +730,7 @@ module Superposition (B : Orderings.Blob) =
               | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals
       in
-        debug "Simplified new goals with active clauses";
+        debug (lazy "Simplified new goals with active clauses");
       bag, maxvar, List.rev new_goals
     ;;