we demodulate them with active+current
(was: only with current)
+let no_more_passive_goals = function
+ | _,[] -> true
+ | _ -> false
+;;
+
let size_of_passive ((passive_list, ps), _) = List.length passive_list
(* EqualitySet.cardinal ps *)
;;
let size_of_passive ((passive_list, ps), _) = List.length passive_list
(* EqualitySet.cardinal ps *)
;;
-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 active_goals, passive_goals = goals in
- let l,table,_ = build_table [current] in
- simplify_goal_set env goals (l,table)
+ simplify_goal_set env goals active
+ let l,table,_ = build_table [current] in
active_goals,
List.fold_left
(fun acc g ->
active_goals,
List.fold_left
(fun acc g ->
| None ->
(* SELECTION *)
if passive_is_empty passive then
| 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 *)
else
begin
(* COLLECTION OF GARBAGED EQUALITIES *)
prerr_endline "infer";
let new' = infer eq_uri env current active in
prerr_endline "infer goal";
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 ->
(*
match check_if_goals_set_is_solved env active goals with
| Some p ->
let al, tbl = active in
al @ [current], Indexing.index tbl current
in
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 =
(* FORWARD AND BACKWARD SIMPLIFICATION *)
prerr_endline "fwd/back simpl";
let rec simplify new' active passive =