Use context manager for assumptions

[cjdrake]

It would be cool to do something like this:

with a & b & c:
    f.satisfy_one()

# OR

with a, b, c:
    f.restrict({...})

Would require a static stack of constraints located in the expr.py module. It would be very useful to integrate this with the PicoSAT assumptions capability, since that has nice performance.

[cjdrake]

Implemented support for satisfy_one b/c it's obvious. Also implemented for restrict. Still need to look into satisfy_all. I'm having second thoughts about whether it makes sense to do this for restrict. Will consider walking that one back before the next release.