# 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 ()];