Quelle nunchaku_tool.ML Sprache: SML

(*  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;

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.