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

Tactics and probes #652

Closed LeventErkok closed 1 year ago

LeventErkok commented 1 year ago

z3 provides tactics and probes.

Currently, the only way to access these from SBV to send raw strings to the solver. So, in a sense we have access to them. But it's clunky, and doesn't really match the SBV mentality.

We should explore if we can somehow make it fit better with SBV, come up with a tactic/probe language, and manipulate the terms perhaps. The design space needs to be explored before committing to any particular API, of course. (In particular, with regards to tactic combinators like repeat, orElse etc.

LeventErkok commented 1 year ago

This really doesn't have much of a use in SBV, since we don't really track goals like z3py does, for instance. Without a true motivating example, it's just a curiosity.