New demodulation (innermost, optimized to avoid reducing already normalized

subterms).

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 994a141c93f5d8215ac4f7e9930b6528aa1e6cfe..53d2958d1c2d1788fc2ff36ac843a9d2b864aafe 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -22,8 +22,8 @@ module Superposition (B : Orderings.Blob) =
     
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
-    let debug s = prerr_endline s;;
-    let debug _ = ();;
+    (* let debug s = prerr_endline s;; *)
+    let debug _ = ();; 
     let enable = true;;
 
     let rec list_first f = function
@@ -95,11 +95,40 @@ module Superposition (B : Orderings.Blob) =
                   (bag, [hd], List.tl l, id) l
               in
                 bag, Terms.Node l, id
-            else bag,t,id1
+            else bag,t,id1 
+            (* else aux bag pos ctx id1 t *) 
       | _ -> assert false
       in
         aux bag pos ctx id t
     ;;
+
+    let visit bag pos ctx id t f =
+      let rec aux bag pos ctx id subst = function
+      | Terms.Leaf _ as t -> 
+         let  bag,subst,t,id = f bag t pos ctx id
+         in assert (subst=[]); bag,t,id
+      | Terms.Var i as t ->  
+         let t= Subst.apply_subst subst t in
+           bag,t,id
+      | Terms.Node (hd::l) ->
+          let bag, l, _, id = 
+            List.fold_left
+              (fun (bag,pre,post,id) t ->
+                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
+                 let newpos = (List.length pre)::pos in
+                 let bag,newt,id = aux bag newpos newctx id subst t in
+                   if post = [] then bag, pre@[newt], [], id
+                   else bag, pre @ [newt], List.tl post, id)
+              (bag, [hd], List.map (Subst.apply_subst subst) (List.tl l), id) l
+          in
+         let bag,subst,t,id1 = f bag (Terms.Node l) pos ctx id
+         in
+           if id1 = id then (assert (subst=[]); bag,t,id)
+           else aux bag pos ctx id1 subst t
+      | _ -> assert false
+      in
+        aux bag pos ctx id [] t
+    ;;
     
     let build_clause bag filter rule t subst id id2 pos dir =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
@@ -177,6 +206,80 @@ module Superposition (B : Orderings.Blob) =
       prof_demod.HExtlib.profile (demod table varlist) x
     ;;
 
+    let mydemod table varlist subterm =
+      let cands = 
+        prof_demod_r.HExtlib.profile 
+         (IDX.DT.retrieve_generalizations table) subterm 
+      in
+      list_first
+        (fun (dir, (id,lit,vl,_)) ->
+           match lit with
+           | Terms.Predicate _ -> assert false
+           | Terms.Equation (l,r,_,o) ->
+               let side, newside = if dir=Terms.Left2Right then l,r else r,l in
+               try 
+                 let subst =
+                   prof_demod_u.HExtlib.profile 
+                     (Unif.unification (* (varlist@vl) *) varlist subterm) side 
+                 in 
+                 let iside = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) side 
+                 in
+                 let inewside = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) newside 
+                 in
+                 if o = Terms.Incomparable || o = Terms.Invertible then
+                   let o = 
+                     prof_demod_o.HExtlib.profile 
+                      (Order.compare_terms inewside) iside in
+                   (* Riazanov, pp. 45 (ii) *)
+                   if o = Terms.Lt then
+                     Some (newside, subst, id, dir)
+                   else 
+                     ((*prerr_endline ("Filtering: " ^ 
+                        Pp.pp_foterm side ^ " =(< || =)" ^ 
+                        Pp.pp_foterm newside ^ " coming from " ^ 
+                        Pp.pp_unit_clause uc );*)None)
+                 else
+                   Some (newside, subst, id, dir)
+               with FoUnif.UnificationFailure _ -> None)
+        (IDX.ClauseSet.elements cands)
+    ;;
+
+    let ctx_demod table vl bag t pos ctx id =
+      match mydemod table vl t with
+        | None -> (bag,[],t,id)
+        | Some (newside, subst, id2, dir) ->
+           let inewside = Subst.apply_subst subst newside in
+            match build_clause bag (fun _ -> true)
+              Terms.Demodulation (ctx inewside) subst id id2 pos dir
+            with
+              | None -> assert false
+              | Some (bag,(id,_,_,_)) ->
+                    (bag,subst,newside,id)
+    ;;
+      
+    let rec demodulate ~jump_to_right bag (id, literal, vl, pr) table =
+       match literal with
+      | Terms.Predicate t -> assert false
+      | Terms.Equation (l,r,ty,_) ->
+          let bag,l,id1 = 
+           visit bag [2]
+            (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l
+            (ctx_demod table vl)
+         in 
+         let bag,_,id2 = 
+            visit bag [3]
+              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r
+              (ctx_demod table vl)
+         in
+          let cl,_,_ = Terms.get_from_bag id2 bag in
+           bag,cl
+    ;;
+      
+  
     let demodulate_once_old ~jump_to_right bag (id, literal, vl, pr) table =
       match literal with
       | Terms.Predicate t -> assert false
@@ -242,19 +345,20 @@ module Superposition (B : Orderings.Blob) =
                 Some ((bag,cl),jump_to_right)
     ;;
 
-    let rec demodulate ~jump_to_right bag clause table =
+    let rec demodulate_old ~jump_to_right bag clause table =
       match demodulate_once ~jump_to_right bag clause table with
       | None -> bag, clause
       | Some ((bag, clause),r) -> demodulate ~jump_to_right:r
           bag clause table
     ;;
-
+(*
     let rec demodulate_old ~jump_to_right bag clause table =
       match demodulate_once_old ~jump_to_right bag clause table with
         | None -> bag, clause
         | Some ((bag, clause),r) -> demodulate_old ~jump_to_right:r
           bag clause table
     ;;
+*)
 
     let are_alpha_eq cl1 cl2 =
       let get_term (_,lit,_,_) =
@@ -268,19 +372,27 @@ module Superposition (B : Orderings.Blob) =
     ;;
 
     let demodulate bag clause table =
-(*      let (bag1,c1), (_,c2) =*)
-         demodulate ~jump_to_right:false bag clause table 
-(*         demodulate_old ~jump_to_right:false bag clause table *)
-(*      in
+      demodulate ~jump_to_right:false bag clause table
+;;  
+(*
+    let (bag1,c1), (bag2,c2) =
+        demodulate ~jump_to_right:false bag clause table,
+        demodulate_old ~jump_to_right:false bag clause table 
+      in
         if are_alpha_eq c1 c2 then bag1,c1
-        else begin
+        else 
+         begin
+          prerr_endline (Pp.pp_unit_clause clause);
           prerr_endline (Pp.pp_unit_clause c1);
           prerr_endline (Pp.pp_unit_clause c2);
-          prerr_endline "Bag :";
+          prerr_endline "Bag1 :";
           prerr_endline (Pp.pp_bag bag1);
+         prerr_endline "Bag2 :";
+          prerr_endline (Pp.pp_bag bag2);
           assert false
-        end*)
-    ;;
+          end
+    ;; *)
+
     let prof_demodulate = HExtlib.profile ~enable "demodulate";;
     let demodulate bag clause x =
       prof_demodulate.HExtlib.profile (demodulate bag clause) x