Skip to content

Timeout Handling #65

Open
Open
@lucasberent

Description

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.

Metadata

Assignees

No one assigned

    Labels

    featureNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions