--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Jun 22 10:50:18 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Jun 22 16:59:14 2017 +0200
@@ -12,7 +12,8 @@
datatype mode = Auto_Try | Try | Normal
type mode_of_operation_params =
- {falsify: bool,
+ {solvers: string list,
+ falsify: bool,
assms: bool,
spy: bool,
overlord: bool,
@@ -74,7 +75,8 @@
datatype mode = Auto_Try | Try | Normal;
type mode_of_operation_params =
- {falsify: bool,
+ {solvers: string list,
+ falsify: bool,
assms: bool,
spy: bool,
overlord: bool,
@@ -138,7 +140,7 @@
val timeout_slack = seconds 1.0;
fun run_chaku_on_prop state
- ({mode_of_operation_params = {falsify, assms, spy, overlord, expect},
+ ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect},
scope_of_search_params = {wfs, whacks, cards, monos},
output_format_params = {verbose, debug, evals, atomss, ...},
optimization_params = {specialize, ...},
@@ -157,8 +159,9 @@
val das_wort_Model = if falsify then "Countermodel" else "Model";
val das_wort_model = if falsify then "countermodel" else "model";
- val tool_params = {overlord = overlord, debug = debug, specialize = specialize,
- timeout = timeout};
+ val tool_params =
+ {solvers = solvers, overlord = overlord, debug = debug, specialize = specialize,
+ timeout = timeout};
fun run () =
let