--- a/src/HOL/Nunchaku/Nunchaku.thy Thu Jun 22 10:50:18 2017 +0200
+++ b/src/HOL/Nunchaku/Nunchaku.thy Thu Jun 22 16:59:14 2017 +0200
@@ -11,7 +11,7 @@
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4 and Kodkodi are necessary to use these backends.
+for CVC4 and Kodkodi are necessary to use these backend solvers.
*)
theory Nunchaku
--- 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
--- a/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Thu Jun 22 10:50:18 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Thu Jun 22 16:59:14 2017 +0200
@@ -27,6 +27,7 @@
("max_genuine", "1"),
("max_potential", "1"),
("overlord", "false"),
+ ("solvers", "cvc4 kodkod paradox smbc"),
("specialize", "true"),
("spy", "false"),
("timeout", "30"),
@@ -100,6 +101,7 @@
val raw_lookup = AList.lookup (op =) raw_params;
val lookup = Option.map stringify_raw_param_value o raw_lookup;
val lookup_string = the_default "" o lookup;
+ val lookup_strings = these o Option.map (space_explode " ") o lookup;
fun general_lookup_bool option default_value name =
(case lookup name of
@@ -161,28 +163,33 @@
Const x => x
| t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t));
+ val solvers = lookup_strings "solvers";
+ val falsify = lookup_bool "falsify";
+ val assms = lookup_bool "assms";
+ val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
+ val overlord = lookup_bool "overlord";
+ val expect = lookup_string "expect";
+
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
val whacks = lookup_bool_assigns read_term_polymorphic "whack";
val cards = lookup_int_range_assigns read_type_polymorphic "card";
val monos = lookup_bool_option_assigns read_type_polymorphic "mono";
- val falsify = lookup_bool "falsify";
+
val debug = (mode <> Auto_Try andalso lookup_bool "debug");
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose");
- val overlord = lookup_bool "overlord";
- val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
- val assms = lookup_bool "assms";
+ val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
+ val max_genuine = Int.max (0, lookup_int "max_genuine");
+ val evals = these (lookup_term_list_option_polymorphic "eval");
+ val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
+
val specialize = lookup_bool "specialize";
+ val multithread = mode = Normal andalso lookup_bool "multithread";
+
val timeout = lookup_time "timeout";
val wf_timeout = lookup_time "wf_timeout";
- val multithread = mode = Normal andalso lookup_bool "multithread";
- val evals = these (lookup_term_list_option_polymorphic "eval");
- val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
- val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
- val max_genuine = Int.max (0, lookup_int "max_genuine");
- val expect = lookup_string "expect";
val mode_of_operation_params =
- {falsify = falsify, assms = assms, spy = spy, overlord = overlord,
+ {solvers = solvers, falsify = falsify, assms = assms, spy = spy, overlord = overlord,
expect = expect};
val scope_of_search_params =
--- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Thu Jun 22 10:50:18 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Thu Jun 22 16:59:14 2017 +0200
@@ -12,7 +12,8 @@
type nun_problem = Nunchaku_Problem.nun_problem
type tool_params =
- {overlord: bool,
+ {solvers: string list,
+ overlord: bool,
debug: bool,
specialize: bool,
timeout: Time.time}
@@ -45,7 +46,8 @@
open Nunchaku_Problem;
type tool_params =
- {overlord: bool,
+ {solvers: string list,
+ overlord: bool,
debug: bool,
specialize: bool,
timeout: Time.time};
@@ -73,10 +75,10 @@
val nunchaku_home_env_var = "NUNCHAKU_HOME";
-val cached_outcome =
- Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
+val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
+ (NONE : ((string list * nun_problem) * nun_outcome) option);
-fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
+fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params)
(problem as {sound, complete, ...}) =
with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
if getenv nunchaku_home_env_var = "" then
@@ -87,6 +89,7 @@
"PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
+ "--solvers \"" ^ Bash_Syntax.string (space_implode " " solvers) ^ "\" " ^
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
File.bash_path prob_path;
val comments =
@@ -114,23 +117,25 @@
simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
end);
-fun solve_nun_problem (params as {overlord, debug, ...}) problem =
- (case (overlord orelse debug,
- AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) problem) of
- (false, SOME outcome) => outcome
- | _ =>
- let
- val outcome = uncached_solve_nun_problem params problem;
+fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
+ let val key = (solvers, problem) in
+ (case (overlord orelse debug,
+ AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of
+ (false, SOME outcome) => outcome
+ | _ =>
+ let
+ val outcome = uncached_solve_nun_problem params problem;
- fun update_cache () =
- Synchronized.change cached_outcome (K (SOME (problem, outcome)));
- in
- (case outcome of
- Unsat => update_cache ()
- | Sat _ => update_cache ()
- | Unknown _ => update_cache ()
- | _ => ());
- outcome
- end);
+ fun update_cache () =
+ Synchronized.change cached_outcome (K (SOME (key, outcome)));
+ in
+ (case outcome of
+ Unsat => update_cache ()
+ | Sat _ => update_cache ()
+ | Unknown _ => update_cache ()
+ | _ => ());
+ outcome
+ end)
+ end;
end;