+(* sorts the list of passive goals to minimize the search for a proof (doesn't
+ work that well yet...) *)
+let sort_passive_goals goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) ->
+ let r1 = d2 - d1
+ and r2 = (List.length l1) - (List.length l2) in
+ let foldfun ht (_, _, t) =
+ let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t)
+ in ht
+ in
+ let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1)
+ and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2)
+ in let r3 = m1 - m2 in
+ if r3 <> 0 then r3
+ else if r2 <> 0 then r2
+ else r1)
+ (* let _, _, g1 = List.hd l1 *)
+(* and _, _, g2 = List.hd l2 in *)
+(* let e1 = if Inference.term_is_equality g1 then 0 else 1 *)
+(* and e2 = if Inference.term_is_equality g2 then 0 else 1 *)
+(* in let r4 = e1 - e2 in *)
+(* if r4 <> 0 then r3 else r1) *)
+ goals
+;;
+
+
+let print_goals goals =
+ (String.concat "\n"
+ (List.map
+ (fun (d, gl) ->
+ let gl' =
+ List.map
+ (fun (p, _, t) ->
+ (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
+ in
+ Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
+;;
+
+
+(* tries to prove the first conjunction in goals with applications of
+ theorems/equalities, returning new sub-goals or an indication of success *)
+let apply_goal_to_theorems dbd env theorems ?passive active goals =
+ let theorems, _ = theorems in
+ let a_goals, p_goals = goals in
+ let goal = List.hd a_goals in
+ let not_in_active gl =
+ not
+ (List.exists
+ (fun (_, gl') ->
+ if (List.length gl) = (List.length gl') then
+ List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl'
+ else
+ false)
+ a_goals)
+ in
+ let aux theorems =
+ let res = apply_to_goal_conj env theorems ?passive active goal in
+ match res with
+ | `Ok newgoals ->
+ true, ([newgoals], [])
+ | `No _ ->
+ false, (a_goals, p_goals)
+ | `GoOn newgoals ->
+ let newgoals =
+ List.filter
+ (fun (d, gl) ->
+ (d <= !maxdepth) && (List.length gl) <= !maxwidth &&
+ not_in_active gl)
+ newgoals in
+ let p_goals = newgoals @ p_goals in
+ let p_goals = sort_passive_goals p_goals in
+ false, (a_goals, p_goals)
+ in
+ aux theorems
+;;
+
+
+let apply_theorem_to_goals env theorems active goals =
+ let a_goals, p_goals = goals in
+ let theorem = List.hd (fst theorems) in
+ let theorems = [theorem] in
+ let rec aux p = function
+ | [] -> false, ([], p)
+ | goal::tl ->
+ let res = apply_to_goal_conj env theorems active goal in
+ match res with
+ | `Ok newgoals -> true, ([newgoals], [])
+ | `No _ -> aux p tl
+ | `GoOn newgoals -> aux (newgoals @ p) tl
+ in
+ let ok, (a, p) = aux p_goals a_goals in
+ if ok then
+ ok, (a, p)
+ else
+ let p_goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) ->
+ let r = d2 - d1 in
+ if r <> 0 then r
+ else let r = (List.length l1) - (List.length l2) in
+ if r <> 0 then r
+ else
+ let res = ref 0 in
+ let _ =
+ List.exists2
+ (fun (_, _, t1) (_, _, t2) ->
+ let r = Pervasives.compare t1 t2 in
+ if r <> 0 then (res := r; true) else false) l1 l2
+ in !res)
+ p
+ in
+ ok, (a_goals, p_goals)
+;;
+
+
+(* given-clause algorithm with lazy reduction strategy *)
+let rec given_clause dbd env goals theorems passive active =
+ let goals = simplify_goals env goals active in
+ let ok, goals = activate_goal goals in
+ (* let theorems = simplify_theorems env theorems active in *)
+ if ok then
+ let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_aux dbd env goals theorems passive active
+ else
+(* let ok', theorems = activate_theorem theorems in *)
+ let ok', theorems = false, theorems in
+ if ok' then
+ let ok, goals = apply_theorem_to_goals env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_aux dbd env goals theorems passive active
+ else
+ if (passive_is_empty passive) then ParamodulationFailure
+ else given_clause_aux dbd env goals theorems passive active