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

tuning

correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code

removed needless complication for modern SMT solvers

interleave (co)datatypes in the right order w.r.t. dependencies

added codatatype support for CVC4

added interface for CVC4 extensions

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

avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files

corrected treatment of applications of built-in functions to higher-order terms

removed debugging facilities accidentally left in the committed code

generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)

moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)

allow lambda-lifting without triggers

generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
maintain extra-logical information when introducing explicit application;
handle let-expressions properly

export lambda-lifting code as there is potential use for it within Sledgehammer

slightly more general treatment of mutually recursive datatypes;
treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)

made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)

fixed eta-expansion: use correct order to apply new bound variables

unfold and eta-contract let expressions before lambda-lifting to avoid bad terms

wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions

re-implemented support for datatypes (including records and typedefs);
added test cases for datatypes, records and typedefs

avoid ML structure aliases (especially single-letter abbreviations)

removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
removed odd retyping during folify (instead, keep all terms well-typed)

fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
fixed introduction of explicit application: use explicit application for every additional argument (grouping of arguments caused confusion when translating into the intermediate format)

tuned;

fix lambda-lifting: take level of bound variables into account and also apply bound variables from outer scope

made sml/nj happy

fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

fixed eta-expansion: introduce a couple of abstractions at once

fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor

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

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)

tuned

eta-reduce on the fly to prevent an exception

be more precise: only treat constant 'distinct' applied to an explicit list as built-in

added support for quantifier weight annotations

share and use more utility functions;
slightly reduced complexity for Z3 proof rule 'rewrite'

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)

introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list

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

do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)

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

reverse order of datatype declarations so that declarations only depend on already declared datatypes

added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet

hide constants and types introduced by SMT,
simplified SMT patterns syntax,
added examples for SMT patterns

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

integrated SMT into the HOL image