Delete trailing whitespace in src/

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.

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.

Delete trailing whitespace in src/

This needs doing periodically, and is best done to a whole bunch of files
at once.

added documentation for quantifier heuristics library