| Wed, 18 Dec 2024 10:21:58 +0100 |
desharna |
added option "cache_dir" to Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 10:56:23 +0100 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| Mon, 11 Jul 2022 15:03:42 +0200 |
blanchet |
milder Sledgehammer messages
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalize slicing format
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
thread slices through
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalized output for forthcoming slicing model
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
disable slicing within SMT (in preparation for factoring it out)
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 17:23:01 +0200 |
desharna |
refactored Sledgehammer option "induction_rules"
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 15:25:30 +0200 |
desharna |
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
|
file |
diff |
annotate
|
| Wed, 12 May 2021 12:22:44 +0200 |
wenzelm |
avoid duplicate loading of ML file;
|
file |
diff |
annotate
| base
|