--- a/src/Tools/auto_counterexample.ML Mon Sep 13 16:44:20 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: Tools/auto_counterexample.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Counterexample Search Unit (do not abbreviate!).
-*)
-
-signature AUTO_COUNTEREXAMPLE =
-sig
- val time_limit: int Unsynchronized.ref
-
- val register_tool :
- string * (Proof.state -> bool * Proof.state) -> theory -> theory
-end;
-
-structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
-struct
-
-(* preferences *)
-
-val time_limit = Unsynchronized.ref 2500
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.nat_pref time_limit
- "auto-counterexample-time-limit"
- "Time limit for automatic counterexample search (in milliseconds).")
-
-
-(* configuration *)
-
-structure Data = Theory_Data
-(
- type T = (string * (Proof.state -> bool * Proof.state)) list
- val empty = []
- val extend = I
- fun merge data : T = AList.merge (op =) (K true) data
-)
-
-val register_tool = Data.map o AList.update (op =)
-
-
-(* automatic testing *)
-
-val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- case !time_limit of
- 0 => state
- | ms =>
- TimeLimit.timeLimit (Time.fromMilliseconds ms)
- (fn () =>
- if interact andalso not (!Toplevel.quiet) then
- fold_rev (fn (_, tool) => fn (true, state) => (true, state)
- | (false, state) => tool state)
- (Data.get (Proof.theory_of state)) (false, state) |> snd
- else
- state) ()
- handle TimeLimit.TimeOut =>
- (warning "Automatic counterexample search timed out."; state)))
-
-end;