get rid of visibility in MaSh -- it slows it down more than it helps

avoid loading MaSh file first time around for higher responsiveness of Sledgehammer

optimization in MaSh parsing

tuned ML

killed final stops in Sledgehammer and friends

be more careful before filtering out chained facts in Sledgehammer

proper consideration of chained facts in 'try0' minimization

a more generous hard timeout

early warning when Sledgehammer finds a proof

tuned signature -- clarified modules;

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

clarified modules;
tuned signature;

preplaying of 'smt' and 'metis' more in sync with actual method

preplaying of 'smt' and 'metis' more in sync with actual method

further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes

further reduced dependency on legacy async thread manager

removed legacy asynchronous mode in Sledgehammer

clarified markup;
tuned signature;

removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs

keep 'Pure.all' in goals when preplaying

use right context for preplay, to avoid errors in fact lookup

tuned signature -- prefer qualified names;

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

explicit message channels for "state", "information";
separate state_message_color;

renamed "pairself" to "apply2", in accordance to @{apply 2};

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

prefer explicit Keyword.keywords;

eliminated obsolete Proof.goal_message -- print outcome more directly;

discontinued obsolete Output.urgent_message;

don't call 'hd' on a possibly empty list

default on 'metis' for ATPs if preplaying is disabled

more informative preplay failures

rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures

honor 'dont_minimize' option when preplaying one-liner proof

record MaSh algorithm in spying data

tuned message

reintroduced MaSh hints, this time as persistent creatures

tuned output

tuning

export ML function

restored a bit of laziness

further minimize one-liner

tuning

eliminated needlessly complex message tail

eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)

rationalized preplaying by eliminating (now superfluous) laziness

moved code around

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

optimized computation

properly reconstruct helpers in Z3 proofs

shorten Sledgehammer output, as suggested by Andrei Popescu

avoid markup-generating @{make_string}

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures

renamed ML file

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

tuning

tuning

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

pass constant arguments to the built-in check function, cf. d2b1fc1b8e19

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)

handle "max_relevant" uniformly

honor the default max relevant facts setting from the SMT solvers in Sledgehammer

trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases

reraise interrupt exceptions

replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us

put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs

adjust Sledgehammer/SMT fudge factor

cosmetics

set Metis option on correct context, lest it be ignored

make "debug" mode of Sledgehammer/SMT more liberal

more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers

more precise error handling for Z3;
refactored some of the error handling code shared by ATP and SMT

use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on

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

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

better error message

better error message

cosmetics

interpret SMT_Failure.Solver_Crashed correctly

pick up SMT solver crashes and report them to the user/Mirabelle if desired

make SML/NJ happy

reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving

compile -- 7550b2cba1cb broke the build

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)

make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice

always use a hard timeout in Mirabelle

don't pass too many facts on the first iteration of the SMT solver

catch TimeOut exception

ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns

if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed

invoke SMT solver in a loop, with fewer and fewer facts, in case of error

cosmetics

use the SMT integration's official list of built-ins

standardize on seconds for Nitpick and Sledgehammer timeouts

clear identification;
thread "Auto S/H" (vs. manual S/H) setting through SMT

adapted SMT solver error handling to reflect latest changes in "SMT_Solver"

better list of irrelevant SMT constants

if "debug" is on, print list of relevant facts (poweruser request);
internal renaming

standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module

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

remove needless context argument;
prefer "Proof.context_of" to "#context o Proof.goal", since it considers any "using [[...]]"

tuning

proper error handling for SMT solvers in Sledgehammer

integrated "smt" proof method with Sledgehammer

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

tuning

more robust handling of "remote_" vs. non-"remote_" provers

generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)

replaced references with proper record that's threaded through

fixed signature of "is_smt_solver_installed";
renaming

renamed modules

remove more needless code ("run_smt_solvers");
tuning

got rid of duplicate functionality ("run_smt_solver_somehow");
added minimization command to SMT solver message

bring ATPs and SMT solvers more in line with each other

make Sledgehammer minimizer fully work with SMT

generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well

first step in adding support for an SMT backend to Sledgehammer

use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."

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

move SPASS's Flotter hack to "Sledgehammer_Reconstruct"

skip some "important" messages

refactoring: move ATP proof and error extraction code to "ATP_Proof" module

use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs

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

finish support for E 1.2 proof reconstruction;
this involves picking up the axiom and conjecture names specified using a "file" annotation in the TSTP file, since we cannot rely anymore on formula numbers (E 1.2 adds a strange offset)

clarify message

use same hack as in "Async_Manager" to work around Proof General bug

handle relevance filter corner cases more gracefully;
e.g. the minimizer selects 15 facts but "max_relevant = 14"

Sledgehammer should be called in "prove" mode;
otherwise the proof text won't fit into the proof document

tuning

tuning

implemented Auto Sledgehammer

more precise error messages when Vampire is interrupted or SPASS runs into an internal bug

better error reporting when the Sledgehammer minimizer is interrupted

use Future.fork rather than Thread.fork, so that the thread is part of the global thread management

some results of concurrency code inspection;

show the number of facts for each prover in "verbose" mode

make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread

If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user

show real CPU time

factor out code shared by all ATPs so that it's run only once

handle all whitespace, not just ASCII 32

speed up SPASS hack + output time information in "blocking" mode

minor refactoring

translate the axioms to FOF once and for all ATPs

run relevance filter in a thread, to avoid blocking

only kill ATP threads in nonblocking mode

share the relevance filter among the provers

got rid of the "theory_relevant" option;
instead, have fudge factors that behave more smoothly for all provers

rename sledgehammer config attributes

finished renaming

added "expect" feature of Nitpick to Sledgehammer, for regression testing

added "blocking" option to Sledgehammer to run in synchronous mode;
sometimes useful, e.g. for testing

remove useless var

remove needless parameter

improve SPASS hack, when a clause comes from several facts

consider "locality" when assigning weights to facts

renaming

reorganize options regarding to the relevance threshold and decay

make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
"max_relevant" is more reliable than "max_relevant_per_iter";
also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before;
SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)

get rid of "defs_relevant" feature;
nobody uses it and it works poorly

renamed "relevance_convergence" to "relevance_decay"

make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts

clean handling of whether a fact is chained or not;
more elegant and reliable than encoding it in the name

weed out junk in relevance filter

be more generous towards SPASS's -SOS mode

prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc.

tuning

no spurious trailing "\n" at the end of Sledgehammer's output

get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"

added "max_relevant_per_iter" option to Sledgehammer

improve SPASS clause numbering hack

more debug output

prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch

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

reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF

fix embarrassing bug in elim rule handling, introduced during the port to FOF

fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization

don't choke on synonyms when parsing SPASS's Flotter output + renamings;
the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

fix bug in the newly introduced "bound concealing" code

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
this replaces the previous, somewhat messy solution of adding "extra" clauses

handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"

work around atomization failures

perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs

fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)

generate correct names for "$true" and "$false";
this was lost somewhere in the non-clausification

don't assume canonical rule format

avoid "clause" and "cnf" terminology where it no longer makes sense

"axiom_clauses" -> "axioms" (these are no longer clauses)

remove the "extra_clauses" business introduced in 19a5f1c8a844;
it isn't working reliably because of:
* relevance_override
* it is ignored anyway by TPTP generator
A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable

handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on

minor refactoring

fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses

revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
we can no longer just count the formulas, because for some reason E's numbering either no longer starts at 1 or it doesn't increment by 1 at each step

renaming

improve detection of installed SPASS

minor refactoring

more refactoring

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

rename

--HG--
rename : src/HOL/Tools/ATP_Manager/atp_manager.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML