Change the interface for creating symbolic values in SBV so they

can be done in `IO` rather than the `Symbolic` monad.

This involves pulling out the SBV `State` value and making it avalaible
to operations via the `SBV` backend type that is passed into operations.
We guard the `State` value with an MVar to avoid potential data races.

In addition, let SBV automatically decide the quantifier type for variables
based on the type of query; we were previously doing this manually.