| #
1c2225f4 |
|
29-Aug-2015 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
quantHeuristicsLib: fix handling of pairs, context cleanup
The heuristic for instantiating product variables was broken.
Nested pairs were broken. Pairs like (a, b, c) worked, while ((a,b), c)
did not. Moreover, context heuristics that recurse are now not any more
part of the basic quant parameter. This stops the quant-heuristics
looping sometimes, when the user isn't careful.
|
| #
7a88492a |
|
04-Jan-2013 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in src/
|
| #
e8736117 |
|
27-Dec-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
minor tweaks on quantHeuristicsLib, adept Holfoot to changes with MEM
|
| #
8c683b58 |
|
11-Oct-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
quantHeuristicLib tuning
- better name for traces
- list_no_len_qp added
- predefined filter functions added
|
| #
f9bf2f12 |
|
05-Oct-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
A bit more work on list_qp in order to handle LENGTH. For
LENGTH with large numbers, list_len_qp added.
Experimental support for removing redundant function application on
quantified variables added.
|
| #
5854343a |
|
21-Sep-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
bug-fix in Sanity.sml another cleanup of quantHeuristicsLib
|
| #
b0d02af8 |
|
18-Sep-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
extended interface for quantifier heuristics
Now additional context as well as lemmata used for weakening / strengthening can be added to quantifier heuristic parameters.
|
| #
68865120 |
|
11-Sep-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
Added support for context to quantifier heuristics, add sum_qp
|
| #
4480c57d |
|
24-Aug-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
cleanup of quantifier heuristics library
- more sensible names for guesses
- quantHeuristicsLib renamed to quantHeuristicsLibBase
- quantHeuristicsLibArgs renamed to quantHeuristicsLibParameters
- new shorter signature defined in quantHeuristicsLib
- adaptation of usage of quantHeuristicsLib
|