X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=eb4a35d6c443f823e2b94438b4c4f13f6cc17549;hb=b1bad322d0daf6c25f95a82c4349f057a753ab7c;hp=c0a7ec61180450d9e1633f4001bac144d7fbdc38;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index c0a7ec611..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 @@ -486,7 +488,19 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) - else None + 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 @@ -513,10 +527,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 + 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 = { @@ -598,7 +620,7 @@ 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 is_duplicate new_pos + new_neg, List.filter subs (List.filter is_duplicate new_pos) ;; @@ -634,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 ( @@ -671,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 @@ -685,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 @@ -1677,6 +1699,76 @@ and given_clause_fullred_aux 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 + 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) + (string_of_equality ~env current))); + let new' = infer env sign 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 + in + let rec simplify new' active passive = + let new' = forward_simplify_new env new' ~passive active in + let active, passive, newa, retained = + 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 + in + let active, passive, new' = simplify new' active passive in + let _ = + 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 -> + 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 + let new' = match new' with _, pos -> [], List.filter accept_fun pos 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 @@ -1693,6 +1785,7 @@ let main dbd full term metasenv ugraph = 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 = @@ -1751,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 @@ -1789,8 +1882,8 @@ let main dbd full term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) - (equalities @ library_equalities))); + (string_of_equality ~env) equalities)); +(* (equalities @ library_equalities))); *) print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; @@ -1912,6 +2005,7 @@ let saturate 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 = @@ -1927,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 @@ -2069,3 +2163,217 @@ if connect_to_auto then ( AutoTactic.term_is_equality := Inference.term_is_equality; );; + +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 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))) +;; + + +let main_demod_equalities dbd term metasenv ugraph = + let module C = Cic in + let module T = CicTypeChecker in + let module PET = ProofEngineTypes in + let module PP = CicPp in + let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in + let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let proof, goals = status in + let goal' = List.nth goals 0 in + let _, metasenv, meta_proof, _ = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let 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\nTRYING TO INFER EQUALITIES MATCHING: %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 + try + 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 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 [] 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" + (String.concat "\n" + (List.map + (string_of_equality ~env) equalities)); + print_endline "--------------------------------------------------"; + let start = Unix.gettimeofday () in + print_endline "GO!"; + start_time := Unix.gettimeofday (); + if !time_limit < 1. then time_limit := 60.; + let ra, rp = + 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 e -> CicPp.ppterm (term_of_equality e)) active)) +(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) + (String.concat "\n" + (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive)); + print_newline (); + with e -> + debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) +;;