# HG changeset patch
# User blanchet
# Date 1504821736 -7200
# Node ID 984c179a00d39ac379b6cf06ce0325087498fbdf
# Parent  556e19e43e4d412f5a0ac95ef95dbb279b33f235
more precise output for Nunchaku

diff -r 556e19e43e4d -r 984c179a00d3 src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:15 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:16 2017 +0200
@@ -137,8 +137,8 @@
 val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort);
 
 val unprefix_error =
-  perhaps (try (unprefix "Error: "))
-  #> perhaps (try (unprefix "failure: "));
+  perhaps (try (unprefix "failure: "))
+  #> perhaps (try (unprefix "Error: "));
 
 (* Give the soft timeout a chance. *)
 val timeout_slack = seconds 1.0;
@@ -219,20 +219,20 @@
             fun unknown () =
               (print_n ("No " ^ das_wort_model ^ " found"); (unknownN, NONE));
 
-            fun unsat_or_unknown complete =
+            fun unsat_or_unknown solver complete =
               if complete then
-                (print_n ("No " ^ das_wort_model ^ " exists" ^
+                (print_n ("No " ^ das_wort_model ^ " exists (according to " ^ solver ^ ")" ^
                    (if falsify andalso unsat_means_theorem () then "\nThe goal is a theorem"
                     else ""));
                  (noneN, NONE))
               else
                 unknown ();
 
-            fun sat_or_maybe_sat sound output =
+            fun sat_or_maybe_sat solver sound output =
               let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in
                 (case (null poly_axioms, none_true wfs) of
                   (true, true) =>
-                  (print (header ^ ":\n" ^
+                  (print (header ^ " (according to " ^ solver ^ "):\n" ^
                      model_str output); print_any_hints ();
                    (genuineN, isa_model_opt output))
                 | (no_poly, no_wf) =>
@@ -241,7 +241,8 @@
                       |> not no_poly ? cons "polymorphic axioms"
                       |> not no_wf ? cons "unchecked well-foundedness";
                   in
-                    (print (header ^ " (ignoring " ^ space_implode " and " ignorings ^ "):\n" ^
+                    (print (header ^ " (according to " ^ solver ^
+                       ", ignoring " ^ space_implode " and " ignorings ^ "):\n" ^
                        model_str output ^
                        (if no_poly then
                           ""
@@ -254,10 +255,10 @@
               end;
           in
             (case solve_nun_problem tool_params nice_nun_problem of
-              Unsat => unsat_or_unknown complete
-            | Sat (output, _) => sat_or_maybe_sat sound output
+              Unsat solver => unsat_or_unknown solver complete
+            | Sat (solver, output, _) => sat_or_maybe_sat solver sound output
             | Unknown NONE => unknown ()
-            | Unknown (SOME (output, _)) => sat_or_maybe_sat false output
+            | Unknown (SOME (solver, output, _)) => sat_or_maybe_sat solver false output
             | Timeout => (print_n "Time out"; (unknownN, NONE))
             | Nunchaku_Var_Not_Set =>
               (print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE))
diff -r 556e19e43e4d -r 984c179a00d3 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:15 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:16 2017 +0200
@@ -23,9 +23,9 @@
      tms: (tm * tm) list}
 
   datatype nun_outcome =
-    Unsat
-  | Sat of string * nun_solution
-  | Unknown of (string * nun_solution) option
+    Unsat of string
+  | Sat of string * string * nun_solution
+  | Unknown of (string * string * nun_solution) option
   | Timeout
   | Nunchaku_Var_Not_Set
   | Nunchaku_Cannot_Execute
@@ -57,9 +57,9 @@
    tms: (tm * tm) list};
 
 datatype nun_outcome =
-  Unsat
-| Sat of string * nun_solution
-| Unknown of (string * nun_solution) option
+  Unsat of string
+| Sat of string * string * nun_solution
+| Unknown of (string * string * nun_solution) option
 | Timeout
 | Nunchaku_Var_Not_Set
 | Nunchaku_Cannot_Execute
@@ -75,6 +75,8 @@
 
 val nunchaku_home_env_var = "NUNCHAKU_HOME";
 
+val unknown_solver = "unknown";
+
 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
   (NONE : ((string list * nun_problem) * nun_outcome) option);
 
@@ -97,11 +99,20 @@
         val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
         val _ = File.write prob_path prob_str;
         val ((output, error), code) = bash_output_error bash_cmd;
+
+        val backend =
+          (case filter_out (curry (op =) "") (split_lines output) of
+            [] => unknown_solver
+          | lines =>
+            (case try (unprefix "{backend:") (List.last lines) of
+              NONE => unknown_solver
+            | SOME "" => unknown_solver
+            | SOME s => hd (space_explode "," s)));
       in
         if String.isPrefix "SAT" output then
-          (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
+          (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []})
         else if String.isPrefix "UNSAT" output then
-          if complete then Unsat else Unknown NONE
+          if complete then Unsat backend else Unknown NONE
         else if String.isSubstring "TIMEOUT" output
             (* FIXME: temporary *)
             orelse String.isSubstring "kodkod failed (errcode 152)" error then
@@ -130,7 +141,7 @@
           Synchronized.change cached_outcome (K (SOME (key, outcome)));
       in
         (case outcome of
-          Unsat => update_cache ()
+          Unsat _ => update_cache ()
         | Sat _ => update_cache ()
         | Unknown _ => update_cache ()
         | _ => ());