# HG changeset patch
# User blanchet
# Date 1498143554 -7200
# Node ID 45d3d43abee7147fd43e63a6b4ba6340a5d4b74f
# Parent  65cd285f6b9cf3147b73a5d3a744582c7bbbaec2
added 'solvers' option to Nunchaku

diff -r 65cd285f6b9c -r 45d3d43abee7 src/HOL/Nunchaku/Nunchaku.thy
--- 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
diff -r 65cd285f6b9c -r 45d3d43abee7 src/HOL/Nunchaku/Tools/nunchaku.ML
--- 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
diff -r 65cd285f6b9c -r 45d3d43abee7 src/HOL/Nunchaku/Tools/nunchaku_commands.ML
--- 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 =
diff -r 65cd285f6b9c -r 45d3d43abee7 src/HOL/Nunchaku/Tools/nunchaku_tool.ML
--- 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;