src/HOL/Nunchaku/Tools/nunchaku_tool.ML

added Nunchaku integration

(*  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 =
    {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_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 =
  {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_env_var = "NUNCHAKU";

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

fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
    (problem as {sound, complete, ...}) =
  with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
    if getenv nunchaku_env_var = "" then
      Nunchaku_Var_Not_Set
    else
      let
        val bash_cmd =
          "\"$" ^ nunchaku_env_var ^ "\" \
          \--skolems-in-model --no-color " ^
          (if specialize then "" else "--no-specialize ") ^
          "--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.isPrefix "UNKNOWN" output then
          Unknown NONE
        else if String.isPrefix "TIMEOUT" output then
          Timeout
        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 {overlord, debug, ...}) problem =
  (case (overlord orelse debug,
      AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) problem) of
    (false, SOME outcome) => outcome
  | _ =>
    let
      val outcome = uncached_solve_nun_problem params problem;

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

end;