<commit_before>(*  Title:      HOL/Tools/SMT/smt_solver.ML
    Author:     <NAME>, <NAME>

SMT solvers registry and SMT tactic.
*)

signature SMT_SOLVER =
sig
  (*configuration*)
  type interface = {
    class: SMT_Config.class,
    extra_norm: SMT_Normalize.extra_norm,
    translate: SMT_Translate.config }
  datatype outcome = Unsat | Sat | Unknown
  type solver_config = {
    name: string,
    env_var: string,
    is_remote: bool,
    options: Proof.context -> string list,
    interface: interface,
    outcome: string -> string list -> outcome * string list,
    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
      term list * term list) option,
    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
      (int list * thm) * Proof.context) option,
    default_max_relevant: int }

  (*registry*)
  type solver = bool option -> Proof.context -> (int * thm) list ->
    int list * thm
  val add_solver: solver_config -> theory -> theory
  val solver_name_of: Proof.context -> string
  val solver_of: Proof.context -> solver
  val available_solvers_of: Proof.context -> string list
  val is_locally_installed: Proof.context -> string -> bool
  val is_remotely_available: Proof.context -> string -> bool
  val default_max_relevant: Proof.context -> string -> int

  (*filter*)
  val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
    run_time_in_msecs: int option}

  (*tactic*)
  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic

  (*setup*)
  val setup: theory -> theory
end

structure SMT_Solver: SMT_SOLVER =
struct

structure C = SMT_Config


(* configuration *)

type interface = {
  class: SMT_Config.class,
  extra_norm: SMT_Normalize.extra_norm,
  translate: SMT_Translate.config }

datatype outcome = Unsat | Sat | Unknown

type solver_config = {
  name: string,
  env_var: string,
  is_remote: bool,
  options: Proof.context -> string list,
  interface: interface,
  outcome: string -> string list -> outcome * string list,
  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    term list * term list) option,
  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    (int list * thm) * Proof.context) option,
  default_max_relevant: int }


(* interface to external solvers *)

fun get_local_solver env_var =
  let val local_solver = getenv env_var
  in if local_solver <> "" then SOME local_solver else NONE end

local

fun choose (rm, env_var, is_remote, name) =
  let
    val force_local = (case rm of SOME false => true | _ => false)
    val force_remote = (case rm of SOME true => true | _ => false)
    val lsolver = get_local_solver env_var
    val remote_url = getenv "REMOTE_SMT_URL"
    val trace = if is_some rm then K () else tracing
  in
    if not force_remote andalso is_some lsolver
    then 
     (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
      [the lsolver])
    else if not force_local andalso is_remote
    then
     (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^
        quote remote_url ^ " ...");
      [getenv "REMOTE_SMT", name])
    else if force_remote
    then error ("The SMT solver " ^ quote name ^ " is not remotely available.")
    else error ("The SMT solver " ^ quote name ^ " has not been found " ^
      "on this computer. Please set the Isabelle environment variable " ^
      quote env_var ^ ".")
  end

fun make_cmd solver args problem_path proof_path = space_implode " " (
  map File.shell_quote (solver @ args) @
  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])

fun run ctxt cmd args input =
  (case C.certificates_of ctxt of
    NONE =>
      if Config.get ctxt C.debug_files = "" then
        Cache_IO.run (make_cmd (choose cmd) args) input
      else
        let
          val base_path = Path.explode (Config.get ctxt C.debug_files)
          val in_path = Path.ext "smt_in" base_path
          val out_path = Path.ext "smt_out" base_path
        in
          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
        end
  | SOME certs =>
      (case Cache_IO.lookup certs input of
        (NONE, key) =>
          if Config.get ctxt C.fixed then
            error ("Bad certificates cache: missing certificate")
          else
            Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
      | (SOME output, _) =>
         (tracing ("Using cached certificate from " ^
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
          output)))

in

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

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

    val {redirected_output=res, output=err, return_code} =
      C.with_timeout ctxt (run ctxt cmd args) input
    val _ = C.trace_msg ctxt (pretty "Solver:") err

    val ls = rev (snd (chop_while (equal "") (rev res)))
    val _ = C.trace_msg ctxt (pretty "Result:") ls

    val _ = null ls andalso return_code <> 0 andalso
      raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
  in ls end

end

fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))

fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
  let
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
  in
    C.trace_msg ctxt (fn () =>
      Pretty.string_of (Pretty.big_list "Names:" [
        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
  end

fun invoke translate_config name cmd options irules ctxt =
  let
    val args = C.solver_options_of ctxt @ options ctxt
    val comments = ("solver: " ^ name) ::
      ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
      "arguments:" :: args
  in
    irules
    |> tap (trace_assms ctxt)
    |> SMT_Translate.translate translate_config ctxt comments
    ||> tap (trace_recon_data ctxt)
    |>> run_solver ctxt cmd args
    |> rpair ctxt
  end

fun discharge_definitions thm =
  if Thm.nprems_of thm = 0 then thm
  else discharge_definitions (@{thm reflexive} RS thm)

fun set_has_datatypes with_datatypes translate =
  let
    val {prefixes, header, is_fol, has_datatypes, serialize} = translate
    val with_datatypes' = has_datatypes andalso with_datatypes
    val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
      has_datatypes=with_datatypes', serialize=serialize}<commit_msg>tuned<commit_after>(*  Title:      HOL/Tools/SMT/smt_solver.ML
    Author:     <NAME>, <NAME>

SMT solvers registry and SMT tactic.
*)

signature SMT_SOLVER =
sig
  (*configuration*)
  type interface = {
    class: SMT_Config.class,
    extra_norm: SMT_Normalize.extra_norm,
    translate: SMT_Translate.config }
  datatype outcome = Unsat | Sat | Unknown
  type solver_config = {
    name: string,
    env_var: string,
    is_remote: bool,
    options: Proof.context -> string list,
    interface: interface,
    outcome: string -> string list -> outcome * string list,
    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
      term list * term list) option,
    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
      (int list * thm) * Proof.context) option,
    default_max_relevant: int }

  (*registry*)
  type solver = bool option -> Proof.context -> (int * thm) list ->
    int list * thm
  val add_solver: solver_config -> theory -> theory
  val solver_name_of: Proof.context -> string
  val solver_of: Proof.context -> solver
  val available_solvers_of: Proof.context -> string list
  val is_locally_installed: Proof.context -> string -> bool
  val is_remotely_available: Proof.context -> string -> bool
  val default_max_relevant: Proof.context -> string -> int

  (*filter*)
  val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
    run_time_in_msecs: int option}

  (*tactic*)
  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic

  (*setup*)
  val setup: theory -> theory
end

structure SMT_Solver: SMT_SOLVER =
struct

structure C = SMT_Config


(* configuration *)

type interface = {
  class: SMT_Config.class,
  extra_norm: SMT_Normalize.extra_norm,
  translate: SMT_Translate.config }

datatype outcome = Unsat | Sat | Unknown

type solver_config = {
  name: string,
  env_var: string,
  is_remote: bool,
  options: Proof.context -> string list,
  interface: interface,
  outcome: string -> string list -> outcome * string list,
  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    term list * term list) option,
  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    (int list * thm) * Proof.context) option,
  default_max_relevant: int }


(* interface to external solvers *)

fun get_local_solver env_var =
  let val local_solver = getenv env_var
  in if local_solver <> "" then SOME local_solver else NONE end

local

fun choose (rm, env_var, is_remote, name) =
  let
    val force_local = (case rm of SOME false => true | _ => false)
    val force_remote = (case rm of SOME true => true | _ => false)
    val lsolver = get_local_solver env_var
    val remote_url = getenv "REMOTE_SMT_URL"
    val trace = if is_some rm then K () else tracing
  in
    if not force_remote andalso is_some lsolver
    then 
     (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
      [the lsolver])
    else if not force_local andalso is_remote
    then
     (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^
        quote remote_url ^ " ...");
      [getenv "REMOTE_SMT", name])
    else if force_remote
    then error ("The SMT solver " ^ quote name ^ " is not remotely available.")
    else error ("The SMT solver " ^ quote name ^ " has not been found " ^
      "on this computer. Please set the Isabelle environment variable " ^
      quote env_var ^ ".")
  end

fun make_cmd solver args problem_path proof_path = space_implode " " (
  map File.shell_quote (solver @ args) @
  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])

fun run ctxt cmd args input =
  (case C.certificates_of ctxt of
    NONE =>
      if Config.get ctxt C.debug_files = "" then
        Cache_IO.run (make_cmd (choose cmd) args) input
      else
        let
          val base_path = Path.explode (Config.get ctxt C.debug_files)
          val in_path = Path.ext "smt_in" base_path
          val out_path = Path.ext "smt_out" base_path
        in
          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
        end
  | SOME certs =>
      (case Cache_IO.lookup certs input of
        (NONE, key) =>
          if Config.get ctxt C.fixed then
            error ("Bad certificates cache: missing certificate")
          else
            Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
      | (SOME output, _) =>
         (tracing ("Using cached certificate from " ^
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
          output)))

in

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

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

    val {redirected_output=res, output=err, return_code} =
      C.with_timeout ctxt (run ctxt cmd args) input
    val _ = C.trace_msg ctxt (pretty "Solver:") err

    val ls = rev (snd (chop_while (equal "") (rev res)))
    val _ = C.trace_msg ctxt (pretty "Result:") ls

    val _ = null ls andalso return_code <> 0 andalso
      raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
  in ls end

end

fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))

fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
  let
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
  in
    C.trace_msg ctxt (fn () =>
      Pretty.string_of (Pretty.big_list "Names:" [
        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
  end

fun invoke translate_config name cmd options irules ctxt =
  let
    val args = C.solver_options_of ctxt @ options ctxt
    val comments = ("solver: " ^ name) ::
      ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
      "arguments:" :: args
  in
    irules
    |> tap (trace_assms ctxt)
    |> SMT_Translate.translate translate_config ctxt comments
    ||> tap (trace_recon_data ctxt)
    |>> run_solver ctxt cmd args
    |> rpair ctxt
  end

fun discharge_definitions thm =
  if Thm.nprems_of thm = 0 then thm
  else discharge_definitions (@{thm reflexive} RS thm)

fun set_has_datatypes with_datatypes translate =
  let
    val {prefixes, header, is_fol, has_datatypes, serialize} = translate
    val with_datatypes' = has_datatypes andalso with_datatypes
    val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
      has_datatypes=with_datatypes', serialize=serialize}
{'fraction_non_alphanumeric': 0.1045253141570422, 'fraction_numerical': 0.0005810997312413743, 'mean_word_length': 3.0506031185642835, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 135, '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': '3690339', 'n_tokens_mistral': 4721, 'n_tokens_neox': 4536, 'n_words': 1386}