From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 29 Jun 2006 11:17:46 +0000 (+0000)
Subject: before goals are inferred with current,
X-Git-Tag: make_still_working~7123
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a004949b379723275993bbbda15b004908572871;p=helm.git

before goals are inferred with current,
we demodulate them with active+current
(was: only with current)
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 26db9567c..cbf15f0df 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -126,7 +126,11 @@ let passive_is_empty = function
   | _ -> false
 ;;
 
-
+let no_more_passive_goals = function
+  | _,[] -> true
+  | _ -> false
+;;
+  
 let size_of_passive ((passive_list, ps), _) = List.length passive_list
 (* EqualitySet.cardinal ps *)
 ;;
@@ -1069,12 +1073,12 @@ let infer_goal_set env active goals =
 ;;
 *)
 
-let infer_goal_set_with_current env current goals = 
+let infer_goal_set_with_current env current goals active = 
   let active_goals, passive_goals = goals in
-  let l,table,_  = build_table [current] in
   let active_goals, _ = 
-    simplify_goal_set env goals (l,table)
+    simplify_goal_set env goals active
   in
+  let l,table,_  = build_table [current] in
   active_goals, 
   List.fold_left 
     (fun acc g ->
@@ -1156,7 +1160,11 @@ let given_clause
       | None -> 
           (* SELECTION *)
           if passive_is_empty passive then
-            ParamodulationFailure "No more passive"(*maybe this is a success! *)
+            if no_more_passive_goals goals then 
+              ParamodulationFailure "No more passive equations/goals"
+              (*maybe this is a success! *)
+            else
+              step goals theorems passive active (iterno+1)
           else
             begin
               (* COLLECTION OF GARBAGED EQUALITIES *)
@@ -1193,7 +1201,6 @@ let given_clause
                   prerr_endline "infer";
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
-                  let goals = infer_goal_set_with_current env current goals in
 (*
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
@@ -1207,6 +1214,9 @@ let given_clause
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
                   in
+                  let goals = 
+                    infer_goal_set_with_current env current goals active 
+                  in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
                   prerr_endline "fwd/back simpl";
                   let rec simplify new' active passive =