5 (* set to false to disable paramodulation inside auto_tac *)
6 let connect_to_auto = true;;
9 (* profiling statistics... *)
10 let infer_time = ref 0.;;
11 let forward_simpl_time = ref 0.;;
12 let forward_simpl_new_time = ref 0.;;
13 let backward_simpl_time = ref 0.;;
14 let passive_maintainance_time = ref 0.;;
16 (* limited-resource-strategy related globals *)
17 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
18 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
19 let start_time = ref 0.;; (* time at which the execution started *)
20 let elapsed_time = ref 0.;;
21 (* let maximal_weight = ref None;; *)
22 let maximal_retained_equality = ref None;;
24 (* equality-selection related globals *)
25 let use_fullred = ref true;;
26 let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *)
27 let weight_age_counter = ref !weight_age_ratio;;
28 let symbols_ratio = ref (* 0 *) 3;;
29 let symbols_counter = ref 0;;
31 (* non-recursive Knuth-Bendix term ordering by default *)
32 Utils.compare_terms := Utils.nonrec_kbo;;
35 let derived_clauses = ref 0;;
36 let kept_clauses = ref 0;;
38 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
43 | ParamodulationFailure
44 | ParamodulationSuccess of Inference.equality option * environment
49 let symbols_of_equality (_, (_, left, right), _, _) =
50 TermSet.union (symbols_of_term left) (symbols_of_term right)
54 let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
55 let m1 = symbols_of_term left in
60 let c = TermMap.find k res in
61 TermMap.add k (c+v) res
64 (symbols_of_term right) m1
66 (* Printf.printf "symbols_of_equality %s:\n" *)
67 (* (string_of_equality equality); *)
68 (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
69 (* print_newline (); *)
74 module OrderedEquality = struct
75 type t = Inference.equality
78 match meta_convertibility_eq eq1 eq2 with
81 let w1, _, (ty, left, right, _), _, a = eq1
82 and w2, _, (ty', left', right', _), _, a' = eq2 in
83 (* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
84 (* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
85 (* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
86 match Pervasives.compare w1 w2 with
88 let res = (List.length a) - (List.length a') in
89 if res <> 0 then res else (
91 let res = Pervasives.compare (List.hd a) (List.hd a') in
92 if res <> 0 then res else Pervasives.compare eq1 eq2
93 with Failure "hd" -> Pervasives.compare eq1 eq2
94 (* match a, a' with *)
95 (* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
96 (* let res = Pervasives.compare i j in *)
97 (* if res <> 0 then res else Pervasives.compare eq1 eq2 *)
98 (* | _, _ -> Pervasives.compare eq1 eq2 *)
103 module EqualitySet = Set.Make(OrderedEquality);;
106 let select env passive (active, _) =
107 processed_clauses := !processed_clauses + 1;
109 let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
111 List.filter (fun e -> e <> eq) l
113 if !weight_age_ratio > 0 then
114 weight_age_counter := !weight_age_counter - 1;
115 match !weight_age_counter with
117 weight_age_counter := !weight_age_ratio;
118 match neg_list, pos_list with
120 (* Negatives aren't indexed, no need to remove them... *)
122 ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
125 Indexing.remove_index passive_table hd
126 (* if !use_fullred then Indexing.remove_index passive_table hd *)
127 (* else passive_table *)
130 (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
131 | _, _ -> assert false
133 | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
134 symbols_counter := !symbols_counter - 1;
135 let cardinality map =
136 TermMap.fold (fun k v res -> res + v) map 0
139 | (Negative, e)::_ ->
140 let symbols = symbols_of_equality e in
141 let card = cardinality symbols in
142 let foldfun k v (r1, r2) =
143 if TermMap.mem k symbols then
144 let c = TermMap.find k symbols in
145 let c1 = abs (c - v) in
151 let f equality (i, e) =
153 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
155 let c = others + (abs (common - card)) in
156 if c < i then (c, equality)
157 (* else if c = i then *)
158 (* match OrderedEquality.compare equality e with *)
159 (* | -1 -> (c, equality) *)
160 (* | res -> (i, e) *)
163 let e1 = EqualitySet.min_elt pos_set in
166 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
168 (others + (abs (common - card))), e1
170 let _, current = EqualitySet.fold f pos_set initial in
171 (* Printf.printf "\nsymbols-based selection: %s\n\n" *)
172 (* (string_of_equality ~env current); *)
174 Indexing.remove_index passive_table current
175 (* if !use_fullred then Indexing.remove_index passive_table current *)
176 (* else passive_table *)
180 (remove current pos_list, EqualitySet.remove current pos_set),
183 let current = EqualitySet.min_elt pos_set in
185 Indexing.remove_index passive_table current
186 (* if !use_fullred then Indexing.remove_index passive_table current *)
187 (* else passive_table *)
191 (remove current pos_list, EqualitySet.remove current pos_set),
194 (Positive, current), passive
197 symbols_counter := !symbols_ratio;
198 let set_selection set = EqualitySet.min_elt set in
199 if EqualitySet.is_empty neg_set then
200 let current = set_selection pos_set in
203 (remove current pos_list, EqualitySet.remove current pos_set),
204 Indexing.remove_index passive_table current
205 (* if !use_fullred then Indexing.remove_index passive_table current *)
206 (* else passive_table *)
208 (Positive, current), passive
210 let current = set_selection neg_set in
212 (remove current neg_list, EqualitySet.remove current neg_set),
216 (Negative, current), passive
220 let make_passive neg pos =
221 let set_of equalities =
222 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
225 List.fold_left (fun tbl e -> Indexing.index tbl e)
226 (Indexing.empty_table ()) pos
227 (* if !use_fullred then *)
228 (* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
229 (* (Indexing.empty_table ()) pos *)
231 (* Indexing.empty_table () *)
240 [], Indexing.empty_table ()
244 let add_to_passive passive (new_neg, new_pos) =
245 let (neg_list, neg_set), (pos_list, pos_set), table = passive in
246 let ok set equality = not (EqualitySet.mem equality set) in
247 let neg = List.filter (ok neg_set) new_neg
248 and pos = List.filter (ok pos_set) new_pos in
250 List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
251 (* if !use_fullred then *)
252 (* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
256 let add set equalities =
257 List.fold_left (fun s e -> EqualitySet.add e s) set equalities
259 (neg @ neg_list, add neg_set neg),
260 (pos_list @ pos, add pos_set pos),
265 let passive_is_empty = function
266 | ([], _), ([], _), _ -> true
271 let size_of_passive ((_, ns), (_, ps), _) =
272 (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
276 let size_of_active (active_list, _) =
277 List.length active_list
281 let prune_passive howmany (active, _) passive =
282 let (nl, ns), (pl, ps), tbl = passive in
283 let howmany = float_of_int howmany
284 and ratio = float_of_int !weight_age_ratio in
287 int_of_float (if t -. v < 0.5 then t else v)
289 let in_weight = round (howmany *. ratio /. (ratio +. 1.))
290 and in_age = round (howmany /. (ratio +. 1.)) in
291 debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
294 | (Negative, e)::_ ->
295 let symbols = symbols_of_equality e in
296 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
300 let counter = ref !symbols_ratio in
301 let rec pickw w ns ps =
303 if not (EqualitySet.is_empty ns) then
304 let e = EqualitySet.min_elt ns in
305 let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
306 EqualitySet.add e ns', ps
307 else if !counter > 0 then
309 counter := !counter - 1;
310 if !counter = 0 then counter := !symbols_ratio
314 let e = EqualitySet.min_elt ps in
315 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
316 ns, EqualitySet.add e ps'
318 let foldfun k v (r1, r2) =
319 if TermMap.mem k symbols then
320 let c = TermMap.find k symbols in
321 let c1 = abs (c - v) in
327 let f equality (i, e) =
329 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
331 let c = others + (abs (common - card)) in
332 if c < i then (c, equality)
335 let e1 = EqualitySet.min_elt ps in
338 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
340 (others + (abs (common - card))), e1
342 let _, e = EqualitySet.fold f ps initial in
343 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
344 ns, EqualitySet.add e ps'
346 let e = EqualitySet.min_elt ps in
347 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
348 ns, EqualitySet.add e ps'
350 EqualitySet.empty, EqualitySet.empty
352 (* let in_weight, ns = pickw in_weight ns in *)
353 (* let _, ps = pickw in_weight ps in *)
354 let ns, ps = pickw in_weight ns ps in
355 let rec picka w s l =
359 | hd::tl when not (EqualitySet.mem hd s) ->
360 let w, s, l = picka (w-1) s tl in
361 w, EqualitySet.add hd s, hd::l
363 let w, s, l = picka w s tl in
368 let in_age, ns, nl = picka in_age ns nl in
369 let _, ps, pl = picka in_age ps pl in
370 if not (EqualitySet.is_empty ps) then
371 (* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
372 maximal_retained_equality := Some (EqualitySet.max_elt ps);
375 (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
376 (* if !use_fullred then *)
377 (* EqualitySet.fold *)
378 (* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
382 (nl, ns), (pl, ps), tbl
386 let infer env sign current (active_list, active_table) =
387 let new_neg, new_pos =
391 Indexing.superposition_left !maxmeta env active_table current in
396 Indexing.superposition_right !maxmeta env active_table current in
398 let rec infer_positive table = function
400 | (Negative, equality)::tl ->
402 Indexing.superposition_left !maxmeta env table equality in
404 let neg, pos = infer_positive table tl in
406 | (Positive, equality)::tl ->
408 Indexing.superposition_right !maxmeta env table equality in
410 let neg, pos = infer_positive table tl in
413 let curr_table = Indexing.index (Indexing.empty_table ()) current in
414 let neg, pos = infer_positive curr_table active_list in
417 derived_clauses := !derived_clauses + (List.length new_neg) +
418 (List.length new_pos);
419 match !maximal_retained_equality with
420 | None -> new_neg, new_pos
422 (* if we have a maximal_retained_equality, we can discard all equalities
423 "greater" than it, as they will never be reached... An equality is
424 greater than maximal_retained_equality if it is bigger
425 wrt. OrderedEquality.compare and it is less similar than
426 maximal_retained_equality to the current goal *)
428 match active_list with
429 | (Negative, e)::_ ->
430 let symbols = symbols_of_equality e in
431 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
438 List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
441 if OrderedEquality.compare e eq <= 0 then
444 let foldfun k v (r1, r2) =
445 if TermMap.mem k symbols then
446 let c = TermMap.find k symbols in
447 let c1 = abs (c - v) in
455 TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
456 others + (abs (common - card))
459 TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
460 let c = others + (abs (common - card)) in
461 if c < initial then true else false
463 List.filter filterfun new_pos
469 let contains_empty env (negative, positive) =
470 let metasenv, context, ugraph = env in
474 (fun (w, proof, (ty, left, right, ordering), m, a) ->
475 fst (CicReduction.are_convertible context left right ugraph))
484 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
485 let pl, passive_table =
488 | Some ((pn, _), (pp, _), pt) ->
489 let pn = List.map (fun e -> (Negative, e)) pn
490 and pp = List.map (fun e -> (Positive, e)) pp in
493 let all = if pl = [] then active_list else active_list @ pl in
495 (* let rec find_duplicate sign current = function *)
497 (* | (s, eq)::tl when s = sign -> *)
498 (* if meta_convertibility_eq current eq then true *)
499 (* else find_duplicate sign current tl *)
500 (* | _::tl -> find_duplicate sign current tl *)
504 (* if sign = Positive then *)
505 (* Indexing.subsumption env active_table current *)
513 let demodulate table current =
514 let newmeta, newcurrent =
515 Indexing.demodulation !maxmeta env table sign current in
517 if is_identity env newcurrent then
518 if sign = Negative then Some (sign, newcurrent)
521 Some (sign, newcurrent)
524 let res = demodulate active_table current in
527 | Some (sign, newcurrent) ->
528 match passive_table with
530 | Some passive_table -> demodulate passive_table newcurrent
534 | Some (Negative, c) ->
537 (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
540 if ok then res else None
541 | Some (Positive, c) ->
542 if Indexing.in_index active_table c then
545 match passive_table with
547 | Some passive_table ->
548 if Indexing.in_index passive_table c then None
551 (* | Some (s, c) -> if find_duplicate s c all then None else res *)
553 (* if s = Utils.Negative then *)
556 (* if Indexing.subsumption env active_table c then *)
559 (* match passive_table with *)
561 (* | Some passive_table -> *)
562 (* if Indexing.subsumption env passive_table c then *)
568 (* let pred (sign, eq) = *)
569 (* if sign <> s then false *)
570 (* else subsumption env c eq *)
572 (* if List.exists pred all then None *)
576 type fs_time_info_t = {
577 mutable build_all: float;
578 mutable demodulate: float;
579 mutable subsumption: float;
582 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
585 let forward_simplify_new env (new_neg, new_pos) ?passive active =
586 let t1 = Unix.gettimeofday () in
588 let active_list, active_table = active in
589 let pl, passive_table =
592 | Some ((pn, _), (pp, _), pt) ->
593 let pn = List.map (fun e -> (Negative, e)) pn
594 and pp = List.map (fun e -> (Positive, e)) pp in
597 let all = active_list @ pl in
599 let t2 = Unix.gettimeofday () in
600 fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
602 let demodulate sign table target =
603 let newmeta, newtarget =
604 Indexing.demodulation !maxmeta env table sign target in
608 (* let f sign' target (sign, eq) = *)
609 (* if sign <> sign' then false *)
610 (* else subsumption env target eq *)
613 let t1 = Unix.gettimeofday () in
615 let new_neg, new_pos =
616 let new_neg = List.map (demodulate Negative active_table) new_neg
617 and new_pos = List.map (demodulate Positive active_table) new_pos in
618 match passive_table with
619 | None -> new_neg, new_pos
620 | Some passive_table ->
621 List.map (demodulate Negative passive_table) new_neg,
622 List.map (demodulate Positive passive_table) new_pos
625 let t2 = Unix.gettimeofday () in
626 fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
631 if not (Inference.is_identity env e) then
632 if EqualitySet.mem e s then s
633 else EqualitySet.add e s
635 EqualitySet.empty new_pos
637 let new_pos = EqualitySet.elements new_pos_set in
640 match passive_table with
642 (fun e -> not (Indexing.subsumption env active_table e))
643 | Some passive_table ->
644 (fun e -> not ((Indexing.subsumption env active_table e) ||
645 (Indexing.subsumption env passive_table e)))
648 let t1 = Unix.gettimeofday () in
650 (* let new_neg, new_pos = *)
651 (* List.filter subs new_neg, *)
652 (* List.filter subs new_pos *)
655 (* let new_neg, new_pos = *)
656 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
657 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
660 let t2 = Unix.gettimeofday () in
661 fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
664 match passive_table with
666 (fun e -> not (Indexing.in_index active_table e))
667 | Some passive_table ->
669 not ((Indexing.in_index active_table e) ||
670 (Indexing.in_index passive_table e)))
672 new_neg, List.filter is_duplicate new_pos
674 (* new_neg, new_pos *)
677 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
678 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
684 let backward_simplify_active env new_pos new_table min_weight active =
685 let active_list, active_table = active in
686 let active_list, newa =
688 (fun (s, equality) (res, newn) ->
689 let ew, _, _, _, _ = equality in
690 if ew < min_weight then
691 (s, equality)::res, newn
693 match forward_simplify env (s, equality) (new_pos, new_table) with
703 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
707 (fun (s, eq) (res, tbl) ->
708 if List.mem (s, eq) res then
710 else if (is_identity env eq) || (find eq res) then (
712 ) (* else if (find eq res) then *)
715 (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
716 active_list ([], Indexing.empty_table ()),
718 (fun (s, eq) (n, p) ->
719 if (s <> Negative) && (is_identity env eq) then (
722 if s = Negative then eq::n, p
727 | [], [] -> active, None
728 | _ -> active, Some newa
732 let backward_simplify_passive env new_pos new_table min_weight passive =
733 let (nl, ns), (pl, ps), passive_table = passive in
734 let f sign equality (resl, ress, newn) =
735 let ew, _, _, _, _ = equality in
736 if ew < min_weight then
737 (* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *)
738 equality::resl, ress, newn
740 match forward_simplify env (sign, equality) (new_pos, new_table) with
741 | None -> resl, EqualitySet.remove equality ress, newn
744 equality::resl, ress, newn
746 let ress = EqualitySet.remove equality ress in
749 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
750 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
753 (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
755 match newn, newp with
756 | [], [] -> ((nl, ns), (pl, ps), passive_table), None
757 | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
761 let backward_simplify env new' ?passive active =
762 let new_pos, new_table, min_weight =
765 let ew, _, _, _, _ = e in
766 (Positive, e)::l, Indexing.index t e, min ew w)
767 ([], Indexing.empty_table (), 1000000) (snd new')
770 backward_simplify_active env new_pos new_table min_weight active in
773 active, (make_passive [] []), newa, None
776 backward_simplify_passive env new_pos new_table min_weight passive in
777 active, passive, newa, newp
781 let get_selection_estimate () =
782 elapsed_time := (Unix.gettimeofday ()) -. !start_time;
783 (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
785 ceil ((float_of_int !processed_clauses) *.
786 ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
790 let rec given_clause env passive active =
791 let time1 = Unix.gettimeofday () in
793 let selection_estimate = get_selection_estimate () in
794 let kept = size_of_passive passive in
796 if !time_limit = 0. || !processed_clauses = 0 then
798 else if !elapsed_time > !time_limit then (
799 debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
800 !time_limit !elapsed_time);
802 ) else if kept > selection_estimate then (
803 debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
804 "(kept: %d, selection_estimate: %d)\n")
805 kept selection_estimate);
806 prune_passive selection_estimate active passive
811 let time2 = Unix.gettimeofday () in
812 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
814 kept_clauses := (size_of_passive passive) + (size_of_active active);
816 match passive_is_empty passive with
817 | true -> ParamodulationFailure
819 let (sign, current), passive = select env passive active in
820 let time1 = Unix.gettimeofday () in
821 let res = forward_simplify env (sign, current) ~passive active in
822 let time2 = Unix.gettimeofday () in
823 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
826 given_clause env passive active
827 | Some (sign, current) ->
828 if (sign = Negative) && (is_identity env current) then (
829 debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
830 (string_of_equality ~env current));
831 ParamodulationSuccess (Some current, env)
833 debug_print "\n================================================";
834 debug_print (Printf.sprintf "selected: %s %s"
835 (string_of_sign sign)
836 (string_of_equality ~env current));
838 let t1 = Unix.gettimeofday () in
839 let new' = infer env sign current active in
840 let t2 = Unix.gettimeofday () in
841 infer_time := !infer_time +. (t2 -. t1);
843 let res, goal = contains_empty env new' in
845 ParamodulationSuccess (goal, env)
847 let t1 = Unix.gettimeofday () in
848 let new' = forward_simplify_new env new' (* ~passive *) active in
849 let t2 = Unix.gettimeofday () in
851 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
857 let t1 = Unix.gettimeofday () in
858 let active, _, newa, _ =
859 backward_simplify env ([], [current]) active
861 let t2 = Unix.gettimeofday () in
862 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
866 let al, tbl = active in
867 let nn = List.map (fun e -> Negative, e) n in
872 Indexing.index tbl e)
878 (* Printf.printf "active:\n%s\n" *)
879 (* (String.concat "\n" *)
881 (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
882 (* (string_of_equality ~env e)) (fst active)))); *)
883 (* print_newline (); *)
886 (* match new' with *)
888 (* Printf.printf "new':\n%s\n" *)
889 (* (String.concat "\n" *)
891 (* (fun e -> "Negative " ^ *)
892 (* (string_of_equality ~env e)) neg) @ *)
894 (* (fun e -> "Positive " ^ *)
895 (* (string_of_equality ~env e)) pos))); *)
896 (* print_newline (); *)
898 match contains_empty env new' with
901 let al, tbl = active in
903 | Negative -> (sign, current)::al, tbl
905 al @ [(sign, current)], Indexing.index tbl current
907 let passive = add_to_passive passive new' in
908 let (_, ns), (_, ps), _ = passive in
909 (* Printf.printf "passive:\n%s\n" *)
910 (* (String.concat "\n" *)
911 (* ((List.map (fun e -> "Negative " ^ *)
912 (* (string_of_equality ~env e)) *)
913 (* (EqualitySet.elements ns)) @ *)
914 (* (List.map (fun e -> "Positive " ^ *)
915 (* (string_of_equality ~env e)) *)
916 (* (EqualitySet.elements ps)))); *)
917 (* print_newline (); *)
918 given_clause env passive active
920 ParamodulationSuccess (goal, env)
925 let rec given_clause_fullred env passive active =
926 let time1 = Unix.gettimeofday () in
928 let selection_estimate = get_selection_estimate () in
929 let kept = size_of_passive passive in
931 if !time_limit = 0. || !processed_clauses = 0 then
933 else if !elapsed_time > !time_limit then (
934 debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
935 !time_limit !elapsed_time);
937 ) else if kept > selection_estimate then (
938 debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
939 "(kept: %d, selection_estimate: %d)\n")
940 kept selection_estimate);
941 prune_passive selection_estimate active passive
946 let time2 = Unix.gettimeofday () in
947 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
949 kept_clauses := (size_of_passive passive) + (size_of_active active);
951 match passive_is_empty passive with
952 | true -> ParamodulationFailure
954 let (sign, current), passive = select env passive active in
955 let time1 = Unix.gettimeofday () in
956 let res = forward_simplify env (sign, current) ~passive active in
957 let time2 = Unix.gettimeofday () in
958 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
961 given_clause_fullred env passive active
962 | Some (sign, current) ->
963 if (sign = Negative) && (is_identity env current) then (
964 debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
965 (string_of_equality ~env current));
966 ParamodulationSuccess (Some current, env)
968 debug_print "\n================================================";
969 debug_print (Printf.sprintf "selected: %s %s"
970 (string_of_sign sign)
971 (string_of_equality ~env current));
973 let t1 = Unix.gettimeofday () in
974 let new' = infer env sign current active in
975 let t2 = Unix.gettimeofday () in
976 infer_time := !infer_time +. (t2 -. t1);
979 if is_identity env current then active
981 let al, tbl = active in
983 | Negative -> (sign, current)::al, tbl
984 | Positive -> al @ [(sign, current)], Indexing.index tbl current
986 let rec simplify new' active passive =
987 let t1 = Unix.gettimeofday () in
988 let new' = forward_simplify_new env new' ~passive active in
989 let t2 = Unix.gettimeofday () in
990 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
991 let t1 = Unix.gettimeofday () in
992 let active, passive, newa, retained =
993 backward_simplify env new' ~passive active in
994 let t2 = Unix.gettimeofday () in
995 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
996 match newa, retained with
997 | None, None -> active, passive, new'
999 | None, Some (n, p) ->
1000 let nn, np = new' in
1001 simplify (nn @ n, np @ p) active passive
1002 | Some (n, p), Some (rn, rp) ->
1003 let nn, np = new' in
1004 simplify (nn @ n @ rn, np @ p @ rp) active passive
1006 let active, passive, new' = simplify new' active passive in
1008 let k = size_of_passive passive in
1009 if k < (kept - 1) then
1010 processed_clauses := !processed_clauses + (kept - 1 - k);
1014 Printf.sprintf "active:\n%s\n"
1017 (fun (s, e) -> (string_of_sign s) ^ " " ^
1018 (string_of_equality ~env e)) (fst active)))))
1024 Printf.sprintf "new':\n%s\n"
1027 (fun e -> "Negative " ^
1028 (string_of_equality ~env e)) neg) @
1030 (fun e -> "Positive " ^
1031 (string_of_equality ~env e)) pos))))
1033 match contains_empty env new' with
1035 let passive = add_to_passive passive new' in
1036 (* let (_, ns), (_, ps), _ = passive in *)
1037 (* Printf.printf "passive:\n%s\n" *)
1038 (* (String.concat "\n" *)
1039 (* ((List.map (fun e -> "Negative " ^ *)
1040 (* (string_of_equality ~env e)) *)
1041 (* (EqualitySet.elements ns)) @ *)
1042 (* (List.map (fun e -> "Positive " ^ *)
1043 (* (string_of_equality ~env e)) *)
1044 (* (EqualitySet.elements ps)))); *)
1045 (* print_newline (); *)
1046 given_clause_fullred env passive active
1048 ParamodulationSuccess (goal, env)
1053 let given_clause_ref = ref given_clause;;
1056 let main dbd term metasenv ugraph =
1057 let module C = Cic in
1058 let module T = CicTypeChecker in
1059 let module PET = ProofEngineTypes in
1060 let module PP = CicPp in
1061 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1062 let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1063 let proof, goals = status in
1064 let goal' = List.nth goals 0 in
1065 let _, metasenv, meta_proof, _ = proof in
1066 let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1067 let equalities, maxm = find_equalities context proof in
1068 let library_equalities, maxm =
1069 find_library_equalities ~dbd context (proof, goal') (maxm+2)
1071 maxmeta := maxm+2; (* TODO ugly!! *)
1072 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1073 let new_meta_goal, metasenv, type_of_goal =
1074 let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1075 Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
1077 Cic.Meta (maxm+1, irl),
1078 (maxm+1, context, ty)::metasenv,
1081 (* let new_meta_goal = Cic.Meta (goal', irl) in *)
1082 let env = (metasenv, context, ugraph) in
1084 let term_equality = equality_of_term new_meta_goal goal in
1085 let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
1086 if is_identity env term_equality then
1088 Cic.Appl [Cic.MutConstruct (* reflexivity *)
1089 (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
1093 Printf.printf "OK, found a proof!\n";
1094 let names = names_of_context context in
1095 print_endline (PP.pp proof names)
1100 let equalities = equalities @ library_equalities in
1102 Printf.sprintf "equalities:\n%s\n"
1104 (List.map string_of_equality equalities)));
1105 debug_print "SIMPLYFYING EQUALITIES...";
1106 let rec simpl e others others_simpl =
1107 let active = others @ others_simpl in
1110 (fun t (_, e) -> Indexing.index t e)
1111 (Indexing.empty_table ()) active
1113 let res = forward_simplify env e (active, tbl) in
1117 | None -> simpl hd tl others_simpl
1118 | Some e -> simpl hd tl (e::others_simpl)
1122 | None -> others_simpl
1123 | Some e -> e::others_simpl
1126 match equalities with
1129 let others = List.map (fun e -> (Positive, e)) tl in
1131 List.rev (List.map snd (simpl (Positive, hd) others []))
1134 Printf.sprintf "equalities AFTER:\n%s\n"
1136 (List.map string_of_equality res)));
1139 let active = make_active () in
1140 let passive = make_passive [term_equality] equalities in
1141 Printf.printf "\ncurrent goal: %s\n"
1142 (string_of_equality ~env term_equality);
1143 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1144 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1145 Printf.printf "\nequalities:\n%s\n"
1148 (string_of_equality ~env)
1149 (equalities @ library_equalities)));
1150 print_endline "--------------------------------------------------";
1151 let start = Unix.gettimeofday () in
1152 print_endline "GO!";
1153 start_time := Unix.gettimeofday ();
1155 (if !use_fullred then given_clause_fullred else given_clause)
1158 let finish = Unix.gettimeofday () in
1161 | ParamodulationFailure ->
1162 Printf.printf "NO proof found! :-(\n\n"
1163 | ParamodulationSuccess (Some goal, env) ->
1164 let proof = Inference.build_proof_term goal in
1167 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
1172 CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1174 Printf.printf "OK, found a proof!\n";
1175 (* REMEMBER: we have to instantiate meta_proof, we should use
1176 apply the "apply" tactic to proof and status
1178 let names = names_of_context context in
1179 print_endline (PP.pp proof names);
1180 (* print_endline (PP.ppterm proof); *)
1182 print_endline (string_of_float (finish -. start));
1184 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
1185 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1187 (fst (CicReduction.are_convertible
1188 context type_of_goal ty ug)));
1190 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
1191 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
1192 print_endline (string_of_float (finish -. start));
1196 | ParamodulationSuccess (None, env) ->
1197 Printf.printf "Success, but no proof?!?\n\n"
1199 Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1200 "forward_simpl_new_time: %.9f\n" ^^
1201 "backward_simpl_time: %.9f\n")
1202 !infer_time !forward_simpl_time !forward_simpl_new_time
1203 !backward_simpl_time;
1204 Printf.printf "passive_maintainance_time: %.9f\n"
1205 !passive_maintainance_time;
1206 Printf.printf " successful unification/matching time: %.9f\n"
1207 !Indexing.match_unif_time_ok;
1208 Printf.printf " failed unification/matching time: %.9f\n"
1209 !Indexing.match_unif_time_no;
1210 Printf.printf " indexing retrieval time: %.9f\n"
1211 !Indexing.indexing_retrieval_time;
1212 Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
1213 !Indexing.build_newtarget_time;
1214 Printf.printf "derived %d clauses, kept %d clauses.\n"
1215 !derived_clauses !kept_clauses;
1217 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1222 let saturate dbd (proof, goal) =
1223 let module C = Cic in
1226 let uri, metasenv, meta_proof, term_to_prove = proof in
1227 let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1228 let equalities, maxm = find_equalities context proof in
1229 let new_meta_goal, metasenv, type_of_goal =
1231 CicMkImplicit.identity_relocation_list_for_metavariable context in
1232 let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1233 debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty));
1234 Cic.Meta (maxm+1, irl),
1235 (maxm+1, context, ty)::metasenv,
1238 let ugraph = CicUniv.empty_ugraph in
1239 let env = (metasenv, context, ugraph) in
1241 let term_equality = equality_of_term new_meta_goal goal in
1243 if is_identity env term_equality then
1244 let w, _, (eq_ty, left, right, o), m, a = term_equality in
1246 Cic.Appl [Cic.MutConstruct (* reflexivity *)
1247 (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
1250 (ParamodulationSuccess
1251 (Some (0, Inference.BasicProof proof,
1252 (eq_ty, left, right, o), m, a), env), 0.)
1254 let library_equalities, maxm =
1255 find_library_equalities ~dbd context (proof, goal') (maxm+2)
1259 let equalities = equalities @ library_equalities in
1261 Printf.sprintf "equalities:\n%s\n"
1263 (List.map string_of_equality equalities)));
1264 debug_print "SIMPLYFYING EQUALITIES...";
1265 let rec simpl e others others_simpl =
1266 let active = others @ others_simpl in
1269 (fun t (_, e) -> Indexing.index t e)
1270 (Indexing.empty_table ()) active
1272 let res = forward_simplify env e (active, tbl) in
1276 | None -> simpl hd tl others_simpl
1277 | Some e -> simpl hd tl (e::others_simpl)
1281 | None -> others_simpl
1282 | Some e -> e::others_simpl
1285 match equalities with
1288 let others = List.map (fun e -> (Positive, e)) tl in
1290 List.rev (List.map snd (simpl (Positive, hd) others []))
1293 Printf.sprintf "equalities AFTER:\n%s\n"
1295 (List.map string_of_equality res)));
1298 let active = make_active () in
1299 let passive = make_passive [term_equality] equalities in
1300 let start = Unix.gettimeofday () in
1301 let res = given_clause_fullred env passive active in
1302 let finish = Unix.gettimeofday () in
1303 (res, finish -. start)
1306 | ParamodulationSuccess (Some goal, env) ->
1307 debug_print "OK, found a proof!";
1308 let proof = Inference.build_proof_term goal in
1309 let names = names_of_context context in
1312 match new_meta_goal with
1313 | C.Meta (i, _) -> i | _ -> assert false
1316 (* match meta_proof with *)
1317 (* | C.Meta (i, _) -> i *)
1319 (* Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *)
1320 (* (CicPp.pp meta_proof names) (string_of_int goal'); *)
1321 (* print_newline (); *)
1324 List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
1329 CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1331 debug_print (CicPp.pp proof [](* names *));
1334 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
1335 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1337 (fst (CicReduction.are_convertible
1338 context type_of_goal ty ug))));
1339 let equality_for_replace i t1 =
1341 | C.Meta (n, _) -> n = i
1345 ProofEngineReduction.replace
1346 ~equality:equality_for_replace
1347 ~what:[goal'] ~with_what:[proof]
1351 Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
1352 (match uri with Some uri -> UriManager.string_of_uri uri
1354 (print_metasenv newmetasenv)
1355 (CicPp.pp real_proof [](* names *))
1356 (CicPp.pp term_to_prove names));
1357 ((uri, newmetasenv, real_proof, term_to_prove), [])
1358 with CicTypeChecker.TypeCheckerFailure _ ->
1359 debug_print "THE PROOF DOESN'T TYPECHECK!!!";
1360 debug_print (CicPp.pp proof names);
1361 raise (ProofEngineTypes.Fail
1362 "Found a proof, but it doesn't typecheck")
1364 debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time);
1367 raise (ProofEngineTypes.Fail "NO proof found")
1369 (* raise (Failure "saturation failed") *)
1373 (* dummy function called within matita to trigger linkage *)
1377 (* UGLY SIDE EFFECT... *)
1378 if connect_to_auto then (
1379 AutoTactic.paramodulation_tactic := saturate;
1380 AutoTactic.term_is_equality := Inference.term_is_equality;