let cond = Condition.create ();;
let mutex = Mutex.create ();;
let hint = ref None;;
+let prune_hint = ref [];;
let step _ = Condition.signal cond;;
let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+ prune_hint := hint :: !prune_hint
+;;
let check_pause _ =
if !in_pause then
aux todo
;;
-
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+ let s =
+ HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
+ in
+ List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint l =
+ let prune = !prune_hint in
+ prune_hint := []; (* possible race... *)
+ if prune = [] then l
+ else List.filter (condition_for_prune_hint prune) l
+;;
let auto_main tables maxm context flags universe cache elems =
auto_context := context;
let rec aux tables maxm flags cache (elems : status) =
auto_status := elems;
check_pause ();
*)
+ let elems = filter_prune_hint elems in
match elems with
- | (m, s, size, don, todo, fl)::orlist as status when !hint <> None ->
+ | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
(match !hint with
| Some i when condition_for_hint i todo ->
aux tables maxm flags cache orlist
let pp_proofterm = Equality.pp_proofterm;;
let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100