| author | wenzelm |
| Wed, 30 Sep 2009 00:27:19 +0200 | |
| changeset 32770 | c6e6a4665ff5 |
| parent 32574 | 719426c9e1eb |
| permissions | -rw-r--r-- |
| 32469 | 1 |
Options for sledgehammer: |
2 |
||
3 |
* prover=NAME: name of the external prover to call |
|
|
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32541
diff
changeset
|
4 |
* prover_timeout=TIME: timeout for invoked ATP (seconds of process time) |
|
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32541
diff
changeset
|
5 |
* prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time) |
| 32469 | 6 |
* keep=PATH: path where to keep temporary files created by sledgehammer |
| 32525 | 7 |
* full_types: enable full-typed encoding |
8 |
* minimize: enable minimization of theorem set found by sledgehammer |
|
|
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32541
diff
changeset
|
9 |
* minimize_timeout=TIME: timeout for each minimization step (seconds of |
|
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32541
diff
changeset
|
10 |
process time) |
|
32522
1b70db55c811
Mirabelle: command-line action options may either be key=value or just key
boehmes
parents:
32511
diff
changeset
|
11 |
* metis: apply metis with the theorems found by sledgehammer |