# HG changeset patch
# User blanchet
# Date 1477488076 -7200
# Node ID 5c5b9d945625c03b642c26023a17ac2ee5688fac
# Parent  492de9062cd22c62ba1541e6dcd63892b06fbc35
proper Nunchaku setup to use CVC4 and Kodkod

diff -r 492de9062cd2 -r 5c5b9d945625 src/HOL/Nunchaku/Nunchaku.thy
--- 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
diff -r 492de9062cd2 -r 5c5b9d945625 src/HOL/Nunchaku/Tools/nunchaku.ML
--- 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 ();
diff -r 492de9062cd2 -r 5c5b9d945625 src/HOL/Nunchaku/Tools/nunchaku_tool.ML
--- 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) ^ " " ^