diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index c522ab49e74d876adaef806ad24a51e718581a89..ea1615c44a3bf77ecf00f8a8443e243dc074205f 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -1151,11 +1151,14 @@ let create_rem_list = Buffer.contents b +exception CannotRunBisectionOn of proofAttemptID + + let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_id = let ses = c.controller_session in let pa = get_proof_attempt_node ses pa_id in if not (proof_is_complete pa) then - invalid_arg "bisect: proof attempt should be valid"; + raise (CannotRunBisectionOn pa_id); (* proof attempt should be valid *) let goal_id = pa.parent in let prover = pa.prover in let limit = { pa.limit with @@ -1221,12 +1224,12 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i *) let rem = create_rem_list rem in let callback st = - callback_tr "remove" [rem] st; begin match st with | TSscheduled -> Debug.dprintf debug - "[Bisect] transformation 'remove' scheduled@." + "[Bisect] transformation 'remove' scheduled@."; + callback_tr "remove" [rem] st; | TSfailed(_,exn) -> (* may happen if removing a type or a lsymbol that is used later on. We do has if proof fails. *) @@ -1244,6 +1247,7 @@ later on. We do has if proof fails. *) Debug.dprintf debug "[Bisect] transformation 'remove' succeeds@."; + callback_tr "remove" [rem] st; match get_sub_tasks ses trid with | [pn] -> let limit = { limit with Call_provers.limit_time = !timelimit; } in diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli index 85bd76b4a91a2ccc08f6880e45ad984f3ce28d31..21e7c44fae2ccfcf89be457af7e37a4d1137dbdf 100644 --- a/src/session/controller_itp.mli +++ b/src/session/controller_itp.mli @@ -343,6 +343,7 @@ val replay: *) +exception CannotRunBisectionOn of proofAttemptID val bisect_proof_attempt: callback_tr:(string -> string list -> transformation_status -> unit) -> @@ -350,5 +351,23 @@ val bisect_proof_attempt: notification:notifier -> removed:notifier -> controller -> proofAttemptID -> unit - + (** [bisect_proof_attempt ~callback_tr ~callback_pa ~notification + ~removed cont id] runs a bisection process + based on the proof attempt [id] of the session managed by [cont]. + + The proof attempt [id] must be a successful one, otherwise, + exception [CannotRunBisectionOn id] is raised. + + Bisection tries to remove from the context the largest number of + definitions and axioms, using the `remove` transformation (bound + to [Cut.remove_list]). It proceeeds by dichotomy of the + context. Note that there is no garantee that the removed data at + the end is globally maximal. During that process, [callback_tr] + is called each time the `remove` transformation is added to the session, + [callback_pa] is called each time the prover is called on a + reduced task, [notification] is called when a proof node is + created or modified, and [removed] is called when a node is + removed. + + *) end diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 8406dc29b574b5ffbf2ce5148a719128a028cde2..39b748530bd02ea7309805fbc41d09bd142dd6c9 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -1197,6 +1197,11 @@ end (Message (Information "for bisection please select some proof attempt")) + | C.CannotRunBisectionOn _ -> + P.notify + (Message + (Error + "for bisection please select a successful proof attempt")) (* ----------------- run strategy -------------------- *)