src/HOL/Library/Old_SMT/old_smt_config.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 62519 a564458f94db
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_config.ML
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     3
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     4
Configuration options and diagnostic tools for SMT.
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     5
*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_CONFIG =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     8
sig
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     9
  (*solver*)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    10
  type solver_info = {
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    11
    name: string,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    12
    class: Proof.context -> Old_SMT_Utils.class,
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    13
    avail: unit -> bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    14
    options: Proof.context -> string list }
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    15
  val add_solver: solver_info -> Context.generic -> Context.generic
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    16
  val set_solver_options: string * string -> Context.generic -> Context.generic
46736
4dc7ddb47350 SMT fails if the chosen SMT solver is not installed
boehmes
parents: 46042
diff changeset
    17
  val is_available: Proof.context -> string -> bool
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    18
  val available_solvers_of: Proof.context -> string list
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    19
  val select_solver: string -> Context.generic -> Context.generic
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    20
  val solver_of: Proof.context -> string
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    21
  val solver_class_of: Proof.context -> Old_SMT_Utils.class
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    22
  val solver_options_of: Proof.context -> string list
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    23
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    24
  (*options*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    25
  val oracle: bool Config.T
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    26
  val datatypes: bool Config.T
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    27
  val timeout: real Config.T
41121
5c5d05963f93 added option to modify the random seed of SMT solvers
boehmes
parents: 41059
diff changeset
    28
  val random_seed: int Config.T
47152
446cfc760ccf renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents: 46961
diff changeset
    29
  val read_only_certificates: bool Config.T
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    30
  val verbose: bool Config.T
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    31
  val trace: bool Config.T
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    32
  val trace_used_facts: bool Config.T
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    33
  val monomorph_limit: int Config.T
41762
00060198de12 limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents: 41761
diff changeset
    34
  val monomorph_instances: int Config.T
41125
4a9eec045f2a added option to enable trigger inference;
boehmes
parents: 41124
diff changeset
    35
  val infer_triggers: bool Config.T
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    36
  val filter_only_facts: bool Config.T
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40513
diff changeset
    37
  val debug_files: string Config.T
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    38
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    39
  (*tools*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    40
  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    41
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    42
  (*diagnostics*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    43
  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    44
  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    45
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    46
  (*certificates*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    47
  val select_certificates: string -> Context.generic -> Context.generic
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    48
  val certificates_of: Proof.context -> Cache_IO.cache option
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    49
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    50
  (*setup*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    51
  val setup: theory -> theory
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    52
  val print_setup: Proof.context -> unit
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    53
end
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    54
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    55
structure Old_SMT_Config: OLD_SMT_CONFIG =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    56
struct
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    57
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    58
(* solver *)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    59
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    60
type solver_info = {
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    61
  name: string,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    62
  class: Proof.context -> Old_SMT_Utils.class,
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    63
  avail: unit -> bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    64
  options: Proof.context -> string list }
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    65
46042
ab32a87ba01a comments;
wenzelm
parents: 42616
diff changeset
    66
(* FIXME just one data slot (record) per program unit *)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    67
structure Solvers = Generic_Data
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    68
(
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    69
  type T = (solver_info * string list) Symtab.table * string option
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    70
  val empty = (Symtab.empty, NONE)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    71
  val extend = I
41499
d54fe826250e be more precise: also merge option values
boehmes
parents: 41498
diff changeset
    72
  fun merge ((ss1, s1), (ss2, s2)) =
d54fe826250e be more precise: also merge option values
boehmes
parents: 41498
diff changeset
    73
    (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    74
)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    75
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    76
fun set_solver_options (name, options) =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    77
  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40578
diff changeset
    78
  in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    79
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    80
fun add_solver (info as {name, ...} : solver_info) context =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    81
  if Symtab.defined (fst (Solvers.get context)) name then
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    82
    error ("Solver already registered: " ^ quote name)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    83
  else
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    84
    context
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    85
    |> Solvers.map (apfst (Symtab.update (name, (info, []))))
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
    86
    |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options"))
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46736
diff changeset
    87
        (Scan.lift (@{keyword "="} |-- Args.name) >>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    88
          (Thm.declaration_attribute o K o set_solver_options o pair name))
60312
ee6f9a97205d tuned message;
wenzelm
parents: 59936
diff changeset
    89
        ("additional command line options for SMT solver " ^ quote name))
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    90
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    91
fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    92
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    93
fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    94
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    95
fun is_available ctxt name =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    96
  (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    97
    SOME ({avail, ...}, _) => avail ()
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    98
  | NONE => false)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
    99
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   100
fun available_solvers_of ctxt =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   101
  filter (is_available ctxt) (all_solvers_of ctxt)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   102
52699
abed4121c17e tuned signature;
wenzelm
parents: 51658
diff changeset
   103
fun warn_solver (Context.Proof ctxt) name =
56294
85911b8a6868 prefer Context_Position where a context is available;
wenzelm
parents: 56208
diff changeset
   104
      if Context_Position.is_visible ctxt then
52699
abed4121c17e tuned signature;
wenzelm
parents: 51658
diff changeset
   105
        warning ("The SMT solver " ^ quote name ^ " is not installed.")
56294
85911b8a6868 prefer Context_Position where a context is available;
wenzelm
parents: 56208
diff changeset
   106
      else ()
52699
abed4121c17e tuned signature;
wenzelm
parents: 51658
diff changeset
   107
  | warn_solver _ _ = ();
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   108
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   109
fun select_solver name context =
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   110
  let
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   111
    val ctxt = Context.proof_of context
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   112
    val upd = Solvers.map (apsnd (K (SOME name)))
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   113
  in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   114
    if not (member (op =) (all_solvers_of ctxt) name) then
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   115
      error ("Trying to select unknown solver: " ^ quote name)
41498
a45cfc6dfd10 only print warning in a visible context (previously, the warning was printed more than once)
boehmes
parents: 41472
diff changeset
   116
    else if not (is_available ctxt name) then
a45cfc6dfd10 only print warning in a visible context (previously, the warning was printed more than once)
boehmes
parents: 41472
diff changeset
   117
      (warn_solver context name; upd context)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   118
    else upd context
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   119
  end
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   120
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40578
diff changeset
   121
fun no_solver_err () = error "No SMT solver selected"
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   122
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   123
fun solver_of ctxt =
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   124
  (case solver_name_of ctxt of
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   125
    SOME name => name
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   126
  | NONE => no_solver_err ())
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   127
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   128
fun solver_info_of default select ctxt =
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40578
diff changeset
   129
  (case Solvers.get (Context.Proof ctxt) of
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   130
    (solvers, SOME name) => select (Symtab.lookup solvers name)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   131
  | (_, NONE) => default ())
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40578
diff changeset
   132
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40578
diff changeset
   133
fun solver_class_of ctxt =
48043
3ff2c76c9f64 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents: 47152
diff changeset
   134
  let fun class_of ({class, ...}: solver_info, _) = class ctxt
3ff2c76c9f64 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents: 47152
diff changeset
   135
  in solver_info_of no_solver_err (class_of o the) ctxt end
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   136
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   137
fun solver_options_of ctxt =
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   138
  let
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   139
    fun all_options NONE = []
41438
272fe1f37b65 made SML/NJ happy
boehmes
parents: 41432
diff changeset
   140
      | all_options (SOME ({options, ...} : solver_info, opts)) =
272fe1f37b65 made SML/NJ happy
boehmes
parents: 41432
diff changeset
   141
          opts @ options ctxt
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   142
  in solver_info_of (K []) all_options ctxt end
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   143
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   144
val setup_solver =
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   145
  Attrib.setup @{binding old_smt_solver}
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46736
diff changeset
   146
    (Scan.lift (@{keyword "="} |-- Args.name) >>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   147
      (Thm.declaration_attribute o K o select_solver))
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   148
    "SMT solver configuration"
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   149
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   150
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   151
(* options *)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   152
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   153
val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   154
val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   155
val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   156
val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   157
val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   158
val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   159
val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   160
val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   161
val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   162
val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   163
val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   164
val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false)
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   165
val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "")
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   166
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   167
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   168
(* diagnostics *)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   169
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   170
fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   171
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   172
fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   173
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   174
fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   175
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   176
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   177
(* tools *)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   178
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   179
fun with_timeout ctxt f x =
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 60312
diff changeset
   180
  Timeout.apply (seconds (Config.get ctxt timeout)) f x
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 60312
diff changeset
   181
    handle Timeout.TIMEOUT _ => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   182
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   183
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   184
(* certificates *)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   185
46042
ab32a87ba01a comments;
wenzelm
parents: 42616
diff changeset
   186
(* FIXME just one data slot (record) per program unit *)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   187
structure Certificates = Generic_Data
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   188
(
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   189
  type T = Cache_IO.cache option
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   190
  val empty = NONE
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   191
  val extend = I
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41441
diff changeset
   192
  fun merge (s, _) = s  (* FIXME merge options!? *)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   193
)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   194
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   195
val get_certificates_path =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   196
  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   197
40513
1204d268464f look for certificates relative to the theory
boehmes
parents: 40424
diff changeset
   198
fun select_certificates name context = context |> Certificates.put (
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   199
  if name = "" then NONE
40513
1204d268464f look for certificates relative to the theory
boehmes
parents: 40424
diff changeset
   200
  else
1204d268464f look for certificates relative to the theory
boehmes
parents: 40424
diff changeset
   201
    Path.explode name
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 54041
diff changeset
   202
    |> Path.append (Resources.master_directory (Context.theory_of context))
50317
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 48043
diff changeset
   203
    |> SOME o Cache_IO.unsynchronized_init)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   204
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   205
val certificates_of = Certificates.get o Context.Proof
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   206
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   207
val setup_certificates =
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   208
  Attrib.setup @{binding old_smt_certificates}
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46736
diff changeset
   209
    (Scan.lift (@{keyword "="} |-- Args.name) >>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   210
      (Thm.declaration_attribute o K o select_certificates))
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   211
    "SMT certificates configuration"
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   212
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   213
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   214
(* setup *)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   215
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   216
val setup =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   217
  setup_solver #>
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   218
  setup_certificates
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   219
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   220
fun print_setup ctxt =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   221
  let
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   222
    fun string_of_bool b = if b then "true" else "false"
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   223
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   224
    val names = available_solvers_of ctxt
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   225
    val ns = if null names then ["(none)"] else sort_strings names
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41125
diff changeset
   226
    val n = the_default "(none)" (solver_name_of ctxt)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   227
    val opts = solver_options_of ctxt
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   228
    
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   229
    val t = string_of_real (Config.get ctxt timeout)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   230
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   231
    val certs_filename =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   232
      (case get_certificates_path ctxt of
41944
b97091ae583a Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents: 41762
diff changeset
   233
        SOME path => Path.print path
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   234
      | NONE => "(disabled)")
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   235
  in
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   236
    Pretty.writeln (Pretty.big_list "SMT setup:" [
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   237
      Pretty.str ("Current SMT solver: " ^ n),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   238
      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   239
      Pretty.str_list "Available SMT solvers: "  "" ns,
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   240
      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   241
      Pretty.str ("With proofs: " ^
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   242
        string_of_bool (not (Config.get ctxt oracle))),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   243
      Pretty.str ("Certificates cache: " ^ certs_filename),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   244
      Pretty.str ("Fixed certificates: " ^
47152
446cfc760ccf renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents: 46961
diff changeset
   245
        string_of_bool (Config.get ctxt read_only_certificates))])
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   246
  end
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   247
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   248
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 58893
diff changeset
   249
  Outer_Syntax.command @{command_keyword old_smt_status}
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   250
    "show the available SMT solvers, the currently selected SMT solver, \
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
   251
    \and the values of SMT configuration options"
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51575
diff changeset
   252
    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   253
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
   254
end