compile

removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)

isabelle update -u path_cartouches;

tuned;

isabelle update_cartouches;

more explicit indication of Async_Manager_Legacy as Proof General legacy;

--HG--
rename : src/HOL/Tools/Sledgehammer/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager_legacy.ML

modernized header uniformly as section;

made 'moura' tactic more powerful

moved skolem method

added 'skolem' method, esp. for 'obtain's generated from Z3 proofs

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

fixed parsing of one-argument 'file()' in TSTP files

use right delimiters for Waldmeister proofs

simplified code

moved code around

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML => src/HOL/Tools/ATP/atp_waldmeister.ML

tuned dependencies

reduces Sledgehammer dependencies

moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle

removed old SMT module from Sledgehammer

undo rewrite rules (e.g. for 'fun_app') in Isar

more simplification of trivial steps

integrate SMT2 with Sledgehammer

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

got rid of 'try0' step that is now redundant

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

moved ML code around

refactor large ML file

renamed many Sledgehammer ML files to clarify structure

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_run.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_print.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

tuned ML file name

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)

hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps

optimize isar-proofs by trying different proof methods

moved code -> easier debugging

split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations

simplified byline, isar_qualifier

renamed sledgehammer_shrink to sledgehammer_compress

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML => src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML

move preplaying to own structure

renamed sledgehammer_isar_reconstruct to sledgehammer_proof

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML

put shrink in own structure

put annotate in own structure

added proof minimization code from Steffen Smolka

prefer ML_file over old uses;

renamed ML files

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML

rationalize relevance filter, slowing moving code from Iter to MaSh

moved most of MaSh exporter code to Sledgehammer

further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)

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

first step in sharing more code between ATP and Metis translation

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML => src/HOL/Tools/ATP/atp_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML => src/HOL/Tools/ATP/atp_translate.ML

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

compile

split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

load "try" after "Metis" and move "Async_Manager" back to Sledgehammer

--HG--
rename : src/HOL/Tools/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager.ML

integrated "smt" proof method with Sledgehammer

reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers

moved sledgehammer to Plain; tuned dependencies

renamed files

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure

tuning

move Metis into Plain

--HG--
rename : src/HOL/Tools/Sledgehammer/metis_reconstruct.ML => src/HOL/Tools/Metis/metis_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactics.ML
rename : src/HOL/Tools/Sledgehammer/metis_translate.ML => src/HOL/Tools/Metis/metis_translate.ML

remove Meson from Sledgehammer

encode number of skolem assumptions in them, for more efficient retrieval later

finished renaming file and module

rename file

--HG--
rename : src/HOL/Tools/Sledgehammer/meson_clausifier.ML => src/HOL/Tools/Sledgehammer/meson_clausify.ML

rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"

--HG--
rename : src/HOL/Tools/Sledgehammer/clausifier.ML => src/HOL/Tools/Sledgehammer/meson_clausifier.ML

added new "Metis_Reconstruct" module, temporarily empty

rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"

--HG--
rename : src/HOL/Tools/Sledgehammer/metis_clauses.ML => src/HOL/Tools/Sledgehammer/metis_translate.ML

factored out TSTP/SPASS/Vampire proof parsing;
from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"

rename internal Sledgehammer constant

setup Auto Sledgehammer

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine

finish moving file

finished renaming

encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed

move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML

consequence of directory renaming

minor refactoring

standardize "Author" tags

reorder ML files in theory

more refactoring

rename "ATP_Manager" ML module to "Sledgehammer";
more refactoring to come

complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"

no setup is necessary anymore

factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration

reorder ML files

renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML => src/HOL/Tools/Sledgehammer/metis_clauses.ML

merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME

renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML => src/HOL/Tools/Sledgehammer/clausifier.ML

more moving around of ML files in "Sledgehammer.thy"

move "MESON" up;
the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti

never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts

killed legacy "neg_clausify" and "clausify"

factor out TPTP format output into file of its own, to facilitate further changes

adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"

proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter

added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)

move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"

now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script

--HG--
rename : src/HOL/Tools/ATP_Manager/atp_wrapper.ML => src/HOL/Tools/ATP_Manager/atp_systems.ML

renamed module "ATP_Wrapper" to "ATP_Systems"

move the minimizer to the Sledgehammer directory

--HG--
rename : src/HOL/Tools/ATP_Manager/atp_minimal.ML => src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML

added "modulus" and "sorts" options to control Sledgehammer's Isar proof output

get rid of Polyhash, since it's no longer used

add new file "sledgehammer_util.ML" to setup

move all ATP setup code into ATP_Wrapper

move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later

more Sledgehammer refactoring

renamed "ATP_Linkup" theory to "Sledgehammer"

--HG--
rename : src/HOL/ATP_Linkup.thy => src/HOL/Sledgehammer.thy