do not infer on closed goals

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 435c95024416b3f232ce280855605de6e0cc1fb1..6c3c5118d62362eadc982fa63ecfbd9672b635cc 100644 (file)
--- 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 8070b4b5db69a2334ccc1e536009ae38895136ea..84de696df9f088f3c0e7cbc4a244e86952355176 100644 (file)
--- 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 f3c6a8bd17a7351e99ce8e59905fda76a37cbf08..25e67131fca0487c4390d310d8307722b5058067 100644 (file)
--- 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