Re-formulate memoization in checkers (expiry scheme/order of checking?)

[bestchai]

The current memoization schemes in the map trace (find first occurrence) and prefix tree (sub-formula memoization) need some rethinking because they take up ludicrous amounts of space. Consider the memory taken by the call to Texada Map (on the right):

(It's taking 5.7 Gbs -- and this is with the on-the-fly instantiator.)

Clearly some more resarch into effective memoization in C++ needs to be done. The hash function mechanism for unordered_map likely needs to be re-examined as well.

For the prefix tree, there has been some discussion of generating instantiations to take advantage of memoization on a certain binding by generating instantiations around that binding, For the map trace, it might be useful to reconsider the time saving of memoizing the first occurrence of individual events vs. how much space this takes.

[Issue created by carolemieux: 2014-09-01]
[Last updated on bitbucket: 2015-06-04]

[Comment created by carolemieux: 2015-05-05]
Full memoization for map trace checker revised in df183a2da4a0 solves much of the memory usage, but we don't have a deletion/expiry scheme yet.

[Comment created by carolemieux: 2015-04-29]
This will be done by adding new options for height of formula to be checked, and generating instantiations in an order s.t. the most subformulae have those instantiations.

[Comment created by carolemieux: 2015-06-04]
Issue 39 branch now deals solely with deletion/expiry scheme