From: Enrico Tassi 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 =