# HG changeset patch # User blanchet # Date 1504821750 -7200 # Node ID 4145169ae609d20c4243032f0aba15c990f97760 # Parent e3dccf7725a380d747609e9c9a0f724786e020c9 extended and renamed Nunchaku's Kodkod bounds diff -r e3dccf7725a3 -r 4145169ae609 src/HOL/Tools/Nunchaku/nunchaku.ML --- 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}; diff -r e3dccf7725a3 -r 4145169ae609 src/HOL/Tools/Nunchaku/nunchaku_commands.ML --- 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, diff -r e3dccf7725a3 -r 4145169ae609 src/HOL/Tools/Nunchaku/nunchaku_tool.ML --- 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 ()];