From 67165a0c7b9141667a4c604d30c14ed33d73c726 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 5 Dec 2005 12:32:06 +0000 Subject: [PATCH] added function saturate_equations that tries to infer as many equations as possible within the time limit --- helm/ocaml/paramodulation/saturate_main.ml | 6 + helm/ocaml/paramodulation/saturation.ml | 173 +++++++++++++++++++++ 2 files changed, 179 insertions(+) diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 69d50e3a0..3b5f999cf 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -87,6 +87,8 @@ let full = ref false;; let retrieve_only = ref false;; +let demod_equalities = ref false;; + let _ = let module S = Saturation in let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v @@ -104,6 +106,7 @@ let _ = and set_depth d = S.maxdepth := d and set_full () = full := true and set_retrieve () = retrieve_only := true + and set_demod_equalities () = demod_equalities := true in Arg.parse [ "-full", Arg.Unit set_full, "Enable full mode"; @@ -132,6 +135,7 @@ let _ = Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth; "-retrieve", Arg.Unit set_retrieve, "retrieve only"; + "-demod-equalities", Arg.Unit set_demod_equalities, "demod equalities"; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; @@ -146,6 +150,8 @@ in let term, metasenv, ugraph = get_from_user ~dbd in if !retrieve_only then Saturation.retrieve_and_print dbd term metasenv ugraph +else if !demod_equalities then + Saturation.main_demod_equalities dbd term metasenv ugraph else Saturation.main dbd !full term metasenv ugraph ;; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 8e67bc7a0..4b4650b11 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1697,6 +1697,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 @@ -2183,3 +2253,106 @@ let retrieve_and_print dbd term metasenv ugraph = (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_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 [] 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 + Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" + (String.concat "\n" + (List.map (fun (s, e) -> (string_of_equality ~env e)) (fst ra))) + (String.concat "\n" + (List.map (string_of_equality ~env) + (match rp with (n, _), (p, _), _ -> p))); + print_newline (); + with e -> + debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) +;; -- 2.39.2