Fixed nasty bug in superposition and freshing of clauses

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 63507aea6b4aeda4c0eb16f00e52fadf09b2452a..51269d2b3956fdbcd3ec4f9cc0300ff640eea823 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -24,7 +24,7 @@ module Superposition (B : Orderings.Blob) =
     exception Success of B.t Terms.bag * int * B.t Terms.clause
 
     let debug s = prerr_endline (Lazy.force s);;
-    (* let debug _ = ();; *)
+    let debug _ = ();;
     let enable = true;;
 
     let rec list_first f = function
@@ -118,10 +118,10 @@ module Superposition (B : Orderings.Blob) =
         let vl = Clauses.vars_of_clause cl in
         let cl,maxvar = 
             if fresh then Clauses.fresh_clause ~subst maxvar (0, nlit, plit, vl, proof) 
-            else cl,maxvar
+            else (0,nlit,plit,vl,proof),maxvar
         in
         let bag, cl = 
-          Terms.add_to_bag (0, nlit, plit, vl, proof) bag
+          Terms.add_to_bag cl bag
         in
         Some (bag, maxvar, cl, literal)
       else
@@ -287,6 +287,7 @@ module Superposition (B : Orderings.Blob) =
       | _ -> false
 
     let fold_build_new_clause bag maxvar id rule filter res clause_ctx =
+      debug (lazy (string_of_int (List.length res)));
       let (bag, maxvar), res =
        HExtlib.filter_map_acc 
          (fun (bag, maxvar) (t,subst,id2,pos,dir) ->
@@ -334,6 +335,7 @@ module Superposition (B : Orderings.Blob) =
 
     let is_subsumed ~unify bag maxvar (id, nlit, plit, vl, _) table =
       match nlit,plit with
+      |  [Terms.Equation (l,r,ty,_) ,_],[] 
       | [],[Terms.Equation (l,r,ty,_) ,_]-> 
           (match rewrite_eq ~unify l r ty vl table with
             | None -> None
@@ -566,7 +568,6 @@ module Superposition (B : Orderings.Blob) =
         if no_demod then bag, clause else demodulate bag clause table 
       in
       if List.exists (Clauses.are_alpha_eq_cl clause) g_actives then None else
-      (debug (lazy (Pp.pp_clause clause));
       if (is_goal_trivial clause)
       then raise (Success (bag, maxvar, clause))
       else   
@@ -583,7 +584,7 @@ module Superposition (B : Orderings.Blob) =
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
              prerr_endline "Goal subsumed";
-             raise (Success (bag,maxvar,cl)))
+             raise (Success (bag,maxvar,cl))
 (*
       else match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)
@@ -603,11 +604,13 @@ module Superposition (B : Orderings.Blob) =
     (* this is OK for both the sup_left and sup_right inference steps *)
     let superposition table varlist is_pos subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
-      HExtlib.filter_map
+      let res = HExtlib.filter_map
         (fun (dir, is_cand_pos, _, (id,nlit,plit,vl,_ (*as uc*))) ->
            match nlit,plit with
            | [],[Terms.Equation (l,r,_,o),_] ->
                (let side, newside = if dir=Terms.Left2Right then l,r else r,l in
+               debug (lazy (Pp.pp_foterm subterm));
+               debug (lazy (Pp.pp_foterm side));
                try 
                  let subst = 
                    Unif.unification (* (varlist@vl)*)  [] subterm side 
@@ -620,14 +623,16 @@ module Superposition (B : Orderings.Blob) =
                    if o <> Terms.Lt && o <> Terms.Eq then  
                      Some (context newside, subst, id, pos, dir)
                    else 
-                     ((*prerr_endline ("Filtering: " ^ 
-                        Pp.pp_foterm side ^ " =(< || =)" ^ 
-                        Pp.pp_foterm newside);*)None)
+                     (debug (lazy "Filtering out..."); None)
                  else
                    Some (context newside, subst, id, pos, dir)
                with FoUnif.UnificationFailure _ -> None)
             | _ -> assert false)
         (IDX.ClauseSet.elements cands)
+        in
+        debug (lazy (string_of_int (List.length (IDX.ClauseSet.elements cands)) ^ " candidates"));
+        debug (lazy (string_of_int (List.length res) ^ " results"));
+        res
     ;;
 
     (* Superposes selected equation with equalities in table *)
@@ -765,7 +770,7 @@ module Superposition (B : Orderings.Blob) =
         List.fold_left (superpose_literal id vl atable false)
             (bag,maxvar,[],List.tl nlit,[]) nlit
       in
-        debug (lazy "Superposed goal with active clauses");
+        debug (lazy (string_of_int (List.length new_goals) ^ " new goals"));
         (* We simplify the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left