extended and renamed Nunchaku's Kodkod bounds

--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:25 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:30 2017 +0200
@@ -22,7 +22,8 @@
   type scope_of_search_params =
     {wfs: ((string * typ) option * bool option) list,
      whacks: (term option * bool) list,
-     initial_bound: int,
+     min_bound: int,
+     max_bound: int option,
      bound_increment: int,
      cards: (typ option * (int option * int option)) list,
      monos: (typ option * bool option) list}
@@ -87,7 +88,8 @@
 type scope_of_search_params =
   {wfs: ((string * typ) option * bool option) list,
    whacks: (term option * bool) list,
-   initial_bound: int,
+   min_bound: int,
+   max_bound: int option,
    bound_increment: int,
    cards: (typ option * (int option * int option)) list,
    monos: (typ option * bool option) list};
@@ -149,7 +151,7 @@
 
 fun run_chaku_on_prop state
     ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect},
-      scope_of_search_params = {wfs, whacks, initial_bound, bound_increment, cards, monos},
+      scope_of_search_params = {wfs, whacks, min_bound, max_bound, bound_increment, cards, monos},
       output_format_params = {verbose, debug, evals, atomss, ...},
       optimization_params = {specialize, ...},
       timeout_params = {timeout, wf_timeout}})
@@ -168,7 +170,7 @@
     val das_wort_model = if falsify then "countermodel" else "model";
 
     val tool_params =
-      {solvers = solvers, overlord = overlord, initial_bound = initial_bound,
+      {solvers = solvers, overlord = overlord, min_bound = min_bound, max_bound = max_bound,
        bound_increment = bound_increment, debug = debug, specialize = specialize,
        timeout = timeout};
 

--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:25 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:30 2017 +0200
@@ -25,7 +25,8 @@
    ("bound_increment", "2"),
    ("debug", "false"),
    ("falsify", "true"),
-   ("initial_bound", "2"),
+   ("min_bound", "2"),
+   ("max_bound", "none"),
    ("max_genuine", "1"),
    ("max_potential", "1"),
    ("overlord", "false"),
@@ -164,6 +165,7 @@
       #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type;
     val read_term_polymorphic =
       Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt);
+
     val lookup_term_list_option_polymorphic =
       AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic);
 
@@ -172,6 +174,11 @@
         Const x => x
       | t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t));
 
+    fun lookup_none_option lookup' name =
+      (case lookup name of
+        SOME "none" => NONE
+      | _ => SOME (lookup' name))
+
     val solvers = lookup_strings "solvers";
     val falsify = lookup_bool "falsify";
     val assms = lookup_bool "assms";
@@ -180,7 +187,8 @@
     val expect = lookup_string "expect";
 
     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
-    val initial_bound = lookup_int "initial_bound";
+    val min_bound = lookup_int "min_bound";
+    val max_bound = lookup_none_option lookup_int "max_bound";
     val bound_increment = lookup_int "bound_increment";
     val whacks = lookup_bool_assigns read_term_polymorphic "whack";
     val cards = lookup_int_range_assigns read_type_polymorphic "card";
@@ -204,8 +212,8 @@
        expect = expect};
 
     val scope_of_search_params =
-      {wfs = wfs, whacks = whacks, initial_bound = initial_bound, bound_increment = bound_increment,
-       cards = cards, monos = monos};
+      {wfs = wfs, whacks = whacks, min_bound = min_bound, max_bound = max_bound,
+       bound_increment = bound_increment, cards = cards, monos = monos};
 
     val output_format_params =
       {verbose = verbose, debug = debug, max_potential = max_potential, max_genuine = max_genuine,

--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:25 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:30 2017 +0200
@@ -14,7 +14,8 @@
   type tool_params =
     {solvers: string list,
      overlord: bool,
-     initial_bound: int,
+     min_bound: int,
+     max_bound: int option,
      bound_increment: int,
      debug: bool,
      specialize: bool,
@@ -50,7 +51,8 @@
 type tool_params =
   {solvers: string list,
    overlord: bool,
-   initial_bound: int,
+   min_bound: int,
+   max_bound: int option,
    bound_increment: int,
    debug: bool,
    specialize: bool,
@@ -84,8 +86,8 @@
 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
   (NONE : ((tool_params * nun_problem) * nun_outcome) option);
 
-fun uncached_solve_nun_problem
-    ({solvers, overlord, initial_bound, bound_increment, specialize, timeout, ...} : tool_params)
+fun uncached_solve_nun_problem ({solvers, overlord, min_bound, max_bound, bound_increment,
+      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
@@ -98,8 +100,9 @@
           (if specialize then "" else "--no-specialize ") ^
           "--solvers \"" ^ space_implode "," (map Bash_Syntax.string solvers) ^ "\" " ^
           "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
-          "--kodkod-initial-size " ^ string_of_int initial_bound ^ " " ^
-          "--kodkod-size-increment " ^ string_of_int bound_increment ^ " " ^
+          "--kodkod-min-bound " ^ string_of_int min_bound ^ " " ^
+          (case max_bound of NONE => "" | SOME n => "--kodkod-max-bound " ^ string_of_int n ^ " ") ^
+          "--kodkod-bound-increment " ^ string_of_int bound_increment ^ " " ^
           File.bash_path prob_path;
         val comments =
           [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];