New management of resulting subst in deep_eq: used to be malformed.

diff --git a/matitaB/components/ng_paramodulation/nCicProof.ml b/matitaB/components/ng_paramodulation/nCicProof.ml
index 50c25315f91bd7ab1758892c857d6d7c6b854fde..5f8ed1733ccfd44888287e0affc9a6b380a923a1 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicProof.ml
+++ b/matitaB/components/ng_paramodulation/nCicProof.ml
@@ -231,24 +231,7 @@ let debug c _ = c;;
       let lit = Subst.apply_subst subst lit in
         extract status 0 [] lit in
     (* composition of all subst acting on goal *)
-    let res_subst =
-      let rec rsaux ongoal acc = 
-       function
-         | [] -> acc (* is the final subst for refl *)
-         | id::tl when ongoal ->
-            let lit,vl,proof = get_literal id in
-             (match proof with
-               | Terms.Exact _ -> rsaux ongoal acc tl
-               | Terms.Step (_, _, _, _, _, s) ->
-                   rsaux ongoal (s@acc) tl)
-         | id::tl -> 
-           (* subst is the the substitution for refl *)
-           rsaux (id=mp) subst tl
-      in 
-      let r = rsaux false [] steps in
-       (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
-           prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
-      r
+    let res_subst = subst 
     in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 1152571cedb3e9c5d409f9da6fa6665555c22d54..6628ac9b9373e10bbcea02ed895c21e18d26222f 100644 (file)
--- a/matitaB/components/ng_paramodulation/superposition.ml
+++ b/matitaB/components/ng_paramodulation/superposition.ml
@@ -27,8 +27,7 @@ module Superposition (B : Orderings.Blob) =
       * B.t Terms.substitution
 
     let print s = prerr_endline (Lazy.force s);; 
-    let debug _ = ();;
-    (* let debug = print;; *) 
+    let debug _ = ();; 
     let enable = true;;
 
     let rec list_first f = function
@@ -110,8 +109,8 @@ module Superposition (B : Orderings.Blob) =
     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
+         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
@@ -143,7 +142,16 @@ module Superposition (B : Orderings.Blob) =
           match t with
           | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq ->
                let o = Order.compare_terms l r in
-               Terms.Equation (l, r, ty, o)
+               (* CSC: to avoid equations of the form ? -> T that
+                  can always be applied and that lead to type-checking errors *)
+               (match l,r,o with 
+                   Terms.Var _,_,Terms.Gt
+                 | _,Terms.Var _,Terms.Lt -> assert false
+                 | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
+                    Terms.Equation (l, r, ty, Terms.Lt)
+                 | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
+                    Terms.Equation (l, r, ty, Terms.Gt)
+                 | _ -> Terms.Equation (l, r, ty, o))
           | t -> Terms.Predicate t
         in
         let bag, uc = 
@@ -366,12 +374,17 @@ module Superposition (B : Orderings.Blob) =
        bag, maxvar, res
     ;;
     
-    let rewrite_eq ~unify l r ty vl table =
+    (* rewrite_eq check if in table there an equation matching l=r; 
+       used in subsumption and deep_eq. In deep_eq, we need to match 
+       several times times w.r.t. the same table, hence we should refresh 
+       the retrieved clauses, to avoid clashes of variables *)
+
+    let rewrite_eq ~refresh ~unify maxvar l r ty vl table =
       let retrieve = if unify then IDX.DT.retrieve_unifiables
       else IDX.DT.retrieve_generalizations in
       let lcands = retrieve table l in
       let rcands = retrieve table r in
-      let f b c = 
+      let f b c =
         let id, dir, l, r, vl = 
           match c with
             | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl
@@ -390,8 +403,12 @@ module Superposition (B : Orderings.Blob) =
         | [] -> None
         | (id2,dir,c,vl1)::tl ->
             try
+              let c,maxvar = if refresh then
+                let maxvar,_,r = Utils.relocate maxvar vl1 [] in
+                Subst.apply_subst r c,maxvar
+                else c,maxvar in 
               let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
-              Some (id2, dir, subst)
+              Some (id2, dir, subst, maxvar)
             with FoUnif.UnificationFailure _ -> aux tl
       in
         aux (cands1 @ cands2)
@@ -401,9 +418,9 @@ module Superposition (B : Orderings.Blob) =
       match lit with
       | Terms.Predicate _ -> assert false
       | Terms.Equation (l,r,ty,_) -> 
-          match rewrite_eq ~unify l r ty vl table with
+          match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with
             | None -> None
-            | Some (id2, dir, subst) ->
+            | Some (id2, dir, subst, maxvar) ->
                 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 
@@ -415,38 +432,46 @@ module Superposition (B : Orderings.Blob) =
     (* id refers to a clause proving contextl l = contextr r *)
 
     let rec deep_eq ~unify l r ty pos contextl contextr table acc =
+      (* let _ = prerr_endline ("pos = " ^ String.concat "," 
+            (List.map string_of_int pos)) in *)
       match acc with 
       | None -> None
       | Some(bag,maxvar,(id,lit,vl,p),subst) -> 
           (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
+          (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *)
+          (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *)
           let l = Subst.apply_subst subst l in 
           let r = Subst.apply_subst subst r in 
+          (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *)
+          (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *)
             try 
               let subst1 = Unif.unification (* vl *) [] l r in
               let lit = 
                 match lit with Terms.Predicate _ -> assert false
                   | Terms.Equation (l,r,ty,o) -> 
-                     Terms.Equation (FoSubst.apply_subst subst1 l,
-                       FoSubst.apply_subst subst1 r, ty, o)
+                    let l = Subst.apply_subst subst1 l in 
+                    let r = Subst.apply_subst subst1 r in 
+                     Terms.Equation (l, r, ty, o)
               in
                 Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst)
             with FoUnif.UnificationFailure _ -> 
-              match rewrite_eq ~unify l r ty vl table with
-              | Some (id2, dir, subst1) ->
+              match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with
+              | Some (id2, dir, subst1, maxvar) ->
                  (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
-                    prerr_endline ("old subst = "^Pp.pp_substitution subst);*)
+                   prerr_endline ("old subst = "^Pp.pp_substitution subst); *)
                   let newsubst = Subst.concat subst1 subst in
                   let id_t = 
                     FoSubst.apply_subst newsubst
                       (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r]) 
                   in
-                    (match 
+                  (match 
                       build_new_clause_reloc bag maxvar (fun _ -> true)
                         Terms.Superposition id_t 
-                        subst1 id id2 (pos@[2]) dir 
-                    with
+                        subst1 id id2 (pos@[2]) dir  
+                   with
                     | Some ((bag, maxvar), c), r ->
-                       (* prerr_endline ("r = "^Pp.pp_substitution r); *)
+                     (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *)
+                     (* prerr_endline ("r = "^Pp.pp_substitution r); *)
                        let newsubst = Subst.flat 
                          (Subst.concat r subst) in
                         Some(bag,maxvar,c,newsubst)
@@ -637,7 +662,7 @@ module Superposition (B : Orderings.Blob) =
       let bag, clause = 
         if no_demod then bag, clause else demodulate bag clause table 
       in
-      let _ = debug (lazy ("demodulated goal  : " 
+      let _ = debug(lazy ("demodulated goal  : " 
                             ^ Pp.pp_unit_clause clause))
       in
       if List.exists (are_alpha_eq clause) g_actives then None
@@ -660,12 +685,13 @@ module Superposition (B : Orderings.Blob) =
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
              debug (lazy "Goal subsumed");
+             debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst));
              raise (Success (bag,maxvar,cl,subst))
 (*
         match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)
         | Some ((bag,maxvar),c) -> 
-            prerr_endline "Goal subsumed";
+            debug (lazy "Goal subsumed");
             raise (Success (bag,maxvar,c))
 *)
     ;;