Fixed (yet another) nasty bug, in deep_eq this time

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 51269d2b3956fdbcd3ec4f9cc0300ff640eea823..fd7be3b7e0478430f98aadb0fb23b194ce909f3a 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -123,6 +123,7 @@ module Superposition (B : Orderings.Blob) =
         let bag, cl = 
           Terms.add_to_bag cl bag
         in
+        debug (lazy (Pp.pp_clause cl));
         Some (bag, maxvar, cl, literal)
       else
         ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
@@ -228,7 +229,7 @@ module Superposition (B : Orderings.Blob) =
          | Some ((bag, id, lit),jump) ->
              demod_lit ~jump_to_right:jump bag id lit clause_ctx
       in
-      (*let cmp_bag,cmp_cl = match nlit,plit with
+      (*match nlit,plit with
       |[],[lit,_] ->
         let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> nlit, [l,true])
         in
@@ -239,8 +240,7 @@ module Superposition (B : Orderings.Blob) =
         in
         let cl,_,_ = Terms.get_from_bag id bag in
         bag,cl
-      |_ -> assert false
- in*)
+      |_ -> assert false*)
       let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id
        else List.fold_left
        (fun (pre,post,bag,id) (lit,sel) ->
@@ -354,7 +354,7 @@ module Superposition (B : Orderings.Blob) =
     let rec deep_eq ~unify l r ty pos contextl contextr table acc =
       match acc with 
       | None -> None
-      | Some(bag,maxvar,(id,nlit,plit,vl,p),subst) -> 
+      | Some(bag,maxvar,(id,nlit,plit,vl,p as cl),subst) -> 
           let l = Subst.apply_subst subst l in 
           let r = Subst.apply_subst subst r in 
             try 
@@ -364,9 +364,9 @@ module Superposition (B : Orderings.Blob) =
                   | [Terms.Equation (l,r,ty,o),_],[] -> 
                      Terms.Equation (FoSubst.apply_subst subst1 l,
                        FoSubst.apply_subst subst1 r, ty, o)
-                  | _ -> assert false
+                  | _ -> debug (lazy (Pp.pp_clause cl));assert false
               in
-                Some(bag,maxvar,(id,[],[lit,true],vl,p),Subst.concat subst1 subst)
+                Some(bag,maxvar,(id,[lit,true],[],vl,p),Subst.concat subst1 subst)
             with FoUnif.UnificationFailure _ -> 
               match rewrite_eq ~unify l r ty vl table with
               | Some (id2, dir, subst1) ->
@@ -378,7 +378,7 @@ module Superposition (B : Orderings.Blob) =
                     (match 
                       build_clause ~fresh:true bag maxvar (fun _ -> true)
                         Terms.Superposition id_t 
-                        subst1 id id2 (pos@[2]) dir (fun l -> [],[l,true])
+                        subst1 id id2 (pos@[2]) dir (fun l -> [l,true],[])
                     with
                     | Some (bag, maxvar, c, _) -> 
                         Some(bag,maxvar,c,newsubst)
@@ -604,7 +604,7 @@ 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
-      let res = HExtlib.filter_map
+      HExtlib.filter_map
         (fun (dir, is_cand_pos, _, (id,nlit,plit,vl,_ (*as uc*))) ->
            match nlit,plit with
            | [],[Terms.Equation (l,r,_,o),_] ->
@@ -629,10 +629,6 @@ module Superposition (B : Orderings.Blob) =
                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 *)
@@ -732,17 +728,18 @@ module Superposition (B : Orderings.Blob) =
          * variables clauses refer to are known.                 *)
       let bag, (id,nlit,plit,vl,_) = Terms.add_to_bag fresh_current bag in
         (* We superpose current with active clauses *)
-      let bag, maxvar, _, _, new_clauses =
-         if nlit = [] then bag,maxvar,[],[],new_clauses
+      let bag, maxvar, _, _, additional_new_clauses =
+         if nlit = [] then bag,maxvar,[],[],[]
          else List.fold_left
-         (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,new_clauses) nlit
+         (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,[]) nlit
       in
-      let bag, maxvar, _, _, new_clauses =
-         if plit = [] then bag,maxvar,[],[],new_clauses
+      let bag, maxvar, _, _, additional_new_clauses =
+         if plit = [] then bag,maxvar,[],[],[]
          else List.fold_left
-          (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,new_clauses) plit
+          (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,additional_new_clauses) plit
       in 
         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 =