File ‹Tools/SMT/smt_config.ML›

(*  Title:      HOL/Tools/SMT/smt_config.ML
    Author:     Sascha Boehme, TU Muenchen

Configuration options and diagnostic tools for SMT.
*)

signature SMT_CONFIG =
sig
  (*solver*)
  type solver_info = {
    name: string,
    dummy: bool,
    sledgehammer_default: bool,
    class: Proof.context -> SMT_Util.class list,
    avail: unit -> bool,
    options: Proof.context -> string list }
  val add_solver: solver_info -> Context.generic -> Context.generic
  val set_solver_options: string * string -> Context.generic -> Context.generic
  val all_solvers_of: Proof.context -> string list
  val all_nondummy_solvers_of: Proof.context -> string list
  val all_nondummy_sledgehammer_solvers_of: Proof.context -> string list
  val is_available: Proof.context -> string -> bool
  val available_solvers_of: Proof.context -> string list
  val select_solver: string -> Context.generic -> Context.generic
  val solver_of: Proof.context -> string
  val solver_class_of: Proof.context -> SMT_Util.class list
  val solver_options_of: Proof.context -> string list

  (*options*)
  val oracle: bool Config.T
  val timeout: real Config.T
  val reconstruction_step_timeout: real Config.T
  val random_seed: int Config.T
  val read_only_certificates: bool Config.T
  val verbose: bool Config.T
  val trace: bool Config.T
  val statistics: bool Config.T

  val monomorph_limit: int Config.T
  val monomorph_instances: int Config.T
  val explicit_application: int Config.T
  val higher_order: bool Config.T
  val native_bv: bool Config.T
  val native_set: bool Config.T
  val native_datatypes: bool Config.T
  val native_codatatypes: bool Config.T
  val nat_as_int: bool Config.T
  val infer_triggers: bool Config.T
  val integer_induction: bool Config.T
  val structural_induction: bool Config.T

  val problem_dest_file : string Config.T
  val proof_dest_file : string Config.T
  val unique_dest_file : bool Config.T
  val sat_solver: string Config.T
  val check_external: bool Config.T
  val slice_only_no_full_proof_attr: bool Config.T
  val compress_alethe_proofs: Proof.context -> bool
  val alethe_use_prop_skeleton: Proof.context -> bool
  val cvc5_word_experimental: bool Config.T

  (*tools*)
  val get_timeout: Proof.context -> Time.time option
  val with_time_limit: Proof.context -> string -> real Config.T -> ('a -> 'b) -> 'a -> 'b
  val with_timeout: Proof.context -> string -> ('a -> 'b) -> 'a -> 'b

  (*diagnostics*)
  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
  val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
  val verit_msg: Proof.context -> (unit -> 'a) -> unit
  val verit_arith_msg: Proof.context -> (unit -> 'a) -> unit
  datatype debugging_verbosity = off | low | middle | high
  val alethe_debug_msg: Proof.context -> string -> debugging_verbosity -> (unit -> 'a) -> unit
  val alethe_debug_msg_tac: Proof.context -> string -> debugging_verbosity -> string -> tactic
  val spy_cvc: Proof.context -> bool
  val spy_verit: Proof.context -> bool
  val spy_Z3: Proof.context -> bool
  val check_smt_is_slicing: Proof.context -> bool
  val use_alethe_proof_from_cvc: Proof.context -> bool
  val alethe_no_provided_assms: Proof.context -> bool
  val alethe_set_no_provided_assms: bool -> Proof.context -> Proof.context

  (*certificates*)
  val select_certificates: string -> Context.generic -> Context.generic
  val certificates_of: Proof.context -> Cache_IO.cache option

  (*setup*)
  val print_setup: Proof.context -> unit
end

structure SMT_Config: SMT_CONFIG =
struct

(* context data *)

type solver_info = {
  name: string,
  dummy: bool,
  sledgehammer_default: bool,
  class: Proof.context -> SMT_Util.class list,
  avail: unit -> bool,
  options: Proof.context -> string list};

structure Data = Generic_Data
(
  type T =
    (solver_info * string list) Symtab.table *  (*all solvers*)
    string option *  (*selected solver*)
    Cache_IO.cache option;  (*certificates*)
  val empty: T = (Symtab.empty, NONE, NONE);
  fun merge ((ss1, s1, c1): T, (ss2, s2, c2): T) =
    (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2), merge_options (c1, c2));
);

val get_solvers' = #1 o Data.get;
val get_solvers = get_solvers' o Context.Proof;
val get_solver = #2 o Data.get o Context.Proof;
val certificates_of = #3 o Data.get o Context.Proof;

val map_solvers = Data.map o @{apply 3(1)}
val put_solver = Data.map o @{apply 3(2)} o K o SOME;
val put_certificates = Data.map o @{apply 3(3)} o K;

val defined_solvers = Symtab.defined o get_solvers';

fun set_solver_options (name, options) =
  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
  in map_solvers (Symtab.map_entry name (apsnd (K opts))) end;

fun add_solver (info as {name, ...} : solver_info) context =
  if defined_solvers context name then
    error ("Solver already registered: " ^ quote name)
  else
    context
    |> map_solvers (Symtab.update (name, (info, [])))
    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
        (Scan.lift (\<^keyword>‹=› |-- Args.name) >>
          (Thm.declaration_attribute o K o set_solver_options o pair name))
        ("additional command-line options for SMT solver " ^ quote name));

val all_solvers_of' = Symtab.keys o get_solvers';
val all_solvers_of = all_solvers_of' o Context.Proof;

fun all_nondummy_solvers_of (ctxt : Proof.context) : string list =
  let
    val solvers = get_solvers' (Context.Proof ctxt)
    fun cons_nondummy (name, ({dummy = false, ...}, _)) names = name :: names
      | cons_nondummy _ names = names
  in
    Library.build (Symtab.fold_rev cons_nondummy solvers)
  end
fun all_nondummy_sledgehammer_solvers_of (ctxt : Proof.context) : string list =
  let
    val solvers = get_solvers' (Context.Proof ctxt)
    fun cons_nondummy (name, ({dummy = false, sledgehammer_default = true, ...}, _)) names =
          name :: names
      | cons_nondummy _ names = names
  in
    Library.build (Symtab.fold_rev cons_nondummy solvers)
  end

fun is_available' context name =
  (case Symtab.lookup (get_solvers' context) name of
    SOME ({avail, ...}, _) => avail ()
  | NONE => false);

val is_available = is_available' o Context.Proof;

fun available_solvers_of ctxt =
  filter (is_available ctxt) (all_solvers_of ctxt);

fun warn_solver (Context.Proof ctxt) name =
      if Context_Position.is_visible ctxt then
        warning ("The SMT solver " ^ quote name ^ " is not installed")
      else ()
  | warn_solver _ _ = ();

fun select_solver name context =
  if not (defined_solvers context name) then
    error ("Trying to select unknown solver: " ^ quote name)
  else if not (is_available' context name) then
    (warn_solver context name; put_solver name context)
  else put_solver name context;

fun no_solver_err () = error "No SMT solver selected";

fun solver_of ctxt =
  (case get_solver ctxt of
    SOME name => name
  | NONE => no_solver_err ());

fun solver_info_of default select ctxt =
  (case get_solver ctxt of
    NONE => default ()
  | SOME name => select (Symtab.lookup (get_solvers ctxt) name));

fun solver_class_of ctxt =
  let fun class_of ({class, ...}: solver_info, _) = class ctxt
  in solver_info_of no_solver_err (class_of o the) ctxt end;

fun solver_options_of ctxt =
  let
    fun all_options NONE = []
      | all_options (SOME ({options, ...} : solver_info, opts)) =
          opts @ options ctxt
  in solver_info_of (K []) all_options ctxt end;

val _ =
  Theory.setup (Attrib.setup \<^binding>‹smt_solver›
    (Scan.lift (\<^keyword>‹=› |-- Args.name) >>
      (Thm.declaration_attribute o K o select_solver))
    "SMT solver configuration");


(* options *)

val oracle = Attrib.setup_config_bool \<^binding>‹smt_oracle› (K true);
val timeout = Attrib.setup_config_real \<^binding>‹smt_timeout› (K 0.0);
val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>‹smt_reconstruction_step_timeout› (K 10.0);
val random_seed = Attrib.setup_config_int \<^binding>‹smt_random_seed› (K 1);
val read_only_certificates = Attrib.setup_config_bool \<^binding>‹smt_read_only_certificates› (K false);
val verbose = Attrib.setup_config_bool \<^binding>‹smt_verbose› (K true);
val trace = Attrib.setup_config_bool \<^binding>‹smt_trace› (K false);
val trace_verit = Attrib.setup_config_bool \<^binding>‹smt_debug_verit› (K false);
val slice_only_no_full_proof_attr = Attrib.setup_config_bool \<^binding>‹smt_alethe_slice› (K false);
val trace_expert_debug_alethe_level = Attrib.setup_config_int \<^binding>‹smt_expert_debug_alethe_level› (K 0);
val trace_expert_debug_alethe_files = Attrib.setup_config_string \<^binding>‹smt_expert_debug_alethe_files› (K "all");
val spy_cvc_attr = Attrib.setup_config_bool \<^binding>‹smt_spy_cvc› (K false);
val spy_verit_attr = Attrib.setup_config_bool \<^binding>‹smt_spy_verit› (K false);
val spy_z3 = Attrib.setup_config_bool \<^binding>‹smt_spy_z3› (K false);
val trace_arith_verit = Attrib.setup_config_bool \<^binding>‹smt_debug_arith_verit› (K false);
val trace_verit_compression = Attrib.setup_config_bool \<^binding>‹verit_compress_proofs› (K true);
val trace_alethe_use_prop_skeleton = Attrib.setup_config_bool \<^binding>‹alethe_use_propositional_skeleton› (K true);
val statistics = Attrib.setup_config_bool \<^binding>‹smt_statistics› (K false);

val monomorph_limit = Attrib.setup_config_int \<^binding>‹smt_monomorph_limit› (K 10);
val monomorph_instances = Attrib.setup_config_int \<^binding>‹smt_monomorph_instances› (K 500);
val explicit_application = Attrib.setup_config_int \<^binding>‹smt_explicit_application› (K 1);
val higher_order = Attrib.setup_config_bool \<^binding>‹smt_higher_order› (K false);
val native_bv = Attrib.setup_config_bool \<^binding>‹native_bv› (K true);
val native_set = Attrib.setup_config_bool \<^binding>‹native_set› (K false);
val native_datatypes = Attrib.setup_config_bool \<^binding>‹smt_native_datatypes› (K false);
val native_codatatypes = Attrib.setup_config_bool \<^binding>‹smt_native_codatatypes› (K false);
val nat_as_int = Attrib.setup_config_bool \<^binding>‹smt_nat_as_int› (K false);
val infer_triggers = Attrib.setup_config_bool \<^binding>‹smt_infer_triggers› (K false);
val integer_induction = Attrib.setup_config_bool \<^binding>‹smt_integer_induction› (K false)
val structural_induction = Attrib.setup_config_bool \<^binding>‹smt_structural_induction› (K false)

val problem_dest_file = Attrib.setup_config_string \<^binding>‹smt_problem_dest_dir› (K "");
val proof_dest_file = Attrib.setup_config_string \<^binding>‹smt_proof_dest_dir› (K "");
val unique_dest_file = Attrib.setup_config_bool \<^binding>‹smt_unique_dest_file› (K false);
val sat_solver = Attrib.setup_config_string \<^binding>‹smt_sat_solver› (K "cdclite");
val check_external = Attrib.setup_config_bool \<^binding>‹smt_check_external› (K false);
val cvc_experimental_alethe = Attrib.setup_config_bool \<^binding>‹smt_cvc_alethe› (K false);
val alethe_no_assumption = Attrib.setup_config_bool \<^binding>‹smt_alethe_no_assumption› (K false);
val cvc5_word_experimental = Attrib.setup_config_bool \<^binding>‹smt_cvc5_word_experimental› (K false);


(* diagnostics *)

fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ();

fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose);
fun trace_msg ctxt = cond_trace (Config.get ctxt trace);
fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics);

fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ();
fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ();

datatype debugging_verbosity = off | low | middle | high
datatype debugging_files = all | alethe_proof

fun debug_to_int off = 0 |
    debug_to_int low = 1 |
    debug_to_int middle = 2 |
    debug_to_int high = 3

fun alethe_debug_msg ctxt file verbosity (x : unit -> 'a) =
let
  val part = Config.get ctxt trace_expert_debug_alethe_files
  val min = Config.get ctxt trace_expert_debug_alethe_level
in
 if (min > 0 andalso min >= debug_to_int verbosity andalso (part = "all" orelse part = file)) then ignore(x ()) else ()
end

fun alethe_debug_msg_tac ctxt file verbosity (msg: string) =
let
  val part = Config.get ctxt trace_expert_debug_alethe_files
  val min = Config.get ctxt trace_expert_debug_alethe_level
in
 if (min > 0 andalso min >= debug_to_int verbosity andalso (part = "all" orelse part = file))
 then (print_tac ctxt msg) else TRY no_tac
end


fun check_smt_is_slicing ctxt  = Config.get ctxt slice_only_no_full_proof_attr

fun spy_cvc ctxt  = Config.get ctxt spy_cvc_attr
fun spy_verit ctxt  = Config.get ctxt spy_verit_attr
fun spy_Z3 ctxt  = Config.get ctxt spy_z3
fun compress_alethe_proofs ctxt = Config.get ctxt trace_verit_compression
fun alethe_use_prop_skeleton ctxt = Config.get ctxt trace_alethe_use_prop_skeleton

fun use_alethe_proof_from_cvc ctxt = Config.get ctxt cvc_experimental_alethe
fun alethe_no_provided_assms ctxt = Config.get ctxt alethe_no_assumption
fun alethe_set_no_provided_assms b = Config.map alethe_no_assumption (K b)


(* tools *)

fun get_timeout ctxt =
  let val t = seconds (Config.get ctxt timeout);
  in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;

fun with_time_limit ctxt error_msg timeout_config f x =
  Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT (SMT_Failure.Time_Out error_msg)

fun with_timeout ctxt error_msg = with_time_limit ctxt error_msg timeout;


(* certificates *)

val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of;

fun select_certificates name context = context |> put_certificates (
  if name = "" then NONE
  else
    let val dir = Resources.master_directory (Context.theory_of context) + Path.explode name
    in SOME (Cache_IO.unsynchronized_init dir) end);

val _ =
  Theory.setup (Attrib.setup \<^binding>‹smt_certificates›
    (Scan.lift (\<^keyword>‹=› |-- Args.name) >>
      (Thm.declaration_attribute o K o select_certificates))
    "SMT certificates configuration");


(* print_setup *)

fun print_setup ctxt =
  let
    val names = available_solvers_of ctxt;
    val ns = if null names then ["(none)"] else sort_strings names;
    val n = the_default "(none)" (get_solver ctxt);
    val opts = solver_options_of ctxt;
    val t = seconds (Config.get ctxt timeout)

    val certs_filename =
      (case get_certificates_path ctxt of
        SOME path => Path.print path
      | NONE => "(disabled)");

    val items =
     [Pretty.str ("Current SMT solver: " ^ n),
      Pretty.str ("Current SMT solver options: " ^ implode_space opts),
      Pretty.str_list "Available SMT solvers: "  "" ns,
      Pretty.str ("Current timeout: " ^ (if Timeout.ignored t then "(none)" else Time.message t)),
      Pretty.str ("With proofs: " ^ Value.print_bool (not (Config.get ctxt oracle))),
      Pretty.str ("Certificates cache: " ^ certs_filename),
      Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))];
  in Pretty.writeln (Pretty.big_list "SMT setup:" (map (Pretty.item o single) items)) end;

val _ =
  Outer_Syntax.command \<^command_keyword>‹smt_status›
    "show the available SMT solvers, the currently selected SMT solver, \
    \and the values of SMT configuration options"
    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))

end