Set support for cvc5 about sbv HOT 1 CLOSED

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!

from sbv.