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
242 stars 34 forks source link

Support abduction in CVC5 #643

Closed LeventErkok closed 1 year ago

LeventErkok commented 1 year ago

These days CVC5 can produce abducts. Would be cool to see if we can support this in SBV, at least as a technology preview.

LeventErkok commented 1 year ago

Some info: https://cvc5.github.io/docs/cvc5-1.0.2/api/python/base/solver.html?highlight=abduct#cvc5.Solver.getAbduct

The easiest way would be to do this in query mode, and then send the solver the string (get-abduct) and (get-abduct-next) and see how that goes. Specifying the grammar might be a stretch goal, or something for the future. Translating the abduct back should be targeted first.

LeventErkok commented 1 year ago

Here's a simple example:

(set-logic QF_LIA)
(set-option :produce-abducts true)
(declare-fun x () Int)
(declare-fun y () Int)

(assert (>= x 0))
(get-abduct A (>= (+ x y) 2))

This prints:

(define-fun A () Bool (= y 2))

Intuitively, what this means is that to make sure the conjecture x + y >= 2 is true, you need to add the constraint y == 2.

Other than displaying the output string to the user, it's not clear to me how to integrate this better into SBV. So, perhaps this will be very similar to getInterpolant.