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

Timeout Handling #65

Open
lucasberent opened this issue May 31, 2022 · 0 comments
Open

Timeout Handling #65

lucasberent opened this issue May 31, 2022 · 0 comments
Labels
feature New feature or request

Comments

@lucasberent
Copy link
Contributor

The timeout handling for the Exact Mapper could be improved:

  • currently, timeout is set to True (ExactMapper.757) whenever z3 returns does not return sat (ExactMapper.690), hence it is not possible to tell these situations apart from those in which unsat or unknown is reported (might be useful for debugging purposes).
  • the timeout set in the Configuration (Configuration.hpp.53) is merely passed to Z3. For one this seems to lead to problems as even though a timeout of e.g. 5400s is set, mapping times >5400 are reported in the MappingResult.
    Furthermore, simply passing the timeout to Z3 means that it is not a timeout for the whole mapping task (as implied by the name of the field). It would be nice to separate these notions of timeout and to enable the possibility of setting a timeout after which the whole task is simply killed, e.g., by using a process or thread like mechanism.
  • In relation to the previous aspect, it would be desirable to report both, times for the duration of the mapping construction and the SAT solving part instead of only the time needed by Z3 to do the solving.
@burgholzer burgholzer added the feature New feature or request label Jun 3, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants