X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=8e67bc7a05cee8147a2f0a774f56f0fe7073d12e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=634df11ffb4a766f6ca18080f55197dcd815b3dd;hpb=bdc855b1b6c9552a49a01769cb906a438ca60cc4;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 634df11ff..8e67bc7a0 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1,43 +1,84 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + 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 false;; -let weight_age_ratio = ref 0;; (* settable by the user from the command line *) +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;; +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;; +(* varbiables controlling the search-space *) +let maxdepth = ref 3;; +let maxwidth = ref 3;; + type result = - | Failure - | Success of Cic.term option * environment + | ParamodulationFailure + | ParamodulationSuccess of Inference.proof option * environment ;; +type goal = proof * Cic.metasenv * Cic.term;; -(* -let symbols_of_equality (_, (_, left, right), _, _) = - TermSet.union (symbols_of_term left) (symbols_of_term right) -;; -*) +type theorem = Cic.term * Cic.term * Cic.metasenv;; -let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) = + +let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = let m1 = symbols_of_term left in let m = TermMap.fold @@ -49,10 +90,6 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) = 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 ;; @@ -64,22 +101,32 @@ module OrderedEquality = struct match meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let _, (ty, left, right, _), _, _ = eq1 - and _, (ty', left', right', _), _, _ = 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 + let w1, _, (ty, left, right, _), _, a = eq1 + and w2, _, (ty', left', right', _), _, a' = eq2 in match Pervasives.compare w1 w2 with - | 0 -> Pervasives.compare eq1 eq2 + | 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 + ) | res -> res end module EqualitySet = Set.Make(OrderedEquality);; -let select env passive (active, _) = +(** + selects one equality from passive. The selection strategy is a combination + of weight, age and goal-similarity +*) +let select env goals passive (active, _) = processed_clauses := !processed_clauses + 1; - + let goal = + match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false + in let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = List.filter (fun e -> e <> eq) l @@ -97,8 +144,6 @@ let select env passive (active, _) = | [], 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) @@ -109,59 +154,43 @@ let select env passive (active, _) = 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 (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 + let symbols = + let _, _, term = goal in + symbols_of_term term + 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 (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 + let passive_table = + Indexing.remove_index passive_table current + in + (Positive, current), + (([], neg_set), + (remove current pos_list, EqualitySet.remove current pos_set), + passive_table) ) | _ -> symbols_counter := !symbols_ratio; @@ -172,8 +201,6 @@ let select env passive (active, _) = (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 @@ -187,6 +214,7 @@ let select env passive (active, _) = ;; +(* initializes the passive set of equalities *) let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities @@ -194,11 +222,6 @@ let make_passive neg pos = 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), @@ -211,17 +234,15 @@ let make_active () = ;; +(* adds to passive a list of equalities: new_neg is a list of negative + equalities, new_pos a list of positive equalities *) 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 *) + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities @@ -243,13 +264,25 @@ let size_of_passive ((_, ns), (_, ps), _) = ;; +let size_of_active (active_list, _) = + List.length active_list +;; + + +(* removes from passive equalities that are estimated impossible to activate + within the current time limit *) 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 in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.)) - and in_age = int_of_float (howmany /. (ratio +. 1.)) in - Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age; + 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 + (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); let symbols, card = match active with | (Negative, e)::_ -> @@ -310,8 +343,6 @@ let prune_passive howmany (active, _) passive = 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 @@ -324,30 +355,29 @@ let prune_passive howmany (active, _) passive = let w, s, l = picka w s tl in w, s, hd::l else - 0, s, [] + 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_retained_equality := Some (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 ;; +(** inference of new equalities between current and some in active *) let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with | Negative -> - Indexing.superposition_left env active_table current, [] + 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 @@ -355,7 +385,9 @@ let infer env sign current (active_list, active_table) = let rec infer_positive table = function | [] -> [], [] | (Negative, equality)::tl -> - let res = Indexing.superposition_left env table equality in + 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 -> @@ -369,11 +401,54 @@ let infer env sign current (active_list, active_table) = 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 -> - let new_pos = - List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos in + (* 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 ;; @@ -381,18 +456,19 @@ let infer env sign current (active_list, active_table) = let contains_empty env (negative, positive) = let metasenv, context, ugraph = env in try - let (proof, _, _, _) = + let found = List.find - (fun (proof, (ty, left, right, ordering), m, a) -> + (fun (w, proof, (ty, left, right, ordering), m, a) -> fst (CicReduction.are_convertible context left right ugraph)) negative in - true, Some proof + true, Some found with Not_found -> false, None ;; +(** simplifies current using active and passive *) let forward_simplify env (sign, current) ?passive (active_list, active_table) = let pl, passive_table = match passive with @@ -403,20 +479,26 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = 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 demodulate table current = let newmeta, newcurrent = - Indexing.demodulation !maxmeta env table current in + Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then - if sign = Negative then Some (sign, newcurrent) else None + if sign = Negative then Some (sign, newcurrent) + else ( +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) +(* (string_of_equality current) *) +(* (string_of_equality newcurrent))); *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "active is: %s" *) +(* (String.concat "\n" *) +(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) + None + ) else Some (sign, newcurrent) in @@ -443,33 +525,18 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = None else match passive_table with - | None -> res + | None -> + if fst (Indexing.subsumption env active_table c) then + None + else + 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 *) + if Indexing.in_index passive_table c then None + else + let r1, _ = Indexing.subsumption env active_table c in + if r1 then None else + let r2, _ = Indexing.subsumption env passive_table c in + if r2 then None else res ;; type fs_time_info_t = { @@ -481,6 +548,7 @@ type fs_time_info_t = { let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };; +(** simplifies new using active and passive *) let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in @@ -498,26 +566,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); - let demodulate table target = - let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in + let demodulate sign table target = + let newmeta, newtarget = + Indexing.demodulation_equality !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 active_table) new_neg - and new_pos = List.map (demodulate active_table) new_pos in + 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 passive_table) new_neg, - List.map (demodulate passive_table) new_pos + List.map (demodulate Negative passive_table) new_neg, + List.map (demodulate Positive passive_table) new_pos in let t2 = Unix.gettimeofday () in @@ -526,71 +590,55 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let new_pos_set = List.fold_left (fun s e -> - if not (Inference.is_identity env e) then EqualitySet.add e s else s) + 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 subs = + match passive_table with + | None -> + (fun e -> not (fst (Indexing.subsumption env active_table e))) + | Some passive_table -> + (fun e -> not ((fst (Indexing.subsumption env active_table e)) || + (fst (Indexing.subsumption env passive_table e)))) + in +(* let t1 = Unix.gettimeofday () 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)) + | 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))) + (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 *) + new_neg, List.filter subs (List.filter is_duplicate new_pos) ;; -let backward_simplify_active env (new_neg, new_pos) active = +(** simplifies active usign new *) +let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in - let new_pos, new_table = - List.fold_left - (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) - ([], Indexing.empty_table ()) new_pos - in let active_list, newa = List.fold_right (fun (s, equality) (res, newn) -> - 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) + 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 = @@ -599,16 +647,19 @@ let backward_simplify_active env (new_neg, new_pos) active = let active, newa = List.fold_right (fun (s, eq) (res, tbl) -> - if (is_identity env eq) || (find eq res) then + if List.mem (s, eq) res then res, tbl + else if (is_identity env eq) || (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 + if (s <> Negative) && (is_identity env eq) then ( (n, p) - else + ) else if s = Negative then eq::n, p else n, eq::p) newa ([], []) @@ -619,22 +670,22 @@ let backward_simplify_active env (new_neg, new_pos) active = ;; -let backward_simplify_passive env (new_neg, new_pos) passive = - let new_pos, new_table = - List.fold_left - (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) - ([], Indexing.empty_table ()) new_pos - in +(** simplifies passive using new *) +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) = - 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 + let ew, _, _, _, _ = equality in + if ew < min_weight then + 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 @@ -649,77 +700,774 @@ let backward_simplify_passive env (new_neg, new_pos) passive = let backward_simplify env new' ?passive active = - let active, newa = backward_simplify_active env new' active in + 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' passive in + backward_simplify_passive env new_pos new_table min_weight passive in active, passive, newa, newp ;; +(* returns an estimation of how many equalities in passive can be activated + within the current time limit *) 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 /. !elapsed_time -. 1.))) + ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.))) ;; - -let rec given_clause env passive active = + +(** initializes the set of goals *) +let make_goals goal = + let active = [] + and passive = [0, [goal]] in + active, passive +;; + + +(** initializes the set of theorems *) +let make_theorems theorems = + theorems, [] +;; + + +let activate_goal (active, passive) = + match passive with + | goal_conj::tl -> true, (goal_conj::active, tl) + | [] -> false, (active, passive) +;; + + +let activate_theorem (active, passive) = + match passive with + | theorem::tl -> true, (theorem::active, tl) + | [] -> false, (active, passive) +;; + + +(** simplifies a goal with equalities in active and passive *) +let simplify_goal env goal ?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 demodulate table goal = + let newmeta, newgoal = + Indexing.demodulation_goal !maxmeta env table goal in + maxmeta := newmeta; + goal != newgoal, newgoal + in + let changed, goal = + match passive_table with + | None -> demodulate active_table goal + | Some passive_table -> + let changed, goal = demodulate active_table goal in + let changed', goal = demodulate passive_table goal in + (changed || changed'), goal + in + changed, goal +;; + + +let simplify_goals env goals ?passive active = + let a_goals, p_goals = goals in + let p_goals = + List.map + (fun (d, gl) -> + let gl = + List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in + d, gl) + p_goals + in + let goals = + List.fold_left + (fun (a, p) (d, gl) -> + let changed = ref false in + let gl = + List.map + (fun g -> + let c, g = simplify_goal env g ?passive active in + changed := !changed || c; g) gl in + if !changed then (a, (d, gl)::p) else ((d, gl)::a, p)) + ([], p_goals) a_goals + in + goals +;; + + +let simplify_theorems env theorems ?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 a_theorems, p_theorems = theorems in + let demodulate table theorem = + let newmeta, newthm = + Indexing.demodulation_theorem !maxmeta env table theorem in + maxmeta := newmeta; + theorem != newthm, newthm + in + let foldfun table (a, p) theorem = + let changed, theorem = demodulate table theorem in + if changed then (a, theorem::p) else (theorem::a, p) + in + let mapfun table theorem = snd (demodulate table theorem) in + match passive_table with + | None -> + let p_theorems = List.map (mapfun active_table) p_theorems in + List.fold_left (foldfun active_table) ([], p_theorems) a_theorems + | Some passive_table -> + let p_theorems = List.map (mapfun active_table) p_theorems in + let p_theorems, a_theorems = + List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in + let p_theorems = List.map (mapfun passive_table) p_theorems in + List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems +;; + + +(* applies equality to goal to see if the goal can be closed *) +let apply_equality_to_goal env equality goal = + let module C = Cic in + let module HL = HelmLibraryObjects in + let module I = Inference in + let metasenv, context, ugraph = env in + let _, proof, (ty, left, right, _), metas, args = equality in + let eqterm = + C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in + let gproof, gmetas, gterm = goal in +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *) +(* (string_of_equality equality) (CicPp.ppterm gterm))); *) + try + let subst, metasenv', _ = + let menv = metasenv @ metas @ gmetas in + Inference.unification menv context eqterm gterm ugraph + in + let newproof = + match proof with + | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t) + | I.ProofBlock (s, uri, nt, t, pe, p) -> + I.ProofBlock (subst @ s, uri, nt, t, pe, p) + | _ -> assert false + in + let newgproof = + let rec repl = function + | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp) + | I.NoProof -> newproof + | I.BasicProof p -> newproof + | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p) + | _ -> assert false + in + repl gproof + in + true, subst, newgproof + with CicUnification.UnificationFailure _ -> + false, [], I.NoProof +;; + + + +let new_meta metasenv = + let m = CicMkImplicit.new_meta metasenv [] in + incr maxmeta; + while !maxmeta <= m do incr maxmeta done; + !maxmeta +;; + + +(* applies a theorem or an equality to goal, returning a list of subgoals or + an indication of failure *) +let apply_to_goal env theorems ?passive active goal = + let metasenv, context, ugraph = env in + let proof, metas, term = goal in + (* debug_print *) + (* (lazy *) + (* (Printf.sprintf "apply_to_goal with goal: %s" *) + (* (\* (string_of_proof proof) *\)(CicPp.ppterm term))); *) + let status = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let proof', newmeta = + let rec get_meta = function + | SubProof (t, i, p) -> + let t', i' = get_meta p in + if i' = -1 then t, i else t', i' + | ProofGoalBlock (_, p) -> get_meta p + | _ -> Cic.Implicit None, -1 + in + let p, m = get_meta proof in + if m = -1 then + let n = new_meta (metasenv @ metas) in + Cic.Meta (n, irl), n + else + p, m + in + let metasenv = (newmeta, context, term)::metasenv @ metas in + let bit = new_meta metasenv, context, term in + let metasenv' = bit::metasenv in + ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta) + in + let rec aux = function + | [] -> `No + | (theorem, thmty, _)::tl -> + try + let subst, (newproof, newgoals) = + PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status + in + if newgoals = [] then + let _, _, p, _ = newproof in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof p, gp) + | Inference.NoProof -> Inference.BasicProof p + | Inference.BasicProof _ -> Inference.BasicProof p + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + let _, m = status in + let subst = List.filter (fun (i, _) -> i = m) subst in + `Ok (subst, [newp, metas, term]) + else + let _, menv, p, _ = newproof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let goals = + List.map + (fun i -> + let _, _, ty = CicUtil.lookup_meta i menv in + let p' = + let rec gp = function + | SubProof (t, i, p) -> + SubProof (t, i, gp p) + | ProofGoalBlock (sp1, sp2) -> + ProofGoalBlock (sp1, gp sp2) + | BasicProof _ + | NoProof -> + SubProof (p, i, BasicProof (Cic.Meta (i, irl))) + | ProofSymBlock (s, sp) -> + ProofSymBlock (s, gp sp) + | ProofBlock (s, u, nt, t, pe, sp) -> + ProofBlock (s, u, nt, t, pe, gp sp) + in gp proof + in + (p', menv, ty)) + newgoals + in + let goals = + let weight t = + let w, m = weight_of_term t in + w + 2 * (List.length m) + in + List.sort + (fun (_, _, t1) (_, _, t2) -> + Pervasives.compare (weight t1) (weight t2)) + goals + in + let best = aux tl in + match best with + | `Ok (_, _) -> best + | `No -> `GoOn ([subst, goals]) + | `GoOn sl -> `GoOn ((subst, goals)::sl) + with ProofEngineTypes.Fail msg -> + aux tl + in + let r, s, l = + if Inference.term_is_equality term then + let rec appleq_a = function + | [] -> false, [], [] + | (Positive, equality)::tl -> + let ok, s, newproof = apply_equality_to_goal env equality goal in + if ok then true, s, [newproof, metas, term] else appleq_a tl + | _::tl -> appleq_a tl + in + let rec appleq_p = function + | [] -> false, [], [] + | equality::tl -> + let ok, s, newproof = apply_equality_to_goal env equality goal in + if ok then true, s, [newproof, metas, term] else appleq_p tl + in + let al, _ = active in + match passive with + | None -> appleq_a al + | Some (_, (pl, _), _) -> + let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl + else + false, [], [] + in + if r = true then `Ok (s, l) else aux theorems +;; + + +(* sorts a conjunction of goals in order to detect earlier if it is + unsatisfiable. Non-predicate goals are placed at the end of the list *) +let sort_goal_conj (metasenv, context, ugraph) (depth, gl) = + let gl = + List.stable_sort + (fun (_, e1, g1) (_, e2, g2) -> + let ty1, _ = + CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph + and ty2, _ = + CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph + in + let prop1 = + let b, _ = + CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph + in + if b then 0 else 1 + and prop2 = + let b, _ = + CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph + in + if b then 0 else 1 + in + if prop1 = 0 && prop2 = 0 then + 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 + e1 - e2 + else + prop1 - prop2) + gl + in + (depth, gl) +;; + + +let is_meta_closed goals = + List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals +;; + + +(* applies a series of theorems/equalities to a conjunction of goals *) +let rec apply_to_goal_conj env theorems ?passive active (depth, goals) = + let aux (goal, r) tl = + let propagate_subst subst (proof, metas, term) = + let rec repl = function + | NoProof -> NoProof + | BasicProof t -> + BasicProof (CicMetaSubst.apply_subst subst t) + | ProofGoalBlock (p, pb) -> + let pb' = repl pb in + ProofGoalBlock (p, pb') + | SubProof (t, i, p) -> + let t' = CicMetaSubst.apply_subst subst t in + let p = repl p in + SubProof (t', i, p) + | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) + | ProofBlock (s, u, nty, t, pe, p) -> + ProofBlock (subst @ s, u, nty, t, pe, p) + in (repl proof, metas, term) + in + (* let r = apply_to_goal env theorems ?passive active goal in *) ( + match r with + | `No -> `No (depth, goals) + | `GoOn sl -> + let l = + List.map + (fun (s, gl) -> + let tl = List.map (propagate_subst s) tl in + sort_goal_conj env (depth+1, gl @ tl)) sl + in + `GoOn l + | `Ok (subst, gl) -> + if tl = [] then + `Ok (depth, gl) + else + let p, _, _ = List.hd gl in + let subproof = + let rec repl = function + | SubProof (_, _, p) -> repl p + | ProofGoalBlock (p1, p2) -> + ProofGoalBlock (repl p1, repl p2) + | p -> p + in + build_proof_term (repl p) + in + let i = + let rec get_meta = function + | SubProof (_, i, p) -> + let i' = get_meta p in + if i' = -1 then i else i' +(* max i (get_meta p) *) + | ProofGoalBlock (_, p) -> get_meta p + | _ -> -1 + in + get_meta p + in + let subst = + let _, (context, _, _) = List.hd subst in + [i, (context, subproof, Cic.Implicit None)] + in + let tl = List.map (propagate_subst subst) tl in + let conj = sort_goal_conj env (depth(* +1 *), tl) in + `GoOn ([conj]) + ) + in + if depth > !maxdepth || (List.length goals) > !maxwidth then + `No (depth, goals) + else + let rec search_best res = function + | [] -> res + | goal::tl -> + let r = apply_to_goal env theorems ?passive active goal in + match r with + | `Ok _ -> (goal, r) + | `No -> search_best res tl + | `GoOn l -> + let newres = + match res with + | _, `Ok _ -> assert false + | _, `No -> goal, r + | _, `GoOn l2 -> + if (List.length l) < (List.length l2) then goal, r else res + in + search_best newres tl + in + let hd = List.hd goals in + let res = hd, (apply_to_goal env theorems ?passive active hd) in + let best = + match res with + | _, `Ok _ -> res + | _, _ -> search_best res (List.tl goals) + in + let res = aux best (List.filter (fun g -> g != (fst best)) goals) in + match res with + | `GoOn ([conj]) when is_meta_closed (snd conj) && + (List.length (snd conj)) < (List.length goals)-> + apply_to_goal_conj env theorems ?passive active conj + | _ -> res +;; + + +(* +module OrderedGoals = struct + type t = int * (Inference.proof * Cic.metasenv * Cic.term) list + + let compare g1 g2 = + let d1, l1 = g1 + and d2, l2 = g2 in + 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 +end + +module GoalsSet = Set.Make(OrderedGoals);; + + +exception SearchSpaceOver;; +*) + + +(* +let apply_to_goals env is_passive_empty theorems active goals = + debug_print (lazy "\n\n\tapply_to_goals\n\n"); + let add_to set goals = + List.fold_left (fun s g -> GoalsSet.add g s) set goals + in + let rec aux set = function + | [] -> + debug_print (lazy "HERE!!!"); + if is_passive_empty then raise SearchSpaceOver else false, set + | goals::tl -> + let res = apply_to_goal_conj env theorems active goals in + match res with + | `Ok newgoals -> + let _ = + let d, p, t = + match newgoals with + | (d, (p, _, t)::_) -> d, p, t + | _ -> assert false + in + debug_print + (lazy + (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n" + d (string_of_proof p) (CicPp.ppterm t))) + in + true, GoalsSet.singleton newgoals + | `GoOn newgoals -> + let set' = add_to set (goals::tl) in + let set' = add_to set' newgoals in + false, set' + | `No newgoals -> + aux set tl + in + let n = List.length goals in + let res, goals = aux (add_to GoalsSet.empty goals) goals in + let goals = GoalsSet.elements goals in + debug_print (lazy "\n\tapply_to_goals end\n"); + let m = List.length goals in + if m = n && is_passive_empty then + raise SearchSpaceOver + else + res, goals +;; +*) + + +(* 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 + +and given_clause_aux dbd env goals theorems 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 ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print + (lazy (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 -> Failure + | true -> (* ParamodulationFailure *) + given_clause dbd env goals theorems passive active | false -> - let (sign, current), passive = select env passive active in - match forward_simplify env (sign, current) ~passive active with + let (sign, current), passive = select env (fst goals) 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 + given_clause dbd env goals theorems passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - let proof, _, _, _ = current in - Success (Some proof, env) + debug_print + (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current))); + let _, proof, _, _, _ = current in + ParamodulationSuccess (Some proof, env) ) else ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + debug_print + (lazy "\n================================================"); + debug_print (lazy (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, proof = contains_empty env new' in + let res, goal' = contains_empty env new' in if res then - Success (proof, env) + let proof = + match goal' with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof, env) else let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' (* ~passive *) active in + let new' = forward_simplify_new env new' active in let t2 = Unix.gettimeofday () in let _ = - forward_simpl_time := !forward_simpl_time +. (t2 -. t1) + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1) in let active = match sign with @@ -730,7 +1478,8 @@ let rec given_clause env passive active = backward_simplify env ([], [current]) active in let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); + backward_simpl_time := + !backward_simpl_time +. (t2 -. t1); match newa with | None -> active | Some (n, p) -> @@ -745,27 +1494,6 @@ let rec given_clause env passive active = 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 = @@ -777,59 +1505,117 @@ let rec given_clause env passive active = 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, proof -> - Success (proof, env) + given_clause dbd env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> + let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof, env) ) ;; -let rec given_clause_fullred env passive active = +(** given-clause algorithm with full reduction strategy *) +let rec given_clause_fullred dbd env goals theorems passive active = + let goals = simplify_goals env goals ~passive active in + let ok, goals = activate_goal goals in +(* let theorems = simplify_theorems env theorems ~passive active in *) + if ok then +(* let _ = *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *) +(* (print_goals (fst goals)) (print_goals (snd goals)))); *) +(* let current = List.hd (fst goals) in *) +(* let p, _, t = List.hd (snd current) in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "goal activated:\n%s\n%s\n" *) +(* (CicPp.ppterm t) (string_of_proof p))); *) +(* in *) + let ok, goals = + apply_goal_to_theorems dbd env theorems ~passive active goals + in + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_fullred_aux dbd env goals theorems passive active + else +(* let ok', theorems = activate_theorem 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_fullred_aux env goals theorems passive active *) +(* else *) + if (passive_is_empty passive) then ParamodulationFailure + else given_clause_fullred_aux dbd env goals theorems passive active + +and given_clause_fullred_aux dbd env goals theorems 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 ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print + (lazy (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 -> Failure + | true -> (* ParamodulationFailure *) + given_clause_fullred dbd env goals theorems passive active | false -> - let (sign, current), passive = select env passive active in - match forward_simplify env (sign, current) ~passive active with + let (sign, current), passive = select env (fst goals) 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 + given_clause_fullred dbd env goals theorems passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - let proof, _, _, _ = current in - Success (Some proof, env) + debug_print + (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current))); + let _, proof, _, _, _ = current in + ParamodulationSuccess (Some proof, env) ) else ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + debug_print + (lazy "\n================================================"); + debug_print (lazy (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 @@ -842,13 +1628,15 @@ let rec given_clause_fullred env passive active = let al, tbl = active in match sign with | Negative -> (sign, current)::al, tbl - | Positive -> al @ [(sign, current)], Indexing.index tbl current + | 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_time := !forward_simpl_time +. (t2 -. t1); + 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 @@ -871,142 +1659,527 @@ let rec given_clause_fullred env passive active = processed_clauses := !processed_clauses + (kept - 1 - k); 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 (); + debug_print + (lazy + (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 -> - 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 (); + debug_print + (lazy + (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 - given_clause_fullred env passive active - | true, proof -> - Success (proof, env) + given_clause_fullred dbd env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof, env) ) ;; -let get_from_user () = - let dbd = Mysql.quick_connect - ~host:"localhost" ~user:"helm" ~database:"mowgli" () in - let rec get () = - match read_line () with - | "" -> [] - | t -> t::(get ()) - in - let term_string = String.concat "\n" (get ()) in - let env, metasenv, term, ugraph = - List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0 - in - term, metasenv, ugraph -;; - -let given_clause_ref = ref given_clause;; - - -let main () = +let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in let module PP = CicPp in - let term, metasenv, ugraph = get_from_user () in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in - let proof, goals = - PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in - let goal = List.nth goals 0 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 - maxmeta := maxm; (* TODO ugly!! *) + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, equalities, maxm = find_equalities context proof in + let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) + in + let library_equalities = List.map snd library_equalities 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 + debug_print + (lazy + (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty))); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in let env = (metasenv, context, ugraph) in + let t1 = Unix.gettimeofday () in + let theorems = + if full then + let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = find_context_hypotheses env eq_indexes in + context_hyp @ theorems, [] + else + let refl_equal = + let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") + in + let t = CicUtil.term_of_uri refl_equal in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + [(t, ty, [])], [] + in + let t2 = Unix.gettimeofday () in + debug_print + (lazy + (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); + let _ = + debug_print + (lazy + (Printf.sprintf + "Theorems:\n-------------------------------------\n%s\n" + (String.concat "\n" + (List.map + (fun (t, ty, _) -> + Printf.sprintf + "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) + (fst theorems))))) + in try - let term_equality = equality_of_term meta_proof goal in - let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in + let goal = Inference.BasicProof new_meta_goal, [], goal in + let equalities = + let equalities = equalities @ library_equalities in + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "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 + (lazy + (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 passive = make_passive [] equalities in Printf.printf "\ncurrent goal: %s\n" - (string_of_equality ~env term_equality); + (let _, _, g = goal in CicPp.ppterm g); 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)); - 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 - match res with - | Failure -> - Printf.printf "NO proof found! :-(\n\n" - | Success (Some proof, env) -> - Printf.printf "OK, found a proof!:\n%s\n%.9f\n" - (PP.pp proof (names_of_context context)) - (finish -. start); - Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ - "backward_simpl_time: %.9f\n") - !infer_time !forward_simpl_time !backward_simpl_time; -(* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *) -(* " demodulate: %.9f\n subsumption: %.9f\n") *) -(* fs_time_info.build_all fs_time_info.demodulate *) -(* fs_time_info.subsumption; *) - | Success (None, env) -> - Printf.printf "Success, but no proof?!?\n\n" + (string_of_equality ~env) equalities)); +(* (equalities @ library_equalities))); *) + print_endline "--------------------------------------------------"; + let start = Unix.gettimeofday () in + print_endline "GO!"; + start_time := Unix.gettimeofday (); + let res = + let goals = make_goals goal in + (if !use_fullred then given_clause_fullred else given_clause) + dbd env goals theorems passive active + in + let finish = Unix.gettimeofday () in + let _ = + match res with + | ParamodulationFailure -> + Printf.printf "NO proof found! :-(\n\n" + | ParamodulationSuccess (Some proof, env) -> + let proof = Inference.build_proof_term proof 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); + 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 + 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 configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; +let default_depth = !maxdepth +and default_width = !maxwidth;; + +let reset_refs () = + maxmeta := 0; + symbols_counter := 0; + weight_age_counter := !weight_age_ratio; + processed_clauses := 0; + start_time := 0.; + elapsed_time := 0.; + maximal_retained_equality := None; + infer_time := 0.; + forward_simpl_time := 0.; + forward_simpl_new_time := 0.; + backward_simpl_time := 0.; + passive_maintainance_time := 0.; + derived_clauses := 0; + kept_clauses := 0; +;; -let _ = - let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) - and set_sel v = symbols_ratio := v; symbols_counter := v; - and set_conf f = configuration_file := f - and set_lpo () = Utils.compare_terms := lpo - and set_kbo () = Utils.compare_terms := nonrec_kbo - and set_fullred () = use_fullred := true - and set_time_limit v = time_limit := float_of_int v +let saturate + dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = + let module C = Cic in + reset_refs (); + Indexing.init_index (); + maxdepth := depth; + maxwidth := width; + let proof, goal = status in + let goal' = goal in + let uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, 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 + (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty))); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty in - Arg.parse [ - "-f", Arg.Unit set_fullred, "Use full-reduction strategy"; - - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)"; + let ugraph = CicUniv.empty_ugraph in + let env = (metasenv, context, ugraph) in + let goal = Inference.BasicProof new_meta_goal, [], goal in + let res, time = + let t1 = Unix.gettimeofday () in + let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) + in + let library_equalities = List.map snd library_equalities in + let t2 = Unix.gettimeofday () in + maxmeta := maxm+2; + let equalities = + let equalities = equalities @ library_equalities in + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "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 + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); + res + in + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); + let t1 = Unix.gettimeofday () in + let theorems = + if full then + let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = find_context_hypotheses env eq_indexes in + context_hyp @ thms, [] + else + let refl_equal = + let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") + in + let t = CicUtil.term_of_uri refl_equal in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + [(t, ty, [])], [] + in + let t2 = Unix.gettimeofday () in + let _ = + debug_print + (lazy + (Printf.sprintf + "Theorems:\n-------------------------------------\n%s\n" + (String.concat "\n" + (List.map + (fun (t, ty, _) -> + Printf.sprintf + "Term: %s, type: %s" + (CicPp.ppterm t) (CicPp.ppterm ty)) + (fst theorems))))); + debug_print + (lazy + (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); + in + let active = make_active () in + let passive = make_passive [] equalities in + let start = Unix.gettimeofday () in + let res = + let goals = make_goals goal in + given_clause_fullred dbd env goals theorems passive active + in + let finish = Unix.gettimeofday () in + (res, finish -. start) + in + match res with + | ParamodulationSuccess (Some proof, env) -> + debug_print (lazy "OK, found a proof!"); + let proof = Inference.build_proof_term proof in + let names = names_of_context context in + let newmetasenv = + let i1 = + match new_meta_goal with + | C.Meta (i, _) -> i | _ -> 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 (lazy (CicPp.pp proof [](* names *))); + debug_print + (lazy + (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 + (lazy + (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 (lazy "THE PROOF DOESN'T TYPECHECK!!!"); + debug_print (lazy (CicPp.pp proof names)); + raise (ProofEngineTypes.Fail + (lazy "Found a proof, but it doesn't typecheck")) + in + debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); + newstatus + | _ -> + raise (ProofEngineTypes.Fail (lazy "NO proof found")) +;; - "-s", Arg.Int set_sel, - "symbols-based selection ratio (relative to the weight ratio)"; +(* dummy function called within matita to trigger linkage *) +let init () = ();; - "-c", Arg.String set_conf, "Configuration file (for the db connection)"; - "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; +(* UGLY SIDE EFFECT... *) +if connect_to_auto then ( + AutoTactic.paramodulation_tactic := saturate; + AutoTactic.term_is_equality := Inference.term_is_equality; +);; - "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; - "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; - ] (fun a -> ()) "Usage:" -in -Helm_registry.load_from !configuration_file; -main () +let retrieve_and_print 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 uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, 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 + (lazy (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 + let goal = Inference.BasicProof new_meta_goal, [], goal in + let t1 = Unix.gettimeofday () in + let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) + in + let t2 = Unix.gettimeofday () in + maxmeta := maxm+2; + let equalities = + let equalities = (* equalities @ *) library_equalities in + debug_print + (lazy + (Printf.sprintf "\n\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let (u, e) = e in + let active = List.map (fun (u, e) -> (Positive, e)) + (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 (Positive, e) (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl ((u, (snd e))::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> (u, (snd e))::others_simpl + ) + in + match equalities with + | [] -> [] + | hd::tl -> + let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let res = + List.rev (simpl (*(Positive,*) hd others []) + in + debug_print + (lazy + (Printf.sprintf "\nequalities AFTER:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> + Printf.sprintf "%s: %s" + (UriManager.string_of_uri u) + (string_of_equality e) + ) + res)))); + res + in + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) +;;