+let ids_of_goal g =
+ let p,_,_ = g in
+ let ids = List.map (fun _,_,i,_,_ -> i) p in
+ ids
+;;
+
+let ids_of_goal_set (ga,gp) =
+ List.flatten (List.map ids_of_goal ga) @
+ List.flatten (List.map ids_of_goal gp)
+;;
+
+let size_of_goal_set_a (l,_) = List.length l;;
+let size_of_goal_set_p (_,l) = List.length l;;
+
+(** given-clause algorithm with full reduction strategy: NEW implementation *)
+(* here goals is a set of goals in OR *)
+let given_clause
+ eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
+=
+ let names = names_of_context context in
+ let initial_time = Unix.gettimeofday () in
+ let iterations_left iterno =
+ let now = Unix.gettimeofday () in
+ let time_left = max_time -. now in
+ let time_spent_until_now = now -. initial_time in
+ let iteration_medium_cost =
+ time_spent_until_now /. (float_of_int iterno)
+ in
+ let iterations_left = time_left /. iteration_medium_cost in
+ int_of_float iterations_left
+ in
+ let rec step goals theorems passive active iterno =
+ if iterno > max_iterations then
+ (ParamodulationFailure "No more iterations to spend")
+ else if Unix.gettimeofday () > max_time then
+ (ParamodulationFailure "No more time to spend")
+ else
+(*
+ let _ = prerr_endline "simpl goal with active" in
+ let _ = <:start<simplify goal set active>> in
+ let goals = simplify_goal_set env goals passive active in
+ let _ = <:stop<simplify goal set active>> in
+*)
+ let _ =
+ prerr_endline
+ (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
+ iterno (size_of_active active) (size_of_passive passive)
+ (size_of_goal_set_a goals) (size_of_goal_set_p goals))
+ in
+ (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
+ let passive =
+ let selection_estimate = iterations_left iterno in
+ let kept = size_of_passive passive in
+ if kept > selection_estimate then
+ begin
+ (*Printf.eprintf "Too many passive equalities: pruning...";
+ prune_passive selection_estimate active*) passive
+ end
+ else
+ passive
+ in
+ kept_clauses := (size_of_passive passive) + (size_of_active active);
+ let goals = infer_goal_set env active goals in
+ 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 ->
+ (* SELECTION *)
+ if passive_is_empty passive then
+ ParamodulationFailure "No more passive"(*maybe this is a success! *)
+ else
+ begin
+ (* COLLECTION OF GARBAGED EQUALITIES *)
+ if iterno mod 40 = 0 then
+ begin
+ let active = List.map Equality.id_of (fst active) in
+ let passive = List.map Equality.id_of (fst (fst passive)) in
+ let goal = ids_of_goal_set goals in
+ Equality.collect active passive goal
+ end;
+ let current, passive = select env goals passive in
+ let _ =
+ List.iter
+ (fun _,_,g ->
+ prerr_endline (Printf.sprintf "Current goal = %s\n"
+ (CicPp.pp g names)))
+ (fst goals);
+ prerr_endline (Printf.sprintf "Selected = %s\n"
+ (Equality.string_of_equality ~env current))
+ in
+ (* SIMPLIFICATION OF CURRENT *)
+ let res =
+ forward_simplify eq_uri env (Positive, current) active
+ in
+ match res with
+ | None -> step goals theorems passive active (iterno+1)
+ | Some current ->
+ (* GENERATION OF NEW EQUATIONS *)
+ 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
+ let active =
+ let al, tbl = active in
+ al @ [current], Indexing.index tbl current
+ in
+ (* FORWARD AND BACKWARD SIMPLIFICATION *)
+ prerr_endline "fwd/back simpl";
+ let rec simplify new' active passive =
+ let new' =
+ forward_simplify_new eq_uri env new' ~passive active
+ in
+ let active, passive, newa, retained, pruned =
+ backward_simplify eq_uri env new' ~passive active
+ in
+ let passive =
+ List.fold_left filter_dependent passive pruned
+ in
+ match newa, retained with
+ | None, None -> active, passive, new'
+ | Some p, None
+ | None, Some p -> simplify (new' @ p) active passive
+ | Some p, Some rp -> simplify (new' @ p @ rp) 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 env goals passive (a,b) in
+ let _ = <:stop<simplify_goal_set new>> in
+ rc
+ in
+ let passive = add_to_passive passive new' in
+ step goals theorems passive active (iterno+1)
+ end
+ in
+ step goals theorems passive active 1
+;;
+
+let rec saturate_equations eq_uri env goal accept_fun passive active =