ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

`depqbfPath`: Detect whether `--no-dynamic-nenofex` is needed based on the `depqbf` version #94

Closed RyanGlScott closed 1 month ago

RyanGlScott commented 1 month ago

Currently, the depqbfPath function only passes --qdo to the depqbf executable. This works well enough for versions of depqbf prior to 6.03. In version 6.03, however, depqbf also requires the use of the --no-dynamic-nenofex flag (see this comment). What's more, this flag is not backwards-compatible with pre-6.03 versions, as passing the flag to older versions will result in an error.

This results in an unfortunate situation where depqbfPath—which ideally should just do the right thing for most users—will only do the right thing for old versions of depqbfPath. For newer versions, ersatz users have no choice but to manually specify --no-dynamic-nenofex, like what was done in #93. We ought to do better, and I think we can. I propose that:

I have no idea how stable the output of depqbf --version is, but I hope it is stable enough to rely on.