src/HOL/Nunchaku/Tools/nunchaku_tool.ML

added 'solvers' option to Nunchaku

(*  Title:      HOL/Nunchaku/Tools/nunchaku_tool.ML
    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
    Copyright   2015, 2016

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,
     debug: bool,
     specialize: bool,
     timeout: Time.time}

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

  datatype nun_outcome =
    Unsat
  | Sat of string * nun_solution
  | Unknown of (string * nun_solution) option
  | Timeout
  | Nunchaku_Var_Not_Set
  | Nunchaku_Cannot_Execute
  | Nunchaku_Not_Found
  | CVC4_Cannot_Execute
  | CVC4_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,
   debug: bool,
   specialize: bool,
   timeout: Time.time};

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

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

fun bash_output_error s =
  let val {out, err, rc, ...} = Bash.process s in
    ((out, err), rc)
  end;

val nunchaku_home_env_var = "NUNCHAKU_HOME";

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

fun uncached_solve_nun_problem ({solvers, overlord, 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=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
          nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
          (if specialize then "" else "--no-specialize ") ^
          "--solvers \"" ^ Bash_Syntax.string (space_implode " " solvers) ^ "\" " ^
          "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
          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 ((output, error), code) = bash_output_error bash_cmd;
      in
        if String.isPrefix "SAT" output then
          (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
        else if String.isPrefix "UNSAT" output then
          if complete then Unsat else Unknown NONE
        else if String.isSubstring "TIMEOUT" output
            (* FIXME: temporary *)
            orelse String.isSubstring "kodkod failed (errcode 152)" error then
          Timeout
        else if String.isPrefix "UNKNOWN" output then
          Unknown NONE
        else if code = 126 then
          Nunchaku_Cannot_Execute
        else if code = 127 then
          Nunchaku_Not_Found
        else
          Unknown_Error (code,
            simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
      end);

fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
  let val key = (solvers, 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;