Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Utilize the reader monad in sbv to season the solver #7

Open
doyougnu opened this issue Nov 13, 2020 · 1 comment
Open

Utilize the reader monad in sbv to season the solver #7

doyougnu opened this issue Nov 13, 2020 · 1 comment
Assignees
Labels
enhancement New feature or request performance related to runtime performance

Comments

@doyougnu
Copy link
Owner

  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~.
@doyougnu doyougnu self-assigned this Nov 13, 2020
@doyougnu doyougnu added enhancement New feature or request performance related to runtime performance labels Nov 13, 2020
@doyougnu
Copy link
Owner Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request performance related to runtime performance
Projects
None yet
Development

No branches or pull requests

1 participant