X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=96b16bb07b6a66dd674495d750e76075185faae2;hb=68a557b997805b4a96fb2851cb4d2ab2076bba36;hp=d058be2533fd83faf8e99a31fd4b0e99d0a58331;hpb=2701c980f48541dd5e8317b5a5661b439ced8b29;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index d058be253..96b16bb07 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -15,14 +15,14 @@ module Superposition (B : Terms.Blob) =
   struct
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
-    module Subst = FoSubst (*.Subst(B)*)
+    module Subst = FoSubst 
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
     
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
-(*    let debug s = prerr_endline s;;*)
+    let debug s = prerr_endline s;;
     let debug _ = ();;
 
     let rec list_first f = function
@@ -92,7 +92,7 @@ module Superposition (B : Terms.Blob) =
           | t -> Terms.Predicate t
         in
         let bag, uc = 
-          Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
+          Terms.add_to_bag (0, literal, vars_of_term t, proof) bag
         in
         Some (bag, uc)
       else
@@ -133,7 +133,6 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table =
-      (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
@@ -252,24 +251,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 
@@ -290,13 +298,11 @@ module Superposition (B : Terms.Blob) =
                                  footail postl, footail postr))
 			  (acc,[a],List.tl la,List.tl lb) la lb
 		      in acc
-                  | Terms.Var _, _
-                  | _, Terms.Var _ -> assert false
                   | _,_ -> None
     ;;
 
     let rec orphan_murder bag acc i =
-      match Terms.M.find i bag with
+      match Terms.get_from_bag i bag with
 	| (_,_,_,Terms.Exact _),discarded -> (discarded,acc)
 	| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc)
 	| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false ->
@@ -306,18 +312,19 @@ module Superposition (B : Terms.Blob) =
 	      | (false,acc) ->
 		  let (res,acc) = orphan_murder bag acc i2 in
 		  if res then res,acc else res,i::acc
-;;
+    ;;
 
-    let orphan_murder bag cl =
+    let orphan_murder bag actives cl =
       let (id,_,_,_) = cl in
-      let (res,_) = orphan_murder bag [] id in
+      let actives = List.map (fun (i,_,_,_) -> i) actives in
+      let (res,_) = orphan_murder bag actives id in
 	if res then debug "Orphan murdered"; res
-;;
+    ;;
 
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       if is_identity_clause ~unify:false clause then bag,None
-      (* else if orphan_murder bag clause then bag,None *)
+      (* else if orphan_murder bag actives clause then bag,None *)
       else let bag, clause = demodulate bag clause table in
       if is_identity_clause ~unify:false clause then bag,None
       else
@@ -328,10 +335,14 @@ module Superposition (B : Terms.Blob) =
 
     let simplify table maxvar bag clause =
       match simplify table maxvar bag clause with
-	| bag, None -> let (id,_,_,_) = clause in
-	    Terms.M.add id (clause,true) bag, None
+	| bag, None ->
+	    Terms.replace_in_bag (clause,true) bag, None
 	| bag, Some clause -> bag, Some clause
-;;
+    (*let (id,_,_,_) = clause in
+	    if orphan_murder bag clause then
+	      Terms.M.add id (clause,true) bag, Some clause
+	    else bag, Some clause*)
+    ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
@@ -359,7 +370,8 @@ module Superposition (B : Terms.Blob) =
 	(* Simplification of new_clause with :      *
 	 * - actives and cl if new_clause is not cl *
 	 * - only actives otherwise                 *)
-	match simplify atable1 maxvar bag new_clause with
+	match
+	  simplify atable1 maxvar bag new_clause with
 	  | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
 	  | bag,Some clause ->
 	      (* Simplification of each active clause with clause *
@@ -432,34 +444,35 @@ module Superposition (B : Terms.Blob) =
 ;;
 
     (* this is like simplify but raises Success *)
-    let simplify_goal maxvar table bag g_actives clause = 
-      let bag, clause = demodulate bag clause table in
+    let simplify_goal ~no_demod maxvar table bag g_actives clause = 
+      let bag, clause = 
+	if no_demod then bag, clause else demodulate bag clause table 
+      in
+      if List.exists (are_alpha_eq clause) g_actives then None else
       if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
-(*
       else   
 	let (id,lit,vl,_) = clause in 
-	let l,r,ty = 
-	  match lit with
-	    | Terms.Equation(l,r,ty,_) -> l,r,ty
-	    | _ -> 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
-	| 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))
-*)
+        if vl = [] then Some (bag,clause)
+        else
+	 let l,r,ty = 
+	   match lit with
+	     | Terms.Equation(l,r,ty,_) -> l,r,ty
+	     | _ -> 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
+	 | None -> Some (bag,clause)
+	 | Some (bag,maxvar,cl,subst) -> 
+	     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)
+	| None -> 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 ===================== *)
@@ -560,7 +573,7 @@ module Superposition (B : Terms.Blob) =
       let fresh_current, maxvar = Utils.fresh_unit_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 = Utils.add_to_bag bag fresh_current in
+      let bag, fresh_current = 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 
@@ -578,6 +591,8 @@ module Superposition (B : Terms.Blob) =
 
     let infer_left bag maxvar goal (_alist, atable) =
 	(* 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 
       in
@@ -586,7 +601,7 @@ module Superposition (B : Terms.Blob) =
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g -> 
-	    match simplify_goal maxvar atable bag [] g with
+	    match simplify_goal ~no_demod:false maxvar atable bag [] g with
 	      | None -> assert false
 	      | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals