With the parallel version of vsmt we have to season the solver with the
variational core. This means that we actually compute ~n~ ~IL~'s where ~n~
is the number of threads. This is likely a small price to pay for the
parallelism but could certainly be reduced. SBVs ~SymbolicT~ is a reader
monad over ~IO~ but sbv doesn't export the ~ReaderT~ type class instance,
so in the main thread we can season, then grab the state with
~T.symbolicEnv~ but then there is no way for me to call ~local~ over the
thread instances and thus no way to replace the thread states with the
seasoned state. Hence, we are forced recompute the state for each thread
with a call with ~toIL~.
Note that we could season the solver for every recursive call, that is:
You start solving
generate a variational core
capture solver state
season threads with solver state
when a new choice is found, each alternative will be tried
this means that the new vpl formulas, which represent each alternative's variant, will introduce new non-variational terms that were previously blocked by the choice
thus we generate a new variational core for each alternative
then at this point we can capture the solver state, and re-season whichever thread receives the request to process that alternative
hence we'd save time calculating the new variational core for any subsequent recursive calls which would result from finding new un-seen choices in the recursive call