Refactor and fix bug.

Now we start a new copy of the solver for each major action we
need to perform (improvement or solving).  This does lead to a little
repeated work but not much:  we just end asserting the givens in nested
implications multiple times.  Since implications tend not be nested
very many times, and usually there aren't many givens anyway, this
should not be a problem.

Note that we are still making extensive use if the solver's incremental
abilities: each of the major actions we perform makes multiple calls
to the solver, and it is important that we can reuse the state we've
already built up.