deep subsumption activated

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 2536f6443c9f95cbabf1f70fc50cb0d441c34260..89660143de5e426b53f9cdc291442237aed5dc57 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -24,6 +24,7 @@ let nparamod rdb metasenv subst context t table =
     = NCicBlob.NCicBlob(C) 
   in
   let module P = Paramod.Paramod(B) in
+  let module Pp = Pp.Pp(B) in
   let bag, maxvar = Terms.M.empty, 0 in
   let (bag,maxvar), passives = 
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
@@ -37,6 +38,9 @@ let nparamod rdb metasenv subst context t table =
   in
   List.map 
     (fun (bag,i,l) ->
+      List.iter (fun x ->
+        print_endline (Pp.pp_unit_clause ~margin:max_int
+          (fst(Terms.M.find x bag)))) l;
       let stamp = Unix.gettimeofday () in
       let proofterm = NCicProof.mk_proof bag i l in
       prerr_endline (Printf.sprintf "Got proof term in %fs"

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 1e50999e9e14243fd6dc976f7c4eb0372c2ccaf2..37abd6edfc2809c2a91bb9b9bb2e03489f48c8ba 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -71,9 +71,16 @@
           match t with
           | Terms.Leaf _ 
           | Terms.Var _ -> 
-(*                prerr_endline ("term: " ^ ppfot ft);             *)
+             let module Pp = 
+               Pp.Pp(NCicBlob.NCicBlob(
+                       struct
+                         let metasenv = [] let subst = [] let context = []
+                       end))
+             in  
+               prerr_endline ("term: " ^ Pp.pp_foterm ft);
                prerr_endline ("path: " ^ String.concat "," 
                  (List.map string_of_int p1));
+              prerr_endline ("leading to: " ^ Pp.pp_foterm t);
                assert false
           | Terms.Node l -> 
               let l = 
@@ -150,7 +157,7 @@
                if ongoal then id1,id,get_literal id1
                else id,id1,(lit,vl,proof)
              in
-             let vl = if ongoal then Subst.filter subst vl else vl in
+             let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
               let proof_of_id id = 
                 let vars = List.rev (vars_of id seen) in
                 let args = List.map (Subst.apply_subst subst) vars in

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index d058be2533fd83faf8e99a31fd4b0e99d0a58331..6a4cc0d791564d79cd317378028abf6cca97bccf 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -252,24 +252,33 @@ module Superposition (B : Terms.Blob) =
     let rec deep_eq ~unify l r ty pos contextl contextr table acc =
       match acc with 
       | None -> None
-      | Some(bag,maxvar,[],subst) -> assert false
-      | Some(bag,maxvar,(id,_,vl,_)::clauses,subst) -> 
+      | Some(bag,maxvar,(id,lit,vl,p),subst) -> 
          let l = Subst.apply_subst subst l in 
          let r = Subst.apply_subst subst r in 
            try 
              let subst1,vl1 = Unif.unification vl [] l r in
-               Some(bag,maxvar,clauses,Subst.concat subst1 subst)
+              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)
+             in
+               Some(bag,maxvar,(id,lit,vl1,p),Subst.concat subst1 subst)
            with FoUnif.UnificationFailure _ -> 
              match rewrite_eq ~unify l r ty vl table with
               | Some (id2, dir, subst1) ->
+                 let newsubst = Subst.concat subst1 subst in
                  let id_t = 
-                   Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r] in
+                    FoSubst.apply_subst newsubst
+                     (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) 
+                 in
                    (match 
                      build_new_clause bag maxvar (fun _ -> true)
-                       Terms.Superposition id_t subst1 [] id id2 (2::pos) dir 
+                       Terms.Superposition id_t 
+                         subst1 [] id id2 (pos@[2]) dir 
                    with
                    | Some ((bag, maxvar), c) -> 
-                       Some(bag,maxvar,c::clauses,Subst.concat subst1 subst)
+                       Some(bag,maxvar,c,newsubst)
                    | None -> assert false)
              | None ->
                  match l,r with 
@@ -436,7 +445,7 @@ module Superposition (B : Terms.Blob) =
       let bag, clause = demodulate bag clause table in
       if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
-(*
+
       else   
        let (id,lit,vl,_) = clause in 
        let l,r,ty = 
@@ -445,21 +454,21 @@ module Superposition (B : Terms.Blob) =
            | _ -> assert false 
        in
        match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) 
-         table (Some(bag,maxvar,[clause],Subst.id_subst)) with
+         table (Some(bag,maxvar,clause,Subst.id_subst)) with
        | None -> 
            if List.exists (are_alpha_eq clause) g_actives then None
            else Some (bag, clause)
        | Some (bag,maxvar,cl,subst) -> 
-           debug "Goal subsumed";
-           raise (Success (bag,maxvar,List.hd cl))
-*)
+           prerr_endline "Goal subsumed";
+           raise (Success (bag,maxvar,cl))
+           (*
       else match is_subsumed ~unify:true bag maxvar clause table with
        | None -> 
            if List.exists (are_alpha_eq clause) g_actives then None
            else Some (bag, clause)
        | Some ((bag,maxvar),c) -> 
-           debug "Goal subsumed";
-           raise (Success (bag,maxvar,c)) 
+           prerr_endline "Goal subsumed";
+           raise (Success (bag,maxvar,c))*) 
     ;;
 
     (* =================== inference ===================== *)