Change behaviour when ProgramBddContext::Assign fails

used to return bddfalse, now returns bddtrue. This is an overapproximation of
the intended assignment transformer, bddfalse would cause unsoundness in
solvers using the transformer.
cprover parser, change semantics of dead statement.

The hotfix so far was a skip statement.
Quoting Gerard Basler's PhD thesis, the meaning of dead statements for a model
checker is the same as non-deterministic assignment to the dead variables.
Using these semantics now.
Add a way to log the modifying operations on a ProgramBddContext, and then replay them.

This can be used to generate an identical buddy environment offline, to load
back a perviously saved bdd.
Test for replaying history.
Refactor test_semelem_impl a little bit

This will allow it to report more than failure at a time
Change BddLessThan::operator() to const
In WFA, use SemElemSet::ElementSet instead of the concrete type
Introduce new optional SemElem virtual functions hash() and containerLessThan()

These are used by SemElemSet; which one is used depends on the backing set type,
and will be used later. I suggest not overriding these functions if they cannot
operate quickly.

(containerLessThan() imposes an arbitrary strict weak order on semiring elements;
different pointers to the same element need to behave consistently and it needs to
be consistent with equals(), but aside from those requirements that's all that
needs to be met. In particular, semelem implementers needn't make it relate to the
semantic meaning, and users should not assume that it does.)

Both functions abort() in their default implementation.
Use unordered_map as the backing set for SemElemSet

This makes use of the hash() function introduced before. Commented-out
lines in SemElemSet.hpp allow switching between a couple different
choices (std::map, a node-based tree; boost::containers::flat_map, a
sorted-vector-based tree; and unordered_map, a hash table).

I had to comment out two test files because of these changes, but they
should be re-enabled soon.
Add more tests of SemElemSet and WFA::computeAllReachingWeights
Introduce SemElem::underApproximates()

Also put tests in test_semelem_impl
Override underApproximates() in BinRel to call bddImplies
Introduce SemElemSet::KeepWhat enum and related behavior:

- SemElemSet's constructors now take a KeepWhat
- The KeepWhat parameter controls whether the semiring will
  keep all (nonduplicate) elements, only minimal elements,
  or only maximal elements
- Only the KeepAllNonduplicates behavior is currently tested
- Extend/combine/equal/etc. can only be done between two
  SemElemSet instances with the same setting for KeepWhat
Fix test bug
Weired error in bp_parser. Now fixed

but I still think that I haven't semantically changed anything.
Add hash() override to SemElemSet

This just records the hash during initialization (we have to iterate
the set anyway) and returns it on request.
Add equal(sem_elem_t) to SemElemSet

The equal(SemElem*) override caused the equal(sem_elem_t) from SemElem
to be hidden, so you couldn't pass a sem_elem_t if the static type of
the SemElemSet was actually SemElemSet.
Test for saving a bdd, and restoring with a clean slate after restoring environment.
Rename stuff
Fix bug in SemElemSet:

For the KeepMinimalElements and KeepMaximalElements versions, we ALWAYS
added the new element even if it was subsumed by existing ones. (We
removed elements that were subsumed by the new one, but not the other
way around.)