search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

fast-all-sat does not support uninterpreted functions #583

Closed LeventErkok closed 3 years ago

LeventErkok commented 3 years ago

The fast allSat algorithm currently does not handle uninterpreted functions. If those exist, we fall back to the regular (slow) allSat algorithm.

NB. Fast all-sat also doesn't support if you have uninterpreted sorts; nothing much we can do there since domain splitting is not possible with an uninterpreted sort.

This is very low ROI, but we can add support for fast-all-sat with uninterpreted functions. But the code required is rather hefty, and this is really not the common use case at all; so probably not worth the effort complexity. Dropping this here as a note should someone be inclined to play around with this and see how it goes.

LeventErkok commented 3 years ago

On second thought, this is actually much harder than I thought because there's no standard way of writing a lambda in SMTLib. So, better go the slow route if there are uninterpreted functions.