Added check for trivial (identity) goal

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 47119d4770e25beab157df62540aa120c0d1533e..413ab93b657d41d4a1da2189d8d3f3491b59a555 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -258,12 +258,19 @@ module Superposition (B : Orderings.Blob) =
     (* move away *)
     let is_identity_clause ~unify = function
       | _, [], [Terms.Equation (_,_,_,Terms.Eq),_], _, _ -> true
-      | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
+      | _, [], [Terms.Equation (l,r,_,_),_], vl, _ when unify ->
           (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
       | _ -> false
     ;;
 
+    let is_goal_trivial = function
+      | _, [Terms.Equation (_,_,_,Terms.Eq),_], [], _, _ -> true
+      | _, [Terms.Equation (l,r,_,_),_], [], vl, _ ->
+          (try ignore(Unif.unification (* vl *) [] l r); true
+          with FoUnif.UnificationFailure _ -> false)
+      | _ -> false
+
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
       let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
       (Subst.apply_subst subst t)) subst in
@@ -553,7 +560,7 @@ module Superposition (B : Orderings.Blob) =
         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)
+      if (is_goal_trivial clause)
       then raise (Success (bag, maxvar, clause))
       else   
         let (id,nlit,plit,vl,_) = clause in