#
1c653e3e |
|
06-Feb-2017 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
implement simple quantifier heuristics The quantifier heuristics library is powerful, but often slow. The unwind conversions are fast, but have serious restrictions. This commits adds simple quantifier heuristics. They are based on the techniques developed for quantifier heuristics library, but only search gap guesses that don't contain free variables. Some very limited experiments suggest that it is similarly fast as unwind. It can handle all the cases unwind can handle. However, it supports also a much richer syntax. Moreover, it can instantiate in addition to universal and existential quantifiers also unique existential quantifiers, eliminate select and some. Moreover, it knows about pairs and lists.
|
#
136e6cb0 |
|
29-Aug-2015 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
fix selftest of quantHeuristicsLib The recent changes to how context is processed were unluckily not propagated to the selftests. This fixes the resulting errors.
|
#
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.
|
#
43f15686 |
|
02-Oct-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace in src/
|
#
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
|
#
d7a852e2 |
|
31-Jul-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
More on quantfier heuristics (I did not add all changes to the first commit)
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
e09c9510 |
|
18-Sep-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- reimplementation of quantHeuristicsLib. - move parts of quantHeuristicsLib to quantHeuristicsTools - selftest added Before guesses were justified by hand crafted theorems. There were modified using low level forward proof techniques. This resulted in quantHeuristicsLib being hard to understand and maintain. This reimplementation exploits recent addition to pairTools about handling paired quantification in order to introduce general predicates for guess theorems. Defining special predicates allows proving general lemmata easily. quantHeuristicsLib can the use the lemmata instead of low level proofs. However, this comes with the additional cost of introducing and eliminating tupled quantifiers. The new version is easier to understand and maintain. Moreover, it became much simpler to add user specified heuristics. The behavior changed slightly. For example, unnecessary priming of newly introduced variables has been eliminated.
|
#
aabca67e |
|
21-Dec-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
DISCH_ASM_CONV_TAC and DISCH_ASM_CONSEQ_CONV_TAC moved to ConseqConv.
|
#
92e8ca6b |
|
25-Nov-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
The changes that were discussed during my ARG Lunch talk last Tuesday. - "quant_heuristic_combine_argument" (qhca) has been renamed to "quant_param" (qp). - qp for record-types added - the pair_qp was modified to allow passing in functions to decide which pairs to split and how to name the new variables - for easier interaction with the simplifier "QUANT_INST_ss" was added - examples updated
|
#
cbad2295 |
|
16-Nov-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Some speed improvements. The most noticeable one is that minimising the number of occurences of a quantified variable (which is a very expensive operation) can be turned off now.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
e26ebae4 |
|
01-Aug-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
VARIANT_TAC and VARIANT_CONV added
|
#
630e97c5 |
|
29-Jul-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Now occurences of a variable are tried to be removed before a possible instantiation is searched. For example "?x. P /\ (f 2 = f x) /\ (Q (f x))" is simplied to "?x. P /\ (f 2 = f x) /\ (Q (f 2))" before an instantiation for x is searched. This enables the heuristics to instantiate x with 2. Moreover, an additional field was added to qhcas. Now one can specifiy a list of theorems used for the final simplification after an instantiation has been picked.
|
#
6f74d25a |
|
29-Jul-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Cheanup in interface of quantHeuristicsLib, added documentation to source code, clearer handling of stateful heuristics. Heuristics for common datatypes like pairs, lists, option types and nums have been defined in a new library quantHeuristicsArgsLib
|
#
84351d48 |
|
31-May-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
QUANT_CONV added
|
#
7231863d |
|
29-May-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Consolidation of the change, that quantHeuristics can now be restricted to work on just a few instantiations. The examples have been adapted and new examples for the new features added.
|
#
2feca92a |
|
28-May-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
added a filter function, that allows to just instantiate variables that are accepted by this filter
|
#
4eb9826d |
|
29-Jan-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some extensions of the interface, interface for caching added
|
#
388b0f45 |
|
27-Jan-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
EXT_PURE_QUANT_INSTANTIATE_CONSEQ_CONV and EXT_QUANT_INSTANTIATE_CONSEQ_CONV added
|
#
4d656577 |
|
08-Jan-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Major extensions and preformance improvements. Notice that the interface to write own heuristics changed.
|
#
9a7e8f8a |
|
17-Dec-2008 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
quantHeuristics is a library that instantiates quantifiers with guesses found by heuristics. Please see quantHeuristicsLib-examples.txt for some documentation and examples.
|