added Nunchaku component and tuned Nunchaku integration accordingly
authorblanchet
Mon Nov 07 14:55:39 2016 +0100 (2016-11-07)
changeset 64469488d4e627238
parent 64468 ed8940d6295c
child 64470 85bb70e1260b
added Nunchaku component and tuned Nunchaku integration accordingly
Admin/components/components.sha1
Admin/components/main
src/HOL/Nunchaku/Nunchaku.thy
src/HOL/Nunchaku/Tools/nunchaku.ML
src/HOL/Nunchaku/Tools/nunchaku_tool.ML
     1.1 --- a/Admin/components/components.sha1	Sun Nov 06 22:51:40 2016 +0100
     1.2 +++ b/Admin/components/components.sha1	Mon Nov 07 14:55:39 2016 +0100
     1.3 @@ -115,6 +115,7 @@
     1.4  377e36efb8608e6c828c7718d890e97fde2006a4  linux_app-20131007.tar.gz
     1.5  0aab4f73ff7f5e36f33276547e10897e1e56fb1d  macos_app-20130716.tar.gz
     1.6  ad5d0e640ce3609a885cecab645389a2204e03bb  macos_app-20150916.tar.gz
     1.7 +26df569cee9c2fd91b9ac06714afd43f3b37a1dd  nunchaku-0.3.tar.gz
     1.8  1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb  polyml-5.4.1.tar.gz
     1.9  a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56  polyml-5.5.0-1.tar.gz
    1.10  7d604a99355efbfc1459d80db3279ffa7ade3e39  polyml-5.5.0-2.tar.gz
     2.1 --- a/Admin/components/main	Sun Nov 06 22:51:40 2016 +0100
     2.2 +++ b/Admin/components/main	Mon Nov 07 14:55:39 2016 +0100
     2.3 @@ -9,6 +9,7 @@
     2.4  jfreechart-1.0.14-1
     2.5  jortho-1.0-2
     2.6  kodkodi-1.5.2
     2.7 +nunchaku-0.3
     2.8  polyml-5.6-1
     2.9  scala-2.11.8
    2.10  ssh-java-20161009
     3.1 --- a/src/HOL/Nunchaku/Nunchaku.thy	Sun Nov 06 22:51:40 2016 +0100
     3.2 +++ b/src/HOL/Nunchaku/Nunchaku.thy	Mon Nov 07 14:55:39 2016 +0100
     3.3 @@ -9,9 +9,9 @@
     3.4  
     3.5      https://github.com/nunchaku-inria
     3.6  
     3.7 -The "$NUNCHAKU" environment variable must be set to the absolute file name of
     3.8 -the "nunchaku" executable. The Isabelle components for CVC4 and Kodkodi are
     3.9 -necessary to use these backends.
    3.10 +The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
    3.11 +the directory containing the "nunchaku" executable. The Isabelle components
    3.12 +for CVC4 and Kodkodi are necessary to use these backends.
    3.13  *)
    3.14  
    3.15  theory Nunchaku
     4.1 --- a/src/HOL/Nunchaku/Tools/nunchaku.ML	Sun Nov 06 22:51:40 2016 +0100
     4.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku.ML	Mon Nov 07 14:55:39 2016 +0100
     4.3 @@ -256,7 +256,7 @@
     4.4              | Unknown (SOME (output, _)) => sat_or_maybe_sat false output
     4.5              | Timeout => (print_n "Time out"; (unknownN, NONE))
     4.6              | Nunchaku_Var_Not_Set =>
     4.7 -              (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE))
     4.8 +              (print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE))
     4.9              | Nunchaku_Cannot_Execute =>
    4.10                (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
    4.11              | Nunchaku_Not_Found =>
     5.1 --- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML	Sun Nov 06 22:51:40 2016 +0100
     5.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML	Mon Nov 07 14:55:39 2016 +0100
     5.3 @@ -33,7 +33,7 @@
     5.4    | CVC4_Not_Found
     5.5    | Unknown_Error of int * string
     5.6  
     5.7 -  val nunchaku_env_var: string
     5.8 +  val nunchaku_home_env_var: string
     5.9  
    5.10    val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
    5.11  end;
    5.12 @@ -71,7 +71,7 @@
    5.13      ((out, err), rc)
    5.14    end;
    5.15  
    5.16 -val nunchaku_env_var = "NUNCHAKU";
    5.17 +val nunchaku_home_env_var = "NUNCHAKU_HOME";
    5.18  
    5.19  val cached_outcome =
    5.20    Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
    5.21 @@ -79,13 +79,13 @@
    5.22  fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
    5.23      (problem as {sound, complete, ...}) =
    5.24    with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
    5.25 -    if getenv nunchaku_env_var = "" then
    5.26 +    if getenv nunchaku_home_env_var = "" then
    5.27        Nunchaku_Var_Not_Set
    5.28      else
    5.29        let
    5.30          val bash_cmd =
    5.31 -          "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ nunchaku_env_var ^ "\" \
    5.32 -          \--skolems-in-model --no-color " ^
    5.33 +          "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
    5.34 +          nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
    5.35            (if specialize then "" else "--no-specialize ") ^
    5.36            "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
    5.37            File.bash_path prob_path;
    5.38 @@ -99,10 +99,12 @@
    5.39            (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
    5.40          else if String.isPrefix "UNSAT" output then
    5.41            if complete then Unsat else Unknown NONE
    5.42 +        else if String.isSubstring "TIMEOUT" output
    5.43 +            (* FIXME: temporary *)
    5.44 +            orelse String.isSubstring "kodkod failed (errcode 152)" error then
    5.45 +          Timeout
    5.46          else if String.isPrefix "UNKNOWN" output then
    5.47            Unknown NONE
    5.48 -        else if String.isPrefix "TIMEOUT" output then
    5.49 -          Timeout
    5.50          else if code = 126 then
    5.51            Nunchaku_Cannot_Execute
    5.52          else if code = 127 then