SMT-style push/pop assertion levels

[dewert99]

This adds push and pop methods to the SolverInterface, similar in style to the SMT-LIB (push) and (pop n).

push works by creating a fresh literal, and adding it as an assumption to each call solve_limited_th until the next pop. These literals are also implicitly added to each clause that is added until the next pop. This is fairly similar to how they could be manually implemented on top of a SolverInterface but has a few optimization from being implemented internally.

1. solver.v.assumptions can be reused to store literals corresponding to assertion levels instead of requiring a separate buffer.
2. solver.v.ok is now a u32 (0 corresponds to what would have been false, and anything else corresponds to what would have been true) which remembers what assertion levels are already known to be contradictory to avoid extra work.

[dewert99]

Sorry, this branch is ahead of #14, if you decide you don't want to merge #14 but you do want to merge this, I can try redo the change by itself.

[c-cube]

sorry, I think this belongs in an outer layer (a SMT solver, typically). I personally think push/pop is a bad interface anyway and check-sat-with-assumptions is better in almost all cases.