src/HOL/Tools/Nunchaku/nunchaku_tool.ML

clarified name and status of auxiliary operation

(*  Title:      HOL/Tools/Nunchaku/nunchaku_tool.ML
    Author:     Jasmin Blanchette, VU Amsterdam
    Copyright   2015, 2016, 2017

Interface to the external "nunchaku" tool.
*)

signature NUNCHAKU_TOOL =
sig
  type ty = Nunchaku_Problem.ty
  type tm = Nunchaku_Problem.tm
  type nun_problem = Nunchaku_Problem.nun_problem

  type tool_params =
    {solvers: string list,
     overlord: bool,
     min_bound: int,
     max_bound: int option,
     bound_increment: int,
     debug: bool,
     specialize: bool,
     timeout: Time.time}

  type nun_solution =
    {tys: (ty * tm list) list,
     tms: (tm * tm) list}

  datatype nun_outcome =
    Unsat of string
  | Sat of string * string * nun_solution
  | Unknown of (string * string * nun_solution) option
  | Timeout
  | Nunchaku_Var_Not_Set
  | Nunchaku_Cannot_Execute
  | Nunchaku_Not_Found
  | Unknown_Error of int * string

  val nunchaku_home_env_var: string

  val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
end;

structure Nunchaku_Tool : NUNCHAKU_TOOL =
struct

open Nunchaku_Util;
open Nunchaku_Problem;

type tool_params =
  {solvers: string list,
   overlord: bool,
   min_bound: int,
   max_bound: int option,
   bound_increment: int,
   debug: bool,
   specialize: bool,
   timeout: Time.time};

type nun_solution =
  {tys: (ty * tm list) list,
   tms: (tm * tm) list};

datatype nun_outcome =
  Unsat of string
| Sat of string * string * nun_solution
| Unknown of (string * string * nun_solution) option
| Timeout
| Nunchaku_Var_Not_Set
| Nunchaku_Cannot_Execute
| Nunchaku_Not_Found
| Unknown_Error of int * string;

val nunchaku_home_env_var = "NUNCHAKU_HOME";

val unknown_solver = "unknown";

val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
  (NONE : ((tool_params * nun_problem) * nun_outcome) option);

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
      Nunchaku_Var_Not_Set
    else
      let
        val bash_cmd =
          "PATH=\"$CVC5_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
          nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
          (if specialize then "" else "--no-specialize ") ^
          "--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^
          "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
          "--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 ()];
        val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
        val _ = File.write prob_path prob_str;
        val res = Isabelle_System.bash_process (Bash.script bash_cmd);
        val rc = Process_Result.rc res;
        val out = Process_Result.out res;
        val err = Process_Result.err res;

        val backend =
          (case map_filter (try (unprefix "{backend:")) (split_lines out) of
            [s] => hd (space_explode "," s)
          | _ => unknown_solver);
      in
        if String.isPrefix "SAT" out then
          (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []})
        else if String.isPrefix "UNSAT" out then
          if complete then Unsat backend else Unknown NONE
        else if String.isSubstring "TIMEOUT" out
            (* FIXME: temporary *)
            orelse String.isSubstring "kodkod failed (errcode 152)" err then
          Timeout
        else if String.isPrefix "UNKNOWN" out then
          Unknown NONE
        else if rc = 126 then
          Nunchaku_Cannot_Execute
        else if rc = 127 then
          Nunchaku_Not_Found
        else
          Unknown_Error (rc,
            simplify_spaces (elide_string 1000 (if err <> "" then err else out)))
      end);

fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
  let val key = (params, problem) in
    (case (overlord orelse debug,
        AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of
      (false, SOME outcome) => outcome
    | _ =>
      let
        val outcome = uncached_solve_nun_problem params problem;

        fun update_cache () =
          Synchronized.change cached_outcome (K (SOME (key, outcome)));
      in
        (case outcome of
          Unsat _ => update_cache ()
        | Sat _ => update_cache ()
        | Unknown _ => update_cache ()
        | _ => ());
        outcome
      end)
  end;

end;