You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
The timeout handling for the Exact Mapper could be improved:
sat
(ExactMapper.690), hence it is not possible to tell these situations apart from those in whichunsat
orunknown
is reported (might be useful for debugging purposes).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.
The text was updated successfully, but these errors were encountered: