|
(* 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.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
