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 3;; (* settable by the user from the command line *)
27 let weight_age_counter = ref !weight_age_ratio;;
28 let symbols_ratio = ref 2;;
29 let symbols_counter = ref 0;;
32 let derived_clauses = ref 0;;
33 let kept_clauses = ref 0;;
35 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
40 | ParamodulationFailure
41 | ParamodulationSuccess of Inference.equality option * environment
46 let symbols_of_equality (_, (_, left, right), _, _) =
47 TermSet.union (symbols_of_term left) (symbols_of_term right)
51 let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
52 let m1 = symbols_of_term left in
57 let c = TermMap.find k res in
58 TermMap.add k (c+v) res
61 (symbols_of_term right) m1
63 (* Printf.printf "symbols_of_equality %s:\n" *)
64 (* (string_of_equality equality); *)
65 (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
66 (* print_newline (); *)
71 module OrderedEquality = struct
72 type t = Inference.equality
75 match meta_convertibility_eq eq1 eq2 with
78 let w1, _, (ty, left, right, _), _, a = eq1
79 and w2, _, (ty', left', right', _), _, a' = 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 match Pervasives.compare w1 w2 with
85 let res = (List.length a) - (List.length a') in
86 if res <> 0 then res else (
88 let res = Pervasives.compare (List.hd a) (List.hd a') in
89 if res <> 0 then res else Pervasives.compare eq1 eq2
90 with Failure "hd" -> Pervasives.compare eq1 eq2
91 (* match a, a' with *)
92 (* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
93 (* let res = Pervasives.compare i j in *)
94 (* if res <> 0 then res else Pervasives.compare eq1 eq2 *)
95 (* | _, _ -> Pervasives.compare eq1 eq2 *)
100 module EqualitySet = Set.Make(OrderedEquality);;
103 let select env passive (active, _) =
104 processed_clauses := !processed_clauses + 1;
106 let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
108 List.filter (fun e -> e <> eq) l
110 if !weight_age_ratio > 0 then
111 weight_age_counter := !weight_age_counter - 1;
112 match !weight_age_counter with
114 weight_age_counter := !weight_age_ratio;
115 match neg_list, pos_list with
117 (* Negatives aren't indexed, no need to remove them... *)
119 ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
122 Indexing.remove_index passive_table hd
123 (* if !use_fullred then Indexing.remove_index passive_table hd *)
124 (* else passive_table *)
127 (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
128 | _, _ -> assert false
130 | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
131 symbols_counter := !symbols_counter - 1;
132 let cardinality map =
133 TermMap.fold (fun k v res -> res + v) map 0
136 | (Negative, e)::_ ->
137 let symbols = symbols_of_equality e in
138 let card = cardinality symbols in
139 let foldfun k v (r1, r2) =
140 if TermMap.mem k symbols then
141 let c = TermMap.find k symbols in
142 let c1 = abs (c - v) in
148 let f equality (i, e) =
150 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
152 let c = others + (abs (common - card)) in
153 if c < i then (c, equality)
154 (* else if c = i then *)
155 (* match OrderedEquality.compare equality e with *)
156 (* | -1 -> (c, equality) *)
157 (* | res -> (i, e) *)
160 let e1 = EqualitySet.min_elt pos_set in
163 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
165 (others + (abs (common - card))), e1
167 let _, current = EqualitySet.fold f pos_set initial in
168 (* Printf.printf "\nsymbols-based selection: %s\n\n" *)
169 (* (string_of_equality ~env current); *)
171 Indexing.remove_index passive_table current
172 (* if !use_fullred then Indexing.remove_index passive_table current *)
173 (* else passive_table *)
177 (remove current pos_list, EqualitySet.remove current pos_set),
180 let current = EqualitySet.min_elt pos_set in
182 Indexing.remove_index passive_table current
183 (* if !use_fullred then Indexing.remove_index passive_table current *)
184 (* else passive_table *)
188 (remove current pos_list, EqualitySet.remove current pos_set),
191 (Positive, current), passive
194 symbols_counter := !symbols_ratio;
195 let set_selection set = EqualitySet.min_elt set in
196 if EqualitySet.is_empty neg_set then
197 let current = set_selection pos_set in
200 (remove current pos_list, EqualitySet.remove current pos_set),
201 Indexing.remove_index passive_table current
202 (* if !use_fullred then Indexing.remove_index passive_table current *)
203 (* else passive_table *)
205 (Positive, current), passive
207 let current = set_selection neg_set in
209 (remove current neg_list, EqualitySet.remove current neg_set),
213 (Negative, current), passive
217 let make_passive neg pos =
218 let set_of equalities =
219 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
222 List.fold_left (fun tbl e -> Indexing.index tbl e)
223 (Indexing.empty_table ()) pos
224 (* if !use_fullred then *)
225 (* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
226 (* (Indexing.empty_table ()) pos *)
228 (* Indexing.empty_table () *)
237 [], Indexing.empty_table ()
241 let add_to_passive passive (new_neg, new_pos) =
242 let (neg_list, neg_set), (pos_list, pos_set), table = passive in
243 let ok set equality = not (EqualitySet.mem equality set) in
244 let neg = List.filter (ok neg_set) new_neg
245 and pos = List.filter (ok pos_set) new_pos in
247 List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
248 (* if !use_fullred then *)
249 (* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
253 let add set equalities =
254 List.fold_left (fun s e -> EqualitySet.add e s) set equalities
256 (neg @ neg_list, add neg_set neg),
257 (pos_list @ pos, add pos_set pos),
262 let passive_is_empty = function
263 | ([], _), ([], _), _ -> true
268 let size_of_passive ((_, ns), (_, ps), _) =
269 (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
273 let size_of_active (active_list, _) =
274 List.length active_list
278 let prune_passive howmany (active, _) passive =
279 let (nl, ns), (pl, ps), tbl = passive in
280 let howmany = float_of_int howmany
281 and ratio = float_of_int !weight_age_ratio in
282 let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
283 and in_age = int_of_float (howmany /. (ratio +. 1.)) in
284 debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
287 | (Negative, e)::_ ->
288 let symbols = symbols_of_equality e in
289 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
293 let counter = ref !symbols_ratio in
294 let rec pickw w ns ps =
296 if not (EqualitySet.is_empty ns) then
297 let e = EqualitySet.min_elt ns in
298 let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
299 EqualitySet.add e ns', ps
300 else if !counter > 0 then
302 counter := !counter - 1;
303 if !counter = 0 then counter := !symbols_ratio
307 let e = EqualitySet.min_elt ps in
308 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
309 ns, EqualitySet.add e ps'
311 let foldfun k v (r1, r2) =
312 if TermMap.mem k symbols then
313 let c = TermMap.find k symbols in
314 let c1 = abs (c - v) in
320 let f equality (i, e) =
322 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
324 let c = others + (abs (common - card)) in
325 if c < i then (c, equality)
328 let e1 = EqualitySet.min_elt ps in
331 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
333 (others + (abs (common - card))), e1
335 let _, e = EqualitySet.fold f ps initial in
336 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
337 ns, EqualitySet.add e ps'
339 let e = EqualitySet.min_elt ps in
340 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
341 ns, EqualitySet.add e ps'
343 EqualitySet.empty, EqualitySet.empty
345 (* let in_weight, ns = pickw in_weight ns in *)
346 (* let _, ps = pickw in_weight ps in *)
347 let ns, ps = pickw in_weight ns ps in
348 let rec picka w s l =
352 | hd::tl when not (EqualitySet.mem hd s) ->
353 let w, s, l = picka (w-1) s tl in
354 w, EqualitySet.add hd s, hd::l
356 let w, s, l = picka w s tl in
361 let in_age, ns, nl = picka in_age ns nl in
362 let _, ps, pl = picka in_age ps pl in
363 if not (EqualitySet.is_empty ps) then
364 (* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
365 maximal_retained_equality := Some (EqualitySet.max_elt ps);
368 (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
369 (* if !use_fullred then *)
370 (* EqualitySet.fold *)
371 (* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
375 (nl, ns), (pl, ps), tbl
379 let infer env sign current (active_list, active_table) =
380 let new_neg, new_pos =
384 Indexing.superposition_left !maxmeta env active_table current in
389 Indexing.superposition_right !maxmeta env active_table current in
391 let rec infer_positive table = function
393 | (Negative, equality)::tl ->
395 Indexing.superposition_left !maxmeta env table equality in
397 let neg, pos = infer_positive table tl in
399 | (Positive, equality)::tl ->
401 Indexing.superposition_right !maxmeta env table equality in
403 let neg, pos = infer_positive table tl in
406 let curr_table = Indexing.index (Indexing.empty_table ()) current in
407 let neg, pos = infer_positive curr_table active_list in
410 derived_clauses := !derived_clauses + (List.length new_neg) +
411 (List.length new_pos);
412 match (* !maximal_weight *)!maximal_retained_equality with
413 | None -> new_neg, new_pos
416 List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
421 let contains_empty env (negative, positive) =
422 let metasenv, context, ugraph = env in
426 (fun (w, proof, (ty, left, right, ordering), m, a) ->
427 fst (CicReduction.are_convertible context left right ugraph))
436 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
437 let pl, passive_table =
440 | Some ((pn, _), (pp, _), pt) ->
441 let pn = List.map (fun e -> (Negative, e)) pn
442 and pp = List.map (fun e -> (Positive, e)) pp in
445 let all = if pl = [] then active_list else active_list @ pl in
447 (* let rec find_duplicate sign current = function *)
449 (* | (s, eq)::tl when s = sign -> *)
450 (* if meta_convertibility_eq current eq then true *)
451 (* else find_duplicate sign current tl *)
452 (* | _::tl -> find_duplicate sign current tl *)
456 (* if sign = Positive then *)
457 (* Indexing.subsumption env active_table current *)
465 let demodulate table current =
466 let newmeta, newcurrent =
467 Indexing.demodulation !maxmeta env table sign current in
469 if is_identity env newcurrent then
470 if sign = Negative then Some (sign, newcurrent)
473 Some (sign, newcurrent)
476 let res = demodulate active_table current in
479 | Some (sign, newcurrent) ->
480 match passive_table with
482 | Some passive_table -> demodulate passive_table newcurrent
486 | Some (Negative, c) ->
489 (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
492 if ok then res else None
493 | Some (Positive, c) ->
494 if Indexing.in_index active_table c then
497 match passive_table with
499 | Some passive_table ->
500 if Indexing.in_index passive_table c then None
503 (* | Some (s, c) -> if find_duplicate s c all then None else res *)
505 (* if s = Utils.Negative then *)
508 (* if Indexing.subsumption env active_table c then *)
511 (* match passive_table with *)
513 (* | Some passive_table -> *)
514 (* if Indexing.subsumption env passive_table c then *)
520 (* let pred (sign, eq) = *)
521 (* if sign <> s then false *)
522 (* else subsumption env c eq *)
524 (* if List.exists pred all then None *)
528 type fs_time_info_t = {
529 mutable build_all: float;
530 mutable demodulate: float;
531 mutable subsumption: float;
534 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
537 let forward_simplify_new env (new_neg, new_pos) ?passive active =
538 let t1 = Unix.gettimeofday () in
540 let active_list, active_table = active in
541 let pl, passive_table =
544 | Some ((pn, _), (pp, _), pt) ->
545 let pn = List.map (fun e -> (Negative, e)) pn
546 and pp = List.map (fun e -> (Positive, e)) pp in
549 let all = active_list @ pl in
551 let t2 = Unix.gettimeofday () in
552 fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
554 let demodulate sign table target =
555 let newmeta, newtarget =
556 Indexing.demodulation !maxmeta env table sign target in
560 (* let f sign' target (sign, eq) = *)
561 (* if sign <> sign' then false *)
562 (* else subsumption env target eq *)
565 let t1 = Unix.gettimeofday () in
567 let new_neg, new_pos =
568 let new_neg = List.map (demodulate Negative active_table) new_neg
569 and new_pos = List.map (demodulate Positive active_table) new_pos in
570 match passive_table with
571 | None -> new_neg, new_pos
572 | Some passive_table ->
573 List.map (demodulate Negative passive_table) new_neg,
574 List.map (demodulate Positive passive_table) new_pos
577 let t2 = Unix.gettimeofday () in
578 fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
583 if not (Inference.is_identity env e) then
584 if EqualitySet.mem e s then s
585 else EqualitySet.add e s
587 EqualitySet.empty new_pos
589 let new_pos = EqualitySet.elements new_pos_set in
592 match passive_table with
594 (fun e -> not (Indexing.subsumption env active_table e))
595 | Some passive_table ->
596 (fun e -> not ((Indexing.subsumption env active_table e) ||
597 (Indexing.subsumption env passive_table e)))
600 let t1 = Unix.gettimeofday () in
602 (* let new_neg, new_pos = *)
603 (* List.filter subs new_neg, *)
604 (* List.filter subs new_pos *)
607 (* let new_neg, new_pos = *)
608 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
609 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
612 let t2 = Unix.gettimeofday () in
613 fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
616 match passive_table with
618 (fun e -> not (Indexing.in_index active_table e))
619 | Some passive_table ->
621 not ((Indexing.in_index active_table e) ||
622 (Indexing.in_index passive_table e)))
624 new_neg, List.filter is_duplicate new_pos
626 (* new_neg, new_pos *)
629 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
630 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
636 let backward_simplify_active env new_pos new_table active =
637 let active_list, active_table = active in
638 let active_list, newa =
640 (fun (s, equality) (res, newn) ->
641 match forward_simplify env (s, equality) (new_pos, new_table) with
651 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
655 (fun (s, eq) (res, tbl) ->
656 if List.mem (s, eq) res then
658 else if (is_identity env eq) || (find eq res) then (
660 ) (* else if (find eq res) then *)
663 (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
664 active_list ([], Indexing.empty_table ()),
666 (fun (s, eq) (n, p) ->
667 if (s <> Negative) && (is_identity env eq) then (
670 if s = Negative then eq::n, p
675 | [], [] -> active, None
676 | _ -> active, Some newa
680 let backward_simplify_passive env new_pos new_table passive =
681 let (nl, ns), (pl, ps), passive_table = passive in
682 let f sign equality (resl, ress, newn) =
683 match forward_simplify env (sign, equality) (new_pos, new_table) with
684 | None -> resl, EqualitySet.remove equality ress, newn
687 equality::resl, ress, newn
689 let ress = EqualitySet.remove equality ress in
692 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
693 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
696 (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
698 match newn, newp with
699 | [], [] -> ((nl, ns), (pl, ps), passive_table), None
700 | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
704 let backward_simplify env new' ?passive active =
705 let new_pos, new_table =
707 (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
708 ([], Indexing.empty_table ()) (snd new')
710 let active, newa = backward_simplify_active env new_pos new_table active in
713 active, (make_passive [] []), newa, None
716 backward_simplify_passive env new_pos new_table passive in
717 active, passive, newa, newp
721 let get_selection_estimate () =
722 elapsed_time := (Unix.gettimeofday ()) -. !start_time;
723 (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
725 ceil ((float_of_int !processed_clauses) *.
726 ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
730 let rec given_clause env passive active =
731 let time1 = Unix.gettimeofday () in
733 let selection_estimate = get_selection_estimate () in
734 let kept = size_of_passive passive in
736 if !time_limit = 0. || !processed_clauses = 0 then
738 else if !elapsed_time > !time_limit then (
739 debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
740 !time_limit !elapsed_time);
742 ) else if kept > selection_estimate then (
743 debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
744 "(kept: %d, selection_estimate: %d)\n")
745 kept selection_estimate);
746 prune_passive selection_estimate active passive
751 let time2 = Unix.gettimeofday () in
752 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
754 kept_clauses := (size_of_passive passive) + (size_of_active active);
756 match passive_is_empty passive with
757 | true -> ParamodulationFailure
759 let (sign, current), passive = select env passive active in
760 let time1 = Unix.gettimeofday () in
761 let res = forward_simplify env (sign, current) ~passive active in
762 let time2 = Unix.gettimeofday () in
763 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
766 given_clause env passive active
767 | Some (sign, current) ->
768 if (sign = Negative) && (is_identity env current) then (
769 debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
770 (string_of_equality ~env current));
771 ParamodulationSuccess (Some current, env)
773 debug_print "\n================================================";
774 debug_print (Printf.sprintf "selected: %s %s"
775 (string_of_sign sign)
776 (string_of_equality ~env current));
778 let t1 = Unix.gettimeofday () in
779 let new' = infer env sign current active in
780 let t2 = Unix.gettimeofday () in
781 infer_time := !infer_time +. (t2 -. t1);
783 let res, goal = contains_empty env new' in
785 ParamodulationSuccess (goal, env)
787 let t1 = Unix.gettimeofday () in
788 let new' = forward_simplify_new env new' (* ~passive *) active in
789 let t2 = Unix.gettimeofday () in
791 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
797 let t1 = Unix.gettimeofday () in
798 let active, _, newa, _ =
799 backward_simplify env ([], [current]) active
801 let t2 = Unix.gettimeofday () in
802 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
806 let al, tbl = active in
807 let nn = List.map (fun e -> Negative, e) n in
812 Indexing.index tbl e)
818 (* Printf.printf "active:\n%s\n" *)
819 (* (String.concat "\n" *)
821 (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
822 (* (string_of_equality ~env e)) (fst active)))); *)
823 (* print_newline (); *)
826 (* match new' with *)
828 (* Printf.printf "new':\n%s\n" *)
829 (* (String.concat "\n" *)
831 (* (fun e -> "Negative " ^ *)
832 (* (string_of_equality ~env e)) neg) @ *)
834 (* (fun e -> "Positive " ^ *)
835 (* (string_of_equality ~env e)) pos))); *)
836 (* print_newline (); *)
838 match contains_empty env new' with
841 let al, tbl = active in
843 | Negative -> (sign, current)::al, tbl
845 al @ [(sign, current)], Indexing.index tbl current
847 let passive = add_to_passive passive new' in
848 let (_, ns), (_, ps), _ = passive in
849 (* Printf.printf "passive:\n%s\n" *)
850 (* (String.concat "\n" *)
851 (* ((List.map (fun e -> "Negative " ^ *)
852 (* (string_of_equality ~env e)) *)
853 (* (EqualitySet.elements ns)) @ *)
854 (* (List.map (fun e -> "Positive " ^ *)
855 (* (string_of_equality ~env e)) *)
856 (* (EqualitySet.elements ps)))); *)
857 (* print_newline (); *)
858 given_clause env passive active
860 ParamodulationSuccess (goal, env)
865 let rec given_clause_fullred env passive active =
866 let time1 = Unix.gettimeofday () in
868 let selection_estimate = get_selection_estimate () in
869 let kept = size_of_passive passive in
871 if !time_limit = 0. || !processed_clauses = 0 then
873 else if !elapsed_time > !time_limit then (
874 debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
875 !time_limit !elapsed_time);
877 ) else if kept > selection_estimate then (
878 debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
879 "(kept: %d, selection_estimate: %d)\n")
880 kept selection_estimate);
881 prune_passive selection_estimate active passive
886 let time2 = Unix.gettimeofday () in
887 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
889 kept_clauses := (size_of_passive passive) + (size_of_active active);
891 match passive_is_empty passive with
892 | true -> ParamodulationFailure
894 let (sign, current), passive = select env passive active in
895 let time1 = Unix.gettimeofday () in
896 let res = forward_simplify env (sign, current) ~passive active in
897 let time2 = Unix.gettimeofday () in
898 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
901 given_clause_fullred env passive active
902 | Some (sign, current) ->
903 if (sign = Negative) && (is_identity env current) then (
904 debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
905 (string_of_equality ~env current));
906 ParamodulationSuccess (Some current, env)
908 debug_print "\n================================================";
909 debug_print (Printf.sprintf "selected: %s %s"
910 (string_of_sign sign)
911 (string_of_equality ~env current));
913 let t1 = Unix.gettimeofday () in
914 let new' = infer env sign current active in
915 let t2 = Unix.gettimeofday () in
916 infer_time := !infer_time +. (t2 -. t1);
919 if is_identity env current then active
921 let al, tbl = active in
923 | Negative -> (sign, current)::al, tbl
924 | Positive -> al @ [(sign, current)], Indexing.index tbl current
926 let rec simplify new' active passive =
927 let t1 = Unix.gettimeofday () in
928 let new' = forward_simplify_new env new' ~passive active in
929 let t2 = Unix.gettimeofday () in
930 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
931 let t1 = Unix.gettimeofday () in
932 let active, passive, newa, retained =
933 backward_simplify env new' ~passive active in
934 let t2 = Unix.gettimeofday () in
935 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
936 match newa, retained with
937 | None, None -> active, passive, new'
939 | None, Some (n, p) ->
941 simplify (nn @ n, np @ p) active passive
942 | Some (n, p), Some (rn, rp) ->
944 simplify (nn @ n @ rn, np @ p @ rp) active passive
946 let active, passive, new' = simplify new' active passive in
948 let k = size_of_passive passive in
949 if k < (kept - 1) then
950 processed_clauses := !processed_clauses + (kept - 1 - k);
954 Printf.sprintf "active:\n%s\n"
957 (fun (s, e) -> (string_of_sign s) ^ " " ^
958 (string_of_equality ~env e)) (fst active)))))
964 Printf.sprintf "new':\n%s\n"
967 (fun e -> "Negative " ^
968 (string_of_equality ~env e)) neg) @
970 (fun e -> "Positive " ^
971 (string_of_equality ~env e)) pos))))
973 match contains_empty env new' with
975 let passive = add_to_passive passive new' in
976 (* let (_, ns), (_, ps), _ = passive in *)
977 (* Printf.printf "passive:\n%s\n" *)
978 (* (String.concat "\n" *)
979 (* ((List.map (fun e -> "Negative " ^ *)
980 (* (string_of_equality ~env e)) *)
981 (* (EqualitySet.elements ns)) @ *)
982 (* (List.map (fun e -> "Positive " ^ *)
983 (* (string_of_equality ~env e)) *)
984 (* (EqualitySet.elements ps)))); *)
985 (* print_newline (); *)
986 given_clause_fullred env passive active
988 ParamodulationSuccess (goal, env)
993 let given_clause_ref = ref given_clause;;
996 let main dbd term metasenv ugraph =
997 let module C = Cic in
998 let module T = CicTypeChecker in
999 let module PET = ProofEngineTypes in
1000 let module PP = CicPp in
1001 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1002 let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1003 let proof, goals = status in
1004 let goal' = List.nth goals 0 in
1005 let _, metasenv, meta_proof, _ = proof in
1006 let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1007 let equalities, maxm = find_equalities context proof in
1008 (* let library_equalities, maxm = *)
1009 (* find_library_equalities ~dbd context (proof, goal') (maxm+1) *)
1011 maxmeta := maxm+2; (* TODO ugly!! *)
1012 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1013 let new_meta_goal, metasenv, type_of_goal =
1014 let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1015 Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
1017 Cic.Meta (maxm+1, irl),
1018 (maxm+1, context, ty)::metasenv,
1021 (* let new_meta_goal = Cic.Meta (goal', irl) in *)
1022 let env = (metasenv, context, ugraph) in
1024 let term_equality = equality_of_term new_meta_goal goal in
1025 let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
1026 let active = make_active () in
1028 make_passive [term_equality] (equalities (* @ library_equalities *))
1030 Printf.printf "\ncurrent goal: %s\n"
1031 (string_of_equality ~env term_equality);
1032 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1033 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1034 Printf.printf "\nequalities:\n%s\n"
1037 (string_of_equality ~env)
1039 print_endline "--------------------------------------------------";
1040 let start = Unix.gettimeofday () in
1041 print_endline "GO!";
1042 start_time := Unix.gettimeofday ();
1044 (if !use_fullred then given_clause_fullred else given_clause)
1047 let finish = Unix.gettimeofday () in
1050 | ParamodulationFailure ->
1051 Printf.printf "NO proof found! :-(\n\n"
1052 | ParamodulationSuccess (Some goal, env) ->
1053 let proof = Inference.build_proof_term goal in
1056 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
1061 CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1063 Printf.printf "OK, found a proof!\n";
1064 (* REMEMBER: we have to instantiate meta_proof, we should use
1065 apply the "apply" tactic to proof and status
1067 let names = names_of_context context in
1068 print_endline (PP.pp proof names);
1069 (* print_endline (PP.ppterm proof); *)
1071 print_endline (string_of_float (finish -. start));
1073 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
1074 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1076 (fst (CicReduction.are_convertible
1077 context type_of_goal ty ug)));
1079 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
1080 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
1084 | ParamodulationSuccess (None, env) ->
1085 Printf.printf "Success, but no proof?!?\n\n"
1087 Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1088 "forward_simpl_new_time: %.9f\n" ^^
1089 "backward_simpl_time: %.9f\n")
1090 !infer_time !forward_simpl_time !forward_simpl_new_time
1091 !backward_simpl_time;
1092 Printf.printf "passive_maintainance_time: %.9f\n"
1093 !passive_maintainance_time;
1094 Printf.printf " successful unification/matching time: %.9f\n"
1095 !Indexing.match_unif_time_ok;
1096 Printf.printf " failed unification/matching time: %.9f\n"
1097 !Indexing.match_unif_time_no;
1098 Printf.printf " indexing retrieval time: %.9f\n"
1099 !Indexing.indexing_retrieval_time;
1100 Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
1101 !Indexing.build_newtarget_time;
1102 Printf.printf "derived %d clauses, kept %d clauses.\n"
1103 !derived_clauses !kept_clauses;
1105 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1110 let saturate dbd (proof, goal) =
1111 let module C = Cic in
1114 let uri, metasenv, meta_proof, term_to_prove = proof in
1115 let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1116 let equalities, maxm = find_equalities context proof in
1117 let library_equalities, maxm =
1118 find_library_equalities ~dbd context (proof, goal') (maxm+2)
1121 let new_meta_goal, metasenv, type_of_goal =
1123 CicMkImplicit.identity_relocation_list_for_metavariable context in
1124 let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1125 debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty));
1126 Cic.Meta (maxm+1, irl),
1127 (maxm+1, context, ty)::metasenv,
1130 let ugraph = CicUniv.empty_ugraph in
1131 let env = (metasenv, context, ugraph) in
1133 let term_equality = equality_of_term new_meta_goal goal in
1134 let active = make_active () in
1136 make_passive [term_equality] (equalities @ library_equalities)
1138 let res = given_clause_fullred env passive active in
1140 | ParamodulationSuccess (Some goal, env) ->
1141 debug_print "OK, found a proof!";
1142 let proof = Inference.build_proof_term goal in
1143 let names = names_of_context context in
1146 match new_meta_goal with
1147 | C.Meta (i, _) -> i | _ -> assert false
1150 (* match meta_proof with *)
1151 (* | C.Meta (i, _) -> i *)
1153 (* Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *)
1154 (* (CicPp.pp meta_proof names) (string_of_int goal'); *)
1155 (* print_newline (); *)
1158 List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
1163 CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1165 debug_print (CicPp.pp proof [](* names *));
1168 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
1169 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1171 (fst (CicReduction.are_convertible
1172 context type_of_goal ty ug))));
1173 let equality_for_replace i t1 =
1175 | C.Meta (n, _) -> n = i
1179 ProofEngineReduction.replace
1180 ~equality:equality_for_replace
1181 ~what:[goal'] ~with_what:[proof]
1185 Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
1186 (match uri with Some uri -> UriManager.string_of_uri uri
1188 (print_metasenv newmetasenv)
1189 (CicPp.pp real_proof [](* names *))
1190 (CicPp.pp term_to_prove names));
1191 ((uri, newmetasenv, real_proof, term_to_prove), [])
1192 with CicTypeChecker.TypeCheckerFailure _ ->
1193 debug_print "THE PROOF DOESN'T TYPECHECK!!!";
1194 debug_print (CicPp.pp proof names);
1196 (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck")
1200 raise (ProofEngineTypes.Fail "NO proof found")
1202 (* raise (Failure "saturation failed") *)
1206 (* dummy function called within matita to trigger linkage *)
1210 (* UGLY SIDE EFFECT... *)
1211 if connect_to_auto then (
1212 AutoTactic.paramodulation_tactic := saturate;
1213 AutoTactic.term_is_equality := Inference.term_is_equality;