From: denes <??>
Date: Thu, 30 Jul 2009 09:44:05 +0000 (+0000)
Subject: Added check for trivial (identity) goal
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ddba563cd3f42a7947a0e0b464d5dd3c5f9b299d;hp=befd0e7820308a9a09d3499c8131e26578efc462;p=helm.git

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 47119d477..413ab93b6 100644
--- 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