Extend map memoization of ffo/flo to nenoform formulae as well

[bestchai]

Right now, map checker memoizes ffo/flo for formulae which are strict subtrees of the original formula, but the checker often does ffo/flo on the negated nenoform of the formulae, so adding these to the memo table would be of great use.

Steps to implementation

1. Need tree equality b/w LTL formulae

• is top level equal?
• are kids equal (order matter for most binop except xor, <->,)
• are sets of formulae equal
• are constants equal
• are APs equal (by name)

• Test with some parsing tests

2. Collecting relevant APS

• add neno, nneno form to map when collecting for each individual formula
• create form -> nneno map
  • form -> nneno
  • nneno -> neno
  • neno -> nneno

• Test by accessing elements in form -> nneno map and making sure they are equal

3. getting all objects the same

• create top lvl neno, nneno version.
• for each:
  • traverse tree; at each node check both contents of
    • form -> APS: replace key if equal
    • form -> nneno: replace key, vals if equal

• test by using the new neno formulae function and making sure those elements are in the nenoform -> APs map

4. After all of the above, remove the use_memo diasblers around nnenoform calls

[Issue created by carolemieux: 2015-06-04]