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

SMTDefinable for functions beyond 7 arguments? #670

Closed octalsrc closed 9 months ago

octalsrc commented 1 year ago

Is there a technical reason for SMTDefinable instances to stop at functions of 7 arguments?

It looks like I can follow the example of the instances defined here and provide an instance for 8-argument functions; are there any problems I should look-out for when doing so?

https://github.com/LeventErkok/sbv/blob/65e6df79c29ad47fcfa2e2d2cebc739f47977987/Data/SBV/Core/Model.hs#L2552

I'm working on an experiment in which I'm avoiding the SMT datatypes feature, and thus avoiding SBV tuples, so I'm declaring some uninterpreted functions that take many arguments. I finally ran into one that needs 8 arguments. Adding another instance for SMTDefinable seems like the most straightforward way to deal with this.

LeventErkok commented 1 year ago

No reason.. You just have to stop somewhere, and I picked 7.

If you submit a PR adding extra instances, I'd be happy to include merge it.