isabelle update -u path_cartouches;

add reconstruction by veriT in method smt

split SMT reconstruction into library

Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.

avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle

ran isabelle update_op on all sources

more symbols;

euclidean rings need no normalization

--HG--
extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05

added options to make veriT more complete

towards support for HO SMT-LIB

pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better

introduced option for nat-as-int in SMT

isabelle update_cartouches -c -t;

recovered from a9c0572109af;

fixing premises in veriT proof reconstruction

isabelle update_cartouches;

updated SMT module and Sledgehammer to fully open source Z3

more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT

added one more CVC4 option that helps Judgment Day (10 theory version)

added Z3 reconstruction rule suggested by F. Maric

one more CVC4 option that helps

renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names

added CVC4 option that helps on JD

removed explicit '--quant-cf' option to CVC4, now that it's the default

parse CVC4 unsat cores

made CVC4 support work also without unsat cores

modernized header uniformly as section;

use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating

strengthened 'moura' method

made 'moura' tactic more powerful

added interface for CVC4 extensions

added useful options to CVC4

tuned method description

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

updated to named_theorems;
modernized setup;
tuned;

reduces Sledgehammer dependencies

tuning

use 'ctr_sugar' abstraction in SMT(2)

fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective

moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle

full path

removed obsolete remote_cvc3 and remote_z3

activation of Z3 via "z3_non_commercial" system option (without requiring restart);

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;

prefer ML_file over old uses;

more standard method setup;

renamed "smt_fixed" to "smt_read_only_certificates"

declare command keywords via theory header, including strict checking outside Pure;

replace higher-order matching against schematic theorem with dedicated reconstruction method

improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

load lambda-lifting structure earlier, so it can be used in Metis

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)

removed old (unused) SMT monomorphizer

clarified meaning of monomorphization configuration option by renaming it

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

made Z3 the default SMT solver again

tuned text

added hints about licensing restrictions and how to enable Z3

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

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)

only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
hide internal constants z3div and z3mod;
rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod

fixed trigger inference: testing if a theorem already has a trigger was too strict;
fixed monomorphization with respect to triggers (which might occur schematically)

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)

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)

also support higher-order rules for Z3 proof reconstruction

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

added support for quantifier weight annotations

added prove reconstruction for injective functions;
added SMT_Utils to collect frequently used functions

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)

added crafted list of SMT built-in constants

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

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

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

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

load cache_io before code generator; moved adhoc-overloading to generic tools

--HG--
rename : src/HOL/Library/Adhoc_Overloading.thy => src/Tools/Adhoc_Overloading.thy
rename : src/HOL/Library/adhoc_overloading.ML => src/Tools/adhoc_overloading.ML

added function update examples and set examples

renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

use Z3's builtin support for div and mod

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

use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

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

integrated SMT into the HOL image