Mirabelle: added preliminary documentation,
Mirabelle: removed option "verbose",
Mirabelle: actions need to limit their execution time themselves,
sledgehammer: do not report chained facts
(* Title: mirabelle_quickcheck.ML
Author: Jasmin Blanchette and Sascha Boehme
*)
structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct
fun quickcheck_action limit args {pre=st, ...} =
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 limit quickcheck st of
NONE => SOME "no counterexample"
| SOME _ => SOME "counterexample found")
end
fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
end