open Inference;; open Utils;; (* set to false to disable paramodulation inside auto_tac *) let connect_to_auto = true;; (* profiling statistics... *) let infer_time = ref 0.;; let forward_simpl_time = ref 0.;; let forward_simpl_new_time = ref 0.;; let backward_simpl_time = ref 0.;; let passive_maintainance_time = ref 0.;; (* limited-resource-strategy related globals *) let processed_clauses = ref 0;; (* number of equalities selected so far... *) let time_limit = ref 0.;; (* in seconds, settable by the user... *) let start_time = ref 0.;; (* time at which the execution started *) let elapsed_time = ref 0.;; (* let maximal_weight = ref None;; *) let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio;; let symbols_ratio = ref (* 0 *) 3;; let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) Utils.compare_terms := Utils.nonrec_kbo;; (* statistics... *) let derived_clauses = ref 0;; let kept_clauses = ref 0;; (* index of the greatest Cic.Meta created - TODO: find a better way! *) let maxmeta = ref 0;; type result = | ParamodulationFailure | ParamodulationSuccess of Inference.equality option * environment ;; (* let symbols_of_equality (_, (_, left, right), _, _) = TermSet.union (symbols_of_term left) (symbols_of_term right) ;; *) let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = let m1 = symbols_of_term left in let m = TermMap.fold (fun k v res -> try let c = TermMap.find k res in TermMap.add k (c+v) res with Not_found -> TermMap.add k v res) (symbols_of_term right) m1 in (* Printf.printf "symbols_of_equality %s:\n" *) (* (string_of_equality equality); *) (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *) (* print_newline (); *) m ;; module OrderedEquality = struct type t = Inference.equality let compare eq1 eq2 = match meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> let w1, _, (ty, left, right, _), _, a = eq1 and w2, _, (ty', left', right', _), _, a' = eq2 in (* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *) (* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *) (* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *) match Pervasives.compare w1 w2 with | 0 -> let res = (List.length a) - (List.length a') in if res <> 0 then res else ( try let res = Pervasives.compare (List.hd a) (List.hd a') in if res <> 0 then res else Pervasives.compare eq1 eq2 with Failure "hd" -> Pervasives.compare eq1 eq2 (* match a, a' with *) (* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *) (* let res = Pervasives.compare i j in *) (* if res <> 0 then res else Pervasives.compare eq1 eq2 *) (* | _, _ -> Pervasives.compare eq1 eq2 *) ) | res -> res end module EqualitySet = Set.Make(OrderedEquality);; let select env passive (active, _) = processed_clauses := !processed_clauses + 1; let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = List.filter (fun e -> e <> eq) l in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with | 0 -> ( weight_age_counter := !weight_age_ratio; match neg_list, pos_list with | hd::tl, pos -> (* Negatives aren't indexed, no need to remove them... *) (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], hd::tl -> let passive_table = Indexing.remove_index passive_table hd (* if !use_fullred then Indexing.remove_index passive_table hd *) (* else passive_table *) in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) | _, _ -> assert false ) | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> ( symbols_counter := !symbols_counter - 1; let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 in match active with | (Negative, e)::_ -> let symbols = symbols_of_equality e in let card = cardinality symbols in let foldfun k v (r1, r2) = if TermMap.mem k symbols then let c = TermMap.find k symbols in let c1 = abs (c - v) in let c2 = v - c1 in r1 + c2, r2 + c1 else r1, r2 + v in let f equality (i, e) = let common, others = TermMap.fold foldfun (symbols_of_equality equality) (0, 0) in let c = others + (abs (common - card)) in if c < i then (c, equality) (* else if c = i then *) (* match OrderedEquality.compare equality e with *) (* | -1 -> (c, equality) *) (* | res -> (i, e) *) else (i, e) in let e1 = EqualitySet.min_elt pos_set in let initial = let common, others = TermMap.fold foldfun (symbols_of_equality e1) (0, 0) in (others + (abs (common - card))), e1 in let _, current = EqualitySet.fold f pos_set initial in (* Printf.printf "\nsymbols-based selection: %s\n\n" *) (* (string_of_equality ~env current); *) let passive_table = Indexing.remove_index passive_table current (* if !use_fullred then Indexing.remove_index passive_table current *) (* else passive_table *) in (Positive, current), (([], neg_set), (remove current pos_list, EqualitySet.remove current pos_set), passive_table) | _ -> let current = EqualitySet.min_elt pos_set in let passive_table = Indexing.remove_index passive_table current (* if !use_fullred then Indexing.remove_index passive_table current *) (* else passive_table *) in let passive = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), passive_table in (Positive, current), passive ) | _ -> symbols_counter := !symbols_ratio; let set_selection set = EqualitySet.min_elt set in if EqualitySet.is_empty neg_set then let current = set_selection pos_set in let passive = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), Indexing.remove_index passive_table current (* if !use_fullred then Indexing.remove_index passive_table current *) (* else passive_table *) in (Positive, current), passive else let current = set_selection neg_set in let passive = (remove current neg_list, EqualitySet.remove current neg_set), (pos_list, pos_set), passive_table in (Negative, current), passive ;; let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in let table = List.fold_left (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pos (* if !use_fullred then *) (* List.fold_left (fun tbl e -> Indexing.index tbl e) *) (* (Indexing.empty_table ()) pos *) (* else *) (* Indexing.empty_table () *) in (neg, set_of neg), (pos, set_of pos), table ;; let make_active () = [], Indexing.empty_table () ;; let add_to_passive passive (new_neg, new_pos) = let (neg_list, neg_set), (pos_list, pos_set), table = passive in let ok set equality = not (EqualitySet.mem equality set) in let neg = List.filter (ok neg_set) new_neg and pos = List.filter (ok pos_set) new_pos in let table = List.fold_left (fun tbl e -> Indexing.index tbl e) table pos (* if !use_fullred then *) (* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *) (* else *) (* table *) in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities in (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos), table ;; let passive_is_empty = function | ([], _), ([], _), _ -> true | _ -> false ;; let size_of_passive ((_, ns), (_, ps), _) = (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps) ;; let size_of_active (active_list, _) = List.length active_list ;; let prune_passive howmany (active, _) passive = let (nl, ns), (pl, ps), tbl = passive in let howmany = float_of_int howmany and ratio = float_of_int !weight_age_ratio in let round v = let t = ceil v in int_of_float (if t -. v < 0.5 then t else v) in let in_weight = round (howmany *. ratio /. (ratio +. 1.)) and in_age = round (howmany /. (ratio +. 1.)) in debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age); let symbols, card = match active with | (Negative, e)::_ -> let symbols = symbols_of_equality e in let card = TermMap.fold (fun k v res -> res + v) symbols 0 in Some symbols, card | _ -> None, 0 in let counter = ref !symbols_ratio in let rec pickw w ns ps = if w > 0 then if not (EqualitySet.is_empty ns) then let e = EqualitySet.min_elt ns in let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in EqualitySet.add e ns', ps else if !counter > 0 then let _ = counter := !counter - 1; if !counter = 0 then counter := !symbols_ratio in match symbols with | None -> let e = EqualitySet.min_elt ps in let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in ns, EqualitySet.add e ps' | Some symbols -> let foldfun k v (r1, r2) = if TermMap.mem k symbols then let c = TermMap.find k symbols in let c1 = abs (c - v) in let c2 = v - c1 in r1 + c2, r2 + c1 else r1, r2 + v in let f equality (i, e) = let common, others = TermMap.fold foldfun (symbols_of_equality equality) (0, 0) in let c = others + (abs (common - card)) in if c < i then (c, equality) else (i, e) in let e1 = EqualitySet.min_elt ps in let initial = let common, others = TermMap.fold foldfun (symbols_of_equality e1) (0, 0) in (others + (abs (common - card))), e1 in let _, e = EqualitySet.fold f ps initial in let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in ns, EqualitySet.add e ps' else let e = EqualitySet.min_elt ps in let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in ns, EqualitySet.add e ps' else EqualitySet.empty, EqualitySet.empty in (* let in_weight, ns = pickw in_weight ns in *) (* let _, ps = pickw in_weight ps in *) let ns, ps = pickw in_weight ns ps in let rec picka w s l = if w > 0 then match l with | [] -> w, s, [] | hd::tl when not (EqualitySet.mem hd s) -> let w, s, l = picka (w-1) s tl in w, EqualitySet.add hd s, hd::l | hd::tl -> let w, s, l = picka w s tl in w, s, hd::l else 0, s, l in let in_age, ns, nl = picka in_age ns nl in let _, ps, pl = picka in_age ps pl in if not (EqualitySet.is_empty ps) then (* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *) maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) (* if !use_fullred then *) (* EqualitySet.fold *) (* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *) (* else *) (* tbl *) in (nl, ns), (pl, ps), tbl ;; let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with | Negative -> let maxm, res = Indexing.superposition_left !maxmeta env active_table current in maxmeta := maxm; res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in maxmeta := maxm; let rec infer_positive table = function | [] -> [], [] | (Negative, equality)::tl -> let maxm, res = Indexing.superposition_left !maxmeta env table equality in maxmeta := maxm; let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> let maxm, res = Indexing.superposition_right !maxmeta env table equality in maxmeta := maxm; let neg, pos = infer_positive table tl in neg, res @ pos in let curr_table = Indexing.index (Indexing.empty_table ()) current in let neg, pos = infer_positive curr_table active_list in neg, res @ pos in derived_clauses := !derived_clauses + (List.length new_neg) + (List.length new_pos); match !maximal_retained_equality with | None -> new_neg, new_pos | Some eq -> (* if we have a maximal_retained_equality, we can discard all equalities "greater" than it, as they will never be reached... An equality is greater than maximal_retained_equality if it is bigger wrt. OrderedEquality.compare and it is less similar than maximal_retained_equality to the current goal *) let symbols, card = match active_list with | (Negative, e)::_ -> let symbols = symbols_of_equality e in let card = TermMap.fold (fun k v res -> res + v) symbols 0 in Some symbols, card | _ -> None, 0 in let new_pos = match symbols with | None -> List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos | Some symbols -> let filterfun e = if OrderedEquality.compare e eq <= 0 then true else let foldfun k v (r1, r2) = if TermMap.mem k symbols then let c = TermMap.find k symbols in let c1 = abs (c - v) in let c2 = v - c1 in r1 + c2, r2 + c1 else r1, r2 + v in let initial = let common, others = TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in others + (abs (common - card)) in let common, others = TermMap.fold foldfun (symbols_of_equality e) (0, 0) in let c = others + (abs (common - card)) in if c < initial then true else false in List.filter filterfun new_pos in new_neg, new_pos ;; let contains_empty env (negative, positive) = let metasenv, context, ugraph = env in try let found = List.find (fun (w, proof, (ty, left, right, ordering), m, a) -> fst (CicReduction.are_convertible context left right ugraph)) negative in true, Some found with Not_found -> false, None ;; let forward_simplify env (sign, current) ?passive (active_list, active_table) = let pl, passive_table = match passive with | None -> [], None | Some ((pn, _), (pp, _), pt) -> let pn = List.map (fun e -> (Negative, e)) pn and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in let all = if pl = [] then active_list else active_list @ pl in (* let rec find_duplicate sign current = function *) (* | [] -> false *) (* | (s, eq)::tl when s = sign -> *) (* if meta_convertibility_eq current eq then true *) (* else find_duplicate sign current tl *) (* | _::tl -> find_duplicate sign current tl *) (* in *) (* let res = *) (* if sign = Positive then *) (* Indexing.subsumption env active_table current *) (* else *) (* false *) (* in *) (* if res then *) (* None *) (* else *) let demodulate table current = let newmeta, newcurrent = Indexing.demodulation !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) else None else Some (sign, newcurrent) in let res = let res = demodulate active_table current in match res with | None -> None | Some (sign, newcurrent) -> match passive_table with | None -> res | Some passive_table -> demodulate passive_table newcurrent in match res with | None -> None | Some (Negative, c) -> let ok = not ( List.exists (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c) all) in if ok then res else None | Some (Positive, c) -> if Indexing.in_index active_table c then None else match passive_table with | None -> res | Some passive_table -> if Indexing.in_index passive_table c then None else res (* | Some (s, c) -> if find_duplicate s c all then None else res *) (* if s = Utils.Negative then *) (* res *) (* else *) (* if Indexing.subsumption env active_table c then *) (* None *) (* else ( *) (* match passive_table with *) (* | None -> res *) (* | Some passive_table -> *) (* if Indexing.subsumption env passive_table c then *) (* None *) (* else *) (* res *) (* ) *) (* let pred (sign, eq) = *) (* if sign <> s then false *) (* else subsumption env c eq *) (* in *) (* if List.exists pred all then None *) (* else res *) ;; type fs_time_info_t = { mutable build_all: float; mutable demodulate: float; mutable subsumption: float; };; let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };; let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in let active_list, active_table = active in let pl, passive_table = match passive with | None -> [], None | Some ((pn, _), (pp, _), pt) -> let pn = List.map (fun e -> (Negative, e)) pn and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in let all = active_list @ pl in let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); let demodulate sign table target = let newmeta, newtarget = Indexing.demodulation !maxmeta env table sign target in maxmeta := newmeta; newtarget in (* let f sign' target (sign, eq) = *) (* if sign <> sign' then false *) (* else subsumption env target eq *) (* in *) let t1 = Unix.gettimeofday () in let new_neg, new_pos = let new_neg = List.map (demodulate Negative active_table) new_neg and new_pos = List.map (demodulate Positive active_table) new_pos in match passive_table with | None -> new_neg, new_pos | Some passive_table -> List.map (demodulate Negative passive_table) new_neg, List.map (demodulate Positive passive_table) new_pos in let t2 = Unix.gettimeofday () in fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1); let new_pos_set = List.fold_left (fun s e -> if not (Inference.is_identity env e) then if EqualitySet.mem e s then s else EqualitySet.add e s else s) EqualitySet.empty new_pos in let new_pos = EqualitySet.elements new_pos_set in let subs = match passive_table with | None -> (fun e -> not (Indexing.subsumption env active_table e)) | Some passive_table -> (fun e -> not ((Indexing.subsumption env active_table e) || (Indexing.subsumption env passive_table e))) in let t1 = Unix.gettimeofday () in (* let new_neg, new_pos = *) (* List.filter subs new_neg, *) (* List.filter subs new_pos *) (* in *) (* let new_neg, new_pos = *) (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) (* in *) let t2 = Unix.gettimeofday () in fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); let is_duplicate = match passive_table with | None -> (fun e -> not (Indexing.in_index active_table e)) | Some passive_table -> (fun e -> not ((Indexing.in_index active_table e) || (Indexing.in_index passive_table e))) in new_neg, List.filter is_duplicate new_pos (* new_neg, new_pos *) (* let res = *) (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) (* in *) (* res *) ;; let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in let active_list, newa = List.fold_right (fun (s, equality) (res, newn) -> let ew, _, _, _, _ = equality in if ew < min_weight then (s, equality)::res, newn else match forward_simplify env (s, equality) (new_pos, new_table) with | None -> res, newn | Some (s, e) -> if equality = e then (s, e)::res, newn else res, (s, e)::newn) active_list ([], []) in let find eq1 where = List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where in let active, newa = List.fold_right (fun (s, eq) (res, tbl) -> if List.mem (s, eq) res then res, tbl else if (is_identity env eq) || (find eq res) then ( res, tbl ) (* else if (find eq res) then *) (* res, tbl *) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) active_list ([], Indexing.empty_table ()), List.fold_right (fun (s, eq) (n, p) -> if (s <> Negative) && (is_identity env eq) then ( (n, p) ) else if s = Negative then eq::n, p else n, eq::p) newa ([], []) in match newa with | [], [] -> active, None | _ -> active, Some newa ;; let backward_simplify_passive env new_pos new_table min_weight passive = let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = let ew, _, _, _, _ = equality in if ew < min_weight then (* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *) equality::resl, ress, newn else match forward_simplify env (sign, equality) (new_pos, new_table) with | None -> resl, EqualitySet.remove equality ress, newn | Some (s, e) -> if equality = e then equality::resl, ress, newn else let ress = EqualitySet.remove equality ress in resl, ress, e::newn in let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, []) and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in let passive_table = List.fold_left (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl in match newn, newp with | [], [] -> ((nl, ns), (pl, ps), passive_table), None | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp) ;; let backward_simplify env new' ?passive active = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> let ew, _, _, _, _ = e in (Positive, e)::l, Indexing.index t e, min ew w) ([], Indexing.empty_table (), 1000000) (snd new') in let active, newa = backward_simplify_active env new_pos new_table min_weight active in match passive with | None -> active, (make_passive [] []), newa, None | Some passive -> let passive, newp = backward_simplify_passive env new_pos new_table min_weight passive in active, passive, newa, newp ;; let get_selection_estimate () = elapsed_time := (Unix.gettimeofday ()) -. !start_time; (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *) int_of_float ( ceil ((float_of_int !processed_clauses) *. ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.))) ;; let rec given_clause env passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in let kept = size_of_passive passive in let passive = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" !time_limit !elapsed_time); make_passive [] [] ) else if kept > selection_estimate then ( debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ "(kept: %d, selection_estimate: %d)\n") kept selection_estimate); prune_passive selection_estimate active passive ) else passive in let time2 = Unix.gettimeofday () in passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1); kept_clauses := (size_of_passive passive) + (size_of_active active); match passive_is_empty passive with | true -> ParamodulationFailure | false -> let (sign, current), passive = select env passive active in let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in forward_simpl_time := !forward_simpl_time +. (time2 -. time1); match res with | None -> given_clause env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current)); ParamodulationSuccess (Some current, env) ) else ( debug_print "\n================================================"; debug_print (Printf.sprintf "selected: %s %s" (string_of_sign sign) (string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); let res, goal = contains_empty env new' in if res then ParamodulationSuccess (goal, env) else let t1 = Unix.gettimeofday () in let new' = forward_simplify_new env new' (* ~passive *) active in let t2 = Unix.gettimeofday () in let _ = forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1) in let active = match sign with | Negative -> active | Positive -> let t1 = Unix.gettimeofday () in let active, _, newa, _ = backward_simplify env ([], [current]) active in let t2 = Unix.gettimeofday () in backward_simpl_time := !backward_simpl_time +. (t2 -. t1); match newa with | None -> active | Some (n, p) -> let al, tbl = active in let nn = List.map (fun e -> Negative, e) n in let pp, tbl = List.fold_right (fun e (l, t) -> (Positive, e)::l, Indexing.index tbl e) p ([], tbl) in nn @ al @ pp, tbl in (* let _ = *) (* Printf.printf "active:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map *) (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *) (* (string_of_equality ~env e)) (fst active)))); *) (* print_newline (); *) (* in *) (* let _ = *) (* match new' with *) (* | neg, pos -> *) (* Printf.printf "new':\n%s\n" *) (* (String.concat "\n" *) (* ((List.map *) (* (fun e -> "Negative " ^ *) (* (string_of_equality ~env e)) neg) @ *) (* (List.map *) (* (fun e -> "Positive " ^ *) (* (string_of_equality ~env e)) pos))); *) (* print_newline (); *) (* in *) match contains_empty env new' with | false, _ -> let active = let al, tbl = active in match sign with | Negative -> (sign, current)::al, tbl | Positive -> al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in let (_, ns), (_, ps), _ = passive in (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ns)) @ *) (* (List.map (fun e -> "Positive " ^ *) (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) given_clause env passive active | true, goal -> ParamodulationSuccess (goal, env) ) ;; let rec given_clause_fullred env passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in let kept = size_of_passive passive in let passive = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" !time_limit !elapsed_time); make_passive [] [] ) else if kept > selection_estimate then ( debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ "(kept: %d, selection_estimate: %d)\n") kept selection_estimate); prune_passive selection_estimate active passive ) else passive in let time2 = Unix.gettimeofday () in passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1); kept_clauses := (size_of_passive passive) + (size_of_active active); match passive_is_empty passive with | true -> ParamodulationFailure | false -> let (sign, current), passive = select env passive active in let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in forward_simpl_time := !forward_simpl_time +. (time2 -. time1); match res with | None -> given_clause_fullred env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current)); ParamodulationSuccess (Some current, env) ) else ( debug_print "\n================================================"; debug_print (Printf.sprintf "selected: %s %s" (string_of_sign sign) (string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); let active = if is_identity env current then active else let al, tbl = active in match sign with | Negative -> (sign, current)::al, tbl | Positive -> al @ [(sign, current)], Indexing.index tbl current in let rec simplify new' active passive = let t1 = Unix.gettimeofday () in let new' = forward_simplify_new env new' ~passive active in let t2 = Unix.gettimeofday () in forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1); let t1 = Unix.gettimeofday () in let active, passive, newa, retained = backward_simplify env new' ~passive active in let t2 = Unix.gettimeofday () in backward_simpl_time := !backward_simpl_time +. (t2 -. t1); match newa, retained with | None, None -> active, passive, new' | Some (n, p), None | None, Some (n, p) -> let nn, np = new' in simplify (nn @ n, np @ p) active passive | Some (n, p), Some (rn, rp) -> let nn, np = new' in simplify (nn @ n @ rn, np @ p @ rp) active passive in let active, passive, new' = simplify new' active passive in let k = size_of_passive passive in if k < (kept - 1) then processed_clauses := !processed_clauses + (kept - 1 - k); let _ = debug_print ( Printf.sprintf "active:\n%s\n" (String.concat "\n" ((List.map (fun (s, e) -> (string_of_sign s) ^ " " ^ (string_of_equality ~env e)) (fst active))))) in let _ = match new' with | neg, pos -> debug_print ( Printf.sprintf "new':\n%s\n" (String.concat "\n" ((List.map (fun e -> "Negative " ^ (string_of_equality ~env e)) neg) @ (List.map (fun e -> "Positive " ^ (string_of_equality ~env e)) pos)))) in match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in (* let (_, ns), (_, ps), _ = passive in *) (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ns)) @ *) (* (List.map (fun e -> "Positive " ^ *) (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) given_clause_fullred env passive active | true, goal -> ParamodulationSuccess (goal, env) ) ;; let given_clause_ref = ref given_clause;; let main dbd term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in let module PP = CicPp in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in let proof, goals = status in let goal' = List.nth goals 0 in let _, metasenv, meta_proof, _ = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in let library_equalities, maxm = find_library_equalities ~dbd context (proof, goal') (maxm+2) in maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = let _, context, ty = CicUtil.lookup_meta goal' metasenv in Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); print_newline (); Cic.Meta (maxm+1, irl), (maxm+1, context, ty)::metasenv, ty in (* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in try let term_equality = equality_of_term new_meta_goal goal in let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in if is_identity env term_equality then let proof = Cic.Appl [Cic.MutConstruct (* reflexivity *) (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); eq_ty; left] in let _ = Printf.printf "OK, found a proof!\n"; let names = names_of_context context in print_endline (PP.pp proof names) in () else let equalities = let equalities = equalities @ library_equalities in debug_print ( Printf.sprintf "equalities:\n%s\n" (String.concat "\n" (List.map string_of_equality equalities))); debug_print "SIMPLYFYING EQUALITIES..."; let rec simpl e others others_simpl = let active = others @ others_simpl in let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) (Indexing.empty_table ()) active in let res = forward_simplify env e (active, tbl) in match others with | hd::tl -> ( match res with | None -> simpl hd tl others_simpl | Some e -> simpl hd tl (e::others_simpl) ) | [] -> ( match res with | None -> others_simpl | Some e -> e::others_simpl ) in match equalities with | [] -> [] | hd::tl -> let others = List.map (fun e -> (Positive, e)) tl in let res = List.rev (List.map snd (simpl (Positive, hd) others [])) in debug_print ( Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" (List.map string_of_equality res))); res in let active = make_active () in let passive = make_passive [term_equality] equalities in Printf.printf "\ncurrent goal: %s\n" (string_of_equality ~env term_equality); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map (string_of_equality ~env) (equalities @ library_equalities))); print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; start_time := Unix.gettimeofday (); let res = (if !use_fullred then given_clause_fullred else given_clause) env passive active in let finish = Unix.gettimeofday () in let _ = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" | ParamodulationSuccess (Some goal, env) -> let proof = Inference.build_proof_term goal in let newmetasenv = List.fold_left (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities in let _ = try let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in Printf.printf "OK, found a proof!\n"; (* REMEMBER: we have to instantiate meta_proof, we should use apply the "apply" tactic to proof and status *) let names = names_of_context context in print_endline (PP.pp proof names); (* print_endline (PP.ppterm proof); *) print_endline (string_of_float (finish -. start)); Printf.printf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" (CicPp.pp type_of_goal names) (CicPp.pp ty names) (string_of_bool (fst (CicReduction.are_convertible context type_of_goal ty ug))); with e -> Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); Printf.printf "MAXMETA USED: %d\n" !maxmeta; print_endline (string_of_float (finish -. start)); in () | ParamodulationSuccess (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ "forward_simpl_new_time: %.9f\n" ^^ "backward_simpl_time: %.9f\n") !infer_time !forward_simpl_time !forward_simpl_new_time !backward_simpl_time; Printf.printf "passive_maintainance_time: %.9f\n" !passive_maintainance_time; Printf.printf " successful unification/matching time: %.9f\n" !Indexing.match_unif_time_ok; Printf.printf " failed unification/matching time: %.9f\n" !Indexing.match_unif_time_no; Printf.printf " indexing retrieval time: %.9f\n" !Indexing.indexing_retrieval_time; Printf.printf " demodulate_term.build_newtarget_time: %.9f\n" !Indexing.build_newtarget_time; Printf.printf "derived %d clauses, kept %d clauses.\n" !derived_clauses !kept_clauses; with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); raise exc ;; let saturate dbd (proof, goal) = let module C = Cic in maxmeta := 0; let goal' = goal in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let _, context, ty = CicUtil.lookup_meta goal' metasenv in debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)); Cic.Meta (maxm+1, irl), (maxm+1, context, ty)::metasenv, ty in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in (* try *) let term_equality = equality_of_term new_meta_goal goal in let res, time = if is_identity env term_equality then let w, _, (eq_ty, left, right, o), m, a = term_equality in let proof = Cic.Appl [Cic.MutConstruct (* reflexivity *) (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); eq_ty; left] in (ParamodulationSuccess (Some (0, Inference.BasicProof proof, (eq_ty, left, right, o), m, a), env), 0.) else let library_equalities, maxm = find_library_equalities ~dbd context (proof, goal') (maxm+2) in maxmeta := maxm+2; let equalities = let equalities = equalities @ library_equalities in debug_print ( Printf.sprintf "equalities:\n%s\n" (String.concat "\n" (List.map string_of_equality equalities))); debug_print "SIMPLYFYING EQUALITIES..."; let rec simpl e others others_simpl = let active = others @ others_simpl in let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) (Indexing.empty_table ()) active in let res = forward_simplify env e (active, tbl) in match others with | hd::tl -> ( match res with | None -> simpl hd tl others_simpl | Some e -> simpl hd tl (e::others_simpl) ) | [] -> ( match res with | None -> others_simpl | Some e -> e::others_simpl ) in match equalities with | [] -> [] | hd::tl -> let others = List.map (fun e -> (Positive, e)) tl in let res = List.rev (List.map snd (simpl (Positive, hd) others [])) in debug_print ( Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" (List.map string_of_equality res))); res in let active = make_active () in let passive = make_passive [term_equality] equalities in let start = Unix.gettimeofday () in let res = given_clause_fullred env passive active in let finish = Unix.gettimeofday () in (res, finish -. start) in match res with | ParamodulationSuccess (Some goal, env) -> debug_print "OK, found a proof!"; let proof = Inference.build_proof_term goal in let names = names_of_context context in let newmetasenv = let i1 = match new_meta_goal with | C.Meta (i, _) -> i | _ -> assert false in (* let i2 = *) (* match meta_proof with *) (* | C.Meta (i, _) -> i *) (* | t -> *) (* Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *) (* (CicPp.pp meta_proof names) (string_of_int goal'); *) (* print_newline (); *) (* assert false *) (* in *) List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in let newstatus = try let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in debug_print (CicPp.pp proof [](* names *)); debug_print (Printf.sprintf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" (CicPp.pp type_of_goal names) (CicPp.pp ty names) (string_of_bool (fst (CicReduction.are_convertible context type_of_goal ty ug)))); let equality_for_replace i t1 = match t1 with | C.Meta (n, _) -> n = i | _ -> false in let real_proof = ProofEngineReduction.replace ~equality:equality_for_replace ~what:[goal'] ~with_what:[proof] ~where:meta_proof in debug_print ( Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" (match uri with Some uri -> UriManager.string_of_uri uri | None -> "") (print_metasenv newmetasenv) (CicPp.pp real_proof [](* names *)) (CicPp.pp term_to_prove names)); ((uri, newmetasenv, real_proof, term_to_prove), []) with CicTypeChecker.TypeCheckerFailure _ -> debug_print "THE PROOF DOESN'T TYPECHECK!!!"; debug_print (CicPp.pp proof names); raise (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck") in debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time); newstatus | _ -> raise (ProofEngineTypes.Fail "NO proof found") (* with e -> *) (* raise (Failure "saturation failed") *) ;; (* dummy function called within matita to trigger linkage *) let init () = ();; (* UGLY SIDE EFFECT... *) if connect_to_auto then ( AutoTactic.paramodulation_tactic := saturate; AutoTactic.term_is_equality := Inference.term_is_equality; );;