From 94ec1bb0fcb0a82bfaaf965aed6993de3a9e658a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 Jun 2009 14:36:37 +0000
Subject: [PATCH] do not infer on closed goals

---
 .../components/ng_paramodulation/paramod.ml   |  3 +--
 .../ng_paramodulation/superposition.ml        | 26 +++++++++++--------
 .../components/syntax_extensions/.depend      |  3 +++
 3 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 435c95024..6c3c5118d 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -168,8 +168,7 @@ module Paramod (B : Terms.Blob) = struct
       let bag, maxvar, new_goals = 
         List.fold_left 
           (fun (bag,m,acc) g -> 
-             let bag, m, ng = Sup.infer_left bag m g
-               ([current],ctable) in
+             let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
                bag,m,ng@acc) 
           (bag,maxvar,[]) g_actives 
       in
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 8070b4b5d..84de696df 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -454,17 +454,19 @@ module Superposition (B : Terms.Blob) =
       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 -> Some (bag,clause)
-	| Some (bag,maxvar,cl,subst) -> 
-	    prerr_endline "Goal subsumed";
-	    raise (Success (bag,maxvar,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 -> Some (bag, clause)
@@ -590,6 +592,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
diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index f3c6a8bd1..25e67131f 100644
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,2 +1,5 @@
+utf8Macro.cmi: 
+utf8MacroTable.cmo: 
+utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
-- 
2.39.2