# HG changeset patch
# User blanchet
# Date 1504821744 -7200
# Node ID 2cd22f0709293b272727a5819aa61380d6c49d5f
# Parent  308ebcd2f5dca764c00adf4a31776226fa31f34e
added Kodkod-specific options to Nunchaku

diff -r 308ebcd2f5dc -r 2cd22f070929 src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:22 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:24 2017 +0200
@@ -22,6 +22,8 @@
   type scope_of_search_params =
     {wfs: ((string * typ) option * bool option) list,
      whacks: (term option * bool) list,
+     initial_bound: int,
+     bound_increment: int,
      cards: (typ option * (int option * int option)) list,
      monos: (typ option * bool option) list}
 
@@ -85,6 +87,8 @@
 type scope_of_search_params =
   {wfs: ((string * typ) option * bool option) list,
    whacks: (term option * bool) list,
+   initial_bound: int,
+   bound_increment: int,
    cards: (typ option * (int option * int option)) list,
    monos: (typ option * bool option) list};
 
@@ -145,7 +149,7 @@
 
 fun run_chaku_on_prop state
     ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect},
-      scope_of_search_params = {wfs, whacks, cards, monos},
+      scope_of_search_params = {wfs, whacks, initial_bound, bound_increment, cards, monos},
       output_format_params = {verbose, debug, evals, atomss, ...},
       optimization_params = {specialize, ...},
       timeout_params = {timeout, wf_timeout}})
@@ -164,7 +168,8 @@
     val das_wort_model = if falsify then "countermodel" else "model";
 
     val tool_params =
-      {solvers = solvers, overlord = overlord, debug = debug, specialize = specialize,
+      {solvers = solvers, overlord = overlord, initial_bound = initial_bound,
+       bound_increment = bound_increment, debug = debug, specialize = specialize,
        timeout = timeout};
 
     fun run () =
diff -r 308ebcd2f5dc -r 2cd22f070929 src/HOL/Tools/Nunchaku/nunchaku_commands.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:22 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:24 2017 +0200
@@ -22,8 +22,10 @@
 
 val default_default_params =
   [("assms", "true"),
+   ("bound_increment", "2"),
    ("debug", "false"),
    ("falsify", "true"),
+   ("initial_bound", "2"),
    ("max_genuine", "1"),
    ("max_potential", "1"),
    ("overlord", "false"),
@@ -178,6 +180,8 @@
     val expect = lookup_string "expect";
 
     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
+    val initial_bound = lookup_int "initial_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";
     val monos = lookup_bool_option_assigns read_type_polymorphic "mono";
@@ -200,7 +204,8 @@
        expect = expect};
 
     val scope_of_search_params =
-      {wfs = wfs, whacks = whacks, cards = cards, monos = monos};
+      {wfs = wfs, whacks = whacks, initial_bound = initial_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,
diff -r 308ebcd2f5dc -r 2cd22f070929 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:22 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:24 2017 +0200
@@ -14,6 +14,8 @@
   type tool_params =
     {solvers: string list,
      overlord: bool,
+     initial_bound: int,
+     bound_increment: int,
      debug: bool,
      specialize: bool,
      timeout: Time.time}
@@ -48,6 +50,8 @@
 type tool_params =
   {solvers: string list,
    overlord: bool,
+   initial_bound: int,
+   bound_increment: int,
    debug: bool,
    specialize: bool,
    timeout: Time.time};
@@ -80,7 +84,8 @@
 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
   (NONE : ((string list * nun_problem) * nun_outcome) option);
 
-fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params)
+fun uncached_solve_nun_problem
+    ({solvers, overlord, initial_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
@@ -93,6 +98,8 @@
           (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 ^ " " ^
           File.bash_path prob_path;
         val comments =
           [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];