5 (* profiling statistics... *)
6 let infer_time = ref 0.;;
7 let forward_simpl_time = ref 0.;;
8 let backward_simpl_time = ref 0.;;
10 (* limited-resource-strategy related globals *)
11 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
12 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
13 let start_time = ref 0.;; (* time at which the execution started *)
14 let elapsed_time = ref 0.;;
15 let maximal_weight = ref None;;
16 (* let maximal_retained_equality = ref None;; *)
18 (* equality-selection related globals *)
19 let use_fullred = ref false;;
20 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
21 let weight_age_counter = ref !weight_age_ratio;;
22 let symbols_ratio = ref 0;;
23 let symbols_counter = ref 0;;
26 let derived_clauses = ref 0;;
27 let kept_clauses = ref 0;;
29 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
35 | Success of Cic.term option * environment
40 let symbols_of_equality (_, (_, left, right), _, _) =
41 TermSet.union (symbols_of_term left) (symbols_of_term right)
45 let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
46 let m1 = symbols_of_term left in
51 let c = TermMap.find k res in
52 TermMap.add k (c+v) res
55 (symbols_of_term right) m1
57 (* Printf.printf "symbols_of_equality %s:\n" *)
58 (* (string_of_equality equality); *)
59 (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
60 (* print_newline (); *)
65 let weight_of_equality (_, (ty, left, right, _), _, _) =
66 let weight_of t = fst (weight_of_term ~consider_metas:false t) in
67 (weight_of ty) + (weight_of left) + (weight_of right)
71 module OrderedEquality = struct
72 type t = Inference.equality
75 match meta_convertibility_eq eq1 eq2 with
78 let _, (ty, left, right, _), _, _ = eq1
79 and _, (ty', left', right', _), _, _ = eq2 in
80 let weight_of t = fst (weight_of_term ~consider_metas:false t) in
81 let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
82 and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
83 (* let w1 = weight_of_equality eq1 *)
84 (* and w2 = weight_of_equality eq2 in *)
85 match Pervasives.compare w1 w2 with
86 | 0 -> Pervasives.compare eq1 eq2
90 module EqualitySet = Set.Make(OrderedEquality);;
93 let select env passive (active, _) =
94 processed_clauses := !processed_clauses + 1;
96 let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
98 List.filter (fun e -> e <> eq) l
100 if !weight_age_ratio > 0 then
101 weight_age_counter := !weight_age_counter - 1;
102 match !weight_age_counter with
104 weight_age_counter := !weight_age_ratio;
105 match neg_list, pos_list with
107 (* Negatives aren't indexed, no need to remove them... *)
109 ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
112 Indexing.remove_index passive_table hd
113 (* if !use_fullred then Indexing.remove_index passive_table hd *)
114 (* else passive_table *)
117 (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
118 | _, _ -> assert false
120 | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
121 symbols_counter := !symbols_counter - 1;
122 let cardinality map =
123 TermMap.fold (fun k v res -> res + v) map 0
126 | (Negative, e)::_ ->
127 let symbols = symbols_of_equality e in
128 let card = cardinality symbols in
129 let foldfun k v (r1, r2) =
130 if TermMap.mem k symbols then
131 let c = TermMap.find k symbols in
132 let c1 = abs (c - v) in
138 let f equality (i, e) =
140 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
142 let c = others + (abs (common - card)) in
143 if c < i then (c, equality)
146 let e1 = EqualitySet.min_elt pos_set in
149 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
151 (others + (abs (common - card))), e1
153 let _, current = EqualitySet.fold f pos_set initial in
154 (* Printf.printf "\nsymbols-based selection: %s\n\n" *)
155 (* (string_of_equality ~env current); *)
157 Indexing.remove_index passive_table current
158 (* if !use_fullred then Indexing.remove_index passive_table current *)
159 (* else passive_table *)
163 (remove current pos_list, EqualitySet.remove current pos_set),
166 let current = EqualitySet.min_elt pos_set in
168 Indexing.remove_index passive_table current
169 (* if !use_fullred then Indexing.remove_index passive_table current *)
170 (* else passive_table *)
174 (remove current pos_list, EqualitySet.remove current pos_set),
177 (Positive, current), passive
180 symbols_counter := !symbols_ratio;
181 let set_selection set = EqualitySet.min_elt set in
182 if EqualitySet.is_empty neg_set then
183 let current = set_selection pos_set in
186 (remove current pos_list, EqualitySet.remove current pos_set),
187 Indexing.remove_index passive_table current
188 (* if !use_fullred then Indexing.remove_index passive_table current *)
189 (* else passive_table *)
191 (Positive, current), passive
193 let current = set_selection neg_set in
195 (remove current neg_list, EqualitySet.remove current neg_set),
199 (Negative, current), passive
203 let make_passive neg pos =
204 let set_of equalities =
205 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
208 List.fold_left (fun tbl e -> Indexing.index tbl e)
209 (Indexing.empty_table ()) pos
210 (* if !use_fullred then *)
211 (* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
212 (* (Indexing.empty_table ()) pos *)
214 (* Indexing.empty_table () *)
223 [], Indexing.empty_table ()
227 let add_to_passive passive (new_neg, new_pos) =
228 let (neg_list, neg_set), (pos_list, pos_set), table = passive in
229 let ok set equality = not (EqualitySet.mem equality set) in
230 let neg = List.filter (ok neg_set) new_neg
231 and pos = List.filter (ok pos_set) new_pos in
233 List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
234 (* if !use_fullred then *)
235 (* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
239 let add set equalities =
240 List.fold_left (fun s e -> EqualitySet.add e s) set equalities
242 (neg @ neg_list, add neg_set neg),
243 (pos_list @ pos, add pos_set pos),
248 let passive_is_empty = function
249 | ([], _), ([], _), _ -> true
254 let size_of_passive ((_, ns), (_, ps), _) =
255 (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
259 let size_of_active (active_list, _) =
260 List.length active_list
264 let prune_passive howmany (active, _) passive =
265 let (nl, ns), (pl, ps), tbl = passive in
266 let howmany = float_of_int howmany
267 and ratio = float_of_int !weight_age_ratio in
268 let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
269 and in_age = int_of_float (howmany /. (ratio +. 1.)) in
270 Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
273 | (Negative, e)::_ ->
274 let symbols = symbols_of_equality e in
275 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
279 let counter = ref !symbols_ratio in
280 let rec pickw w ns ps =
282 if not (EqualitySet.is_empty ns) then
283 let e = EqualitySet.min_elt ns in
284 let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
285 EqualitySet.add e ns', ps
286 else if !counter > 0 then
288 counter := !counter - 1;
289 if !counter = 0 then counter := !symbols_ratio
293 let e = EqualitySet.min_elt ps in
294 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
295 ns, EqualitySet.add e ps'
297 let foldfun k v (r1, r2) =
298 if TermMap.mem k symbols then
299 let c = TermMap.find k symbols in
300 let c1 = abs (c - v) in
306 let f equality (i, e) =
308 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
310 let c = others + (abs (common - card)) in
311 if c < i then (c, equality)
314 let e1 = EqualitySet.min_elt ps in
317 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
319 (others + (abs (common - card))), e1
321 let _, e = EqualitySet.fold f ps initial in
322 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
323 ns, EqualitySet.add e ps'
325 let e = EqualitySet.min_elt ps in
326 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
327 ns, EqualitySet.add e ps'
329 EqualitySet.empty, EqualitySet.empty
331 (* let in_weight, ns = pickw in_weight ns in *)
332 (* let _, ps = pickw in_weight ps in *)
333 let ns, ps = pickw in_weight ns ps in
334 let rec picka w s l =
338 | hd::tl when not (EqualitySet.mem hd s) ->
339 let w, s, l = picka (w-1) s tl in
340 w, EqualitySet.add hd s, hd::l
342 let w, s, l = picka w s tl in
347 let in_age, ns, nl = picka in_age ns nl in
348 let _, ps, pl = picka in_age ps pl in
349 if not (EqualitySet.is_empty ps) then
350 maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps));
351 (* maximal_retained_equality := Some (EqualitySet.max_elt ps); *)
354 (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
355 (* if !use_fullred then *)
356 (* EqualitySet.fold *)
357 (* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
361 (nl, ns), (pl, ps), tbl
365 let infer env sign current (active_list, active_table) =
366 let new_neg, new_pos =
369 Indexing.superposition_left env active_table current, []
372 Indexing.superposition_right !maxmeta env active_table current in
374 let rec infer_positive table = function
376 | (Negative, equality)::tl ->
377 let res = Indexing.superposition_left env table equality in
378 let neg, pos = infer_positive table tl in
380 | (Positive, equality)::tl ->
382 Indexing.superposition_right !maxmeta env table equality in
384 let neg, pos = infer_positive table tl in
387 let curr_table = Indexing.index (Indexing.empty_table ()) current in
388 let neg, pos = infer_positive curr_table active_list in
391 derived_clauses := !derived_clauses + (List.length new_neg) +
392 (List.length new_pos);
393 match !maximal_weight(* !maximal_retained_equality *) with
394 | None -> new_neg, new_pos
397 List.filter (fun e -> (weight_of_equality e) <= w (* OrderedEquality.compare e eq <= 0 *)) new_pos in
402 let contains_empty env (negative, positive) =
403 let metasenv, context, ugraph = env in
405 let (proof, _, _, _) =
407 (fun (proof, (ty, left, right, ordering), m, a) ->
408 fst (CicReduction.are_convertible context left right ugraph))
417 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
418 let pl, passive_table =
421 | Some ((pn, _), (pp, _), pt) ->
422 let pn = List.map (fun e -> (Negative, e)) pn
423 and pp = List.map (fun e -> (Positive, e)) pp in
426 let all = if pl = [] then active_list else active_list @ pl in
428 (* let rec find_duplicate sign current = function *)
430 (* | (s, eq)::tl when s = sign -> *)
431 (* if meta_convertibility_eq current eq then true *)
432 (* else find_duplicate sign current tl *)
433 (* | _::tl -> find_duplicate sign current tl *)
435 let demodulate table current =
436 let newmeta, newcurrent =
437 Indexing.demodulation !maxmeta env table current in
439 if is_identity env newcurrent then
440 if sign = Negative then Some (sign, newcurrent) else None
442 Some (sign, newcurrent)
445 let res = demodulate active_table current in
448 | Some (sign, newcurrent) ->
449 match passive_table with
451 | Some passive_table -> demodulate passive_table newcurrent
455 | Some (Negative, c) ->
458 (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
461 if ok then res else None
462 | Some (Positive, c) ->
463 if Indexing.in_index active_table c then
466 match passive_table with
468 | Some passive_table ->
469 if Indexing.in_index passive_table c then None else res
471 (* | Some (s, c) -> if find_duplicate s c all then None else res *)
473 (* if s = Utils.Negative then *)
476 (* if Indexing.subsumption env active_table c then *)
479 (* match passive_table with *)
481 (* | Some passive_table -> *)
482 (* if Indexing.subsumption env passive_table c then *)
488 (* let pred (sign, eq) = *)
489 (* if sign <> s then false *)
490 (* else subsumption env c eq *)
492 (* if List.exists pred all then None *)
496 type fs_time_info_t = {
497 mutable build_all: float;
498 mutable demodulate: float;
499 mutable subsumption: float;
502 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
505 let forward_simplify_new env (new_neg, new_pos) ?passive active =
506 let t1 = Unix.gettimeofday () in
508 let active_list, active_table = active in
509 let pl, passive_table =
512 | Some ((pn, _), (pp, _), pt) ->
513 let pn = List.map (fun e -> (Negative, e)) pn
514 and pp = List.map (fun e -> (Positive, e)) pp in
517 let all = active_list @ pl in
519 let t2 = Unix.gettimeofday () in
520 fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
522 let demodulate table target =
523 let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
527 (* let f sign' target (sign, eq) = *)
528 (* if sign <> sign' then false *)
529 (* else subsumption env target eq *)
532 let t1 = Unix.gettimeofday () in
534 let new_neg, new_pos =
535 let new_neg = List.map (demodulate active_table) new_neg
536 and new_pos = List.map (demodulate active_table) new_pos in
537 match passive_table with
538 | None -> new_neg, new_pos
539 | Some passive_table ->
540 List.map (demodulate passive_table) new_neg,
541 List.map (demodulate passive_table) new_pos
544 let t2 = Unix.gettimeofday () in
545 fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
550 if not (Inference.is_identity env e) then EqualitySet.add e s else s)
551 EqualitySet.empty new_pos
553 let new_pos = EqualitySet.elements new_pos_set in
556 (* match passive_table with *)
558 (* (fun e -> not (Indexing.subsumption env active_table e)) *)
559 (* | Some passive_table -> *)
560 (* (fun e -> not ((Indexing.subsumption env active_table e) || *)
561 (* (Indexing.subsumption env passive_table e))) *)
564 let t1 = Unix.gettimeofday () in
566 (* let new_neg, new_pos = *)
567 (* List.filter subs new_neg, *)
568 (* List.filter subs new_pos *)
571 (* let new_neg, new_pos = *)
572 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
573 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
576 let t2 = Unix.gettimeofday () in
577 fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
580 match passive_table with
581 | None -> (fun e -> not (Indexing.in_index active_table e))
582 | Some passive_table ->
583 (fun e -> not ((Indexing.in_index active_table e) ||
584 (Indexing.in_index passive_table e)))
586 new_neg, List.filter is_duplicate new_pos
588 (* new_neg, new_pos *)
591 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
592 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
598 let backward_simplify_active env (new_neg, new_pos) active =
599 let active_list, active_table = active in
600 let new_pos, new_table =
602 (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
603 ([], Indexing.empty_table ()) new_pos
605 let active_list, newa =
607 (fun (s, equality) (res, newn) ->
608 match forward_simplify env (s, equality) (new_pos, new_table) with
618 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
622 (fun (s, eq) (res, tbl) ->
623 if (is_identity env eq) || (find eq res) then
626 (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
627 active_list ([], Indexing.empty_table ()),
629 (fun (s, eq) (n, p) ->
630 if (s <> Negative) && (is_identity env eq) then
633 if s = Negative then eq::n, p
638 | [], [] -> active, None
639 | _ -> active, Some newa
643 let backward_simplify_passive env (new_neg, new_pos) passive =
644 let new_pos, new_table =
646 (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
647 ([], Indexing.empty_table ()) new_pos
649 let (nl, ns), (pl, ps), passive_table = passive in
650 let f sign equality (resl, ress, newn) =
651 match forward_simplify env (sign, equality) (new_pos, new_table) with
652 | None -> resl, EqualitySet.remove equality ress, newn
655 equality::resl, ress, newn
657 let ress = EqualitySet.remove equality ress in
660 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
661 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
664 (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
666 match newn, newp with
667 | [], [] -> ((nl, ns), (pl, ps), passive_table), None
668 | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
672 let backward_simplify env new' ?passive active =
673 let active, newa = backward_simplify_active env new' active in
676 active, (make_passive [] []), newa, None
679 backward_simplify_passive env new' passive in
680 active, passive, newa, newp
684 let get_selection_estimate () =
685 elapsed_time := (Unix.gettimeofday ()) -. !start_time;
686 (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
688 ceil ((float_of_int !processed_clauses) *.
689 ((!time_limit *. 2.) /. !elapsed_time -. 1.)))
693 let rec given_clause env passive active =
694 let selection_estimate = get_selection_estimate () in
695 let kept = size_of_passive passive in
697 if !time_limit = 0. || !processed_clauses = 0 then
699 else if !elapsed_time > !time_limit then (
700 Printf.printf "Time limit (%.2f) reached: %.2f\n"
701 !time_limit !elapsed_time;
703 ) else if kept > selection_estimate then (
704 Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
705 "selection_estimate: %d)\n") kept selection_estimate;
706 prune_passive selection_estimate active passive
711 kept_clauses := (size_of_passive passive) + (size_of_active active);
713 match passive_is_empty passive with
716 let (sign, current), passive = select env passive active in
717 match forward_simplify env (sign, current) ~passive active with
719 given_clause env passive active
720 | Some (sign, current) ->
721 if (sign = Negative) && (is_identity env current) then (
722 Printf.printf "OK!!! %s %s" (string_of_sign sign)
723 (string_of_equality ~env current);
725 let proof, _, _, _ = current in
726 Success (Some proof, env)
728 print_endline "\n================================================";
729 Printf.printf "selected: %s %s"
730 (string_of_sign sign) (string_of_equality ~env current);
733 let t1 = Unix.gettimeofday () in
734 let new' = infer env sign current active in
735 let t2 = Unix.gettimeofday () in
736 infer_time := !infer_time +. (t2 -. t1);
738 let res, proof = contains_empty env new' in
742 let t1 = Unix.gettimeofday () in
743 let new' = forward_simplify_new env new' (* ~passive *) active in
744 let t2 = Unix.gettimeofday () in
746 forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
752 let t1 = Unix.gettimeofday () in
753 let active, _, newa, _ =
754 backward_simplify env ([], [current]) active
756 let t2 = Unix.gettimeofday () in
757 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
761 let al, tbl = active in
762 let nn = List.map (fun e -> Negative, e) n in
767 Indexing.index tbl e)
773 (* Printf.printf "active:\n%s\n" *)
774 (* (String.concat "\n" *)
776 (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
777 (* (string_of_equality ~env e)) (fst active)))); *)
778 (* print_newline (); *)
781 (* match new' with *)
783 (* Printf.printf "new':\n%s\n" *)
784 (* (String.concat "\n" *)
786 (* (fun e -> "Negative " ^ *)
787 (* (string_of_equality ~env e)) neg) @ *)
789 (* (fun e -> "Positive " ^ *)
790 (* (string_of_equality ~env e)) pos))); *)
791 (* print_newline (); *)
793 match contains_empty env new' with
796 let al, tbl = active in
798 | Negative -> (sign, current)::al, tbl
800 al @ [(sign, current)], Indexing.index tbl current
802 let passive = add_to_passive passive new' in
803 (* let (_, ns), (_, ps), _ = passive in *)
804 (* Printf.printf "passive:\n%s\n" *)
805 (* (String.concat "\n" *)
806 (* ((List.map (fun e -> "Negative " ^ *)
807 (* (string_of_equality ~env e)) *)
808 (* (EqualitySet.elements ns)) @ *)
809 (* (List.map (fun e -> "Positive " ^ *)
810 (* (string_of_equality ~env e)) *)
811 (* (EqualitySet.elements ps)))); *)
812 (* print_newline (); *)
813 given_clause env passive active
820 let rec given_clause_fullred env passive active =
821 let selection_estimate = get_selection_estimate () in
822 let kept = size_of_passive passive in
824 if !time_limit = 0. || !processed_clauses = 0 then
826 else if !elapsed_time > !time_limit then (
827 Printf.printf "Time limit (%.2f) reached: %.2f\n"
828 !time_limit !elapsed_time;
830 ) else if kept > selection_estimate then (
831 Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
832 "selection_estimate: %d)\n") kept selection_estimate;
833 prune_passive selection_estimate active passive
838 match passive_is_empty passive with
841 let (sign, current), passive = select env passive active in
842 match forward_simplify env (sign, current) ~passive active with
844 given_clause_fullred env passive active
845 | Some (sign, current) ->
846 if (sign = Negative) && (is_identity env current) then (
847 Printf.printf "OK!!! %s %s" (string_of_sign sign)
848 (string_of_equality ~env current);
850 let proof, _, _, _ = current in
851 Success (Some proof, env)
853 print_endline "\n================================================";
854 Printf.printf "selected: %s %s"
855 (string_of_sign sign) (string_of_equality ~env current);
858 let t1 = Unix.gettimeofday () in
859 let new' = infer env sign current active in
860 let t2 = Unix.gettimeofday () in
861 infer_time := !infer_time +. (t2 -. t1);
864 if is_identity env current then active
866 let al, tbl = active in
868 | Negative -> (sign, current)::al, tbl
869 | Positive -> al @ [(sign, current)], Indexing.index tbl current
871 let rec simplify new' active passive =
872 let t1 = Unix.gettimeofday () in
873 let new' = forward_simplify_new env new' ~passive active in
874 let t2 = Unix.gettimeofday () in
875 forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
876 let t1 = Unix.gettimeofday () in
877 let active, passive, newa, retained =
878 backward_simplify env new' ~passive active in
879 let t2 = Unix.gettimeofday () in
880 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
881 match newa, retained with
882 | None, None -> active, passive, new'
884 | None, Some (n, p) ->
886 simplify (nn @ n, np @ p) active passive
887 | Some (n, p), Some (rn, rp) ->
889 simplify (nn @ n @ rn, np @ p @ rp) active passive
891 let active, passive, new' = simplify new' active passive in
893 let k = size_of_passive passive in
894 if k < (kept - 1) then
895 processed_clauses := !processed_clauses + (kept - 1 - k);
898 Printf.printf "active:\n%s\n"
901 (fun (s, e) -> (string_of_sign s) ^ " " ^
902 (string_of_equality ~env e)) (fst active))));
908 Printf.printf "new':\n%s\n"
911 (fun e -> "Negative " ^
912 (string_of_equality ~env e)) neg) @
914 (fun e -> "Positive " ^
915 (string_of_equality ~env e)) pos)));
918 match contains_empty env new' with
920 let passive = add_to_passive passive new' in
921 given_clause_fullred env passive active
928 let get_from_user () =
929 let dbd = Mysql.quick_connect
930 ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
932 match read_line () with
936 let term_string = String.concat "\n" (get ()) in
937 let env, metasenv, term, ugraph =
938 List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
940 term, metasenv, ugraph
944 let given_clause_ref = ref given_clause;;
948 let module C = Cic in
949 let module T = CicTypeChecker in
950 let module PET = ProofEngineTypes in
951 let module PP = CicPp in
952 let term, metasenv, ugraph = get_from_user () in
953 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
955 PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
956 let goal = List.nth goals 0 in
957 let _, metasenv, meta_proof, _ = proof in
958 let _, context, goal = CicUtil.lookup_meta goal metasenv in
959 let equalities, maxm = find_equalities context proof in
960 maxmeta := maxm; (* TODO ugly!! *)
961 let env = (metasenv, context, ugraph) in
963 let term_equality = equality_of_term meta_proof goal in
964 let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
965 let active = make_active () in
966 let passive = make_passive [term_equality] equalities in
967 Printf.printf "\ncurrent goal: %s\n"
968 (string_of_equality ~env term_equality);
969 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
970 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
971 Printf.printf "\nequalities:\n%s\n"
974 (string_of_equality ~env)
976 print_endline "--------------------------------------------------";
977 let start = Unix.gettimeofday () in
979 start_time := Unix.gettimeofday ();
981 (if !use_fullred then given_clause_fullred else given_clause)
984 let finish = Unix.gettimeofday () in
988 Printf.printf "NO proof found! :-(\n\n"
989 | Success (Some proof, env) ->
990 Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
991 (PP.pp proof (names_of_context context))
993 (* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *)
994 (* " demodulate: %.9f\n subsumption: %.9f\n") *)
995 (* fs_time_info.build_all fs_time_info.demodulate *)
996 (* fs_time_info.subsumption; *)
997 | Success (None, env) ->
998 Printf.printf "Success, but no proof?!?\n\n"
1000 Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1001 "backward_simpl_time: %.9f\n")
1002 !infer_time !forward_simpl_time !backward_simpl_time;
1003 Printf.printf "successful unification/matching time: %.9f\n"
1004 !Indexing.match_unif_time_ok;
1005 Printf.printf "failed unification/matching time: %.9f\n"
1006 !Indexing.match_unif_time_no;
1007 Printf.printf "indexing retrieval time: %.9f\n"
1008 !Indexing.indexing_retrieval_time;
1009 Printf.printf "derived %d clauses, kept %d clauses.\n"
1010 !derived_clauses !kept_clauses;
1012 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1017 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
1020 let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
1021 and set_sel v = symbols_ratio := v; symbols_counter := v;
1022 and set_conf f = configuration_file := f
1023 and set_lpo () = Utils.compare_terms := lpo
1024 and set_kbo () = Utils.compare_terms := nonrec_kbo
1025 and set_fullred () = use_fullred := true
1026 and set_time_limit v = time_limit := float_of_int v
1029 "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
1031 "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
1033 "-s", Arg.Int set_sel,
1034 "symbols-based selection ratio (relative to the weight ratio)";
1036 "-c", Arg.String set_conf, "Configuration file (for the db connection)";
1038 "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
1040 "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
1042 "-l", Arg.Int set_time_limit, "Time limit (in seconds)";
1043 ] (fun a -> ()) "Usage:"
1045 Helm_registry.load_from !configuration_file;