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
239 stars 33 forks source link

Set support for cvc5 #690

Closed paulbrauner-da closed 4 months ago

paulbrauner-da commented 4 months ago

Hello, thank you for the great lib!

Sets are marked as unsupported by cvc5 in sbv, but cvc5 does in fact support them. Unfortunately it doesn't use the same syntax as z3 so SMTLib2.hs would need to emit different assertions based on the target prover, which it seems it doesn't right now.

LeventErkok commented 4 months ago

Correct. It’s a hassle to support different solvers when they disagree on the exact semantics and syntax. Until SMTLib committee takes up sets and standardizes support for them I’m hesitant to go down that route. Current implementation in SBV is rather tied to z3’’s notion of sets which can be either finite or co-finite. I believe CVC5 only supports finite sets, which would make the internals rather tricky to get right.

I recommend contacting SMTLib folks and asking for a standardization. I believe there were attempts in the past, but for whatever reason they didn’t come to bear fruit. If you want to submit a PR that adds support I can merge it provided it comes with enough tests to ensure the solver differences are gracefully handled. Otherwise, I’m afraid not much change will happen in SBV to support CVC5 sets.

Cheers!