| #
8aec7217 |
|
01-Feb-2018 |
wenzelm <none@none> |
tuned signature: more operations;
|
| #
185dcd47 |
|
02-Apr-2016 |
wenzelm <none@none> |
prefer infix operations;
|
| #
456ff485 |
|
01-Feb-2016 |
blanchet <none@none> |
preplaying of 'smt' and 'metis' more in sync with actual method
|
| #
5cbf1a62 |
|
01-Feb-2016 |
blanchet <none@none> |
preplaying of 'smt' and 'metis' more in sync with actual method
|
| #
db1337ca |
|
14-Nov-2015 |
wenzelm <none@none> |
more standard ML, to make SML/NJ more happy;
|
| #
dab127d3 |
|
10-Nov-2015 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
generalized so that is also works for veriT proofs
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
12791f01 |
|
03-Aug-2014 |
blanchet <none@none> |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
| #
66c99a97 |
|
01-Aug-2014 |
blanchet <none@none> |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
| #
5ce41f58 |
|
01-Aug-2014 |
blanchet <none@none> |
careful when compressing 'obtains'
|
| #
b831048c |
|
01-Aug-2014 |
blanchet <none@none> |
try to get rid of skolems first
|
| #
1d5d4aaa |
|
01-Aug-2014 |
blanchet <none@none> |
no need to 'obtain' variables not in formula
|
| #
0f05e678 |
|
30-Jul-2014 |
blanchet <none@none> |
cascading timeout in parallel evaluation, to rapidly find optimum
|
| #
b8f4c9ec |
|
29-Jul-2014 |
blanchet <none@none> |
also try 'metis' with 'full_types'
|
| #
7a20679e |
|
24-Jun-2014 |
blanchet <none@none> |
don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
|
| #
047b3f9c |
|
12-Jun-2014 |
blanchet <none@none> |
renamed Sledgehammer options
|
| #
919b863a |
|
02-Jun-2014 |
blanchet <none@none> |
avoid division by 0
|
| #
312fdfa6 |
|
21-May-2014 |
blanchet <none@none> |
tuning
|
| #
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
|
| #
4bb45d8b |
|
05-Feb-2014 |
blanchet <none@none> |
more exception cleanup + more liberal compressions of steps that timed out
|
| #
0a449e5a |
|
05-Feb-2014 |
blanchet <none@none> |
tuned code to avoid noncanonical (and risky) exception handling
|
| #
52115a9f |
|
05-Feb-2014 |
blanchet <none@none> |
got rid of indices
|
| #
2409f2f5 |
|
05-Feb-2014 |
blanchet <none@none> |
corrected wrong 'meth :: _' pattern maching + tuned code
|
| #
7f5432b9 |
|
04-Feb-2014 |
blanchet <none@none> |
more generous Isar proof compression -- try to remove failing steps
|
| #
484184e5 |
|
04-Feb-2014 |
blanchet <none@none> |
tweaked handling of 'hopeless' methods
|
| #
477409cf |
|
04-Feb-2014 |
blanchet <none@none> |
tuned code
|
| #
a41de456 |
|
04-Feb-2014 |
blanchet <none@none> |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
| #
49489676 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
f45f571b |
|
03-Feb-2014 |
blanchet <none@none> |
more liberal step merging
|
| #
71a89b87 |
|
03-Feb-2014 |
blanchet <none@none> |
don't lose additional outcomes
|
| #
2cd0300a |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
fb11429b |
|
03-Feb-2014 |
blanchet <none@none> |
generate comments in Isar proofs
|
| #
9f4f1efb |
|
03-Feb-2014 |
blanchet <none@none> |
allow merging of steps with subproofs
|
| #
af459cea |
|
03-Feb-2014 |
blanchet <none@none> |
tuned data structure
|
| #
a1950e5b |
|
03-Feb-2014 |
blanchet <none@none> |
more flexible compression, choosing whichever proof method works
|
| #
3da4844f |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
ea1509c7 |
|
03-Feb-2014 |
blanchet <none@none> |
better time slack, to account for ultra-quick proof methods
|
| #
b6111183 |
|
03-Feb-2014 |
blanchet <none@none> |
crucial fix: use right version of the step
|
| #
31457036 |
|
03-Feb-2014 |
blanchet <none@none> |
more thorough, hybrid compression
|
| #
0cc92ff3 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
c0348805 |
|
03-Feb-2014 |
blanchet <none@none> |
centralize more preplaying
|
| #
714b0a4e |
|
03-Feb-2014 |
blanchet <none@none> |
centralize preplaying
|
| #
fcc30082 |
|
03-Feb-2014 |
blanchet <none@none> |
tuned
|
| #
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
|
| #
e8565325 |
|
03-Feb-2014 |
blanchet <none@none> |
when merging, don't try methods that failed or timed out for either of the steps for the combined step
|
| #
58f3d3c0 |
|
02-Feb-2014 |
blanchet <none@none> |
more data structure rationalization
|
| #
f7251444 |
|
02-Feb-2014 |
blanchet <none@none> |
more data structure rationalization
|
| #
96efc941 |
|
02-Feb-2014 |
blanchet <none@none> |
refactoring of data structure (step 2)
|
| #
bcb3a3ff |
|
02-Feb-2014 |
blanchet <none@none> |
refactor data structure (step 1)
|
| #
2ef3a348 |
|
02-Feb-2014 |
blanchet <none@none> |
tuned factor
|
| #
310097d2 |
|
02-Feb-2014 |
blanchet <none@none> |
take intersection rather than union of methods when merging steps -- more efficient and natural
|
| #
a3855579 |
|
02-Feb-2014 |
blanchet <none@none> |
merge proof methods
|
| #
47bd3a59 |
|
02-Feb-2014 |
blanchet <none@none> |
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
|
| #
91ba1387 |
|
02-Feb-2014 |
blanchet <none@none> |
reset timing information after changes
|
| #
348374bc |
|
31-Jan-2014 |
blanchet <none@none> |
generalized preplaying infrastructure to store various results for various methods
|
| #
33d1a2d4 |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
70b7915d |
|
31-Jan-2014 |
blanchet <none@none> |
tuned ML function names
|
| #
fed5d9bd |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
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
|