add reconstruction by veriT in method smt

prefer control symbol antiquotations;

properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)

towards support for HO SMT-LIB

introduced option for nat-as-int in SMT

tuned signature -- clarified modules;

--HG--
rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML

tuned message;

@{command_spec} is superseded by @{command_keyword};

optionally display statistics for Z3 proof reconstruction

avoid more than one data slot per module

limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

renamed new SMT module from 'SMT2' to 'SMT'

--HG--
rename : src/HOL/SMT2.thy => src/HOL/SMT.thy
rename : src/HOL/Tools/SMT2/smt2_builtin.ML => src/HOL/Tools/SMT/smt_builtin.ML
rename : src/HOL/Tools/SMT2/smt2_config.ML => src/HOL/Tools/SMT/smt_config.ML
rename : src/HOL/Tools/SMT2/smt2_datatypes.ML => src/HOL/Tools/SMT/smt_datatypes.ML
rename : src/HOL/Tools/SMT2/smt2_failure.ML => src/HOL/Tools/SMT/smt_failure.ML
rename : src/HOL/Tools/SMT2/smt2_normalize.ML => src/HOL/Tools/SMT/smt_normalize.ML
rename : src/HOL/Tools/SMT2/smt2_real.ML => src/HOL/Tools/SMT/smt_real.ML
rename : src/HOL/Tools/SMT2/smt2_solver.ML => src/HOL/Tools/SMT/smt_solver.ML
rename : src/HOL/Tools/SMT2/smt2_systems.ML => src/HOL/Tools/SMT/smt_systems.ML
rename : src/HOL/Tools/SMT2/smt2_translate.ML => src/HOL/Tools/SMT/smt_translate.ML
rename : src/HOL/Tools/SMT2/smt2_util.ML => src/HOL/Tools/SMT/smt_util.ML
rename : src/HOL/Tools/SMT2/smtlib2.ML => src/HOL/Tools/SMT/smtlib.ML
rename : src/HOL/Tools/SMT2/smtlib2_interface.ML => src/HOL/Tools/SMT/smtlib_interface.ML
rename : src/HOL/Tools/SMT2/smtlib2_isar.ML => src/HOL/Tools/SMT/smtlib_isar.ML
rename : src/HOL/Tools/SMT2/smtlib2_proof.ML => src/HOL/Tools/SMT/smtlib_proof.ML
rename : src/HOL/Tools/SMT2/verit_isar.ML => src/HOL/Tools/SMT/verit_isar.ML
rename : src/HOL/Tools/SMT2/verit_proof.ML => src/HOL/Tools/SMT/verit_proof.ML
rename : src/HOL/Tools/SMT2/verit_proof_parse.ML => src/HOL/Tools/SMT/verit_proof_parse.ML
rename : src/HOL/Tools/SMT2/z3_new_interface.ML => src/HOL/Tools/SMT/z3_interface.ML
rename : src/HOL/Tools/SMT2/z3_new_isar.ML => src/HOL/Tools/SMT/z3_isar.ML
rename : src/HOL/Tools/SMT2/z3_new_proof.ML => src/HOL/Tools/SMT/z3_proof.ML
rename : src/HOL/Tools/SMT2/z3_new_real.ML => src/HOL/Tools/SMT/z3_real.ML
rename : src/HOL/Tools/SMT2/z3_new_replay.ML => src/HOL/Tools/SMT/z3_replay.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_literals.ML => src/HOL/Tools/SMT/z3_replay_literals.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_methods.ML => src/HOL/Tools/SMT/z3_replay_methods.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_rules.ML => src/HOL/Tools/SMT/z3_replay_rules.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_util.ML => src/HOL/Tools/SMT/z3_replay_util.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
rename : src/HOL/Word/Tools/smt2_word.ML => src/HOL/Word/Tools/smt_word.ML

prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;

clarifed module name;

--HG--
rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML
rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala
rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala

make SMT integration slacker w.r.t. bad apples (facts)

tuned signature;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;

new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code

synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
clarified signature -- cache init is unsynchronized and hopefully used at most once per file;

introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)

renamed "smt_fixed" to "smt_read_only_certificates"

outer syntax command definitions based on formal command_spec derived from theory header declarations;

prefer formally checked @{keyword} parser;

SMT fails if the chosen SMT solver is not installed

comments;

added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
proper name bindings;

make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option

Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;

limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
updated SMT certificate

more explicit errors to inform users about problems related to SMT solvers;
fall back to remote SMT solver (if local version does not exist);
extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18

be more precise: also merge option values

only print warning in a visible context (previously, the warning was printed more than once)

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)

made SML/NJ happy

differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
turned individual SMT solvers into components;
made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only");
tuned smt_filter interface

added option to enable trigger inference;
better documentation of triggers and SMT available options

moved SMT classes and dictionary functions to SMT_Utils

added option to modify the random seed of SMT solvers

centralized handling of built-in types and constants;
also store types and constants which are rewritten during preprocessing;
interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols);
removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)

keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)

look for certificates relative to the theory

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)