search

ekmett / ersatz

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

QSAT: depqbf requires extra option to extract model #89

Closed jwaldmann closed 4 months ago

jwaldmann commented 4 months ago

I was trying a QBFSAT example with DepQBF 6.03, and got unexcpected results.

I think the problem is that ersatz calls depqbf --qdo but that gives an error

 [QDPLL] qdpll_get_value at line 18904: Must configure solver with '--no-dynamic-nenofex' to extract values!
Aborted (core dumped)

When I add that option (manually), a model is printed.

I think the most flexible solution is that ersatz should provide 

depqbfPathOptions :: MonadIO m => FilePath -> [Text] -> Solver QSAT m

cf. #44 (for SAT)