search

ddsmt / ddSMT

A delta debugger for SMT benchmarks in SMT-LIB v2.
https://ddsmt.readthedocs.io
Other
50 stars 17 forks source link

Timeouts #6

Closed janeclange closed 6 years ago

janeclange commented 6 years ago

Removed Thread class -- seemed to fix timeouts

janeclange commented 6 years ago

Here's an idea: the initial run doesn't have a timeout, but its time is stored. The --rel flag indicates that timeouts are relative to the initial run. So "-t 2" makes tests time out after 2 seconds, but "-t 2 --rel" makes tests time out when they are 2 seconds longer than the initial run.

mpreiner commented 6 years ago

I would even make --rel -t 0 the default (all runs are limited by the golden runtime). We can also think of having a dynamic timeout, which uses the time of the current successful run as timout for the next runs.

janeclange commented 6 years ago

"--rel" is now "--abs", and the behavior of the previous --rel flag is now the default behavior. There's also "--dyn", which uses the most recent successful run as the basis for comparison instead of the initial run. I ran a few tests with --dyn and it seemed to be too aggressive of a timeout to be useful in the cases I tried, but there might be some other cases where it's good!