Wall-clock timeout

[Tomaqa]

It is possible to set it via API, SMT-LIB, or as a command-line parameter.
I did not implement it within the set-option command, hence within SMTConfig, because the timeout also takes an immediate action by starting a thread, which may stop the evaluation. The configuration may even be supplied by a user externally. It is also possible to specify this command after the solver was already created, which typically happens in SMT-LIB scripts. Using SMTConfig would require special treatment compared to other options, that is, to run an action once the option is set.

Resolves #766

We still do not support a timeout per query for incremental solving (as e.g. CVC5 does).

[Tomaqa]

In the end, I implemented it as a set-option and not as a separate command. If the timeout is set sooner than the existence of MainSolver, it takes effect automatically once the solver is created. Otherwise, the user is responsible for calling setTimeLimit manually if using the API. If parsing, Interpret does that automatically.

[Tomaqa]

In the last commits, except of some refactoring, I resolved compatibility issues with MacOS and fixed some narrowing conversions of SMTOption.

[Tomaqa]

I added more comments on how the synchronization works, based on cppreference.

The regression tests are unstable though (they may fail in the future), and also require large benchmarks.

[Tomaqa]

I moved the regression tests to a separate branch and replaced them with unit tests.
They only test MainSolver::setTimeLimit, though.
They, for example, do not test using SMTConfig::o_time_limit.

[Tomaqa]

I changed the behavior of SMTConfig::o_time_limit s.t. MainSolver checks it every time check() is called, but only if it is not already set. This works even for incremental solving, but if further checks are trigerred even after the timeout, the timeout is reset again. Do we want to, instead, continue returning unknown? If so, the solver must remember its internal state - that it is in timeout state.

With this, it was possible to include unit tests on SMTConfig::o_time_limit. Setting this option only makes sense when set before calling check(), but setting after the call does not affect the already running call.

[Tomaqa]

I changed the behavior of SMTConfig::o_time_limit s.t. MainSolver checks it every time check() is called

I realized that now it is a bit confusing, because the behavior is different if we call MainSolver::setTimeLimit and if we set time-limit in SMTConfig, because setTimeLimit starts the timer immediately, while the limit in SMTConfig is triggered only once check() is called.
There are indeed 3 different scenarios:

1. Time limit for each particular (check-sat) ~ time-limit-per-query (Implemented :time-limit-per-query #863)
2. Time limit since the first call of (check-sat) ~ time-limit ? (the current state)
3. Time limit since the limit is set

The advantage of (2) is that the semantics are clear and independent from the time it is set, as is usual for a configuration. The disadvantage is that, e.g., parsing the formula is excluded from the time limit, which may or may not be desired.

(3) is a bit complicated to implement as an option in SMTConfig outside of MainSolver, to be able to start the timer even before the MainSolver is constructed. We could use a separate SMT-LIB command for that, such as (set-time-limit <ms>), which would immediately start the solver and could only be called after (set-logic ..) (i.e., when MainSolver already exists).

All 3 options can be addressed as separate things. The question is which of them we want.

[Tomaqa]

This works even for incremental solving, but if further checks are trigerred even after the timeout, the timeout is reset again. Do we want to, instead, continue returning unknown? If so, the solver must remember its internal state - that it is in timeout state.

Currently, it actually keeps returning unknown after the first timeout. The reason is that we never reset the stop flag. We should implement resetStop in any case (we already have resetGlobalStop), but I am not sure if we want or do not want to call it at the end of each check() - because returning unknown until the user explicitly resets the timeout state (probably using an additional function for that instead of resetStop, like resetTimeLimit) seems to me as a good behavior.

I checked that CVC5 nor z3 return unknown, they simply terminate the whole program and output sth. like timeout. The timeout in Yices2 is actually time limit per query (supported by CVC5 and z3 as well). In the case of time limits per query, all of them return unknown if the specific query did not finish within the limit, regardless of previous results.

[Tomaqa]

CVC5 only supports tlimit-per in (set-option). Using tlimit in there has no effect. The option is only usable if CVC5 is executed as a binary, but not as a library. They even claim that it has no effect when set via API, if not executed as a binary.

It makes sense to me. I would not include the overall timeout in the options at all, only time-limit-per-query.
However, we can introduce an SMT-LIB command (set-time-limit <ms>) which would immediately start the timer. It would use the API call MainSolver::setTimeLimit, as well as the command line option --time-limit would.

This would ideally also require checking the stop flag not only within the solving, but also within adding assertions and preprocessing.

[Tomaqa]

I reverted to the previous solution where time-limit is executed immediately or as soon as MainSolver is initialized. When set via SMTConfig, it only takes effect implicitly when set before the MainSolver is initialized; otherwise, the user must call setTimeLimit explicitly, which is not a limitation when using the API (where SMTConfig is actually not necessary). Interpret, on the other hand, makes the call to setTimeLimit implicitly at the moment when the set-option is parsed - otherwise the user could not trigger the time limit at the desired moment.

As mentioned above, it should ideally also stop processing formulas and simplifying them once the time limit is reached, i.e., not only in the case of solving.

[BritikovKI]

Hmm, when do you think it will be called with long? 🤔
And why allow it even, if you anyway would cast it to int?

[BritikovKI]

Why not to convert it to int at this line instead of supporting SMTOption(long)?

[BritikovKI]

Also why break if ok is false? 🤔
This is the only place when Ok is used anyway, mb it is possible to omit it? Or do you want to use it in more places eventually?

[BritikovKI]

What's an intuition behind moving it in its own namespace?

[BritikovKI]

Why is separate struct needed for a single bool? 🤔 Do you think it will be extended?

[BritikovKI]

Should it be else if or else { assert(main_solver)}? Can it be that main_solver is null?

[BritikovKI]

Should it be milliseconds? 🤔
Why not seconds, do you think this much precision is needed?

[BritikovKI]

Hmm, does it mean you are not updating limit, but killing current solver and starting a new one basically?