From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 26 Jun 2009 11:02:11 +0000 (+0000)
Subject: deep subsumption activated
X-Git-Tag: make_still_working~3786
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=895efaa0e4375de535226002fcb1ed14d1fa8301;p=helm.git

deep subsumption activated
---

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 2536f6443..89660143d 100644
--- 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 1e50999e9..37abd6edf 100644
--- 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 d058be253..6a4cc0d79 100644
--- 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 ===================== *)