[daniel-raffler]

Hello,

this PR extends the JavaSMT API with a new call Solvers.available() to list all solvers that are supported on the current OS and CPU architecture. The call works similarly to the existing Solvers.values() and can be used to iterate over all available solvers during testing. Unlike Solvers.values() it skips over solvers that are not available on the platform, which helps to avoid failed tests due to missing libraries, when in reality the solver just isn't available for the testing platform

The PR also adds a new ant option "ignoreLinkErrors" to decide if tests should fail if solver binaries are not installed, or when there are linking issues due to missing system libraries. By default all SolverBasedTests are skipped if the solver binary can't be found, and only tests in SolverContextFactoryTest will fail as a warning about the configuration issue. Setting the new option "ignoreLinkErrors" to true causes the tests in SolverContextFactoryTest to also be skipped for the solver, while setting it to false makes all tests fail if there are missing binaries or linking issues

An example for how to use the "ignoreLinkErrors" can be found in the updated gitlab-ci.yml: Several of our solvers need a more recent version of libc than is available on the gitlab runner, and we're now setting "ignoreLinkErrors" to true to skip tests that would otherwise fail when these solver can't be loaded

[baierd]

An example for how to use the "ignoreLinkErrors" can be found in the updated gitlab-ci.yml: Several of our solvers need a more recent version of libc than is available on the gitlab runner, and we're now setting "ignoreLinkErrors" to true to skip tests that would otherwise fail when these solver can't be loaded

This is working as expected!
What we currently do is way too lenient, but we allow it due to our infrastructure lacking behind currently (which is a result of it being tied to other systems that we do not have full control over).

What is the use-case of ignoreLinkErrors besides that?
I currently do not think that we need or want this change at all.

Does ignoreLinkErrors distinguish between solvers not being available due to problems or due to there being no binaries available for a OS? Because the distinction matters! And we do not want to fail on a OS for a solver that is never available as there are no binaries. E.g. Bitwuzla should never fail on Windows or Mac, even with ignoreLinkErrors being false.

[daniel-raffler]

What is the use-case of ignoreLinkErrors besides that?

The other use-case is projects like CPAchecker that re-use our SolverBasedTest class for their own CI. These projects may want to set ignoreLinkErrors to false so that they get an error when some solvers can't be tested on their platform due to missing/outdated libraries, rather than just having the tests for that solver skipped silently

Does ignoreLinkErrors distinguish between solvers not being available due to problems or due to there being no binaries available for a OS?

Yes, we check if the solver is available for the OS/CPU architecture before trying to run the test

Maybe it would be clearer to split up the flag? That is, have one flag so that we can ignore link errors in SolverContextFactory in our gitlab CI, and another to throw an error if one of the SolverBasedTests fails due to missing libraries? Instead of that second flag we could probably also use a new method in SolverBasedTest that can then be overloaded by other users:

protected boolean ignoreLinkErrors() {
  return true;
}

[baierd]

What is the use-case of ignoreLinkErrors besides that?

The other use-case is projects like CPAchecker that re-use our SolverBasedTest class for their own CI. These projects may want to set ignoreLinkErrors to false so that they get an error when some solvers can't be tested on their platform due to missing/outdated libraries, rather than just having the tests for that solver skipped silently

Then, according to the use-case you described, this is not a boolean, but a list of ignored solvers (potentially by OS/CPU infrastructure) i would say.

Does ignoreLinkErrors distinguish between solvers not being available due to problems or due to there being no binaries available for a OS?

Yes, we check if the solver is available for the OS/CPU architecture before trying to run the test

Maybe it would be clearer to split up the flag? That is, have one flag so that we can ignore link errors in SolverContextFactory in our gitlab CI, and another to throw an error if one of the SolverBasedTests fails due to missing libraries? Instead of that second flag we could probably also use a new method in SolverBasedTest that can then be overloaded by other users:

protected boolean ignoreLinkErrors() {
  return true;
}

I don't see why this would be useful.

Before continuing with this, please find a concrete use-case outside of JavaSMT! I.e. a project like CPAchecker that uses JavaSMT and needs this!

[daniel-raffler]

Before continuing with this, please find a concrete use-case outside of JavaSMT! I.e. a project like CPAchecker that uses JavaSMT and needs this!

I added the flag because of this linked issue, specifically the comment here, which includes a possible use-case. To me the part about getting a list of supported solvers for the current platform with Solvers.available is much more important

Should I simply remove the flag for now?

[PhilippWendler]

I think it is crucial that this question is addressed: #692 (comment) (and because it is a conceptual question the discussion seems better placed in the issue).