X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=0514ed5033f732389b8221cf903a5ab10118995f;hb=9262517c80e17d46b9bf9931dc879ac653a633e9;hp=d73428c8ac8081fc53a81f6a0698f9697b7141bd;hpb=b1527286e32c8651d65619af61e3f638b3b89f8d;p=helm.git diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml index d73428c8a..0514ed503 100644 --- a/helm/ocaml/tactics/paramodulation/saturation.ml +++ b/helm/ocaml/tactics/paramodulation/saturation.ml @@ -56,7 +56,7 @@ let symbols_ratio = ref (* 0 *) 3;; let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) -Utils.compare_terms := Utils.rpo;; +(* Utils.compare_terms := Utils.rpo;; *) (* Utils.compare_terms := Utils.nonrec_kbo;; *) (* Utils.compare_terms := Utils.ao;; *) @@ -81,8 +81,7 @@ type goal = proof * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; - -let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = +let symbols_of_equality (_, _, (_, left, right, _), _, _) = let m1 = symbols_of_term left in let m = TermMap.fold @@ -97,7 +96,6 @@ let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = m ;; - module OrderedEquality = struct type t = Inference.equality @@ -564,7 +562,6 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in - let all = active_list @ pl in let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); @@ -771,7 +768,6 @@ let simplify_goal env goal ?passive (active_list, active_table) = 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 = @@ -826,7 +822,6 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = 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 = @@ -1075,7 +1070,7 @@ 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 + | NoProof -> NoProof | BasicProof t -> BasicProof (CicMetaSubst.apply_subst subst t) | ProofGoalBlock (p, pb) -> @@ -1507,7 +1502,6 @@ and given_clause_aux dbd env goals theorems passive active = al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in given_clause dbd env goals theorems passive active | true, goal -> let proof = @@ -2160,13 +2154,6 @@ let saturate let init () = ();; -(* UGLY SIDE EFFECT... -if connect_to_auto then ( - AutoTactic.paramodulation_tactic := saturate; - 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 @@ -2191,72 +2178,69 @@ let retrieve_and_print dbd term metasenv ugraph = 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 + 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 + maxmeta := maxm+2; + 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 - debug_print - (lazy - (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) + 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 + let _equalities = + 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))) ;; @@ -2289,7 +2273,6 @@ let main_demod_equalities dbd term metasenv ugraph = 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 = @@ -2343,23 +2326,19 @@ let main_demod_equalities dbd term metasenv ugraph = (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 = EqualitySet.add e s - (* + let addfun s e = if not (EqualitySet.mem e initial) then EqualitySet.add e s else s - *) in let passive =