X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=eb4a35d6c443f823e2b94438b4c4f13f6cc17549;hb=b1bad322d0daf6c25f95a82c4349f057a753ab7c;hp=4b4650b112eec651776bc1bc748f551974c1abf0;hpb=67165a0c7b9141667a4c604d30c14ed33d73c726;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 4b4650b11..eb4a35d6c 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Inference;; open Utils;; @@ -55,6 +57,7 @@ let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) Utils.compare_terms := Utils.nonrec_kbo;; +(* Utils.compare_terms := Utils.ao;; *) (* statistics... *) let derived_clauses = ref 0;; @@ -141,7 +144,7 @@ let select env goals passive (active, _) = (* Negatives aren't indexed, no need to remove them... *) (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) - | [], hd::tl -> + | [], (hd:EqualitySet.elt)::tl -> let passive_table = Indexing.remove_index passive_table hd in @@ -220,8 +223,7 @@ let make_passive neg pos = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) - (Indexing.empty_table ()) pos + List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos in (neg, set_of neg), (pos, set_of pos), @@ -230,7 +232,7 @@ let make_passive neg pos = let make_active () = - [], Indexing.empty_table () + [], Indexing.empty ;; @@ -363,7 +365,7 @@ let prune_passive howmany (active, _) passive = maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold - (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) + (fun e tbl -> Indexing.index tbl e) ps Indexing.empty in (nl, ns), (pl, ps), tbl ;; @@ -397,7 +399,7 @@ let infer env sign current (active_list, active_table) = let neg, pos = infer_positive table tl in neg, res @ pos in - let curr_table = Indexing.index (Indexing.empty_table ()) current in + let curr_table = Indexing.index Indexing.empty current in let neg, pos = infer_positive curr_table active_list in neg, res @ pos in @@ -654,7 +656,7 @@ let backward_simplify_active env new_pos new_table min_weight active = ) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) - active_list ([], Indexing.empty_table ()), + active_list ([], Indexing.empty), List.fold_right (fun (s, eq) (n, p) -> if (s <> Negative) && (is_identity env eq) then ( @@ -691,7 +693,7 @@ let backward_simplify_passive env new_pos new_table min_weight passive = and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in let passive_table = List.fold_left - (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl + (fun tbl e -> Indexing.index tbl e) Indexing.empty pl in match newn, newp with | [], [] -> ((nl, ns), (pl, ps), passive_table), None @@ -705,7 +707,7 @@ let backward_simplify env new' ?passive active = (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') + ([], Indexing.empty, 1000000) (snd new') in let active, newa = backward_simplify_active env new_pos new_table min_weight active in @@ -1842,7 +1844,7 @@ let main dbd full term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2019,7 +2021,7 @@ let saturate let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2214,7 +2216,7 @@ let retrieve_and_print dbd term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env (Positive, e) (active, tbl) in match others with @@ -2300,7 +2302,7 @@ let main_demod_equalities dbd term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2346,12 +2348,31 @@ let main_demod_equalities dbd term metasenv ugraph = saturate_equations env goal (fun e -> true) passive active in let finish = Unix.gettimeofday () in + + let initial = + List.fold_left (fun s e -> EqualitySet.add e s) + EqualitySet.empty equalities + in + let addfun s e = + if not (EqualitySet.mem e initial) then EqualitySet.add e s else s + in + + let passive = + match rp with + | (n, _), (p, _), _ -> + EqualitySet.elements (List.fold_left addfun EqualitySet.empty p) + in + let active = + let l = List.map snd (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" +(* (String.concat "\n" (List.map (string_of_equality ~env) active)) *) (String.concat "\n" - (List.map (fun (s, e) -> (string_of_equality ~env e)) (fst ra))) + (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) +(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) (String.concat "\n" - (List.map (string_of_equality ~env) - (match rp with (n, _), (p, _), _ -> p))); + (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive)); print_newline (); with e -> debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))