do not infer on closed goals

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

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