Ported innermost strategy for demodulation from trunk

diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt
index 35e10ad429f35528b49242a12f459860950f2bac..8ffa24a0f8eeaaea45d7c8c05a8bc3238ec0bf6d 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -1,9 +1,10 @@
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
+foUtils.cmi: terms.cmi 
+foUnif.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
-foUtils.cmi: terms.cmi orderings.cmi 
+clauses.cmi: terms.cmi orderings.cmi 
 index.cmi: terms.cmi orderings.cmi 
-foUnif.cmi: terms.cmi orderings.cmi 
 superposition.cmi: terms.cmi orderings.cmi index.cmi 
 stats.cmi: terms.cmi orderings.cmi 
 paramod.cmi: terms.cmi orderings.cmi 
@@ -16,24 +17,30 @@ pp.cmo: terms.cmi pp.cmi
 pp.cmx: terms.cmx pp.cmi 
 foSubst.cmo: terms.cmi foSubst.cmi 
 foSubst.cmx: terms.cmx foSubst.cmi 
-orderings.cmo: terms.cmi pp.cmi orderings.cmi 
-orderings.cmx: terms.cmx pp.cmx orderings.cmi 
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
-index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi 
-index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi 
-foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
-foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.cmx foSubst.cmx foUtils.cmi 
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+orderings.cmo: terms.cmi pp.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+    orderings.cmi 
+orderings.cmx: terms.cmx pp.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+    orderings.cmi 
+clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+    clauses.cmi 
+clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+    clauses.cmi 
+index.cmo: terms.cmi orderings.cmi foUtils.cmi clauses.cmi index.cmi 
+index.cmx: terms.cmx orderings.cmx foUtils.cmx clauses.cmx index.cmi 
 superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
-    foUnif.cmi foSubst.cmi superposition.cmi 
+    foUnif.cmi foSubst.cmi clauses.cmi superposition.cmi 
 superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
-    foUnif.cmx foSubst.cmx superposition.cmi 
-stats.cmo: terms.cmi stats.cmi 
-stats.cmx: terms.cmx stats.cmi 
+    foUnif.cmx foSubst.cmx clauses.cmx superposition.cmi 
+stats.cmo: terms.cmi pp.cmi stats.cmi 
+stats.cmx: terms.cmx pp.cmx stats.cmi 
 paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
-    foUtils.cmi foUnif.cmi paramod.cmi 
+    foUtils.cmi foUnif.cmi clauses.cmi paramod.cmi 
 paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
-    foUtils.cmx foUnif.cmx paramod.cmi 
+    foUtils.cmx foUnif.cmx clauses.cmx paramod.cmi 
 nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi 
 nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index ff34709e9c7a262453de6a124ba6e641919b11b6..2b52ce34a29bc50ef15beb831af87eba1124071f 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -94,7 +94,3 @@ let nparamod rdb metasenv subst context (g_t,g_ty) table =
       proofterm, metasenv, subst)
     solutions
 ;;
-  
-  
-
-

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index fd7be3b7e0478430f98aadb0fb23b194ce909f3a..c5db7a4e2ae8bc927c082bd1ceacfeee21afaba2 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -101,7 +101,35 @@ module Superposition (B : Orderings.Blob) =
       in
         aux bag pos ctx id lit t
     ;;
-    
+
+    let visit bag pos ctx id lit t f =
+      let rec aux bag pos ctx id subst lit = function
+      | Terms.Leaf _ as t -> 
+         let  bag,subst,t,id,lit = f bag t pos ctx id lit
+         in assert (subst=[]); bag,t,id,lit
+      | Terms.Var i as t ->  
+         let t= Subst.apply_subst subst t in
+           bag,t,id,lit
+      | Terms.Node (hd::l) ->
+          let bag, l, _, id,lit = 
+            List.fold_left
+              (fun (bag,pre,post,id,lit) t ->
+                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
+                 let newpos = (List.length pre)::pos in
+                 let bag,newt,id,lit = aux bag newpos newctx id subst lit t in
+                   if post = [] then bag, pre@[newt], [], id, lit
+                   else bag, pre @ [newt], List.tl post, id, lit)
+              (bag, [hd], List.map (Subst.apply_subst subst) (List.tl l), id, lit) l
+          in
+         let bag,subst,t,id1,lit = f bag (Terms.Node l) pos ctx id lit
+         in
+           if id1 = id then (assert (subst=[]); bag,t,id,lit)
+           else aux bag pos ctx id1 subst lit t
+      | _ -> assert false
+      in
+        aux bag pos ctx id [] lit t
+    ;;
+
     let build_clause ~fresh bag maxvar filter rule t subst id id2 pos dir clause_ctx =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
       let t = Subst.apply_subst subst t in
@@ -190,6 +218,106 @@ 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, is_pos, pos, (id,nlit,plit,vl,_)) ->
+         match (nlit,plit) with
+          | [],[(lit,_)] ->
+           (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)
+          | _ -> assert false)
+        (IDX.ClauseSet.elements cands)
+    ;;
+
+    let ctx_demod table vl clause_ctx bag t pos ctx id lit =
+      match mydemod table vl t with
+        | None -> (bag,[],t,id,lit)
+        | Some (newside, subst, id2, dir) ->
+           let inewside = Subst.apply_subst subst newside in
+            match build_clause ~fresh:false bag 0 (fun _ -> true)
+              Terms.Demodulation (ctx inewside) subst id id2 pos dir clause_ctx
+            with
+              | None -> assert false
+              | Some (bag,_,(id,_,_,_,_),lit) ->
+                    (bag,subst,newside,id,lit)
+    ;;
+      
+    let rec demodulate bag (id,nlit,plit,vl,proof) table =
+      let rec demod_lit ~jump_to_right bag id lit clause_ctx =
+       (match lit with
+      | Terms.Predicate t -> assert false
+      | Terms.Equation (l,r,ty,_) -> assert false
+          (*let bag,l,id1,lit = 
+           visit bag [2]
+            (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id lit l
+            (ctx_demod table vl clause_ctx)
+         in 
+         let bag,_,id2,lit = 
+            visit bag [3]
+              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 lit r
+              (ctx_demod table vl clause_ctx)
+         in
+          let cl,_,_ = Terms.get_from_bag id2 bag in
+           bag,id2,cl *) )
+      in
+     let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id
+       else List.fold_left
+       (fun (pre,post,bag,id) (lit,sel) ->
+          let bag, id, lit =
+              demod_lit ~jump_to_right:false bag id lit (fun l -> pre@[l,sel]@post,plit)
+          in
+             if post=[] then pre@[(lit,sel)],[],bag,id
+             else pre@[(lit,sel)],List.tl post,bag,id)
+       ([],List.tl nlit, bag, id) nlit
+      in
+      let _,_,bag,id = if plit = [] then plit,[],bag,id
+       else List.fold_left
+       (fun (pre,post,bag,id) (lit,sel) ->
+          let bag, id, lit = 
+              demod_lit ~jump_to_right:false bag id lit (fun l -> nlit,pre@[l,sel]@post)
+          in
+             if post=[] then pre@[(lit,sel)],[],bag,id
+             else pre@[(lit,sel)],List.tl post,bag,id)
+       ([],List.tl plit, bag, id) plit
+      in
+       let cl,_,_ = Terms.get_from_bag id bag in
+        bag,cl
+    ;;
+
     let parallel_demod table vl clause_ctx bag t pos ctx id lit =
       match demod table vl t with
         | None -> (bag,t,id,lit)
@@ -222,7 +350,7 @@ module Superposition (B : Orderings.Blob) =
               Some ((bag,id2,lit),jump_to_right)
     ;;
 
-    let rec demodulate bag (id,nlit,plit,vl,proof) table =
+    let rec demodulate_old bag (id,nlit,plit,vl,proof) table =
       let rec demod_lit ~jump_to_right bag id lit clause_ctx =
          match demodulate_once ~jump_to_right bag id lit vl table clause_ctx with
          | None -> bag, id, lit

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index ad780c82c1e1f3fc645cc6a193b59886d2401dbc..c6877901b8010acf505221a357a5ec1c199798e4 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -75,5 +75,4 @@ module Superposition (B : Orderings.Blob) :
       B.t Terms.clause ->
       bool
 
-
   end

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index c15c85af24a6c4a91d756441a738d4be2833be27..76eda3717c3f8457810e8d03ff86d4cfbc7f1cd7 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -85,7 +85,7 @@ type 'a bag = int (* max ID  *)
 module type Blob =
   sig
     (* Blob is the type for opaque leaves: 
-     * - checking equlity should be efficient
+     * - checking equality should be efficient
      * - atoms have to be equipped with a total order relation
      *)
     type t