<commit_before>(*  Title:      HOL/Tools/SMT2/smt2_solver.ML
    Author:     <NAME>, <NAME>

SMT solvers registry and SMT tactic.
*)

signature SMT2_SOLVER =
sig
  (*configuration*)
  datatype outcome = Unsat | Sat | Unknown
  type solver_config = {
    name: string,
    class: Proof.context -> SMT2_Utils.class,
    avail: unit -> bool,
    command: unit -> string list,
    options: Proof.context -> string list,
    default_max_relevant: int,
    supports_filter: bool,
    outcome: string -> string list -> outcome * string list,
    cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
      term list * term list) option,
    replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
      (int list * Z3_New_Proof.z3_step list) * thm) option }

  (*registry*)
  val add_solver: solver_config -> theory -> theory
  val solver_name_of: Proof.context -> string
  val available_solvers_of: Proof.context -> string list
  val apply_solver: Proof.context -> (int * (int option * thm)) list ->
    (int list * Z3_New_Proof.z3_step list) * thm
  val default_max_relevant: Proof.context -> string -> int

  (*filter*)
  val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int ->
    Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list,
      z3_steps: Z3_New_Proof.z3_step list}

  (*tactic*)
  val smt2_tac: Proof.context -> thm list -> int -> tactic
  val smt2_tac': Proof.context -> thm list -> int -> tactic
end

structure SMT2_Solver: SMT2_SOLVER =
struct


(* interface to external solvers *)

local

fun make_cmd command options problem_path proof_path = space_implode " " (
  "(exec 2>&1;" :: map File.shell_quote (command @ options) @
  [File.shell_path problem_path, ")", ">", File.shell_path proof_path])

fun trace_and ctxt msg f x =
  let val _ = SMT2_Config.trace_msg ctxt (fn () => msg) ()
  in f x end

fun run ctxt name mk_cmd input =
  (case SMT2_Config.certificates_of ctxt of
    NONE =>
      if not (SMT2_Config.is_available ctxt name) then
        error ("The SMT solver " ^ quote name ^ " is not installed.")
      else if Config.get ctxt SMT2_Config.debug_files = "" then
        trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
          (Cache_IO.run mk_cmd) input
      else
        let
          val base_path = Path.explode (Config.get ctxt SMT2_Config.debug_files)
          val in_path = Path.ext "smt2_in" base_path
          val out_path = Path.ext "smt2_out" base_path
        in Cache_IO.raw_run mk_cmd input in_path out_path end
  | SOME certs =>
      (case Cache_IO.lookup certs input of
        (NONE, key) =>
          if Config.get ctxt SMT2_Config.read_only_certificates then
            error ("Bad certificate cache: missing certificate")
          else
            Cache_IO.run_and_cache certs key mk_cmd input
      | (SOME output, _) =>
          trace_and ctxt ("Using cached certificate from " ^
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
            I output))

fun run_solver ctxt name mk_cmd input =
  let
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
      (map Pretty.str ls))

    val _ = SMT2_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input

    val {redirected_output=res, output=err, return_code} =
      SMT2_Config.with_timeout ctxt (run ctxt name mk_cmd) input
    val _ = SMT2_Config.trace_msg ctxt (pretty "Solver:") err

    val output = fst (take_suffix (equal "") res)
    val _ = SMT2_Config.trace_msg ctxt (pretty "Result:") output

    val _ = return_code <> 0 andalso<commit_msg>slacker error code policy for Z3<commit_after>(*  Title:      HOL/Tools/SMT2/smt2_solver.ML
    Author:     <NAME>, <NAME>

SMT solvers registry and SMT tactic.
*)

signature SMT2_SOLVER =
sig
  (*configuration*)
  datatype outcome = Unsat | Sat | Unknown
  type solver_config = {
    name: string,
    class: Proof.context -> SMT2_Utils.class,
    avail: unit -> bool,
    command: unit -> string list,
    options: Proof.context -> string list,
    default_max_relevant: int,
    supports_filter: bool,
    outcome: string -> string list -> outcome * string list,
    cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
      term list * term list) option,
    replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
      (int list * Z3_New_Proof.z3_step list) * thm) option }

  (*registry*)
  val add_solver: solver_config -> theory -> theory
  val solver_name_of: Proof.context -> string
  val available_solvers_of: Proof.context -> string list
  val apply_solver: Proof.context -> (int * (int option * thm)) list ->
    (int list * Z3_New_Proof.z3_step list) * thm
  val default_max_relevant: Proof.context -> string -> int

  (*filter*)
  val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int ->
    Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list,
      z3_steps: Z3_New_Proof.z3_step list}

  (*tactic*)
  val smt2_tac: Proof.context -> thm list -> int -> tactic
  val smt2_tac': Proof.context -> thm list -> int -> tactic
end

structure SMT2_Solver: SMT2_SOLVER =
struct


(* interface to external solvers *)

local

fun make_cmd command options problem_path proof_path = space_implode " " (
  "(exec 2>&1;" :: map File.shell_quote (command @ options) @
  [File.shell_path problem_path, ")", ">", File.shell_path proof_path])

fun trace_and ctxt msg f x =
  let val _ = SMT2_Config.trace_msg ctxt (fn () => msg) ()
  in f x end

fun run ctxt name mk_cmd input =
  (case SMT2_Config.certificates_of ctxt of
    NONE =>
      if not (SMT2_Config.is_available ctxt name) then
        error ("The SMT solver " ^ quote name ^ " is not installed.")
      else if Config.get ctxt SMT2_Config.debug_files = "" then
        trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
          (Cache_IO.run mk_cmd) input
      else
        let
          val base_path = Path.explode (Config.get ctxt SMT2_Config.debug_files)
          val in_path = Path.ext "smt2_in" base_path
          val out_path = Path.ext "smt2_out" base_path
        in Cache_IO.raw_run mk_cmd input in_path out_path end
  | SOME certs =>
      (case Cache_IO.lookup certs input of
        (NONE, key) =>
          if Config.get ctxt SMT2_Config.read_only_certificates then
            error ("Bad certificate cache: missing certificate")
          else
            Cache_IO.run_and_cache certs key mk_cmd input
      | (SOME output, _) =>
          trace_and ctxt ("Using cached certificate from " ^
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
            I output))

(* Z3 returns 1 if "get-model" or "get-model" fails *)
val normal_return_codes = [0, 1]

fun run_solver ctxt name mk_cmd input =
  let
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag (map Pretty.str ls))

    val _ = SMT2_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input

    val {redirected_output=res, output=err, return_code} =
      SMT2_Config.with_timeout ctxt (run ctxt name mk_cmd) input
    val _ = SMT2_Config.trace_msg ctxt (pretty "Solver:") err

    val output = fst (take_suffix (equal "") res)
    val _ = SMT2_Config.trace_msg ctxt (pretty "Result:") output

    val _ = member (op =) normal_return_codes return_code orelse
{'fraction_non_alphanumeric': 0.10554197229013855, 'fraction_numerical': 0.009779951100244499, 'mean_word_length': 2.9543501611170786, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 86, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2627316', 'n_tokens_mistral': 2541, 'n_tokens_neox': 2446, 'n_words': 718}