CVC5 timeout implementation

[Avgor46]

Hi!

I am trying to implement timeout on query to CVC5 solver. I am aware of non-existence of such interface in library (there is ShutdownManager, but it does not implement timeout by itself). If I want to timeout solver, I need to run it in separate thread. So, according to the description of SolverContext, I have to create new SolverContext and transfer formulas from original context to the new one using translateFrom method. This method uses parse method which it is not implemented for CVC5...

I also tried to pass formulas to new context prover without conversion and got error io.github.cvc5.CVC5ApiException: Given term is not associated with the term manager of this solver. And also tried to call isUnsat from old context in new thread which resulted in error in native code.

So, is it real to implement timeout for CVC5 solver? Maybe I am missing something...

[kfriedberger]

Hi.

There’s no need to create a second SolverContext to implement a timeout for a solver. You can use the ShutdownManager to handle this. While the ShutdownManager itself doesn’t provide a built-in timeout mechanism, it can still be effectively used for this purpose by triggering it from a separate thread that monitors the timeout.

There is an example for this in the test files:

java-smt/src/org/sosy_lab/java_smt/test/TimeoutTest.java

Lines 131 to 150 in 08820e3

	private void testBasicProverTimeout(
	Supplier<BasicProverEnvironment<?>> proverConstructor, BooleanFormula instance)
	throws InterruptedException, SolverException {
	Thread t =
	new Thread(
	() -> {
	try {
	Thread.sleep(delay);
	shutdownManager.requestShutdown("Shutdown Request");
	} catch (InterruptedException exception) {
	throw new UnsupportedOperationException("Unexpected interrupt", exception);
	}
	});
	try (BasicProverEnvironment<?> pe = proverConstructor.get()) {
	pe.push(instance);
	t.start();
	assertThrows(InterruptedException.class, pe::isUnsat);
	}
	}

There is a limitation: we currently do not support "timeout per prover instance", because the ShutdownManager is shared across the whole solver instance. Thus, all running SAT-checks are aborted.

[Avgor46]

Could I use corresponding SolverContext after shutdown and try to solve other set of constraints with new prover?

[kfriedberger]

That’s a great question! While I haven’t personally tried this, it appears that once the ShutdownManager is triggered, it sends an interrupt signal to all associated components. Since the shutdown operation is currently designed to be a one-time action, attempting to reuse the SolverContext and shutting it down again might lead to unexpected behaviour. You might need an independent SolverContext for such cases.

[Avgor46]

I'll definitely try to use the same context tomorrow) And if it doesn't work, it seems impossible to reuse previously generated constraints in new CVC5 context due to the unimplemented parse method( Or is there some way to do it even after shutdown? (I hope so)

[Avgor46]

So using the same SolverContext after the shutdown request causes all subsequent calls to isUnsat to throw InterruptedException (not immediately. Maybe it solves the passed constraints, but it does not matter). The only way I can see to use the same set of constraints (with small differences - removing constraints that caused timeout) is to use dumpFormulaImpl and use solver as a binary. That seems like a bad hack...

[kfriedberger]

Well, your use-case is valid and we need to think about a reusable interrupt-handler, i.e., one that can be triggered multiple times.

Instead of the current ShutdownManager, we would need an Interruptmanager that differs in the following features:

• if triggered, notify all registered handlers once. If triggered again, notify them again.
• compatible with ShutdownManager, such that existing use-cases still keep working.

This sounds simple, but the details can be difficult. I would assume that most solvers have no problem with being interrupted several times. We need to test this.