From 430fb6e217b6ca61bfc38bb970c1bc57d5643b4c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 10 Apr 2006 09:02:37 +0000 Subject: [PATCH] Removed negative equations. --- .../tactics/paramodulation/saturation.ml | 1443 +++-------------- components/tactics/paramodulation/utils.ml | 2 +- components/tactics/tactics.mli | 2 +- 3 files changed, 215 insertions(+), 1232 deletions(-) diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index e88a061a3..5b5121e86 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -28,11 +28,6 @@ open Inference;; open Utils;; -let check_table t l = - List.fold_left - (fun b (_,eq) -> b && (Indexing.in_index t eq)) true l - - (* set to false to disable paramodulation inside auto_tac *) let connect_to_auto = true;; @@ -54,7 +49,7 @@ let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; -let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *) +let weight_age_ratio = ref 6 (* 5 *);; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio ;; let symbols_ratio = ref 0 (* 3 *);; let symbols_counter = ref 0;; @@ -75,16 +70,6 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; -let test eq = false -(* - let (_,(_,_,(ty,left,right,_),m1)) = eq in - let actual = - (Inference.metas_of_term left)@(Inference.metas_of_term right) - in - let m = List.filter (fun (i, _, _) -> List.mem i actual) m1 in - m <> m1 -;; *) - type result = | ParamodulationFailure | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option @@ -126,119 +111,50 @@ module OrderedEquality = struct | res -> res end -(* -module OrderedEquality = struct - type t = Inference.equality - - let minor eq = - let w, _, (ty, left, right, o), _ = eq in - match o with - | Lt -> Some left - | Le -> assert false - | Gt -> Some right - | Ge -> assert false - | Eq - | Incomparable -> None - - let compare eq1 eq2 = - let w1, _, (ty, left, right, o1), m1 = eq1 - and w2, _, (ty', left', right', o2), m2 = eq2 in - match Pervasives.compare w1 w2 with - | 0 -> - (match minor eq1, minor eq2 with - | Some t1, Some t2 -> - fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2) - | Some _, None -> -1 - | None, Some _ -> 1 - | _,_ -> - (List.length m2) - (List.length m1) ) - | res -> res - - let compare eq1 eq2 = - match compare eq1 eq2 with - 0 -> Pervasives.compare eq1 eq2 - | res -> res -end -*) - module EqualitySet = Set.Make(OrderedEquality);; exception Empty_list;; let passive_is_empty = function - | ([], _), ([], _), _ -> true + | ([], _), _ -> true | _ -> false ;; -let size_of_passive ((_, ns), (_, ps), _) = - (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps) +let size_of_passive ((passive_list, ps), _) = List.length passive_list +(* EqualitySet.cardinal ps *) ;; -let size_of_active (active_list, _) = - List.length active_list +let size_of_active (active_list, _) = List.length active_list ;; let age_factor = 0.01;; -let min_elt weight l = - fst - (match l with - [] -> raise Empty_list - | a::tl -> - let wa = float_of_int (weight a) in - let x = ref 0. in - List.fold_left - (fun (current,w) arg -> - x:=!x +. 1.; - let w1 = weight arg in - let wa = (float_of_int w1) +. !x *. age_factor in - if wa < w then (arg,wa) else (current,w)) - (a,wa) tl) -;; - -(* -let compare eq1 eq2 = - let w1, _, (ty, left, right, _), m1, _ = eq1 in - let w2, _, (ty', left', right', _), m2, _ = eq2 in - match Pervasives.compare w1 w2 with - | 0 -> (List.length m1) - (List.length m2) - | res -> res -;; -*) - (** selects one equality from passive. The selection strategy is a combination of weight, age and goal-similarity *) -let rec select env goals passive (active, _) = + +let rec select env goals passive = 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 - in + let (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:EqualitySet.elt)::tl -> + match pos_list with + | (hd:EqualitySet.elt)::tl -> let passive_table = Indexing.remove_index passive_table hd - in (Positive, hd), - (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) - | _, _ -> assert false - ) - | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> + in hd, ((tl, EqualitySet.remove hd pos_set), passive_table) + | _ -> assert false) + | _ when (!symbols_counter > 0) -> (symbols_counter := !symbols_counter - 1; let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 @@ -276,43 +192,29 @@ let rec select env goals passive (active, _) = 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) - ) + current, + ((remove current pos_list, EqualitySet.remove current pos_set), + passive_table)) | _ -> symbols_counter := !symbols_ratio; - let set_selection set = EqualitySet.min_elt set in - (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l 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 - 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 current = EqualitySet.min_elt pos_set in + let passive_table = + Indexing.remove_index passive_table current + in + current, + ((remove current pos_list, EqualitySet.remove current pos_set), + passive_table) ;; (* initializes the passive set of equalities *) -let make_passive neg pos = +let make_passive 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 pos in - (neg, set_of neg), (pos, set_of pos), table ;; @@ -323,29 +225,26 @@ 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 +(* adds to passive a list of equalities new_pos *) +let add_to_passive passive new_pos = + let (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 pos = List.filter (ok pos_set) new_pos in let 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 in - (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos), table ;; - +(* TODO *) (* 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 (pl, ps), tbl = passive in let howmany = float_of_int howmany and ratio = float_of_int !weight_age_ratio in let round v = @@ -356,67 +255,26 @@ let prune_passive howmany (active, _) passive = 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)::_ -> - 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 + let symbols, card = None, 0 in let counter = ref !symbols_ratio in - let rec pickw w ns ps = + let rec pickw w 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 + 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' + if !counter = 0 then counter := !symbols_ratio in + let e = EqualitySet.min_elt ps in + let ps' = pickw (w-1) (EqualitySet.remove e ps) in + 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' + let ps' = pickw (w-1) (EqualitySet.remove e ps) in + EqualitySet.add e ps' else - EqualitySet.empty, EqualitySet.empty + EqualitySet.empty in - let ns, ps = pickw in_weight ns ps in + let ps = pickw in_weight ps in let rec picka w s l = if w > 0 then match l with @@ -430,7 +288,6 @@ let prune_passive howmany (active, _) passive = 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_retained_equality := Some (EqualitySet.max_elt ps); @@ -438,167 +295,77 @@ let prune_passive howmany (active, _) passive = EqualitySet.fold (fun e tbl -> Indexing.index tbl e) ps Indexing.empty in - (nl, ns), (pl, ps), tbl + (pl, ps), tbl ;; (** inference of new equalities between current and some in active *) -let infer env sign current (active_list, active_table) = +let infer env current ((active_list:Inference.equality list), active_table) = let (_,c,_) = env in if Utils.debug_metas then (ignore(Indexing.check_target c current "infer1"); - ignore(List.map (function (_,current) -> Indexing.check_target c current "infer2") active_list)); - let new_neg, new_pos = - match sign with - | Negative -> - let maxm, res = - Indexing.superposition_left !maxmeta env active_table current in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup-1") res); - maxmeta := maxm; - res, [] - | Positive -> - let maxm, res = - Indexing.superposition_right !maxmeta env active_table current in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup0") res); - maxmeta := maxm; - let rec infer_positive table = function - | [] -> [], [] - | (Negative, equality)::tl -> - let maxm, res = - Indexing.superposition_left !maxmeta env table equality in - maxmeta := maxm; - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "supl") res); - 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 + ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); + let new_pos = + let maxm, res = + Indexing.superposition_right !maxmeta env active_table current in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup0") res); + maxmeta := maxm; + let rec infer_positive table = function + | [] -> [] + | equality::tl -> + let maxm, res = + Indexing.superposition_right !maxmeta env table equality in maxmeta := maxm; - if Utils.debug_metas then - ignore - (List.map - (function current -> - Indexing.check_target c current "sup2") res); - let neg, pos = infer_positive table tl in - neg, res @ pos - in - let maxm, copy_of_current = Inference.fix_metas !maxmeta current in - maxmeta := maxm; - let curr_table = Indexing.index Indexing.empty current in - let neg, pos = - infer_positive curr_table ((sign,copy_of_current)::active_list) - in - if Utils.debug_metas then - ignore(List.map + if Utils.debug_metas then + ignore + (List.map (function current -> - Indexing.check_target c current "sup3") pos); - neg, res @ pos - in - derived_clauses := !derived_clauses + (List.length new_neg) + - (List.length new_pos); - match !maximal_retained_equality with - | None -> + Indexing.check_target c current "sup2") res); + let pos = infer_positive table tl in + res @ pos + in + let maxm, copy_of_current = Inference.fix_metas !maxmeta current in + maxmeta := maxm; + let curr_table = Indexing.index Indexing.empty current in + let pos = infer_positive curr_table (copy_of_current::active_list) + in if Utils.debug_metas then - (ignore(List.map - (function current -> - Indexing.check_target c current "sup4") new_pos); ignore(List.map (function current -> - Indexing.check_target c current "sup5") new_neg)); - new_neg, new_pos - | Some eq -> + Indexing.check_target c current "sup3") pos); + res @ pos + in + derived_clauses := !derived_clauses + (List.length new_pos); + match !maximal_retained_equality with + | None -> new_pos + | Some eq -> ignore(assert false); (* 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) -> - fst (CicReduction.are_convertible context left right ugraph)) - negative - in - true, Some found - with Not_found -> - false, None + List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos ;; +(* buttare via sign *) (** simplifies current using active and passive *) -let forward_simplify env (sign, current) ?passive (active_list, active_table) = +let forward_simplify env (sign,current) ?passive (active_list, active_table) = let _, context, _ = env in - let pl, passive_table = + let 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 + | None -> None + | Some ((_, _), pt) -> Some pt in - let all = if pl = [] then active_list else active_list @ pl in - let demodulate table current = let newmeta, newcurrent = 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 ( (* debug_print *) (* (lazy *) (* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) @@ -610,41 +377,33 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = (* (String.concat "\n" *) (* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) None - ) else - Some (sign, newcurrent) + Some newcurrent in let rec demod current = if Utils.debug_metas then ignore (Indexing.check_target context current "demod0"); let res = demodulate active_table current in if Utils.debug_metas then - ignore ((function None -> () | Some (_,x) -> + ignore ((function None -> () | Some x -> ignore (Indexing.check_target context x "demod1");()) res); match res with | None -> None - | Some (sign, newcurrent) -> + | Some newcurrent -> match passive_table with | None -> res | Some passive_table -> match demodulate passive_table newcurrent with | None -> None - | Some (sign,newnewcurrent) -> + | Some newnewcurrent -> if newcurrent <> newnewcurrent then demod newnewcurrent - else Some (sign,newnewcurrent) + else Some newnewcurrent in let res = demod current 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) -> + | Some c -> if Indexing.in_index active_table c then None else @@ -676,13 +435,10 @@ 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 forward_simplify_new env new_pos ?passive active = if Utils.debug_metas then begin let m,c,u = env in - ignore(List.map - (fun current -> - Indexing.check_target c current "forward new neg") new_neg); ignore(List.map (fun current -> Indexing.check_target c current "forward new pos") new_pos;) @@ -690,15 +446,11 @@ 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 = + let 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 + | None -> None + | Some ((_, _), pt) -> Some pt in - let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); @@ -709,19 +461,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = newtarget 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 - new_neg,new_pos -(* PROVA - 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 *) + (* we could also demodulate using passive. Currently we don't *) + let new_pos = + List.map (demodulate Positive active_table) new_pos in - let t2 = Unix.gettimeofday () in fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1); @@ -756,19 +499,16 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = not ((Indexing.in_index active_table e) || (Indexing.in_index passive_table e))) in - new_neg, List.filter subs (List.filter is_duplicate new_pos) + List.filter subs (List.filter is_duplicate new_pos) ;; (** simplifies a goal with equalities in active and passive *) let rec simplify_goal env goal ?passive (active_list, active_table) = - let pl, passive_table = + let 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 + | None -> None + | Some ((_, _), pt) -> Some pt in let demodulate table goal = @@ -824,52 +564,49 @@ 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) -> + (fun equality (res, newn) -> let ew, _, _, _ = equality in if ew < min_weight then - (s, equality)::res, newn + equality::res, newn else - match forward_simplify env (s, equality) (new_pos, new_table) with + match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with | None -> res, newn - | Some (s, e) -> + | Some e -> if equality = e then - (s, e)::res, newn + e::res, newn else - res, (s, e)::newn) + res, e::newn) active_list ([], []) in let find eq1 where = - List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where + List.exists (meta_convertibility_eq eq1) where in let active, newa = List.fold_right - (fun (s, eq) (res, tbl) -> - if List.mem (s, eq) res then + (fun eq (res, tbl) -> + if List.mem 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) + eq::res, Indexing.index tbl eq) active_list ([], Indexing.empty), 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 ([], []) + (fun eq p -> + if (is_identity env eq) then p + else eq::p) + newa [] in match newa with - | [], [] -> active, None + | [] -> active, None | _ -> active, Some newa ;; (** 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 (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = let ew, _, _, _ = equality in if ew < min_weight then @@ -877,22 +614,21 @@ let backward_simplify_passive env new_pos new_table min_weight passive = else match forward_simplify env (sign, equality) (new_pos, new_table) with | None -> resl, EqualitySet.remove equality ress, newn - | Some (s, e) -> + | Some e -> if equality = e then equality::resl, ress, newn else let ress = EqualitySet.remove equality ress in - resl, ress, e::newn + 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 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 pl in - match newn, newp with - | [], [] -> ((nl, ns), (pl, ps), passive_table), None - | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp) + match newp with + | [] -> ((pl, ps), passive_table), None + | _ -> ((pl, ps), passive_table), Some (newp) ;; @@ -901,14 +637,14 @@ let backward_simplify env new' ?passive active = List.fold_left (fun (l, t, w) e -> let ew, _, _, _ = e in - (Positive, e)::l, Indexing.index t e, min ew w) - ([], Indexing.empty, 1000000) (snd new') + e::l, Indexing.index t e, min ew w) + ([], Indexing.empty, 1000000) 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 + active, (make_passive []), newa, None | Some passive -> active, passive, newa, None (* prova @@ -923,18 +659,18 @@ let close env new' given = List.fold_left (fun (l, t, w) e -> let ew, _, _, _ = e in - (Positive, e)::l, Indexing.index t e, min ew w) + e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) (snd new') in List.fold_left - (fun (n,p) (s,c) -> - let neg,pos = infer env s c (new_pos,new_table) in - neg@n,pos@p) - ([],[]) given + (fun p c -> + let pos = infer env c (new_pos,new_table) in + pos@p) + [] given ;; let is_commutative_law eq = - let w, proof, (eq_ty, left, right, order), metas = snd eq in + let w, proof, (eq_ty, left, right, order), metas = eq in match left,right with Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> @@ -949,10 +685,9 @@ let prova env new' active = (lazy (Printf.sprintf "symmetric:\n%s\n" (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - (given)))))) in + (List.map + (fun e -> string_of_equality ~env e) + given)))) in close env new' given ;; @@ -1037,10 +772,10 @@ let rec simpl env e others others_simpl = let active = others @ others_simpl in let tbl = List.fold_left - (fun t (_, e) -> Indexing.index t e) + (fun t e -> Indexing.index t e) Indexing.empty active in - let res = forward_simplify env e (active, tbl) in + let res = forward_simplify env (Positive,e) (active, tbl) in match others with | hd::tl -> ( match res with @@ -1064,9 +799,8 @@ let simplify_equalities env equalities = match equalities with | [] -> [] | hd::tl -> - let others = List.map (fun e -> (Positive, e)) tl in let res = - List.rev (List.map snd (simpl env (Positive, hd) others [])) + List.rev (simpl env hd tl []) in debug_print (lazy @@ -1076,433 +810,6 @@ let simplify_equalities env equalities = res ;; -(* -(* 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 = 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', _ = - Inference.unification metas gmetas context eqterm gterm ugraph - in - let newproof = - match proof with - | I.BasicProof (subst',t) -> I.BasicProof (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 _ -> newproof - | I.SubProof (t, i, p) -> - prerr_endline "SUBPROOF!"; - I.SubProof (t, i, repl p) - | _ -> assert false - in - repl gproof - in - true, (subst:Inference.substitution), 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) -> - prerr_endline "apply_to_goal!"; - 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:Cic.substitution),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 (subst',t) -> - BasicProof (subst@subst',t) - | ProofGoalBlock (p, pb) -> - let pb' = repl pb in - ProofGoalBlock (p, pb') - | SubProof (t, i, p) -> - let t' = Inference.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 @@ -1515,241 +822,6 @@ let print_goals goals = 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 _,context,_ = env in - 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 (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time)); - make_passive [] [] - ) else if kept > selection_estimate then ( - 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 -> (* ParamodulationFailure *) - given_clause dbd env goals theorems passive active - | false -> - let (sign, current), passive = select env (fst goals) passive active in - let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in - prerr_endline ("Selected = " ^ - (CicPp.pp (Inference.term_of_equality current) names)); - 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 dbd env goals theorems passive active - | Some (sign, current) -> - if (sign = Negative) && (is_identity env current) then ( - 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 ( - 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, goal' = contains_empty env new' in - if res then - 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' 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 - 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 - 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 check_if_goal_is_subsumed env (proof,menv,ty) table = match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] @@ -1778,11 +850,7 @@ let check_if_goal_is_subsumed env (proof,menv,ty) table = let counter = ref 0 (** given-clause algorithm with full reduction strategy *) -let rec given_clause_fullred dbd env goals theorems passive active = -(* - let table,list = active in - assert (check_table list table); -*) +let rec given_clause_fullred dbd env goals theorems ~passive active = let goals = simplify_goals env goals ~passive active in let _,context,_ = env in let ok, goals = activate_goal goals in @@ -1835,26 +903,6 @@ let rec given_clause_fullred dbd env goals theorems passive active = in if ok then ( prerr_endline "esco qui"; - let active = - List.filter test (fst active) in - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - active))) - in prerr_endline s; - let passive = - List.filter - (fun x -> test (1,x)) - (let x,y,_ = passive in (fst x)@(fst y)) in - let p = Printf.sprintf "passives:\n%s\n" - (String.concat "\n" - ((List.map - (fun e -> - (string_of_equality ~env e)) - passive))) - in prerr_endline p; (* let s = Printf.sprintf "actives:\n%s\n" (String.concat "\n" @@ -1896,7 +944,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active = " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); incr counter; -(* if !counter mod 10 = 0 then +(* + if !counter mod 10 = 0 then begin let size = HExtlib.estimate_size (passive,active) in let sizep = HExtlib.estimate_size (passive) in @@ -1938,7 +987,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = else if !elapsed_time > !time_limit then ( debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" !time_limit !elapsed_time)); - make_passive [] [] + make_passive [] ) else if kept > selection_estimate then ( debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ @@ -1954,13 +1003,12 @@ and given_clause_fullred_aux dbd env goals theorems passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); match passive_is_empty passive with - | true -> (* ParamodulationFailure *) - given_clause_fullred dbd env goals theorems passive active + | true -> ParamodulationFailure + (* given_clause_fullred dbd env goals theorems passive active *) | false -> - let (sign, current), passive = select env (fst goals) passive active in + let current, passive = select env (fst goals) passive in prerr_endline - ("Selected = " ^ (string_of_sign sign) ^ " " ^ - string_of_equality ~env current); + ("Selected = " ^ string_of_equality ~env current); (* ^ (let w,p,(t,l,r,o),m = current in " size w: " ^ string_of_int (HExtlib.estimate_size w)^ @@ -1973,66 +1021,34 @@ and given_clause_fullred_aux dbd env goals theorems passive active = " size m-c: " ^ string_of_int (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *) let time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in + let res = forward_simplify env (Positive, current) ~passive active in let time2 = Unix.gettimeofday () in forward_simpl_time := !forward_simpl_time +. (time2 -. time1); match res with | None -> (* weight_age_counter := !weight_age_counter + 1; *) given_clause_fullred dbd env goals theorems passive active - | Some (sign, current) -> - if test (sign, current) then - (prerr_endline - ("Simplified = " ^ (string_of_sign sign) ^ " " ^ - string_of_equality ~env current); - let active = fst active in - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - active))) - in prerr_endline s; - assert false); - if (sign = Negative) && (is_identity env current) then ( - debug_print - (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current))); - let _, proof, _, m = current in - ParamodulationSuccess (Some (proof, m)) - ) else ( + | Some current -> + debug_print (lazy (Printf.sprintf "selected: %s" + (string_of_equality ~env current))); + let t1 = Unix.gettimeofday () in + let new' = infer env current active in + let _ = 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 _ = - match new' with - | neg, pos -> - debug_print - (lazy - (Printf.sprintf "new' (senza semplificare):\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 - let t2 = Unix.gettimeofday () in + (lazy + (Printf.sprintf "new' (senza semplificare):\n%s\n" + (String.concat "\n" + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) new')))) + 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 + al @ [current], Indexing.index tbl current in let rec simplify new' active passive = let t1 = Unix.gettimeofday () in @@ -2043,27 +1059,22 @@ and given_clause_fullred_aux dbd env goals theorems passive active = 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 + | Some p, None + | None, Some p -> + let np = new' in if Utils.debug_metas then begin List.iter (fun x->Indexing.check_target context x "simplify1") - n; - List.iter - (fun x->Indexing.check_target context x "simplify2") - p + p; end; - 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 + simplify (new' @ p) active passive + | Some p, Some rp -> + simplify (new' @ p @ rp) active passive in let active, _, new' = simplify new' active passive in (* pessima prova @@ -2094,69 +1105,50 @@ end prova *) (Printf.sprintf "active:\n%s\n" (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) + (fun e -> (string_of_equality ~env e)) (fst active)))))) in let _ = - match new' with - | neg, pos -> - 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))))) + debug_print + (lazy + (Printf.sprintf "new':\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) new'))))) in - match contains_empty env new' with - | false, _ -> - let passive = add_to_passive passive new' in - given_clause_fullred dbd env goals theorems passive active - | true, goal -> - let proof = - match goal with - | Some goal -> let _, proof, _, env = goal in Some (proof,env) - | None -> None - in - ParamodulationSuccess proof - ) - + let passive = add_to_passive passive new' in + given_clause_fullred dbd env goals theorems passive active ;; +(* let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred" let given_clause_fullred dbd env goals theorems passive active = profiler0.HExtlib.profile (given_clause_fullred dbd env goals theorems passive) active - +*) + let rec saturate_equations env goal accept_fun passive active = elapsed_time := Unix.gettimeofday () -. !start_time; if !elapsed_time > !time_limit then (active, passive) else - let (sign, current), passive = select env [1, [goal]] passive active in - let res = forward_simplify env (sign, current) ~passive active in + let current, passive = select env [1, [goal]] passive in + let res = forward_simplify env (Positive, current) ~passive active in match res with | None -> saturate_equations env goal accept_fun passive active - | Some (sign, current) -> - assert (sign = Positive); - debug_print - (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) + | Some current -> + debug_print (lazy (Printf.sprintf "selected: %s" (string_of_equality ~env current))); - let new' = infer env sign current active in + let new' = infer env current active in let active = if is_identity env current then active else let al, tbl = active in - al @ [(sign, current)], Indexing.index tbl current + al @ [current], Indexing.index tbl current in let rec simplify new' active passive = let new' = forward_simplify_new env new' ~passive active in @@ -2164,13 +1156,9 @@ let rec saturate_equations env goal accept_fun passive active = backward_simplify env new' ~passive active in 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 + | Some p, None + | None, Some p -> simplify (new' @ p) active passive + | Some p, Some rp -> simplify (new' @ p @ rp) active passive in let active, passive, new' = simplify new' active passive in let _ = @@ -2178,33 +1166,25 @@ let rec saturate_equations env goal accept_fun passive active = (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)))))) + (List.map + (fun e -> string_of_equality ~env e) + (fst active))))) in - let _ = - match new' with - | neg, pos -> - 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))))) + let _ = + debug_print + (lazy + (Printf.sprintf "new':\n%s\n" + (String.concat "\n" + (List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) new')))) in - let new' = match new' with _, pos -> [], List.filter accept_fun pos in + let new' = List.filter accept_fun new' in let passive = add_to_passive passive new' in saturate_equations env goal accept_fun passive active ;; - - let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in @@ -2270,7 +1250,7 @@ let main dbd full term metasenv ugraph = let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in - let passive = make_passive [] equalities in + let passive = make_passive equalities in Printf.printf "\ncurrent goal: %s\n" (let _, _, g = goal in CicPp.ppterm g); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -2455,7 +1435,7 @@ let saturate (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); in let active = make_active () in - let passive = make_passive [] equalities in + let passive = make_passive equalities in let start = Unix.gettimeofday () in let res = let goals = make_goals goal in @@ -2466,6 +1446,7 @@ let saturate in match res with | ParamodulationSuccess (Some (proof, proof_menv)) -> + prerr_endline "OK, found a proof!"; debug_print (lazy "OK, found a proof!"); let proof = Inference.build_proof_term proof in let equality_for_replace i t1 = @@ -2473,6 +1454,7 @@ let saturate | C.Meta (n, _) -> n = i | _ -> false in + prerr_endline "replacing metas"; let proof_menv, what, with_what = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context @@ -2502,9 +1484,10 @@ let saturate let newstatus = try let ty, ug = + prerr_endline "type checking ... "; CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in - debug_print (lazy (CicPp.pp proof [](* names *))); + prerr_endline (CicPp.pp proof [](* names *)); debug_print (lazy (Printf.sprintf @@ -2622,12 +1605,12 @@ let retrieve_and_print dbd term metasenv ugraph = | hd::tl -> ( match res with | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl ((u, (snd e))::others_simpl) + | Some e -> simpl hd tl ((u, e)::others_simpl) ) | [] -> ( match res with | None -> others_simpl - | Some e -> (u, (snd e))::others_simpl + | Some e -> (u, e)::others_simpl ) in let _equalities = @@ -2689,7 +1672,7 @@ let main_demod_equalities dbd term metasenv ugraph = let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in - let passive = make_passive [] equalities in + let passive = make_passive equalities in Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); Printf.printf "\nequalities:\n%s\n" @@ -2714,11 +1697,11 @@ let main_demod_equalities dbd term metasenv ugraph = let passive = match rp with - | (n, _), (p, _), _ -> + | (p, _), _ -> EqualitySet.elements (List.fold_left addfun EqualitySet.empty p) in let active = - let l = List.map snd (fst ra) in + let l = fst ra in EqualitySet.elements (List.fold_left addfun EqualitySet.empty l) in Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 16556588f..db19e87d1 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -291,7 +291,7 @@ end module IntSet = Set.Make(OrderedInt) let compute_equality_weight (ty,left,right,o) = - let factor = 2 in + let factor = 1 in match o with | Lt -> let w, m = (weight_of_term diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 60a485bce..7d55e7589 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 27 15:17:54 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 5 15:04:24 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic -- 2.39.2