| #
75c0bb14 |
|
13-Aug-2016 |
blanchet <none@none> |
killed final stops in Sledgehammer and friends
|
| #
b09f23e4 |
|
27-Mar-2016 |
blanchet <none@none> |
early warning when Sledgehammer finds a proof
|
| #
b72de54b |
|
02-Oct-2015 |
blanchet <none@none> |
removed legacy asynchronous mode in Sledgehammer
|
| #
3c4cd10c |
|
29-Jan-2015 |
wenzelm <none@none> |
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
|
| #
76c7446c |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued obsolete Output.urgent_message;
|
| #
b3c8a973 |
|
12-Oct-2014 |
blanchet <none@none> |
special treatment of extensionality in minimizer
|
| #
21bbd523 |
|
30-Sep-2014 |
blanchet <none@none> |
tuned output in case of one-liner failure
|
| #
63548199 |
|
28-Aug-2014 |
blanchet <none@none> |
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
|
| #
e54369cc |
|
28-Aug-2014 |
blanchet <none@none> |
merged minimize and auto_minimize
|
| #
ac75f5e7 |
|
27-Aug-2014 |
blanchet <none@none> |
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
|
| #
d0ae16b7 |
|
04-Aug-2014 |
blanchet <none@none> |
cleaner 'compress' option
|
| #
46945d2f |
|
01-Aug-2014 |
blanchet <none@none> |
restored a bit of laziness
|
| #
cea8dd9f |
|
01-Aug-2014 |
blanchet <none@none> |
honor 'try0' also for one-liners
|
| #
c91b511e |
|
01-Aug-2014 |
blanchet <none@none> |
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
|
| #
4a5e0afe |
|
01-Aug-2014 |
blanchet <none@none> |
tuning
|
| #
9e867ae3 |
|
01-Aug-2014 |
blanchet <none@none> |
eliminated needlessly complex message tail
|
| #
16de9a98 |
|
01-Aug-2014 |
blanchet <none@none> |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
| #
d6b75aba |
|
01-Aug-2014 |
blanchet <none@none> |
rationalized preplaying by eliminating (now superfluous) laziness
|
| #
2d933a72 |
|
01-Aug-2014 |
blanchet <none@none> |
simplified minimization logic
|
| #
dc13715b |
|
30-Jul-2014 |
blanchet <none@none> |
put faster proof methods first
|
| #
e3069a3c |
|
30-Jul-2014 |
blanchet <none@none> |
use parallel preplay machinery also for one-line proofs
|
| #
3fc452c6 |
|
30-Jul-2014 |
blanchet <none@none> |
always minimize Sledgehammer results by default
|
| #
efb84113 |
|
30-Jul-2014 |
blanchet <none@none> |
added more proof methods for one-liners
|
| #
4c1fa505 |
|
30-Jul-2014 |
fleury <none@none> |
Whitespace and indentation correction.
|
| #
a40467dc |
|
30-Jul-2014 |
fleury <none@none> |
Basic support for the SMT prover veriT.
|
| #
047b3f9c |
|
12-Jun-2014 |
blanchet <none@none> |
renamed Sledgehammer options
|
| #
0b5e2e90 |
|
11-Jun-2014 |
blanchet <none@none> |
removed old SMT module from Sledgehammer
|
| #
c5b00bcc |
|
02-Jun-2014 |
fleury <none@none> |
basic setup for zipperposition prover
|
| #
de96180b |
|
21-May-2014 |
blanchet <none@none> |
properly reconstruct helpers in Z3 proofs
|
| #
312fdfa6 |
|
21-May-2014 |
blanchet <none@none> |
tuning
|
| #
516d4157 |
|
21-May-2014 |
blanchet <none@none> |
avoid markup-generating @{make_string}
|
| #
0798791c |
|
16-May-2014 |
blanchet <none@none> |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
| #
8589cd89 |
|
16-May-2014 |
blanchet <none@none> |
use 'simp add:' syntax in Sledgehammer rather than 'using'
|
| #
ac257535 |
|
13-Mar-2014 |
blanchet <none@none> |
delayed construction of command (and of noncommercial check) + tuning
|
| #
8b8b6855 |
|
13-Mar-2014 |
blanchet <none@none> |
simplified preplaying information
|
| #
c02fb67b |
|
13-Mar-2014 |
blanchet <none@none> |
honor the fact that the new Z3 can generate Isar proofs
|
| #
f936bab5 |
|
13-Mar-2014 |
blanchet <none@none> |
integrate SMT2 with Sledgehammer
|
| #
996c1544 |
|
14-Feb-2014 |
blanchet <none@none> |
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
|
| #
a3ad05b2 |
|
13-Feb-2014 |
blanchet <none@none> |
do the right thing with provers that exist only remotely (e.g. e_sine)
|
| #
e55345e9 |
|
13-Feb-2014 |
blanchet <none@none> |
repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
|
| #
cf3941c9 |
|
13-Feb-2014 |
blanchet <none@none> |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
| #
921f1021 |
|
05-Feb-2014 |
blanchet <none@none> |
try right bunch of methods
|
| #
a41de456 |
|
04-Feb-2014 |
blanchet <none@none> |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
| #
a2e9e36e |
|
03-Feb-2014 |
blanchet <none@none> |
properly overwrite replay data from one compression iteration to another
|
| #
9a5b75f2 |
|
03-Feb-2014 |
blanchet <none@none> |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
| #
62d265e3 |
|
03-Feb-2014 |
blanchet <none@none> |
added 'smt' option to control generation of 'by smt' proofs
|
| #
700f2e9d |
|
03-Feb-2014 |
blanchet <none@none> |
renamed ML file
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
|
| #
70573b75 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
94e4af3c |
|
03-Feb-2014 |
blanchet <none@none> |
merged 'reconstructors' and 'proof methods'
|
| #
fed5d9bd |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
945bedcb |
|
31-Jan-2014 |
blanchet <none@none> |
moved ML code around
|
| #
a16c4f61 |
|
31-Jan-2014 |
blanchet <none@none> |
compile
|
| #
1e8556d0 |
|
31-Jan-2014 |
blanchet <none@none> |
guarded against exception
|
| #
06f3d979 |
|
30-Jan-2014 |
blanchet <none@none> |
refactor large ML file
|
| #
eb52da60 |
|
31-Jan-2014 |
blanchet <none@none> |
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
|
| #
b58b6956 |
|
31-Jan-2014 |
blanchet <none@none> |
renamed ML file
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
|