5 (* profiling statistics... *)
6 let infer_time = ref 0.;;
7 let forward_simpl_time = ref 0.;;
8 let forward_simpl_new_time = ref 0.;;
9 let backward_simpl_time = ref 0.;;
10 let passive_maintainance_time = ref 0.;;
12 (* limited-resource-strategy related globals *)
13 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
14 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
15 let start_time = ref 0.;; (* time at which the execution started *)
16 let elapsed_time = ref 0.;;
17 (* let maximal_weight = ref None;; *)
18 let maximal_retained_equality = ref None;;
20 (* equality-selection related globals *)
21 let use_fullred = ref false;;
22 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
23 let weight_age_counter = ref !weight_age_ratio;;
24 let symbols_ratio = ref 0;;
25 let symbols_counter = ref 0;;
28 let derived_clauses = ref 0;;
29 let kept_clauses = ref 0;;
31 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
37 | Success of Cic.term option * environment
42 let symbols_of_equality (_, (_, left, right), _, _) =
43 TermSet.union (symbols_of_term left) (symbols_of_term right)
47 let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
48 let m1 = symbols_of_term left in
53 let c = TermMap.find k res in
54 TermMap.add k (c+v) res
57 (symbols_of_term right) m1
59 (* Printf.printf "symbols_of_equality %s:\n" *)
60 (* (string_of_equality equality); *)
61 (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
62 (* print_newline (); *)
67 let weight_of_equality (_, (ty, left, right, _), _, _) =
68 let meta_number = ref 0 in
70 let weight, ml = weight_of_term t in
71 meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
74 (weight_of ty) + (weight_of left) + (weight_of right), meta_number
78 module OrderedEquality = struct
79 type t = Inference.equality
82 match meta_convertibility_eq eq1 eq2 with
85 let _, (ty, left, right, _), _, _ = eq1
86 and _, (ty', left', right', _), _, _ = eq2 in
87 (* let w1, m1 = weight_of_equality eq1 *)
88 (* and w2, m2 = weight_of_equality eq2 in *)
89 let weight_of t = fst (weight_of_term ~consider_metas:false t) in
90 let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
91 and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
92 match Pervasives.compare w1 w2 with
93 | 0 -> Pervasives.compare eq1 eq2
94 (* let res = Pervasives.compare m1 m2 in *)
95 (* if res = 0 then Pervasives.compare eq1 eq2 else res *)
99 module EqualitySet = Set.Make(OrderedEquality);;
102 let select env passive (active, _) =
103 processed_clauses := !processed_clauses + 1;
105 let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
107 List.filter (fun e -> e <> eq) l
109 if !weight_age_ratio > 0 then
110 weight_age_counter := !weight_age_counter - 1;
111 match !weight_age_counter with
113 weight_age_counter := !weight_age_ratio;
114 match neg_list, pos_list with
116 (* Negatives aren't indexed, no need to remove them... *)
118 ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
121 Indexing.remove_index passive_table hd
122 (* if !use_fullred then Indexing.remove_index passive_table hd *)
123 (* else passive_table *)
126 (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
127 | _, _ -> assert false
129 | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
130 symbols_counter := !symbols_counter - 1;
131 let cardinality map =
132 TermMap.fold (fun k v res -> res + v) map 0
135 | (Negative, e)::_ ->
136 let symbols = symbols_of_equality e in
137 let card = cardinality symbols in
138 let foldfun k v (r1, r2) =
139 if TermMap.mem k symbols then
140 let c = TermMap.find k symbols in
141 let c1 = abs (c - v) in
147 let f equality (i, e) =
149 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
151 let c = others + (abs (common - card)) in
152 if c < i then (c, equality)
153 (* else if c = i then *)
154 (* match OrderedEquality.compare equality e with *)
155 (* | -1 -> (c, equality) *)
156 (* | res -> (i, e) *)
159 let e1 = EqualitySet.min_elt pos_set in
162 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
164 (others + (abs (common - card))), e1
166 let _, current = EqualitySet.fold f pos_set initial in
167 (* Printf.printf "\nsymbols-based selection: %s\n\n" *)
168 (* (string_of_equality ~env current); *)
170 Indexing.remove_index passive_table current
171 (* if !use_fullred then Indexing.remove_index passive_table current *)
172 (* else passive_table *)
176 (remove current pos_list, EqualitySet.remove current pos_set),
179 let current = EqualitySet.min_elt pos_set in
181 Indexing.remove_index passive_table current
182 (* if !use_fullred then Indexing.remove_index passive_table current *)
183 (* else passive_table *)
187 (remove current pos_list, EqualitySet.remove current pos_set),
190 (Positive, current), passive
193 symbols_counter := !symbols_ratio;
194 let set_selection set = EqualitySet.min_elt set in
195 if EqualitySet.is_empty neg_set then
196 let current = set_selection pos_set in
199 (remove current pos_list, EqualitySet.remove current pos_set),
200 Indexing.remove_index passive_table current
201 (* if !use_fullred then Indexing.remove_index passive_table current *)
202 (* else passive_table *)
204 (Positive, current), passive
206 let current = set_selection neg_set in
208 (remove current neg_list, EqualitySet.remove current neg_set),
212 (Negative, current), passive
216 let make_passive neg pos =
217 let set_of equalities =
218 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
221 List.fold_left (fun tbl e -> Indexing.index tbl e)
222 (Indexing.empty_table ()) pos
223 (* if !use_fullred then *)
224 (* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
225 (* (Indexing.empty_table ()) pos *)
227 (* Indexing.empty_table () *)
236 [], Indexing.empty_table ()
240 let add_to_passive passive (new_neg, new_pos) =
241 let (neg_list, neg_set), (pos_list, pos_set), table = passive in
242 let ok set equality = not (EqualitySet.mem equality set) in
243 let neg = List.filter (ok neg_set) new_neg
244 and pos = List.filter (ok pos_set) new_pos in
246 List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
247 (* if !use_fullred then *)
248 (* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
252 let add set equalities =
253 List.fold_left (fun s e -> EqualitySet.add e s) set equalities
255 (neg @ neg_list, add neg_set neg),
256 (pos_list @ pos, add pos_set pos),
261 let passive_is_empty = function
262 | ([], _), ([], _), _ -> true
267 let size_of_passive ((_, ns), (_, ps), _) =
268 (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
272 let size_of_active (active_list, _) =
273 List.length active_list
277 let prune_passive howmany (active, _) passive =
278 let (nl, ns), (pl, ps), tbl = passive in
279 let howmany = float_of_int howmany
280 and ratio = float_of_int !weight_age_ratio in
281 let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
282 and in_age = int_of_float (howmany /. (ratio +. 1.)) in
283 Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
286 | (Negative, e)::_ ->
287 let symbols = symbols_of_equality e in
288 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
292 let counter = ref !symbols_ratio in
293 let rec pickw w ns ps =
295 if not (EqualitySet.is_empty ns) then
296 let e = EqualitySet.min_elt ns in
297 let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
298 EqualitySet.add e ns', ps
299 else if !counter > 0 then
301 counter := !counter - 1;
302 if !counter = 0 then counter := !symbols_ratio
306 let e = EqualitySet.min_elt ps in
307 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
308 ns, EqualitySet.add e ps'
310 let foldfun k v (r1, r2) =
311 if TermMap.mem k symbols then
312 let c = TermMap.find k symbols in
313 let c1 = abs (c - v) in
319 let f equality (i, e) =
321 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
323 let c = others + (abs (common - card)) in
324 if c < i then (c, equality)
327 let e1 = EqualitySet.min_elt ps in
330 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
332 (others + (abs (common - card))), e1
334 let _, e = EqualitySet.fold f ps initial in
335 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
336 ns, EqualitySet.add e ps'
338 let e = EqualitySet.min_elt ps in
339 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
340 ns, EqualitySet.add e ps'
342 EqualitySet.empty, EqualitySet.empty
344 (* let in_weight, ns = pickw in_weight ns in *)
345 (* let _, ps = pickw in_weight ps in *)
346 let ns, ps = pickw in_weight ns ps in
347 let rec picka w s l =
351 | hd::tl when not (EqualitySet.mem hd s) ->
352 let w, s, l = picka (w-1) s tl in
353 w, EqualitySet.add hd s, hd::l
355 let w, s, l = picka w s tl in
360 let in_age, ns, nl = picka in_age ns nl in
361 let _, ps, pl = picka in_age ps pl in
362 if not (EqualitySet.is_empty ps) then
363 (* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
364 maximal_retained_equality := Some (EqualitySet.max_elt ps);
367 (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
368 (* if !use_fullred then *)
369 (* EqualitySet.fold *)
370 (* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
374 (nl, ns), (pl, ps), tbl
378 let infer env sign current (active_list, active_table) =
379 let new_neg, new_pos =
382 Indexing.superposition_left env active_table current, []
385 Indexing.superposition_right !maxmeta env active_table current in
387 let rec infer_positive table = function
389 | (Negative, equality)::tl ->
390 let res = Indexing.superposition_left env table equality in
391 let neg, pos = infer_positive table tl in
393 | (Positive, equality)::tl ->
395 Indexing.superposition_right !maxmeta env table equality in
397 let neg, pos = infer_positive table tl in
400 let curr_table = Indexing.index (Indexing.empty_table ()) current in
401 let neg, pos = infer_positive curr_table active_list in
404 derived_clauses := !derived_clauses + (List.length new_neg) +
405 (List.length new_pos);
406 match (* !maximal_weight *)!maximal_retained_equality with
407 | None -> new_neg, new_pos
410 List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
415 let contains_empty env (negative, positive) =
416 let metasenv, context, ugraph = env in
418 let (proof, _, _, _) =
420 (fun (proof, (ty, left, right, ordering), m, a) ->
421 fst (CicReduction.are_convertible context left right ugraph))
430 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
431 let pl, passive_table =
434 | Some ((pn, _), (pp, _), pt) ->
435 let pn = List.map (fun e -> (Negative, e)) pn
436 and pp = List.map (fun e -> (Positive, e)) pp in
439 let all = if pl = [] then active_list else active_list @ pl in
441 (* let rec find_duplicate sign current = function *)
443 (* | (s, eq)::tl when s = sign -> *)
444 (* if meta_convertibility_eq current eq then true *)
445 (* else find_duplicate sign current tl *)
446 (* | _::tl -> find_duplicate sign current tl *)
450 (* if sign = Positive then *)
451 (* Indexing.subsumption env active_table current *)
459 let demodulate table current =
460 let newmeta, newcurrent =
461 Indexing.demodulation !maxmeta env table current in
463 if is_identity env newcurrent then
464 if sign = Negative then Some (sign, newcurrent) else None
466 Some (sign, newcurrent)
469 let res = demodulate active_table current in
472 | Some (sign, newcurrent) ->
473 match passive_table with
475 | Some passive_table -> demodulate passive_table newcurrent
479 | Some (Negative, c) ->
482 (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
485 if ok then res else None
486 | Some (Positive, c) ->
487 if Indexing.in_index active_table c then
490 match passive_table with
492 | Some passive_table ->
493 if Indexing.in_index passive_table c then None else res
495 (* | Some (s, c) -> if find_duplicate s c all then None else res *)
497 (* if s = Utils.Negative then *)
500 (* if Indexing.subsumption env active_table c then *)
503 (* match passive_table with *)
505 (* | Some passive_table -> *)
506 (* if Indexing.subsumption env passive_table c then *)
512 (* let pred (sign, eq) = *)
513 (* if sign <> s then false *)
514 (* else subsumption env c eq *)
516 (* if List.exists pred all then None *)
520 type fs_time_info_t = {
521 mutable build_all: float;
522 mutable demodulate: float;
523 mutable subsumption: float;
526 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
529 let forward_simplify_new env (new_neg, new_pos) ?passive active =
530 let t1 = Unix.gettimeofday () in
532 let active_list, active_table = active in
533 let pl, passive_table =
536 | Some ((pn, _), (pp, _), pt) ->
537 let pn = List.map (fun e -> (Negative, e)) pn
538 and pp = List.map (fun e -> (Positive, e)) pp in
541 let all = active_list @ pl in
543 let t2 = Unix.gettimeofday () in
544 fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
546 let demodulate table target =
547 let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
551 (* let f sign' target (sign, eq) = *)
552 (* if sign <> sign' then false *)
553 (* else subsumption env target eq *)
556 let t1 = Unix.gettimeofday () in
558 let new_neg, new_pos =
559 let new_neg = List.map (demodulate active_table) new_neg
560 and new_pos = List.map (demodulate active_table) new_pos in
561 match passive_table with
562 | None -> new_neg, new_pos
563 | Some passive_table ->
564 List.map (demodulate passive_table) new_neg,
565 List.map (demodulate passive_table) new_pos
568 let t2 = Unix.gettimeofday () in
569 fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
574 if not (Inference.is_identity env e) then EqualitySet.add e s else s)
575 EqualitySet.empty new_pos
577 let new_pos = EqualitySet.elements new_pos_set in
580 match passive_table with
582 (fun e -> not (Indexing.subsumption env active_table e))
583 | Some passive_table ->
584 (fun e -> not ((Indexing.subsumption env active_table e) ||
585 (Indexing.subsumption env passive_table e)))
588 let t1 = Unix.gettimeofday () in
590 (* let new_neg, new_pos = *)
591 (* List.filter subs new_neg, *)
592 (* List.filter subs new_pos *)
595 (* let new_neg, new_pos = *)
596 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
597 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
600 let t2 = Unix.gettimeofday () in
601 fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
604 match passive_table with
605 | None -> (fun e -> not (Indexing.in_index active_table e))
606 | Some passive_table ->
607 (fun e -> not ((Indexing.in_index active_table e) ||
608 (Indexing.in_index passive_table e)))
610 new_neg, List.filter is_duplicate new_pos
612 (* new_neg, new_pos *)
615 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
616 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
622 let backward_simplify_active env new_pos new_table active =
623 let active_list, active_table = active in
624 let active_list, newa =
626 (fun (s, equality) (res, newn) ->
627 match forward_simplify env (s, equality) (new_pos, new_table) with
637 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
641 (fun (s, eq) (res, tbl) ->
642 if (is_identity env eq) || (find eq res) then
645 (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
646 active_list ([], Indexing.empty_table ()),
648 (fun (s, eq) (n, p) ->
649 if (s <> Negative) && (is_identity env eq) then
652 if s = Negative then eq::n, p
657 | [], [] -> active, None
658 | _ -> active, Some newa
662 let backward_simplify_passive env new_pos new_table passive =
663 let (nl, ns), (pl, ps), passive_table = passive in
664 let f sign equality (resl, ress, newn) =
665 match forward_simplify env (sign, equality) (new_pos, new_table) with
666 | None -> resl, EqualitySet.remove equality ress, newn
669 equality::resl, ress, newn
671 let ress = EqualitySet.remove equality ress in
674 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
675 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
678 (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
680 match newn, newp with
681 | [], [] -> ((nl, ns), (pl, ps), passive_table), None
682 | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
686 let backward_simplify env new' ?passive active =
687 let new_pos, new_table =
689 (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
690 ([], Indexing.empty_table ()) (snd new')
692 let active, newa = backward_simplify_active env new_pos new_table active in
695 active, (make_passive [] []), newa, None
698 backward_simplify_passive env new_pos new_table passive in
699 active, passive, newa, newp
703 let get_selection_estimate () =
704 elapsed_time := (Unix.gettimeofday ()) -. !start_time;
705 (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
707 ceil ((float_of_int !processed_clauses) *.
708 ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
712 let rec given_clause env passive active =
713 let time1 = Unix.gettimeofday () in
715 let selection_estimate = get_selection_estimate () in
716 let kept = size_of_passive passive in
718 if !time_limit = 0. || !processed_clauses = 0 then
720 else if !elapsed_time > !time_limit then (
721 Printf.printf "Time limit (%.2f) reached: %.2f\n"
722 !time_limit !elapsed_time;
724 ) else if kept > selection_estimate then (
725 Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
726 "selection_estimate: %d)\n") kept selection_estimate;
727 prune_passive selection_estimate active passive
732 let time2 = Unix.gettimeofday () in
733 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
735 kept_clauses := (size_of_passive passive) + (size_of_active active);
737 match passive_is_empty passive with
740 let (sign, current), passive = select env passive active in
741 let time1 = Unix.gettimeofday () in
742 let res = forward_simplify env (sign, current) ~passive active in
743 let time2 = Unix.gettimeofday () in
744 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
747 given_clause env passive active
748 | Some (sign, current) ->
749 if (sign = Negative) && (is_identity env current) then (
750 Printf.printf "OK!!! %s %s" (string_of_sign sign)
751 (string_of_equality ~env current);
753 let proof, _, _, _ = current in
754 Success (Some proof, env)
756 print_endline "\n================================================";
757 Printf.printf "selected: %s %s"
758 (string_of_sign sign) (string_of_equality ~env current);
761 let t1 = Unix.gettimeofday () in
762 let new' = infer env sign current active in
763 let t2 = Unix.gettimeofday () in
764 infer_time := !infer_time +. (t2 -. t1);
766 let res, proof = contains_empty env new' in
770 let t1 = Unix.gettimeofday () in
771 let new' = forward_simplify_new env new' (* ~passive *) active in
772 let t2 = Unix.gettimeofday () in
774 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
780 let t1 = Unix.gettimeofday () in
781 let active, _, newa, _ =
782 backward_simplify env ([], [current]) active
784 let t2 = Unix.gettimeofday () in
785 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
789 let al, tbl = active in
790 let nn = List.map (fun e -> Negative, e) n in
795 Indexing.index tbl e)
801 (* Printf.printf "active:\n%s\n" *)
802 (* (String.concat "\n" *)
804 (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
805 (* (string_of_equality ~env e)) (fst active)))); *)
806 (* print_newline (); *)
809 (* match new' with *)
811 (* Printf.printf "new':\n%s\n" *)
812 (* (String.concat "\n" *)
814 (* (fun e -> "Negative " ^ *)
815 (* (string_of_equality ~env e)) neg) @ *)
817 (* (fun e -> "Positive " ^ *)
818 (* (string_of_equality ~env e)) pos))); *)
819 (* print_newline (); *)
821 match contains_empty env new' with
824 let al, tbl = active in
826 | Negative -> (sign, current)::al, tbl
828 al @ [(sign, current)], Indexing.index tbl current
830 let passive = add_to_passive passive new' in
831 (* let (_, ns), (_, ps), _ = passive in *)
832 (* Printf.printf "passive:\n%s\n" *)
833 (* (String.concat "\n" *)
834 (* ((List.map (fun e -> "Negative " ^ *)
835 (* (string_of_equality ~env e)) *)
836 (* (EqualitySet.elements ns)) @ *)
837 (* (List.map (fun e -> "Positive " ^ *)
838 (* (string_of_equality ~env e)) *)
839 (* (EqualitySet.elements ps)))); *)
840 (* print_newline (); *)
841 given_clause env passive active
848 let rec given_clause_fullred env passive active =
849 let time1 = Unix.gettimeofday () in
851 let selection_estimate = get_selection_estimate () in
852 let kept = size_of_passive passive in
854 if !time_limit = 0. || !processed_clauses = 0 then
856 else if !elapsed_time > !time_limit then (
857 Printf.printf "Time limit (%.2f) reached: %.2f\n"
858 !time_limit !elapsed_time;
860 ) else if kept > selection_estimate then (
861 Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
862 "selection_estimate: %d)\n") kept selection_estimate;
863 prune_passive selection_estimate active passive
868 let time2 = Unix.gettimeofday () in
869 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
871 kept_clauses := (size_of_passive passive) + (size_of_active active);
873 match passive_is_empty passive with
876 let (sign, current), passive = select env passive active in
877 let time1 = Unix.gettimeofday () in
878 let res = forward_simplify env (sign, current) ~passive active in
879 let time2 = Unix.gettimeofday () in
880 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
883 given_clause_fullred env passive active
884 | Some (sign, current) ->
885 if (sign = Negative) && (is_identity env current) then (
886 Printf.printf "OK!!! %s %s" (string_of_sign sign)
887 (string_of_equality ~env current);
889 let proof, _, _, _ = current in
890 Success (Some proof, env)
892 print_endline "\n================================================";
893 Printf.printf "selected: %s %s"
894 (string_of_sign sign) (string_of_equality ~env current);
897 let t1 = Unix.gettimeofday () in
898 let new' = infer env sign current active in
899 let t2 = Unix.gettimeofday () in
900 infer_time := !infer_time +. (t2 -. t1);
903 if is_identity env current then active
905 let al, tbl = active in
907 | Negative -> (sign, current)::al, tbl
908 | Positive -> al @ [(sign, current)], Indexing.index tbl current
910 let rec simplify new' active passive =
911 let t1 = Unix.gettimeofday () in
912 let new' = forward_simplify_new env new' ~passive active in
913 let t2 = Unix.gettimeofday () in
914 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
915 let t1 = Unix.gettimeofday () in
916 let active, passive, newa, retained =
917 backward_simplify env new' ~passive active in
918 let t2 = Unix.gettimeofday () in
919 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
920 match newa, retained with
921 | None, None -> active, passive, new'
923 | None, Some (n, p) ->
925 simplify (nn @ n, np @ p) active passive
926 | Some (n, p), Some (rn, rp) ->
928 simplify (nn @ n @ rn, np @ p @ rp) active passive
930 let active, passive, new' = simplify new' active passive in
932 let k = size_of_passive passive in
933 if k < (kept - 1) then
934 processed_clauses := !processed_clauses + (kept - 1 - k);
937 (* Printf.printf "active:\n%s\n" *)
938 (* (String.concat "\n" *)
940 (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
941 (* (string_of_equality ~env e)) (fst active)))); *)
942 (* print_newline (); *)
945 (* match new' with *)
947 (* Printf.printf "new':\n%s\n" *)
948 (* (String.concat "\n" *)
950 (* (fun e -> "Negative " ^ *)
951 (* (string_of_equality ~env e)) neg) @ *)
953 (* (fun e -> "Positive " ^ *)
954 (* (string_of_equality ~env e)) pos))); *)
955 (* print_newline (); *)
957 match contains_empty env new' with
959 let passive = add_to_passive passive new' in
960 given_clause_fullred env passive active
967 let get_from_user () =
968 let dbd = Mysql.quick_connect
969 ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
971 match read_line () with
975 let term_string = String.concat "\n" (get ()) in
976 let env, metasenv, term, ugraph =
977 List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
979 term, metasenv, ugraph
983 let given_clause_ref = ref given_clause;;
987 let module C = Cic in
988 let module T = CicTypeChecker in
989 let module PET = ProofEngineTypes in
990 let module PP = CicPp in
991 let term, metasenv, ugraph = get_from_user () in
992 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
994 PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
995 let goal = List.nth goals 0 in
996 let _, metasenv, meta_proof, _ = proof in
997 let _, context, goal = CicUtil.lookup_meta goal metasenv in
998 let equalities, maxm = find_equalities context proof in
999 maxmeta := maxm; (* TODO ugly!! *)
1000 let env = (metasenv, context, ugraph) in
1002 let term_equality = equality_of_term meta_proof goal in
1003 let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
1004 let active = make_active () in
1005 let passive = make_passive [term_equality] equalities in
1006 Printf.printf "\ncurrent goal: %s\n"
1007 (string_of_equality ~env term_equality);
1008 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1009 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1010 Printf.printf "\nequalities:\n%s\n"
1013 (string_of_equality ~env)
1015 print_endline "--------------------------------------------------";
1016 let start = Unix.gettimeofday () in
1017 print_endline "GO!";
1018 start_time := Unix.gettimeofday ();
1020 (if !use_fullred then given_clause_fullred else given_clause)
1023 let finish = Unix.gettimeofday () in
1027 Printf.printf "NO proof found! :-(\n\n"
1028 | Success (Some proof, env) ->
1029 Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
1030 (PP.pp proof (names_of_context context))
1032 (* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *)
1033 (* " demodulate: %.9f\n subsumption: %.9f\n") *)
1034 (* fs_time_info.build_all fs_time_info.demodulate *)
1035 (* fs_time_info.subsumption; *)
1036 | Success (None, env) ->
1037 Printf.printf "Success, but no proof?!?\n\n"
1039 Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1040 "forward_simpl_new_time: %.9f\n" ^^
1041 "backward_simpl_time: %.9f\n")
1042 !infer_time !forward_simpl_time !forward_simpl_new_time
1043 !backward_simpl_time;
1044 Printf.printf "passive_maintainance_time: %.9f\n"
1045 !passive_maintainance_time;
1046 Printf.printf " successful unification/matching time: %.9f\n"
1047 !Indexing.match_unif_time_ok;
1048 Printf.printf " failed unification/matching time: %.9f\n"
1049 !Indexing.match_unif_time_no;
1050 Printf.printf " indexing retrieval time: %.9f\n"
1051 !Indexing.indexing_retrieval_time;
1052 Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
1053 !Indexing.build_newtarget_time;
1054 Printf.printf "derived %d clauses, kept %d clauses.\n"
1055 !derived_clauses !kept_clauses;
1057 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1062 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
1065 let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
1066 and set_sel v = symbols_ratio := v; symbols_counter := v;
1067 and set_conf f = configuration_file := f
1068 and set_lpo () = Utils.compare_terms := lpo
1069 and set_kbo () = Utils.compare_terms := nonrec_kbo
1070 and set_fullred () = use_fullred := true
1071 and set_time_limit v = time_limit := float_of_int v
1074 "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
1076 "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
1078 "-s", Arg.Int set_sel,
1079 "symbols-based selection ratio (relative to the weight ratio)";
1081 "-c", Arg.String set_conf, "Configuration file (for the db connection)";
1083 "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
1085 "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
1087 "-l", Arg.Int set_time_limit, "Time limit (in seconds)";
1088 ] (fun a -> ()) "Usage:"
1090 Helm_registry.load_from !configuration_file;