Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)
(* Title: mirabelle_quickcheck.ML
Author: Jasmin Blanchette and Sascha Boehme
*)
structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct
fun quickcheck_action args {pre, timeout, log, ...} =
let
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
in
(case TimeLimit.timeLimit timeout quickcheck pre of
NONE => log "quickcheck: no counterexample"
| SOME _ => log "quickcheck: counterexample found")
end
handle TimeLimit.TimeOut => log "quickcheck: time out"
fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
end