- match res with
- | None -> step goals passive active (g_iterno+1) (s_iterno+1)
- | Some current ->
- (* GENERATION OF NEW EQUATIONS *)
-(* prerr_endline "infer"; *)
- let new' = infer bag eq_uri env current active in
-(* prerr_endline "infer goal"; *)
-(*
- match check_if_goals_set_is_solved env active goals with
- | Some p ->
- prerr_endline
- (Printf.sprintf "Found a proof in: %f\n"
- (Unix.gettimeofday() -. initial_time));
- ParamodulationSuccess p
- | None ->
-*)
-
- let active =
- let al, tbl = active in
- al @ [current], Indexing.index tbl current
- in
- let goals =
- infer_goal_set_with_current bag env current goals active
- in
-
- (* FORWARD AND BACKWARD SIMPLIFICATION *)
-(* prerr_endline "fwd/back simpl"; *)
- let rec simplify new' active passive =
- let new' =
- forward_simplify_new bag eq_uri env new' active
- in
- let active, newa, pruned =
- backward_simplify bag eq_uri env new' active
- in
- let passive =
- List.fold_left (filter_dependent bag) passive pruned
- in
- match newa with
- | None -> active, passive, new'
- | Some p -> simplify (new' @ p) active passive
- in
- let active, passive, new' =
- simplify new' active passive
- in
-
-(* prerr_endline "simpl goal with new"; *)
- let goals =
- let a,b,_ = build_table new' in
-(* let _ = <:start<simplify_goal_set new>> in *)
- let rc = simplify_goal_set bag env goals (a,b) in
-(* let _ = <:stop<simplify_goal_set new>> in *)
- rc
- in
- let passive = add_to_passive passive new' [] in
- step goals passive active (g_iterno+1) (s_iterno+1)
+ if s_iterno > saturation_steps then
+ ParamodulationFailure ("max saturation steps",active,passive,bag)
+ else
+ let current, passive = select env goals passive in
+ match add_to_active_aux bag active passive env eq_uri current with
+ | None, active, passive, bag ->
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
+ | Some new', active, passive, bag ->
+ let bag, active_goals, passive_goals =
+ infer_goal_set_with_current bag env current goals active
+ in
+ let goals =
+ let a,b,_ = build_table new' in
+ let rc =
+ simplify_goal_set bag env (active_goals,passive_goals) (a,b)
+ in
+ rc
+ in
+ step bag goals passive active (g_iterno+1) (s_iterno+1)