--- a/src/HOL/Nunchaku/Nunchaku.thy Wed Oct 26 15:14:17 2016 +0200
+++ b/src/HOL/Nunchaku/Nunchaku.thy Wed Oct 26 15:21:16 2016 +0200
@@ -8,6 +8,10 @@
being actively developed. The sources are available at
https://github.com/nunchaku-inria
+
+The "$NUNCHAKU" environment variable must be set to the absolute file name of
+the "nunchaku" executable. The Isabelle components for CVC4 and Kodkodi are
+necessary to use these backends.
*)
theory Nunchaku
--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Wed Oct 26 15:14:17 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Wed Oct 26 15:21:16 2016 +0200
@@ -210,17 +210,16 @@
null whacks andalso null cards andalso null monos;
fun unknown () =
- (print_n ("No " ^ das_wort_model ^ " can be found \<midarrow> the problem lies \
- \outside Nunchaku's fragment");
+ (print_n ("No " ^ das_wort_model ^ " can be found\n\
+ \The problem lies outside Nunchaku's fragment, or the Nunchaku backends are not \
+ \installed properly");
(unknownN, NONE));
fun unsat_or_unknown complete =
if complete then
(print_n ("No " ^ das_wort_model ^ " exists" ^
- (if falsify andalso unsat_means_theorem () then
- " \<midarrow> the goal is a theorem"
- else
- ""));
+ (if falsify andalso unsat_means_theorem () then "\nThe goal is a theorem"
+ else ""));
(noneN, NONE))
else
unknown ();
--- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Wed Oct 26 15:14:17 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Wed Oct 26 15:21:16 2016 +0200
@@ -84,7 +84,7 @@
else
let
val bash_cmd =
- "\"$" ^ nunchaku_env_var ^ "\" \
+ "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ nunchaku_env_var ^ "\" \
\--skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^