Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: nunchaku_tool.ML Sprache: SML

Original von: Isabelle^©

(*  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
  | 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,
   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
| 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 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=\"$CVC4_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 ((output, error), code) = bash_output_error bash_cmd;

        val backend =
          (case map_filter (try (unprefix "{backend:")) (split_lines output) of
            [s] => hd (space_explode "," s)
          | _ => unknown_solver);
      in
        if String.isPrefix "SAT" output then
          (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []})
        else if String.isPrefix "UNSAT" output then
          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
          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 = (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;

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.