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

`checkSatWith` in analogy to `satWith` #715

Closed andreasabel closed 1 week ago

andreasabel commented 1 month ago

It is easy to get debug output by swapping sat for satWith. https://hackage.haskell.org/package/sbv-10.10/docs/Data-SBV.html#v:satWith

Would be great to have a similarly comfortable checkSatWith that complements checkSat: https://hackage.haskell.org/package/sbv-10.10/docs/Data-SBV-Control.html#v:checkSat

I didn't find a way to set the SMTConfig record in the Query monad so that it would be used for checkSat. But maybe it is easy and I just got lost in the API?

LeventErkok commented 1 month ago

When you have a query, it's wrapped up in a call to runSMT, right? That's where you should be configuring the solver, by using runSMTWith and passing z3{verbose=True}.

Does that not work for you?

LeventErkok commented 3 weeks ago

@andreasabel Is this addressed? If so, I'd like to close the ticket. Cheers..

LeventErkok commented 1 week ago

I think this is handled with the runSMTWith call. Feel free to re-open if you still have issues.