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! *)
41 (* varbiables controlling the search-space *)
42 let maxdepth = ref 3;;
43 let maxwidth = ref 3;;
47 | ParamodulationFailure
48 | ParamodulationSuccess of Inference.proof option * environment
51 type goal = proof * Cic.metasenv * Cic.term;;
53 type theorem = Cic.term * Cic.term * Cic.metasenv;;
57 let symbols_of_equality (_, (_, left, right), _, _) =
58 TermSet.union (symbols_of_term left) (symbols_of_term right)
62 let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
63 let m1 = symbols_of_term left in
68 let c = TermMap.find k res in
69 TermMap.add k (c+v) res
72 (symbols_of_term right) m1
74 (* Printf.printf "symbols_of_equality %s:\n" *)
75 (* (string_of_equality equality); *)
76 (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
77 (* print_newline (); *)
82 module OrderedEquality = struct
83 type t = Inference.equality
86 match meta_convertibility_eq eq1 eq2 with
89 let w1, _, (ty, left, right, _), _, a = eq1
90 and w2, _, (ty', left', right', _), _, a' = eq2 in
91 (* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
92 (* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
93 (* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
94 match Pervasives.compare w1 w2 with
96 let res = (List.length a) - (List.length a') in
97 if res <> 0 then res else (
99 let res = Pervasives.compare (List.hd a) (List.hd a') in
100 if res <> 0 then res else Pervasives.compare eq1 eq2
101 with Failure "hd" -> Pervasives.compare eq1 eq2
102 (* match a, a' with *)
103 (* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
104 (* let res = Pervasives.compare i j in *)
105 (* if res <> 0 then res else Pervasives.compare eq1 eq2 *)
106 (* | _, _ -> Pervasives.compare eq1 eq2 *)
111 module EqualitySet = Set.Make(OrderedEquality);;
114 let select env goals passive (active, _) =
115 processed_clauses := !processed_clauses + 1;
118 match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
121 let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
123 List.filter (fun e -> e <> eq) l
125 if !weight_age_ratio > 0 then
126 weight_age_counter := !weight_age_counter - 1;
127 match !weight_age_counter with
129 weight_age_counter := !weight_age_ratio;
130 match neg_list, pos_list with
132 (* Negatives aren't indexed, no need to remove them... *)
134 ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
137 Indexing.remove_index passive_table hd
138 (* if !use_fullred then Indexing.remove_index passive_table hd *)
139 (* else passive_table *)
142 (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
143 | _, _ -> assert false
145 | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
146 symbols_counter := !symbols_counter - 1;
147 let cardinality map =
148 TermMap.fold (fun k v res -> res + v) map 0
150 (* match active with *)
151 (* | (Negative, e)::_ -> *)
152 (* let symbols = symbols_of_equality e in *)
154 let _, _, term = goal in
157 let card = cardinality symbols in
158 let foldfun k v (r1, r2) =
159 if TermMap.mem k symbols then
160 let c = TermMap.find k symbols in
161 let c1 = abs (c - v) in
167 let f equality (i, e) =
169 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
171 let c = others + (abs (common - card)) in
172 if c < i then (c, equality)
173 (* else if c = i then *)
174 (* match OrderedEquality.compare equality e with *)
175 (* | -1 -> (c, equality) *)
176 (* | res -> (i, e) *)
179 let e1 = EqualitySet.min_elt pos_set in
182 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
184 (others + (abs (common - card))), e1
186 let _, current = EqualitySet.fold f pos_set initial in
187 (* Printf.printf "\nsymbols-based selection: %s\n\n" *)
188 (* (string_of_equality ~env current); *)
190 Indexing.remove_index passive_table current
191 (* if !use_fullred then Indexing.remove_index passive_table current *)
192 (* else passive_table *)
196 (remove current pos_list, EqualitySet.remove current pos_set),
199 (* let current = EqualitySet.min_elt pos_set in *)
200 (* let passive_table = *)
201 (* Indexing.remove_index passive_table current *)
202 (* (\* if !use_fullred then Indexing.remove_index passive_table current *\) *)
203 (* (\* else passive_table *\) *)
206 (* (neg_list, neg_set), *)
207 (* (remove current pos_list, EqualitySet.remove current pos_set), *)
210 (* (Positive, current), passive *)
213 symbols_counter := !symbols_ratio;
214 let set_selection set = EqualitySet.min_elt set in
215 if EqualitySet.is_empty neg_set then
216 let current = set_selection pos_set in
219 (remove current pos_list, EqualitySet.remove current pos_set),
220 Indexing.remove_index passive_table current
221 (* if !use_fullred then Indexing.remove_index passive_table current *)
222 (* else passive_table *)
224 (Positive, current), passive
226 let current = set_selection neg_set in
228 (remove current neg_list, EqualitySet.remove current neg_set),
232 (Negative, current), passive
236 let make_passive neg pos =
237 let set_of equalities =
238 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
241 List.fold_left (fun tbl e -> Indexing.index tbl e)
242 (Indexing.empty_table ()) pos
243 (* if !use_fullred then *)
244 (* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
245 (* (Indexing.empty_table ()) pos *)
247 (* Indexing.empty_table () *)
256 [], Indexing.empty_table ()
260 let add_to_passive passive (new_neg, new_pos) =
261 let (neg_list, neg_set), (pos_list, pos_set), table = passive in
262 let ok set equality = not (EqualitySet.mem equality set) in
263 let neg = List.filter (ok neg_set) new_neg
264 and pos = List.filter (ok pos_set) new_pos in
266 List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
267 (* if !use_fullred then *)
268 (* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
272 let add set equalities =
273 List.fold_left (fun s e -> EqualitySet.add e s) set equalities
275 (neg @ neg_list, add neg_set neg),
276 (pos_list @ pos, add pos_set pos),
281 let passive_is_empty = function
282 | ([], _), ([], _), _ -> true
287 let size_of_passive ((_, ns), (_, ps), _) =
288 (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
292 let size_of_active (active_list, _) =
293 List.length active_list
297 let prune_passive howmany (active, _) passive =
298 let (nl, ns), (pl, ps), tbl = passive in
299 let howmany = float_of_int howmany
300 and ratio = float_of_int !weight_age_ratio in
303 int_of_float (if t -. v < 0.5 then t else v)
305 let in_weight = round (howmany *. ratio /. (ratio +. 1.))
306 and in_age = round (howmany /. (ratio +. 1.)) in
308 (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
311 | (Negative, e)::_ ->
312 let symbols = symbols_of_equality e in
313 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
317 let counter = ref !symbols_ratio in
318 let rec pickw w ns ps =
320 if not (EqualitySet.is_empty ns) then
321 let e = EqualitySet.min_elt ns in
322 let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
323 EqualitySet.add e ns', ps
324 else if !counter > 0 then
326 counter := !counter - 1;
327 if !counter = 0 then counter := !symbols_ratio
331 let e = EqualitySet.min_elt ps in
332 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
333 ns, EqualitySet.add e ps'
335 let foldfun k v (r1, r2) =
336 if TermMap.mem k symbols then
337 let c = TermMap.find k symbols in
338 let c1 = abs (c - v) in
344 let f equality (i, e) =
346 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
348 let c = others + (abs (common - card)) in
349 if c < i then (c, equality)
352 let e1 = EqualitySet.min_elt ps in
355 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
357 (others + (abs (common - card))), e1
359 let _, e = EqualitySet.fold f ps initial in
360 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
361 ns, EqualitySet.add e ps'
363 let e = EqualitySet.min_elt ps in
364 let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
365 ns, EqualitySet.add e ps'
367 EqualitySet.empty, EqualitySet.empty
369 (* let in_weight, ns = pickw in_weight ns in *)
370 (* let _, ps = pickw in_weight ps in *)
371 let ns, ps = pickw in_weight ns ps in
372 let rec picka w s l =
376 | hd::tl when not (EqualitySet.mem hd s) ->
377 let w, s, l = picka (w-1) s tl in
378 w, EqualitySet.add hd s, hd::l
380 let w, s, l = picka w s tl in
385 let in_age, ns, nl = picka in_age ns nl in
386 let _, ps, pl = picka in_age ps pl in
387 if not (EqualitySet.is_empty ps) then
388 (* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
389 maximal_retained_equality := Some (EqualitySet.max_elt ps);
392 (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
393 (* if !use_fullred then *)
394 (* EqualitySet.fold *)
395 (* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
399 (nl, ns), (pl, ps), tbl
403 let infer env sign current (active_list, active_table) =
404 let new_neg, new_pos =
408 Indexing.superposition_left !maxmeta env active_table current in
413 Indexing.superposition_right !maxmeta env active_table current in
415 let rec infer_positive table = function
417 | (Negative, equality)::tl ->
419 Indexing.superposition_left !maxmeta env table equality in
421 let neg, pos = infer_positive table tl in
423 | (Positive, equality)::tl ->
425 Indexing.superposition_right !maxmeta env table equality in
427 let neg, pos = infer_positive table tl in
430 let curr_table = Indexing.index (Indexing.empty_table ()) current in
431 let neg, pos = infer_positive curr_table active_list in
434 derived_clauses := !derived_clauses + (List.length new_neg) +
435 (List.length new_pos);
436 match !maximal_retained_equality with
437 | None -> new_neg, new_pos
439 (* if we have a maximal_retained_equality, we can discard all equalities
440 "greater" than it, as they will never be reached... An equality is
441 greater than maximal_retained_equality if it is bigger
442 wrt. OrderedEquality.compare and it is less similar than
443 maximal_retained_equality to the current goal *)
445 match active_list with
446 | (Negative, e)::_ ->
447 let symbols = symbols_of_equality e in
448 let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
455 List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
458 if OrderedEquality.compare e eq <= 0 then
461 let foldfun k v (r1, r2) =
462 if TermMap.mem k symbols then
463 let c = TermMap.find k symbols in
464 let c1 = abs (c - v) in
472 TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
473 others + (abs (common - card))
476 TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
477 let c = others + (abs (common - card)) in
478 if c < initial then true else false
480 List.filter filterfun new_pos
486 let contains_empty env (negative, positive) =
487 let metasenv, context, ugraph = env in
491 (fun (w, proof, (ty, left, right, ordering), m, a) ->
492 fst (CicReduction.are_convertible context left right ugraph))
501 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
502 let pl, passive_table =
505 | Some ((pn, _), (pp, _), pt) ->
506 let pn = List.map (fun e -> (Negative, e)) pn
507 and pp = List.map (fun e -> (Positive, e)) pp in
510 let all = if pl = [] then active_list else active_list @ pl in
512 (* let rec find_duplicate sign current = function *)
514 (* | (s, eq)::tl when s = sign -> *)
515 (* if meta_convertibility_eq current eq then true *)
516 (* else find_duplicate sign current tl *)
517 (* | _::tl -> find_duplicate sign current tl *)
521 (* if sign = Positive then *)
522 (* Indexing.subsumption env active_table current *)
530 let demodulate table current =
531 let newmeta, newcurrent =
532 Indexing.demodulation_equality !maxmeta env table sign current in
534 if is_identity env newcurrent then
535 if sign = Negative then Some (sign, newcurrent)
538 Some (sign, newcurrent)
541 let res = demodulate active_table current in
544 | Some (sign, newcurrent) ->
545 match passive_table with
547 | Some passive_table -> demodulate passive_table newcurrent
551 | Some (Negative, c) ->
554 (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
557 if ok then res else None
558 | Some (Positive, c) ->
559 if Indexing.in_index active_table c then
562 match passive_table with
564 | Some passive_table ->
565 if Indexing.in_index passive_table c then None
568 (* | Some (s, c) -> if find_duplicate s c all then None else res *)
570 (* if s = Utils.Negative then *)
573 (* if Indexing.subsumption env active_table c then *)
576 (* match passive_table with *)
578 (* | Some passive_table -> *)
579 (* if Indexing.subsumption env passive_table c then *)
585 (* let pred (sign, eq) = *)
586 (* if sign <> s then false *)
587 (* else subsumption env c eq *)
589 (* if List.exists pred all then None *)
593 type fs_time_info_t = {
594 mutable build_all: float;
595 mutable demodulate: float;
596 mutable subsumption: float;
599 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
602 let forward_simplify_new env (new_neg, new_pos) ?passive active =
603 let t1 = Unix.gettimeofday () in
605 let active_list, active_table = active in
606 let pl, passive_table =
609 | Some ((pn, _), (pp, _), pt) ->
610 let pn = List.map (fun e -> (Negative, e)) pn
611 and pp = List.map (fun e -> (Positive, e)) pp in
614 let all = active_list @ pl in
616 let t2 = Unix.gettimeofday () in
617 fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
619 let demodulate sign table target =
620 let newmeta, newtarget =
621 Indexing.demodulation_equality !maxmeta env table sign target in
625 (* let f sign' target (sign, eq) = *)
626 (* if sign <> sign' then false *)
627 (* else subsumption env target eq *)
630 let t1 = Unix.gettimeofday () in
632 let new_neg, new_pos =
633 let new_neg = List.map (demodulate Negative active_table) new_neg
634 and new_pos = List.map (demodulate Positive active_table) new_pos in
635 match passive_table with
636 | None -> new_neg, new_pos
637 | Some passive_table ->
638 List.map (demodulate Negative passive_table) new_neg,
639 List.map (demodulate Positive passive_table) new_pos
642 let t2 = Unix.gettimeofday () in
643 fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
648 if not (Inference.is_identity env e) then
649 if EqualitySet.mem e s then s
650 else EqualitySet.add e s
652 EqualitySet.empty new_pos
654 let new_pos = EqualitySet.elements new_pos_set in
657 match passive_table with
659 (fun e -> not (fst (Indexing.subsumption env active_table e)))
660 | Some passive_table ->
661 (fun e -> not ((fst (Indexing.subsumption env active_table e)) ||
662 (fst (Indexing.subsumption env passive_table e))))
665 let t1 = Unix.gettimeofday () in
667 (* let new_neg, new_pos = *)
668 (* List.filter subs new_neg, *)
669 (* List.filter subs new_pos *)
672 (* let new_neg, new_pos = *)
673 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
674 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
677 let t2 = Unix.gettimeofday () in
678 fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
681 match passive_table with
683 (fun e -> not (Indexing.in_index active_table e))
684 | Some passive_table ->
686 not ((Indexing.in_index active_table e) ||
687 (Indexing.in_index passive_table e)))
689 new_neg, List.filter is_duplicate new_pos
691 (* new_neg, new_pos *)
694 (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
695 (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
701 let backward_simplify_active env new_pos new_table min_weight active =
702 let active_list, active_table = active in
703 let active_list, newa =
705 (fun (s, equality) (res, newn) ->
706 let ew, _, _, _, _ = equality in
707 if ew < min_weight then
708 (s, equality)::res, newn
710 match forward_simplify env (s, equality) (new_pos, new_table) with
720 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
724 (fun (s, eq) (res, tbl) ->
725 if List.mem (s, eq) res then
727 else if (is_identity env eq) || (find eq res) then (
729 ) (* else if (find eq res) then *)
732 (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
733 active_list ([], Indexing.empty_table ()),
735 (fun (s, eq) (n, p) ->
736 if (s <> Negative) && (is_identity env eq) then (
739 if s = Negative then eq::n, p
744 | [], [] -> active, None
745 | _ -> active, Some newa
749 let backward_simplify_passive env new_pos new_table min_weight passive =
750 let (nl, ns), (pl, ps), passive_table = passive in
751 let f sign equality (resl, ress, newn) =
752 let ew, _, _, _, _ = equality in
753 if ew < min_weight then
754 (* let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *)
755 equality::resl, ress, newn
757 match forward_simplify env (sign, equality) (new_pos, new_table) with
758 | None -> resl, EqualitySet.remove equality ress, newn
761 equality::resl, ress, newn
763 let ress = EqualitySet.remove equality ress in
766 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
767 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
770 (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
772 match newn, newp with
773 | [], [] -> ((nl, ns), (pl, ps), passive_table), None
774 | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
778 let backward_simplify env new' ?passive active =
779 let new_pos, new_table, min_weight =
782 let ew, _, _, _, _ = e in
783 (Positive, e)::l, Indexing.index t e, min ew w)
784 ([], Indexing.empty_table (), 1000000) (snd new')
787 backward_simplify_active env new_pos new_table min_weight active in
790 active, (make_passive [] []), newa, None
793 backward_simplify_passive env new_pos new_table min_weight passive in
794 active, passive, newa, newp
798 let get_selection_estimate () =
799 elapsed_time := (Unix.gettimeofday ()) -. !start_time;
800 (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
802 ceil ((float_of_int !processed_clauses) *.
803 ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
807 let make_goals goal =
809 and passive = [0, [goal]] in
814 let make_theorems theorems =
816 (* let active = [] *)
817 (* and passive = theorems in *)
818 (* active, passive *)
822 let activate_goal (active, passive) =
824 | goal_conj::tl -> true, (goal_conj::active, tl)
825 | [] -> false, (active, passive)
829 let activate_theorem (active, passive) =
831 | theorem::tl -> true, (theorem::active, tl)
832 | [] -> false, (active, passive)
836 let simplify_goal env goal ?passive (active_list, active_table) =
837 let pl, passive_table =
840 | Some ((pn, _), (pp, _), pt) ->
841 let pn = List.map (fun e -> (Negative, e)) pn
842 and pp = List.map (fun e -> (Positive, e)) pp in
845 let all = if pl = [] then active_list else active_list @ pl in
847 let demodulate table goal =
848 let newmeta, newgoal =
849 Indexing.demodulation_goal !maxmeta env table goal in
851 goal != newgoal, newgoal
854 match passive_table with
855 | None -> demodulate active_table goal
856 | Some passive_table ->
857 let changed, goal = demodulate active_table goal in
858 let changed', goal = demodulate passive_table goal in
859 (changed || changed'), goal
862 let p, _, t = goal in
865 (Printf.sprintf "Goal after demodulation: %s, %s"
866 (string_of_proof p) (CicPp.ppterm t)))
872 let simplify_goals env goals ?passive active =
873 let a_goals, p_goals = goals in
878 List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
884 (fun (a, p) (d, gl) ->
885 let changed = ref false in
889 let c, g = simplify_goal env g ?passive active in
890 changed := !changed || c; g) gl in
891 if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
892 ([], p_goals) a_goals
898 let simplify_theorems env theorems ?passive (active_list, active_table) =
899 let pl, passive_table =
902 | Some ((pn, _), (pp, _), pt) ->
903 let pn = List.map (fun e -> (Negative, e)) pn
904 and pp = List.map (fun e -> (Positive, e)) pp in
907 let all = if pl = [] then active_list else active_list @ pl in
908 let a_theorems, p_theorems = theorems in
909 let demodulate table theorem =
910 let newmeta, newthm =
911 Indexing.demodulation_theorem !maxmeta env table theorem in
913 theorem != newthm, newthm
915 let foldfun table (a, p) theorem =
916 let changed, theorem = demodulate table theorem in
917 if changed then (a, theorem::p) else (theorem::a, p)
919 let mapfun table theorem = snd (demodulate table theorem) in
920 match passive_table with
922 let p_theorems = List.map (mapfun active_table) p_theorems in
923 List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
924 (* List.map (demodulate active_table) theorems *)
925 | Some passive_table ->
926 let p_theorems = List.map (mapfun active_table) p_theorems in
927 let p_theorems, a_theorems =
928 List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
929 let p_theorems = List.map (mapfun passive_table) p_theorems in
930 List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
931 (* let theorems = List.map (demodulate active_table) theorems in *)
932 (* List.map (demodulate passive_table) theorems *)
936 let apply_equality_to_goal env equality goal =
937 let module C = Cic in
938 let module HL = HelmLibraryObjects in
939 let module I = Inference in
940 let metasenv, context, ugraph = env in
941 let _, proof, (ty, left, right, _), metas, args = equality in
943 C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
944 let gproof, gmetas, gterm = goal in
947 (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s"
948 (string_of_equality equality) (CicPp.ppterm gterm)));
950 let subst, metasenv', _ =
951 let menv = metasenv @ metas @ gmetas in
952 Inference.unification menv context eqterm gterm ugraph
956 | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t)
957 | I.ProofBlock (s, uri, nt, t, pe, p) ->
958 I.ProofBlock (subst @ s, uri, nt, t, pe, p)
962 let rec repl = function
963 | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp)
964 | I.NoProof -> newproof
965 | I.BasicProof p -> newproof
966 | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p)
971 true, subst, newgproof
972 with CicUnification.UnificationFailure _ ->
978 let apply_to_goal env theorems active (depth, goals) =
980 debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals)))
982 let metasenv, context, ugraph = env in
983 let goal = List.hd goals in
984 let proof, metas, term = goal in
986 (* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *)
987 let newmeta = CicMkImplicit.new_meta metasenv [] in
988 let metasenv = (newmeta, context, term)::metasenv @ metas in
989 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
991 ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta)
993 let rec aux = function
994 | [] -> false, [] (* goals *) (* None *)
995 | (theorem, thmty, _)::tl ->
997 let subst_in, (newproof, newgoals) =
998 PrimitiveTactics.apply_tac_verbose ~term:theorem status
1000 if newgoals = [] then
1001 let _, _, p, _ = newproof in
1003 let rec repl = function
1004 | Inference.ProofGoalBlock (_, gp) ->
1005 Inference.ProofGoalBlock (Inference.BasicProof p, gp)
1006 | Inference.NoProof -> Inference.BasicProof p
1007 | Inference.BasicProof _ -> Inference.BasicProof p
1008 | Inference.SubProof (t, i, p2) ->
1009 Inference.SubProof (t, i, repl p2)
1014 true, [[newp, metas, term]] (* Some newp *)
1015 else if List.length newgoals = 1 then
1016 let _, menv, p, _ = newproof in
1018 CicMkImplicit.identity_relocation_list_for_metavariable context
1023 let _, _, ty = CicUtil.lookup_meta i menv in
1026 (p, i, Inference.BasicProof (Cic.Meta (i, irl)))
1027 in (proof, menv, ty))
1030 let res, others = aux tl in
1031 if res then (true, others) else (false, goals::others)
1034 with ProofEngineTypes.Fail msg ->
1035 (* debug_print ("FAIL!!:" ^ msg); *)
1039 if Inference.term_is_equality term then
1040 let rec appleq = function
1042 | (Positive, equality)::tl ->
1043 let ok, _, newproof = apply_equality_to_goal env equality goal in
1044 if ok then true, [(depth, [newproof, metas, term])] else appleq tl
1045 | _::tl -> appleq tl
1047 let al, _ = active in
1052 if r = true then r, l else
1053 let r, l = aux theorems in
1055 r, List.map (fun l -> (depth+1, l)) l
1057 r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l)
1063 incr maxmeta; !maxmeta
1067 let apply_to_goal env theorems ?passive active goal =
1068 let metasenv, context, ugraph = env in
1069 let proof, metas, term = goal in
1072 (Printf.sprintf "apply_to_goal with goal: %s"
1073 (* (string_of_proof proof) *)(CicPp.ppterm term)));
1076 CicMkImplicit.identity_relocation_list_for_metavariable context in
1077 let proof', newmeta =
1078 let rec get_meta = function
1079 | SubProof (t, i, _) -> t, i
1080 | ProofGoalBlock (_, p) -> get_meta p
1082 let n = new_meta () in (* CicMkImplicit.new_meta metasenv [] in *)
1083 Cic.Meta (n, irl), n
1087 (* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
1088 let metasenv = (newmeta, context, term)::metasenv @ metas in
1089 ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta)
1090 (* ((None, metasenv, proof', term), newmeta) *)
1092 let rec aux = function
1093 | [] -> `No (* , [], [] *)
1094 | (theorem, thmty, _)::tl ->
1096 let subst, (newproof, newgoals) =
1097 PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status
1099 if newgoals = [] then
1100 let _, _, p, _ = newproof in
1102 let rec repl = function
1103 | Inference.ProofGoalBlock (_, gp) ->
1104 Inference.ProofGoalBlock (Inference.BasicProof p, gp)
1105 | Inference.NoProof -> Inference.BasicProof p
1106 | Inference.BasicProof _ -> Inference.BasicProof p
1107 | Inference.SubProof (t, i, p2) ->
1108 Inference.SubProof (t, i, repl p2)
1113 let _, m = status in
1114 let subst = List.filter (fun (i, _) -> i = m) subst in
1117 (* (Printf.sprintf "m = %d\nsubst = %s\n" *)
1118 (* m (print_subst subst))); *)
1119 `Ok (subst, [newp, metas, term])
1121 let _, menv, p, _ = newproof in
1123 CicMkImplicit.identity_relocation_list_for_metavariable context
1128 let _, _, ty = CicUtil.lookup_meta i menv in
1130 let rec gp = function
1131 | SubProof (t, i, p) ->
1132 SubProof (t, i, gp p)
1133 | ProofGoalBlock (sp1, sp2) ->
1134 (* SubProof (p, i, sp) *)
1135 ProofGoalBlock (sp1, gp sp2)
1139 SubProof (p, i, BasicProof (Cic.Meta (i, irl)))
1140 | ProofSymBlock (s, sp) ->
1141 ProofSymBlock (s, gp sp)
1142 | ProofBlock (s, u, nt, t, pe, sp) ->
1143 ProofBlock (s, u, nt, t, pe, gp sp)
1144 (* | _ -> assert false *)
1149 (Printf.sprintf "new sub goal: %s"
1150 (* (string_of_proof p') *)(CicPp.ppterm ty)));
1156 let w, m = weight_of_term t in
1157 w + 2 * (List.length m)
1160 (fun (_, _, t1) (_, _, t2) ->
1161 Pervasives.compare (weight t1) (weight t2))
1166 (* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *)
1167 let best = aux tl in
1169 | `Ok (_, _) -> best
1170 | `No -> `GoOn ([subst, goals])
1171 | `GoOn sl(* , subst', goals' *) ->
1172 (* if (List.length goals') < (List.length goals) then best *)
1173 (* else `GoOn, subst, goals *)
1174 `GoOn ((subst, goals)::sl)
1175 with ProofEngineTypes.Fail msg ->
1179 if Inference.term_is_equality term then
1180 let _ = debug_print (lazy "OK, is equality!!") in
1181 let rec appleq_a = function
1182 | [] -> false, [], []
1183 | (Positive, equality)::tl ->
1184 let ok, s, newproof = apply_equality_to_goal env equality goal in
1185 if ok then true, s, [newproof, metas, term] else appleq_a tl
1186 | _::tl -> appleq_a tl
1188 let rec appleq_p = function
1189 | [] -> false, [], []
1191 let ok, s, newproof = apply_equality_to_goal env equality goal in
1192 if ok then true, s, [newproof, metas, term] else appleq_p tl
1194 let al, _ = active in
1196 | None -> appleq_a al
1197 | Some (_, (pl, _), _) ->
1198 let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
1202 if r = true then `Ok (s, l) else aux theorems
1206 let apply_to_goal_conj env theorems ?passive active (depth, goals) =
1207 let rec aux = function
1209 let propagate_subst subst (proof, metas, term) =
1212 (* (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" *)
1213 (* (print_subst subst) (string_of_proof proof) *)
1214 (* (CicPp.ppterm term))); *)
1215 let rec repl = function
1216 | NoProof -> NoProof
1218 BasicProof (CicMetaSubst.apply_subst subst t)
1219 | ProofGoalBlock (p, pb) ->
1220 (* debug_print (lazy "HERE"); *)
1221 let pb' = repl pb in
1222 ProofGoalBlock (p, pb')
1223 | SubProof (t, i, p) ->
1224 let t' = CicMetaSubst.apply_subst subst t in
1227 (* (Printf.sprintf *)
1228 (* "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" *)
1229 (* i (CicPp.ppterm t) (print_subst subst) *)
1230 (* (CicPp.ppterm t'))); *)
1233 | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
1234 | ProofBlock (s, u, nty, t, pe, p) ->
1235 ProofBlock (subst @ s, u, nty, t, pe, p)
1236 in (repl proof, metas, term)
1238 let r = apply_to_goal env theorems ?passive active goal in (
1240 | `No -> `No (depth, goals)
1241 | `GoOn sl (* (subst, gl) *) ->
1242 (* let tl = List.map (propagate_subst subst) tl in *)
1243 (* debug_print (lazy "GO ON!!!"); *)
1247 (depth+1, gl @ (List.map (propagate_subst s) tl))) sl
1251 (* (Printf.sprintf "%s\n" *)
1252 (* (String.concat "; " *)
1254 (* (fun (s, gl) -> *)
1255 (* (Printf.sprintf "[%s]" *)
1256 (* (String.concat "; " *)
1258 (* (fun (p, _, g) -> *)
1259 (* (Printf.sprintf "<%s, %s>" *)
1260 (* (string_of_proof p) *)
1261 (* (CicPp.ppterm g))) gl)))) l)))); *)
1262 `GoOn l (* (depth+1, gl @ tl) *)
1263 | `Ok (subst, gl) ->
1266 (* let p, _, t = List.hd gl in *)
1269 (* (Printf.sprintf "OK: %s, %s\n" *)
1270 (* (string_of_proof p) (CicPp.ppterm t))) *)
1274 let p, _, _ = List.hd gl in
1276 let rec repl = function
1277 | SubProof (_, _, p) -> repl p
1278 | ProofGoalBlock (p1, p2) ->
1279 ProofGoalBlock (repl p1, repl p2)
1282 build_proof_term (repl p)
1285 let rec get_meta = function
1286 | SubProof (_, i, p) -> max i (get_meta p)
1287 | ProofGoalBlock (_, p) -> get_meta p
1288 | _ -> -1 (* assert false *)
1293 let _, (context, _, _) = List.hd subst in
1294 [i, (context, subproof, Cic.Implicit None)]
1296 let tl = List.map (propagate_subst subst) tl in
1297 `GoOn ([depth+1, tl])
1303 (Printf.sprintf "apply_to_goal_conj (%d, [%s])"
1306 (List.map (fun (_, _, t) -> CicPp.ppterm t) goals))));
1307 if depth > !maxdepth || (List.length goals) > !maxwidth then (
1309 (lazy (Printf.sprintf "Pruning because depth = %d, width = %d"
1310 depth (List.length goals)));
1317 module OrderedGoals = struct
1318 type t = int * (Inference.proof * Cic.metasenv * Cic.term) list
1325 else let r = (List.length l1) - (List.length l2) in
1331 (fun (_, _, t1) (_, _, t2) ->
1332 let r = Pervasives.compare t1 t2 in
1339 (* let res = Pervasives.compare g1 g2 in *)
1341 (* let print_goals (d, gl) = *)
1342 (* let gl' = List.map (fun (_, _, t) -> CicPp.ppterm t) gl in *)
1343 (* Printf.sprintf "%d, [%s]" d (String.concat "; " gl') *)
1347 (* (Printf.sprintf "comparing g1:%s and g2:%s, res: %d\n" *)
1348 (* (print_goals g1) (print_goals g2) res)) *)
1353 module GoalsSet = Set.Make(OrderedGoals);;
1356 exception SearchSpaceOver;;
1359 let apply_to_goals env is_passive_empty theorems active goals =
1360 debug_print (lazy "\n\n\tapply_to_goals\n\n");
1361 let add_to set goals =
1362 List.fold_left (fun s g -> GoalsSet.add g s) set goals
1364 let rec aux set = function
1366 debug_print (lazy "HERE!!!");
1367 if is_passive_empty then raise SearchSpaceOver else false, set
1369 let res = apply_to_goal_conj env theorems active goals in
1375 | (d, (p, _, t)::_) -> d, p, t
1380 (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n"
1381 d (string_of_proof p) (CicPp.ppterm t)))
1383 true, GoalsSet.singleton newgoals
1385 (* let print_set set msg = *)
1388 (* (Printf.sprintf "%s:\n%s" msg *)
1389 (* (String.concat "\n" *)
1390 (* (GoalsSet.fold *)
1391 (* (fun (d, gl) l -> *)
1393 (* List.map (fun (_, _, t) -> CicPp.ppterm t) gl *)
1396 (* Printf.sprintf "%d, [%s]" d *)
1397 (* (String.concat "; " gl') *)
1399 (* s::l) set [])))) *)
1403 (* try aux set tl with SearchSpaceOver -> false, GoalsSet.empty *)
1409 let set' = add_to set (goals::tl) in
1410 (* print_set set "SET BEFORE"; *)
1411 (* let n = GoalsSet.cardinal set in *)
1412 let set' = add_to set' newgoals in
1413 (* print_set set "SET AFTER"; *)
1414 (* let m = GoalsSet.cardinal set in *)
1418 (* let _ = print_set set "SET didn't change" in *)
1422 (* let set = add_to set (newgoals::goals::tl) in *)
1423 (* let res, set = aux set tl in *)
1426 let n = List.length goals in
1427 let res, goals = aux (add_to GoalsSet.empty goals) goals in
1428 let goals = GoalsSet.elements goals in
1429 debug_print (lazy "\n\tapply_to_goals end\n");
1430 let m = List.length goals in
1431 if m = n && is_passive_empty then
1432 raise SearchSpaceOver
1438 let apply_goal_to_theorems dbd env theorems ?passive active goals =
1439 (* let theorems, _ = theorems in *)
1440 let context_hyp, library_thms = theorems in
1443 (fun s (u, _, _, _) -> UriManager.UriSet.add u s)
1444 UriManager.UriSet.empty library_thms
1446 let a_goals, p_goals = goals in
1447 let goal = List.hd a_goals in
1448 let rec aux = function
1449 | [] -> false, (a_goals, p_goals)
1451 let res = apply_to_goal_conj env [theorem] ?passive active goal in
1454 true, ([newgoals], [])
1457 (* false, (a_goals, p_goals) *)
1459 let res, (ag, pg) = aux tl in
1466 (d <= !maxdepth) && (List.length gl) <= !maxwidth)
1468 let p_goals = newgoals @ pg in
1471 (fun (d1, l1) (d2, l2) -> (List.length l1) - (List.length l2))
1478 (* match goal with *)
1479 (* | (_, (_, _, t)::_) -> t *)
1480 (* | _ -> assert false *)
1482 (* if CicUtil.is_meta_closed ty then *)
1484 (* debug_print (lazy (Printf.sprintf "META CLOSED: %s" (CicPp.ppterm ty))) *)
1486 (* let metasenv, context, ugraph = env in *)
1488 (* MetadataConstraints.sigmatch ~dbd (MetadataConstraints.signature_of ty) *)
1490 (* let uris = List.sort (fun (i, _) (j, _) -> Pervasives.compare i j) uris in *)
1493 (* (fun u -> UriManager.UriSet.mem u thm_uris) (List.map snd uris) *)
1497 (* let t = CicUtil.term_of_uri u in *)
1498 (* let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in *)
1502 List.map (fun (_, t, ty, m) -> (t, ty, m)) library_thms
1504 aux (context_hyp @ theorems)
1508 let apply_theorem_to_goals env theorems active goals =
1509 let a_goals, p_goals = goals in
1510 let theorem = List.hd (fst theorems) in
1511 let theorems = [theorem] in
1512 let rec aux p = function
1513 | [] -> false, ([], p)
1515 let res = apply_to_goal_conj env theorems active goal in
1517 | `Ok newgoals -> true, ([newgoals], [])
1519 | `GoOn newgoals -> aux (newgoals @ p) tl
1521 let ok, (a, p) = aux p_goals a_goals in
1527 (fun (d1, l1) (d2, l2) ->
1530 else let r = (List.length l1) - (List.length l2) in
1536 (fun (_, _, t1) (_, _, t2) ->
1537 let r = Pervasives.compare t1 t2 in
1538 if r <> 0 then (res := r; true) else false) l1 l2
1542 ok, (a_goals, p_goals)
1546 let rec given_clause dbd env goals theorems passive active =
1547 let goals = simplify_goals env goals active in
1548 let ok, goals = activate_goal goals in
1549 (* let theorems = simplify_theorems env theorems active in *)
1551 let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
1554 match (fst goals) with
1555 | (_, [proof, _, _])::_ -> Some proof
1558 ParamodulationSuccess (proof, env)
1560 given_clause_aux dbd env goals theorems passive active
1562 (* let ok', theorems = activate_theorem theorems in *)
1563 let ok', theorems = false, theorems in
1565 let ok, goals = apply_theorem_to_goals env theorems active goals in
1568 match (fst goals) with
1569 | (_, [proof, _, _])::_ -> Some proof
1572 ParamodulationSuccess (proof, env)
1574 given_clause_aux dbd env goals theorems passive active
1576 if (passive_is_empty passive) then ParamodulationFailure
1577 else given_clause_aux dbd env goals theorems passive active
1579 and given_clause_aux dbd env goals theorems passive active =
1580 let time1 = Unix.gettimeofday () in
1582 let selection_estimate = get_selection_estimate () in
1583 let kept = size_of_passive passive in
1585 if !time_limit = 0. || !processed_clauses = 0 then
1587 else if !elapsed_time > !time_limit then (
1588 debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
1589 !time_limit !elapsed_time));
1591 ) else if kept > selection_estimate then (
1593 (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
1594 "(kept: %d, selection_estimate: %d)\n")
1595 kept selection_estimate));
1596 prune_passive selection_estimate active passive
1601 let time2 = Unix.gettimeofday () in
1602 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
1604 kept_clauses := (size_of_passive passive) + (size_of_active active);
1606 (* (\* let goals = simplify_goals env goals active in *\) *)
1607 (* (\* let theorems = simplify_theorems env theorems active in *\) *)
1608 (* let is_passive_empty = passive_is_empty passive in *)
1610 (* let ok, goals = false, [] in (\* apply_to_goals env is_passive_empty theorems active goals in *\) *)
1613 (* match goals with *)
1614 (* | (_, [proof, _, _])::_ -> Some proof *)
1615 (* | _ -> assert false *)
1617 (* ParamodulationSuccess (proof, env) *)
1619 match passive_is_empty passive with
1620 | true -> (* ParamodulationFailure *)
1621 given_clause dbd env goals theorems passive active
1623 let (sign, current), passive = select env (fst goals) passive active in
1624 let time1 = Unix.gettimeofday () in
1625 let res = forward_simplify env (sign, current) ~passive active in
1626 let time2 = Unix.gettimeofday () in
1627 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
1630 given_clause dbd env goals theorems passive active
1631 | Some (sign, current) ->
1632 if (sign = Negative) && (is_identity env current) then (
1634 (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
1635 (string_of_equality ~env current)));
1636 let _, proof, _, _, _ = current in
1637 ParamodulationSuccess (Some proof (* current *), env)
1640 (lazy "\n================================================");
1641 debug_print (lazy (Printf.sprintf "selected: %s %s"
1642 (string_of_sign sign)
1643 (string_of_equality ~env current)));
1645 let t1 = Unix.gettimeofday () in
1646 let new' = infer env sign current active in
1647 let t2 = Unix.gettimeofday () in
1648 infer_time := !infer_time +. (t2 -. t1);
1650 let res, goal' = contains_empty env new' in
1654 | Some goal -> let _, proof, _, _, _ = goal in Some proof
1657 ParamodulationSuccess (proof (* goal *), env)
1659 let t1 = Unix.gettimeofday () in
1660 let new' = forward_simplify_new env new' active in
1661 let t2 = Unix.gettimeofday () in
1663 forward_simpl_new_time :=
1664 !forward_simpl_new_time +. (t2 -. t1)
1668 | Negative -> active
1670 let t1 = Unix.gettimeofday () in
1671 let active, _, newa, _ =
1672 backward_simplify env ([], [current]) active
1674 let t2 = Unix.gettimeofday () in
1675 backward_simpl_time :=
1676 !backward_simpl_time +. (t2 -. t1);
1680 let al, tbl = active in
1681 let nn = List.map (fun e -> Negative, e) n in
1686 Indexing.index tbl e)
1692 (* Printf.printf "active:\n%s\n" *)
1693 (* (String.concat "\n" *)
1695 (* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
1696 (* (string_of_equality ~env e)) (fst active)))); *)
1697 (* print_newline (); *)
1700 (* match new' with *)
1702 (* Printf.printf "new':\n%s\n" *)
1703 (* (String.concat "\n" *)
1705 (* (fun e -> "Negative " ^ *)
1706 (* (string_of_equality ~env e)) neg) @ *)
1708 (* (fun e -> "Positive " ^ *)
1709 (* (string_of_equality ~env e)) pos))); *)
1710 (* print_newline (); *)
1712 match contains_empty env new' with
1715 let al, tbl = active in
1717 | Negative -> (sign, current)::al, tbl
1719 al @ [(sign, current)], Indexing.index tbl current
1721 let passive = add_to_passive passive new' in
1722 let (_, ns), (_, ps), _ = passive in
1723 (* Printf.printf "passive:\n%s\n" *)
1724 (* (String.concat "\n" *)
1725 (* ((List.map (fun e -> "Negative " ^ *)
1726 (* (string_of_equality ~env e)) *)
1727 (* (EqualitySet.elements ns)) @ *)
1728 (* (List.map (fun e -> "Positive " ^ *)
1729 (* (string_of_equality ~env e)) *)
1730 (* (EqualitySet.elements ps)))); *)
1731 (* print_newline (); *)
1732 given_clause dbd env goals theorems passive active
1737 let _, proof, _, _, _ = goal in Some proof
1740 ParamodulationSuccess (proof (* goal *), env)
1742 (* with SearchSpaceOver -> *)
1743 (* ParamodulationFailure *)
1747 let rec given_clause_fullred dbd env goals theorems passive active =
1748 let goals = simplify_goals env goals ~passive active in
1749 let ok, goals = activate_goal goals in
1750 (* let theorems = simplify_theorems env theorems ~passive active in *)
1753 let print_goals goals =
1760 (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
1762 Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
1766 (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n"
1767 (print_goals (fst goals)) (print_goals (snd goals))))
1770 apply_goal_to_theorems dbd env theorems ~passive active goals
1774 match (fst goals) with
1775 | (_, [proof, _, _])::_ -> Some proof
1778 ParamodulationSuccess (proof, env)
1780 given_clause_fullred_aux dbd env goals theorems passive active
1782 (* let ok', theorems = activate_theorem theorems in *)
1784 (* let ok, goals = apply_theorem_to_goals env theorems active goals in *)
1787 (* match (fst goals) with *)
1788 (* | (_, [proof, _, _])::_ -> Some proof *)
1789 (* | _ -> assert false *)
1791 (* ParamodulationSuccess (proof, env) *)
1793 (* given_clause_fullred_aux env goals theorems passive active *)
1795 if (passive_is_empty passive) then ParamodulationFailure
1796 else given_clause_fullred_aux dbd env goals theorems passive active
1798 and given_clause_fullred_aux dbd env goals theorems passive active =
1799 let time1 = Unix.gettimeofday () in
1801 let selection_estimate = get_selection_estimate () in
1802 let kept = size_of_passive passive in
1804 if !time_limit = 0. || !processed_clauses = 0 then
1806 else if !elapsed_time > !time_limit then (
1807 debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
1808 !time_limit !elapsed_time));
1810 ) else if kept > selection_estimate then (
1812 (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
1813 "(kept: %d, selection_estimate: %d)\n")
1814 kept selection_estimate));
1815 prune_passive selection_estimate active passive
1820 let time2 = Unix.gettimeofday () in
1821 passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
1823 kept_clauses := (size_of_passive passive) + (size_of_active active);
1826 (* let ok, goals = apply_to_goals env is_passive_empty theorems active goals in *)
1829 (* match goals with *)
1830 (* | (_, [proof, _, _])::_ -> Some proof *)
1831 (* | _ -> assert false *)
1833 (* ParamodulationSuccess (proof, env) *)
1837 (* (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); *)
1840 (* (String.concat "\n" *)
1842 (* (fun (d, gl) -> *)
1845 (* (fun (p, _, t) -> *)
1846 (* (\* (string_of_proof p) ^ ", " ^ *\) (CicPp.ppterm t)) gl *)
1848 (* Printf.sprintf "%d: %s" d (String.concat "; " gl')) *)
1851 match passive_is_empty passive with
1852 | true -> (* ParamodulationFailure *)
1853 given_clause_fullred dbd env goals theorems passive active
1855 let (sign, current), passive = select env (fst goals) passive active in
1856 let time1 = Unix.gettimeofday () in
1857 let res = forward_simplify env (sign, current) ~passive active in
1858 let time2 = Unix.gettimeofday () in
1859 forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
1862 given_clause_fullred dbd env goals theorems passive active
1863 | Some (sign, current) ->
1864 if (sign = Negative) && (is_identity env current) then (
1866 (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
1867 (string_of_equality ~env current)));
1868 let _, proof, _, _, _ = current in
1869 ParamodulationSuccess (Some proof (* current *), env)
1872 (lazy "\n================================================");
1873 debug_print (lazy (Printf.sprintf "selected: %s %s"
1874 (string_of_sign sign)
1875 (string_of_equality ~env current)));
1877 let t1 = Unix.gettimeofday () in
1878 let new' = infer env sign current active in
1879 let t2 = Unix.gettimeofday () in
1880 infer_time := !infer_time +. (t2 -. t1);
1883 if is_identity env current then active
1885 let al, tbl = active in
1887 | Negative -> (sign, current)::al, tbl
1889 al @ [(sign, current)], Indexing.index tbl current
1891 let rec simplify new' active passive =
1892 let t1 = Unix.gettimeofday () in
1893 let new' = forward_simplify_new env new' ~passive active in
1894 let t2 = Unix.gettimeofday () in
1895 forward_simpl_new_time :=
1896 !forward_simpl_new_time +. (t2 -. t1);
1897 let t1 = Unix.gettimeofday () in
1898 let active, passive, newa, retained =
1899 backward_simplify env new' ~passive active in
1900 let t2 = Unix.gettimeofday () in
1901 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
1902 match newa, retained with
1903 | None, None -> active, passive, new'
1905 | None, Some (n, p) ->
1906 let nn, np = new' in
1907 simplify (nn @ n, np @ p) active passive
1908 | Some (n, p), Some (rn, rp) ->
1909 let nn, np = new' in
1910 simplify (nn @ n @ rn, np @ p @ rp) active passive
1912 let active, passive, new' = simplify new' active passive in
1914 let k = size_of_passive passive in
1915 if k < (kept - 1) then
1916 processed_clauses := !processed_clauses + (kept - 1 - k);
1921 (Printf.sprintf "active:\n%s\n"
1924 (fun (s, e) -> (string_of_sign s) ^ " " ^
1925 (string_of_equality ~env e))
1933 (Printf.sprintf "new':\n%s\n"
1936 (fun e -> "Negative " ^
1937 (string_of_equality ~env e)) neg) @
1939 (fun e -> "Positive " ^
1940 (string_of_equality ~env e)) pos)))))
1942 match contains_empty env new' with
1944 let passive = add_to_passive passive new' in
1945 (* let (_, ns), (_, ps), _ = passive in *)
1946 (* Printf.printf "passive:\n%s\n" *)
1947 (* (String.concat "\n" *)
1948 (* ((List.map (fun e -> "Negative " ^ *)
1949 (* (string_of_equality ~env e)) *)
1950 (* (EqualitySet.elements ns)) @ *)
1951 (* (List.map (fun e -> "Positive " ^ *)
1952 (* (string_of_equality ~env e)) *)
1953 (* (EqualitySet.elements ps)))); *)
1954 (* print_newline (); *)
1955 given_clause_fullred dbd env goals theorems passive active
1959 | Some goal -> let _, proof, _, _, _ = goal in Some proof
1962 ParamodulationSuccess (proof (* goal *), env)
1964 (* with SearchSpaceOver -> *)
1965 (* ParamodulationFailure *)
1969 (* let given_clause_ref = ref given_clause;; *)
1971 let main dbd full term metasenv ugraph =
1972 let module C = Cic in
1973 let module T = CicTypeChecker in
1974 let module PET = ProofEngineTypes in
1975 let module PP = CicPp in
1976 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1977 let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1978 let proof, goals = status in
1979 let goal' = List.nth goals 0 in
1980 let _, metasenv, meta_proof, _ = proof in
1981 let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1982 let eq_indexes, equalities, maxm = find_equalities context proof in
1983 let lib_eq_uris, library_equalities, maxm =
1984 find_library_equalities dbd context (proof, goal') (maxm+2)
1986 maxmeta := maxm+2; (* TODO ugly!! *)
1987 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1988 let new_meta_goal, metasenv, type_of_goal =
1989 let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1990 Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
1992 Cic.Meta (maxm+1, irl),
1993 (maxm+1, context, ty)::metasenv,
1996 (* let new_meta_goal = Cic.Meta (goal', irl) in *)
1997 let env = (metasenv, context, ugraph) in
2000 let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
2001 let context_hyp = find_context_hypotheses env eq_indexes in
2002 context_hyp, theorems
2005 let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
2006 UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
2008 let t = CicUtil.term_of_uri refl_equal in
2009 let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
2010 [], [(refl_equal, t, ty, [])]
2016 "Theorems:\n-------------------------------------\n%s\n"
2019 (fun (_, t, ty, _) ->
2021 "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
2025 let goal = Inference.BasicProof new_meta_goal, [], goal in
2026 (* let term_equality = equality_of_term new_meta_goal goal in *)
2027 (* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *)
2028 (* if is_identity env term_equality then *)
2030 (* Cic.Appl [Cic.MutConstruct (\* reflexivity *\) *)
2031 (* (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); *)
2035 (* Printf.printf "OK, found a proof!\n"; *)
2036 (* let names = names_of_context context in *)
2037 (* print_endline (PP.pp proof names) *)
2042 let equalities = equalities @ library_equalities in
2045 (Printf.sprintf "equalities:\n%s\n"
2047 (List.map string_of_equality equalities))));
2048 debug_print (lazy "SIMPLYFYING EQUALITIES...");
2049 let rec simpl e others others_simpl =
2050 let active = others @ others_simpl in
2053 (fun t (_, e) -> Indexing.index t e)
2054 (Indexing.empty_table ()) active
2056 let res = forward_simplify env e (active, tbl) in
2060 | None -> simpl hd tl others_simpl
2061 | Some e -> simpl hd tl (e::others_simpl)
2065 | None -> others_simpl
2066 | Some e -> e::others_simpl
2069 match equalities with
2072 let others = List.map (fun e -> (Positive, e)) tl in
2074 List.rev (List.map snd (simpl (Positive, hd) others []))
2078 (Printf.sprintf "equalities AFTER:\n%s\n"
2080 (List.map string_of_equality res))));
2083 let active = make_active () in
2084 let passive = make_passive [] (* [term_equality] *) equalities in
2085 Printf.printf "\ncurrent goal: %s\n"
2086 (let _, _, g = goal in CicPp.ppterm g);
2087 (* (string_of_equality ~env term_equality); *)
2088 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
2089 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
2090 Printf.printf "\nequalities:\n%s\n"
2093 (string_of_equality ~env)
2094 (equalities @ library_equalities)));
2095 print_endline "--------------------------------------------------";
2096 let start = Unix.gettimeofday () in
2097 print_endline "GO!";
2098 start_time := Unix.gettimeofday ();
2100 (* (if !use_fullred then given_clause_fullred else given_clause) *)
2101 (* env [0, [goal]] theorems passive active *)
2104 let goals = make_goals goal in
2105 (* and theorems = make_theorems theorems in *)
2106 (if !use_fullred then given_clause_fullred else given_clause)
2107 dbd env goals theorems passive active
2109 let finish = Unix.gettimeofday () in
2112 | ParamodulationFailure ->
2113 Printf.printf "NO proof found! :-(\n\n"
2114 | ParamodulationSuccess (Some proof (* goal *), env) ->
2115 (* let proof = Inference.build_proof_term goal in *)
2116 let proof = Inference.build_proof_term proof in
2117 Printf.printf "OK, found a proof!\n";
2118 (* REMEMBER: we have to instantiate meta_proof, we should use
2119 apply the "apply" tactic to proof and status
2121 let names = names_of_context context in
2122 print_endline (PP.pp proof names);
2125 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
2128 (* Printf.printf "OK, found a proof!\n"; *)
2129 (* (\* REMEMBER: we have to instantiate meta_proof, we should use *)
2130 (* apply the "apply" tactic to proof and status *)
2132 (* let names = names_of_context context in *)
2133 (* print_endline (PP.pp proof names); *)
2136 CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
2138 (* Printf.printf "OK, found a proof!\n"; *)
2139 (* (\* REMEMBER: we have to instantiate meta_proof, we should use *)
2140 (* apply the "apply" tactic to proof and status *)
2142 (* let names = names_of_context context in *)
2143 (* print_endline (PP.pp proof names); *)
2144 (* print_endline (PP.ppterm proof); *)
2146 print_endline (string_of_float (finish -. start));
2148 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
2149 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
2151 (fst (CicReduction.are_convertible
2152 context type_of_goal ty ug)));
2154 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
2155 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
2156 print_endline (string_of_float (finish -. start));
2160 | ParamodulationSuccess (None, env) ->
2161 Printf.printf "Success, but no proof?!?\n\n"
2163 Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
2164 "forward_simpl_new_time: %.9f\n" ^^
2165 "backward_simpl_time: %.9f\n")
2166 !infer_time !forward_simpl_time !forward_simpl_new_time
2167 !backward_simpl_time;
2168 Printf.printf "passive_maintainance_time: %.9f\n"
2169 !passive_maintainance_time;
2170 Printf.printf " successful unification/matching time: %.9f\n"
2171 !Indexing.match_unif_time_ok;
2172 Printf.printf " failed unification/matching time: %.9f\n"
2173 !Indexing.match_unif_time_no;
2174 Printf.printf " indexing retrieval time: %.9f\n"
2175 !Indexing.indexing_retrieval_time;
2176 Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
2177 !Indexing.build_newtarget_time;
2178 Printf.printf "derived %d clauses, kept %d clauses.\n"
2179 !derived_clauses !kept_clauses;
2181 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
2186 let default_depth = !maxdepth
2187 and default_width = !maxwidth;;
2191 symbols_counter := 0;
2192 weight_age_counter := !weight_age_ratio;
2193 processed_clauses := 0;
2196 maximal_retained_equality := None;
2198 forward_simpl_time := 0.;
2199 forward_simpl_new_time := 0.;
2200 backward_simpl_time := 0.;
2201 passive_maintainance_time := 0.;
2202 derived_clauses := 0;
2207 dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
2208 let module C = Cic in
2210 Indexing.init_index ();
2213 let proof, goal = status in
2215 let uri, metasenv, meta_proof, term_to_prove = proof in
2216 let _, context, goal = CicUtil.lookup_meta goal' metasenv in
2217 let eq_indexes, equalities, maxm = find_equalities context proof in
2218 let new_meta_goal, metasenv, type_of_goal =
2220 CicMkImplicit.identity_relocation_list_for_metavariable context in
2221 let _, context, ty = CicUtil.lookup_meta goal' metasenv in
2223 (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
2224 Cic.Meta (maxm+1, irl),
2225 (maxm+1, context, ty)::metasenv,
2228 let ugraph = CicUniv.empty_ugraph in
2229 let env = (metasenv, context, ugraph) in
2230 let goal = Inference.BasicProof new_meta_goal, [], goal in
2232 let lib_eq_uris, library_equalities, maxm =
2233 find_library_equalities dbd context (proof, goal') (maxm+2)
2237 let equalities = equalities @ library_equalities in
2240 (Printf.sprintf "equalities:\n%s\n"
2242 (List.map string_of_equality equalities))));
2243 debug_print (lazy "SIMPLYFYING EQUALITIES...");
2244 let rec simpl e others others_simpl =
2245 let active = others @ others_simpl in
2248 (fun t (_, e) -> Indexing.index t e)
2249 (Indexing.empty_table ()) active
2251 let res = forward_simplify env e (active, tbl) in
2255 | None -> simpl hd tl others_simpl
2256 | Some e -> simpl hd tl (e::others_simpl)
2260 | None -> others_simpl
2261 | Some e -> e::others_simpl
2264 match equalities with
2267 let others = List.map (fun e -> (Positive, e)) tl in
2269 List.rev (List.map snd (simpl (Positive, hd) others []))
2273 (Printf.sprintf "equalities AFTER:\n%s\n"
2275 (List.map string_of_equality res))));
2281 (* let u = eq_XURI () in *)
2282 (* let t = CicUtil.term_of_uri u in *)
2284 (* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *)
2288 (* let u = UriManager.uri_of_string *)
2289 (* "cic:/matita/nat/orders/le.ind#xpointer(1/1/2)" in *)
2290 (* let t = CicUtil.term_of_uri u in *)
2292 (* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *)
2295 (* let thms = refl_eq::le_S::[] in *)
2296 let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
2297 let context_hyp = find_context_hypotheses env eq_indexes in
2298 (* context_hyp @ thms *)
2302 let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
2303 UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
2305 let t = CicUtil.term_of_uri refl_equal in
2306 let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
2307 [], [(refl_equal, t, ty, [])]
2313 "Theorems:\n-------------------------------------\n%s\n"
2316 (fun (_, t, ty, _) ->
2318 "Term: %s, type: %s"
2319 (CicPp.ppterm t) (CicPp.ppterm ty))
2322 let active = make_active () in
2323 let passive = make_passive [(* term_equality *)] equalities in
2324 let start = Unix.gettimeofday () in
2325 (* let res = given_clause_fullred env [0, [goal]] theorems passive active in *)
2327 let goals = make_goals goal in
2328 (* and theorems = make_theorems theorems in *)
2329 given_clause_fullred dbd env goals theorems passive active
2331 let finish = Unix.gettimeofday () in
2332 (res, finish -. start)
2335 | ParamodulationSuccess (Some proof (* goal *), env) ->
2336 debug_print (lazy "OK, found a proof!");
2337 (* let proof = Inference.build_proof_term goal in *)
2338 let proof = Inference.build_proof_term proof in
2339 let names = names_of_context context in
2342 match new_meta_goal with
2343 | C.Meta (i, _) -> i | _ -> assert false
2345 List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
2350 CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
2352 debug_print (lazy (CicPp.pp proof [](* names *)));
2356 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
2357 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
2359 (fst (CicReduction.are_convertible
2360 context type_of_goal ty ug)))));
2361 let equality_for_replace i t1 =
2363 | C.Meta (n, _) -> n = i
2367 ProofEngineReduction.replace
2368 ~equality:equality_for_replace
2369 ~what:[goal'] ~with_what:[proof]
2374 (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
2375 (match uri with Some uri -> UriManager.string_of_uri uri
2377 (print_metasenv newmetasenv)
2378 (CicPp.pp real_proof [](* names *))
2379 (CicPp.pp term_to_prove names)));
2380 ((uri, newmetasenv, real_proof, term_to_prove), [])
2381 with CicTypeChecker.TypeCheckerFailure _ ->
2382 debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
2383 debug_print (lazy (CicPp.pp proof names));
2384 raise (ProofEngineTypes.Fail
2385 "Found a proof, but it doesn't typecheck")
2387 debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
2390 raise (ProofEngineTypes.Fail "NO proof found")
2393 (* dummy function called within matita to trigger linkage *)
2397 (* UGLY SIDE EFFECT... *)
2398 if connect_to_auto then (
2399 AutoTactic.paramodulation_tactic := saturate;
2400 AutoTactic.term_is_equality := Inference.term_is_equality;