-(* type naif_indexing =
- (Cic.term * ((bool * Inference.equality) list)) list
-;; *)
+(** settable by the command line (-i switch) *)
+let use_index = ref true;;
+
type pos = Left | Right ;;
;;
-let rec find_matches unif_fun metasenv context ugraph lift_amount term =
+let rec find_matches metasenv context ugraph lift_amount term =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
let subst', metasenv', ugraph' =
(* Inference.matching (metasenv @ metas) context term *)
(* (S.lift lift_amount c) ugraph *)
- unif_fun (metasenv @ metas) context
+ Inference.matching (metasenv @ metas) context
term (S.lift lift_amount c) ugraph
in
(* let names = U.names_of_context context in *)
res
with e ->
(* Printf.printf "ERRORE!: %s\n" (Printexc.to_string e); *)
- find_matches unif_fun metasenv context ugraph lift_amount term tl
+ find_matches metasenv context ugraph lift_amount term tl
else
let res = try do_match c other eq_URI with e -> None in
match res with
if order = U.Gt then
res
else
- find_matches unif_fun metasenv context ugraph
- lift_amount term tl
+ find_matches metasenv context ugraph lift_amount term tl
| None ->
- find_matches unif_fun metasenv context ugraph lift_amount term tl
+ find_matches metasenv context ugraph lift_amount term tl
+;;
+
+
+let get_candidates table term =
+ if !use_index then
+ try Hashtbl.find table (head_of_term term) with Not_found -> []
+ else
+ Hashtbl.fold (fun k v l -> v @ l) table []
;;
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let hd_term = head_of_term term in
- let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
+ let candidates = get_candidates table term in
match term with
| C.Meta _ -> None
| term ->
let res =
- find_matches Inference.matching metasenv context ugraph
- lift_amount term candidates
+ find_matches metasenv context ugraph lift_amount term candidates
in
if res <> None then
res
if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
- else (
-(* Printf.printf "Going on 1:\ntarget: %s\nnewtarget: %s\n%s\n\n" *)
-(* (Inference.string_of_equality ~env target) *)
-(* (Inference.string_of_equality ~env newtarget) *)
-(* (string_of_bool (target = newtarget)); *)
+ else
demodulation newmeta env table newtarget
- )
| None ->
let res = demodulate_term metasenv' context ugraph table 0 right in
match res with
if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
- else (
-(* Printf.printf "Going on 2:\ntarget: %s\nnewtarget: %s\n\n" *)
-(* (Inference.string_of_equality ~env target) *)
-(* (Inference.string_of_equality ~env newtarget); *)
+ else
demodulation newmeta env table newtarget
- )
| None ->
newmeta, target
;;
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let hd_term = head_of_term term in
- let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
+ let candidates = get_candidates table term in
let res, lifted_term =
match term with
| C.Meta (i, l) ->
else res
;;
+type fs_time_info_t = {
+ mutable build_all: float;
+ mutable demodulate: float;
+ mutable subsumption: float;
+};;
+
+let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
+
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 =
match passive with
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);
+
let demodulate table target =
let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
maxmeta := newmeta;
newtarget
in
+ let f sign' target (sign, eq) =
+ if sign <> sign' then false
+ else subsumption env target eq
+ in
+
+ let t1 = Unix.gettimeofday () in
+
+ let new_neg, new_pos =
+ (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
+ List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
+ in
+
+ let t2 = Unix.gettimeofday () in
+ fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
+ let t1 = Unix.gettimeofday () in
+
let new_neg, new_pos =
let new_neg = List.map (demodulate active_table) new_neg
and new_pos = List.map (demodulate active_table) new_pos in
List.map (demodulate passive_table) new_neg,
List.map (demodulate passive_table) new_pos
in
+
+ let t2 = Unix.gettimeofday () in
+ fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
+
let new_pos_set =
List.fold_left
(fun s e ->
EqualitySet.empty new_pos
in
let new_pos = EqualitySet.elements new_pos_set in
- let f sign' target (sign, eq) =
- if sign <> sign' then false
- else subsumption env target eq
- in
- (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
- List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
+ new_neg, new_pos
+(* let res = *)
+(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
+(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
+(* in *)
+(* res *)
;;
active, passive, newa, newp
;;
+
+let infer_time = ref 0.;;
+let forward_simpl_time = ref 0.;;
+let backward_simpl_time = ref 0.;;
+
let rec given_clause env passive active =
match passive_is_empty passive with
(string_of_sign sign) (string_of_equality ~env current);
print_newline ();
+ 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, proof = contains_empty env new' in
if res then
Success (proof, env)
- else
+ else
+ let t1 = Unix.gettimeofday () in
let new' = forward_simplify_new env new' active in
+ let t2 = Unix.gettimeofday () in
+ let _ =
+ forward_simpl_time := !forward_simpl_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) ->
(string_of_sign sign) (string_of_equality ~env current);
print_newline ();
+ 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 active =
if is_identity env current then active
| Positive -> al @ [(sign, current)], Indexing.index tbl current
in
let rec simplify new' active passive =
+ let t1 = Unix.gettimeofday () in
let new' = forward_simplify_new env new' ~passive active in
+ let t2 = Unix.gettimeofday () in
+ forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
+ let t1 = Unix.gettimeofday () in
let active, passive, newa, retained =
- backward_simplify env new' ~passive active
- in
+ 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
Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
(PP.pp proof (names_of_context context))
(finish -. start);
+ Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ "backward_simpl_time: %.9f\n")
+ !infer_time !forward_simpl_time !backward_simpl_time;
+ Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^
+ " demodulate: %.9f\n subsumption: %.9f\n")
+ fs_time_info.build_all fs_time_info.demodulate
+ fs_time_info.subsumption;
| Success (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
with exc ->
and set_lpo () = Utils.compare_terms := lpo
and set_kbo () = Utils.compare_terms := nonrec_kbo
and set_fullred () = given_clause_ref := given_clause_fullred
+ and set_use_index v = Indexing.use_index := v
in
Arg.parse [
"-f", Arg.Unit set_fullred, "Use full-reduction strategy";
"-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
"-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
+
+ "-i", Arg.Bool set_use_index, "Use indexing yes/no (default: yes)";
] (fun a -> ()) "Usage:"
in
Helm_registry.load_from !configuration_file;
projects / helm.git / commitdiff