handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)

more direct invocation of Windows exe: avoid extra bash, cygpath, exec;

avoid extra subprocess -- potentially more robust on Cygwin;

isabelle update -u control_cartouches;

add reconstruction by veriT in method smt

clarified take/drop/chop prefix/suffix;

real oracle

clarified modules;

better handling of veriT's 'unknown' status

File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
clarified treatment of whitespace in some bash scripts;

moved remaining display.ML to more_thm.ML;

generate proper error instead of exception if goal cannot be atomized

prefer tactics with explicit context;

clarified context;

Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

made CVC4 support work also without unsat cores

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

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

standardized aliases;

made MaSh evaluation driver work with SMT solvers

prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);

Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here

Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)

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

more standard method setup;

renamed "smt_fixed" to "smt_read_only_certificates"

fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates

SMT fails if the chosen SMT solver is not installed

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

normalized aliases;

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

check if negating the goal is possible (avoids CTERM exception for Pure propositions)

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

made Z3 the default SMT solver again

dropped superfluous error message

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

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

avoid ML structure aliases (especially single-letter abbreviations)

perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required

run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers

make timeout part of the SMT filter's tail

split "smt_filter" into head and tail

fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)

re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context);
proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions);
built-in functions carry additionally their arity and their most general type;
slightly generalized the definition of fun_app

re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
added simple trigger inference mechanism;
added syntactic checks for triggers and quantifier weights;
factored out the normalization of special quantifiers (used to be in the eta-normalization part);
normalization now unfolds abs/min/max (not SMT-LIB-specific);
rules for pairs and function update are not anymore added automatically to the problem;
more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining nat-int coercions);
normalizations are now managed in a class-based manner (similar to built-in symbols)

moved SMT classes and dictionary functions to SMT_Utils

added option to modify the random seed of SMT solvers

tuned

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)

make SML/NJ happy

have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?

return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction

export more information about available SMT solvers

split up Z3 models into constraints on free variables and constant definitions;
reduce Z3 models by replacing unknowns with free variables and constants from the goal;
remove occurrences of the hidden constant fun_app from Z3 models

try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates

use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)

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

renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

honour timeouts which are not rounded to full seconds

trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)

check the return code of the SMT solver and raise an exception if the prover failed

turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user

return the process return code along with the process outputs

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)

simulate more closely the behaviour of the tactic

standardize timeout value based on reals

optionally drop assumptions which cannot be preprocessed

clarified error message

use proper context

trace assumptions before giving them to the SMT solver

capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1

honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter

optionally force the remote version of an SMT solver to be executed

tuned

added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)

joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface

keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs

chop_while replace drop_while and take_while

take_while, drop_while

add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions

more antiquotations;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

make SML/NJ happy

layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

integrated SMT into the HOL image