History log of /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/quantHeuristicsLibBase.sml
Revision Date Author Comments
# 6a81a039 21-May-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove TABs from src

Will also make selftest to check that they aren't introduced


# bd77b8fb 20-Oct-2015 Michael Norrish <Michael.Norrish@nicta.com.au>

Delete trailing whitespace


# 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.


# 059e250f 15-Oct-2014 Piotr Trojanek <piotr.trojanek@gmail.com>

rename Ho_Net.empty_net to Ho_Net.empty

All similar structures (e.g. Net and Raw) use "empty" not "empty_net";
it seems right to follow a single naming convention.


# d2c33299 05-Nov-2014 Michael Norrish <michael.norrish@nicta.com.au>

Remove some Unicode in src/


# 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


# 1b7eb842 17-Oct-2012 Thomas Tuerk <thtuerk@thtuerk-desktop.(none)>

experimental tool, suggested by Ramana, for abbreviating subterms using quantifier heuristics
added


# 9b9370ac 17-Oct-2012 Thomas Tuerk <tt291@cl.cam.ac.uk>

quantifierHeuristics tweaks
- some tweaks to make sum_qp behave nicer
- for this some small changes that can be seen as
bug fixes or minor feature improvements


# 1ee7f40d 14-Oct-2012 Michael Norrish <michael.norrish@nicta.com.au>

Delete trailing whitespace in src and examples.


# 00891b6f 11-Oct-2012 Thomas Tuerk <tt291@cl.cam.ac.uk>

quantHeuristicsLib bug fixes

- back-chaining only applied weakening, if a rule could be applied
for both threngthening and weakening
- trouble with free type-variable clashes fixed


# 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


# 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