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
Is your feature request related to a problem? Please describe.
When checking some complex setup, it is common case when some paths are not covered well because of branching solvers timeouts, especially on working machines with weak CPU. Halmos doesn't print any messages about branching solver timeouts and it may be not obvious for a user that something is wrong and solver-timeout-branching parameter should be increased.
Describe the solution you'd like
I see several ways to enhance it:
Print timeout rate during execution (just like op/s rate, print successful/timeouted branching statements) so user can see that rate is high and increase it in the next run. Or print Halmos warning when it see that timeout rate is high.
Make dynamic solver-timeout-branching option, that is derived from op/s rate. For example, in the start of run 1 ms may be enough, but the longer the run lasts, the more difficult calculations become and op/s rate becoming lower. It is pretty natural for me that branching timeout should be increased in such case.
The text was updated successfully, but these errors were encountered:
Is your feature request related to a problem? Please describe.
When checking some complex setup, it is common case when some paths are not covered well because of branching solvers timeouts, especially on working machines with weak CPU. Halmos doesn't print any messages about branching solver timeouts and it may be not obvious for a user that something is wrong and
solver-timeout-branching
parameter should be increased.Describe the solution you'd like
I see several ways to enhance it:
solver-timeout-branching
option, that is derived from op/s rate. For example, in the start of run 1 ms may be enough, but the longer the run lasts, the more difficult calculations become and op/s rate becoming lower. It is pretty natural for me that branching timeout should be increased in such case.The text was updated successfully, but these errors were encountered: