Now iterating superposition

diff --git a/helm/software/components/ng_paramodulation/clauses.ml b/helm/software/components/ng_paramodulation/clauses.ml
index 5955fcae1d21a63e9c88be8213c64f7d9fe2de5a..f8724601cfc1e236ddc1b71d2d351ad3b0e999d2 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.ml
+++ b/helm/software/components/ng_paramodulation/clauses.ml
@@ -25,8 +25,8 @@ module Clauses (B : Orderings.Blob) = struct
   let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
   let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
     
-  let fresh_clause maxvar (id, nlit, plit, varlist, proof) =
-    let maxvar, varlist, subst = Utils.relocate maxvar varlist FoSubst.id_subst in
+  let fresh_clause maxvar ?(subst=FoSubst.id_subst) (id, nlit, plit, varlist, proof) =
+    let maxvar, varlist, subst = Utils.relocate maxvar varlist subst in
     let apply_subst_on_lit = function
       | Terms.Equation (l,r,ty,o) ->
           let l = FoSubst.apply_subst subst l in
@@ -99,4 +99,14 @@ module Clauses (B : Orderings.Blob) = struct
        with Invalid_argument _ -> false
     ;;
 
+  let vars_of_clause (id,nlit,plit,_,pr) = 
+    let vars_of_lit acc lit =
+      match lit with
+       | (Terms.Predicate t,_) -> Terms.vars_of_term ~start_acc:acc t
+       | (Terms.Equation (l,r,ty,o),_) ->
+            Terms.vars_of_term ~start_acc:(Terms.vars_of_term ~start_acc:acc l) r
+    in
+    List.fold_left vars_of_lit [] (nlit@plit)
+;;
+
 end

diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli
index 81738c2a42314d221825a4a591bab474588c66f1..b857eb01629d5f0ceda19eb4d375a748d881b789 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.mli
+++ b/helm/software/components/ng_paramodulation/clauses.mli
@@ -22,7 +22,9 @@ module Clauses (B : Orderings.Blob) :
 
     val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
     val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int      
-    val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int
+    val fresh_clause : int ->
+         ?subst: B.t Terms.substitution ->
+         B.t Terms.clause -> B.t Terms.clause * int
 
     val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list
                            -> B.t Terms.foterm -> B.t Terms.clause * int
@@ -40,4 +42,10 @@ module Clauses (B : Orderings.Blob) :
     val are_alpha_eq_cl :
            B.t Terms.clause -> B.t Terms.clause -> bool
 
+    val vars_of_clause :
+           B.t Terms.clause -> int list
+
+    (*val apply_subst :
+          B.t Terms.substitution -> B.t Terms.clause -> B.t Terms.clause*)
+
 end

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index daafbd3ac71b6af45ce775e0bc36acdc61f60705..63507aea6b4aeda4c0eb16f00e52fadf09b2452a 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -102,7 +102,7 @@ module Superposition (B : Orderings.Blob) =
         aux bag pos ctx id lit t
     ;;
     
-    let build_clause bag filter rule t subst id id2 pos dir clause_ctx =
+    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
       if filter subst then
@@ -114,16 +114,23 @@ module Superposition (B : Orderings.Blob) =
           | t -> Terms.Predicate t
         in
         let nlit,plit = clause_ctx literal in
-        let bag, uc = 
-          Terms.add_to_bag (0, nlit, plit, Terms.vars_of_term t, proof) bag
+        let cl = (0, nlit, plit, [], proof) in 
+        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
         in
-        Some (bag, uc, literal)
+        let bag, cl = 
+          Terms.add_to_bag (0, nlit, plit, vl, proof) bag
+        in
+        Some (bag, maxvar, cl, literal)
       else
         ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
     ;;
     let prof_build_clause = HExtlib.profile ~enable "build_clause";;
-    let build_clause bag filter rule t subst id id2 pos x =
-      prof_build_clause.HExtlib.profile (build_clause bag filter rule t subst id id2 pos) x
+    let build_clause ~fresh bag maxvar filter rule t subst id id2 pos x =
+      prof_build_clause.HExtlib.profile
+          (build_clause ~fresh bag maxvar filter rule t subst id id2 pos) x
     ;;
       
     
@@ -186,11 +193,11 @@ module Superposition (B : Orderings.Blob) =
       match demod table vl t with
         | None -> (bag,t,id,lit)
         | Some (newside, subst, id2, dir) ->
-            match build_clause bag (fun _ -> true)
+            match build_clause ~fresh:false bag 0 (fun _ -> true)
               Terms.Demodulation (ctx newside) subst id id2 pos dir clause_ctx
             with
               | None -> assert false
-              | Some (bag,(id,_,_,_,_),lit) ->
+              | Some (bag,_,(id,_,_,_,_),lit) ->
                     (bag,newside,id,lit)
     ;;
 
@@ -279,24 +286,14 @@ module Superposition (B : Orderings.Blob) =
           with FoUnif.UnificationFailure _ -> false)
       | _ -> false
 
-    let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
-      let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
-      (Subst.apply_subst subst t)) subst in
-      match build_clause bag filter rule t subst id id2 pos dir (fun x -> [],[(x,true)]) with
-      | Some (bag, c, _) -> Some ((bag, maxvar), c)
-      | None -> None
-    ;;
-    let prof_build_new_clause = HExtlib.profile ~enable "build_new_clause";;
-    let build_new_clause bag maxvar filter rule t subst id id2 pos x =
-      prof_build_new_clause.HExtlib.profile (build_new_clause bag maxvar filter
-      rule t subst id id2 pos) x
-    ;;
-
-    let fold_build_new_clause bag maxvar id rule filter res =
+    let fold_build_new_clause bag maxvar id rule filter res clause_ctx =
       let (bag, maxvar), res =
        HExtlib.filter_map_acc 
          (fun (bag, maxvar) (t,subst,id2,pos,dir) ->
-            build_new_clause bag maxvar filter rule t subst id id2 pos dir)
+           match build_clause ~fresh:true bag maxvar filter 
+                  rule t subst id id2 pos dir clause_ctx with
+            | None -> None
+            | Some (bag,maxvar,res,_) -> Some ((bag,maxvar),res))
          (bag, maxvar) res
       in
        bag, maxvar, res
@@ -342,8 +339,8 @@ module Superposition (B : Orderings.Blob) =
             | None -> None
             | Some (id2, dir, subst) ->
                 let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
-                  build_new_clause bag maxvar (fun _ -> true)
-                  Terms.Superposition id_t subst id id2 [2] dir)
+                  build_clause ~fresh:true bag maxvar (fun _ -> true)
+                  Terms.Superposition id_t subst id id2 [2] dir (fun l -> [],[l,true]))
      | _ -> None (* TODO : implement subsumption for clauses *)
     ;;
     let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";;
@@ -362,7 +359,7 @@ module Superposition (B : Orderings.Blob) =
               let subst1 = Unif.unification (* vl *) [] l r in
               let lit = 
                 match nlit,plit with
-                  | [],[Terms.Equation (l,r,ty,o),_] -> 
+                  | [Terms.Equation (l,r,ty,o),_],[] -> 
                      Terms.Equation (FoSubst.apply_subst subst1 l,
                        FoSubst.apply_subst subst1 r, ty, o)
                   | _ -> assert false
@@ -377,11 +374,11 @@ module Superposition (B : Orderings.Blob) =
                       (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) 
                   in
                     (match 
-                      build_new_clause bag maxvar (fun _ -> true)
+                      build_clause ~fresh:true bag maxvar (fun _ -> true)
                         Terms.Superposition id_t 
-                        subst1 id id2 (pos@[2]) dir 
+                        subst1 id id2 (pos@[2]) dir (fun l -> [],[l,true])
                     with
-                    | Some ((bag, maxvar), c) -> 
+                    | Some (bag, maxvar, c, _) -> 
                         Some(bag,maxvar,c,newsubst)
                     | None -> assert false)
               | None ->
@@ -604,10 +601,10 @@ module Superposition (B : Orderings.Blob) =
     (* =================== inference ===================== *)
 
     (* this is OK for both the sup_left and sup_right inference steps *)
-    let superposition table varlist subterm pos context =
+    let superposition table varlist is_pos subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
       HExtlib.filter_map
-        (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) ->
+        (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
@@ -634,22 +631,22 @@ module Superposition (B : Orderings.Blob) =
     ;;
 
     (* Superposes selected equation with equalities in table *)
-    let superposition_with_table bag maxvar (id,nlit,plit,vl,_) table =
-      match nlit,plit with 
-      | [],[Terms.Equation (l,r,ty,Terms.Lt),_] ->
+    let superposition_with_table bag maxvar id vl lit is_pos clause_ctx table =
+      match lit with 
+      | Terms.Equation (l,r,ty,Terms.Lt) ->
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [3] 
               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
-              r (superposition table vl))
-      | [],[Terms.Equation (l,r,ty,Terms.Invertible),_]
-      | [],[Terms.Equation (l,r,ty,Terms.Gt),_] ->
+              r (superposition table vl is_pos)) clause_ctx
+      | Terms.Equation (l,r,ty,Terms.Invertible)
+      | Terms.Equation (l,r,ty,Terms.Gt) ->
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [2] 
               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
-              l (superposition table vl))
-      | [],[Terms.Equation (l,r,ty,Terms.Incomparable),_] ->
+              l (superposition table vl is_pos)) clause_ctx
+      | Terms.Equation (l,r,ty,Terms.Incomparable) ->
          let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
            let l = Subst.apply_subst subst l in
            let r = Subst.apply_subst subst r in
@@ -661,19 +658,32 @@ module Superposition (B : Orderings.Blob) =
               (filtering Terms.Gt)
               (all_positions [3] 
                 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
-                r (superposition table vl))
+                r (superposition table vl is_pos)) clause_ctx
          in
          let bag, maxvar, l_terms =
            fold_build_new_clause bag maxvar id Terms.Superposition
               (filtering Terms.Lt)
               (all_positions [2] 
                 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
-                l (superposition table vl))
+                l (superposition table vl is_pos)) clause_ctx
          in
            bag, maxvar, r_terms @ l_terms
       | _ -> assert false
     ;;
 
+    let superpose_literal id vl table is_pos (bag,maxvar,pre,post,acc) (lit,sel) =
+      let clause_ctx =
+         if is_pos then fun l -> [],pre@[l,true]@post
+         else fun l -> pre@[l,true]@post,[]
+      in
+      let bag, maxvar, newc =
+        superposition_with_table bag maxvar id vl lit is_pos clause_ctx table
+      in
+         if post = [] then bag,maxvar,pre@[lit,sel],[],newc@acc
+         else bag,maxvar,pre@[lit,sel],List.tl post,newc@acc
+    ;;
+
+
     (* the current equation is normal w.r.t. demodulation with atable
      * (and is not the identity) *)
     let infer_right bag maxvar current (alist,atable) = 
@@ -691,11 +701,18 @@ module Superposition (B : Orderings.Blob) =
       (* We superpose active clauses with current *)
       let bag, maxvar, new_clauses =
         List.fold_left 
-          (fun (bag, maxvar, acc) active ->
-             let bag, maxvar, newc = 
-               superposition_with_table bag maxvar active ctable 
+          (fun (bag, maxvar, acc) (id,nlit,plit,vl,_) ->
+             let bag, maxvar, _, _, acc =
+              if nlit = [] then bag,maxvar,[],[],acc
+              else List.fold_left
+                 (superpose_literal id vl ctable false) (bag,maxvar,[],List.tl nlit,acc) nlit
              in
-             bag, maxvar, newc @ acc)
+              let bag, maxvar, _, _, acc =
+               if plit = [] then bag,maxvar,[],[],acc
+               else List.fold_left
+                 (superpose_literal id vl ctable true) (bag,maxvar,[],List.tl plit,acc) plit
+             in            
+             bag, maxvar, acc)
           (bag, maxvar, []) alist
       in
         debug (lazy "First superpositions");
@@ -708,13 +725,19 @@ module Superposition (B : Orderings.Blob) =
       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
+      let bag, (id,nlit,plit,vl,_) = Terms.add_to_bag fresh_current bag in
         (* We superpose current with active clauses *)
-      let bag, maxvar, additional_new_clauses =
-        superposition_with_table bag maxvar fresh_current atable 
+      let bag, maxvar, _, _, new_clauses =
+         if nlit = [] then bag,maxvar,[],[],new_clauses
+         else List.fold_left
+         (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,new_clauses) nlit
       in
+      let bag, maxvar, _, _, new_clauses =
+         if plit = [] then bag,maxvar,[],[],new_clauses
+         else List.fold_left
+          (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,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 = 
@@ -733,8 +756,14 @@ module Superposition (B : Orderings.Blob) =
         (* We superpose the goal with active clauses *)
      if (match goal with (_,_,_,[],_) -> true | _ -> false) then bag, maxvar, []
      else
-      let bag, maxvar, new_goals =        
-        superposition_with_table bag maxvar goal atable 
+      let (id,nlit,vl) =
+         match goal with
+           | (id,nlit,[],vl,_) -> id,nlit,vl
+           | _ -> assert false
+      in
+      let bag, maxvar, _, _, new_goals = 
+        List.fold_left (superpose_literal id vl atable false)
+            (bag,maxvar,[],List.tl nlit,[]) nlit
       in
         debug (lazy "Superposed goal with active clauses");
         (* We simplify the new goals with active clauses *)