Documentation.SBV.Examples.Queries.Abducts

Demonstrates extraction of abducts via queries.

N.B. Interpolants are only supported by CVC5 currently.

Documentation

example :: IO ()

Abduct extraction example. We have the constraint x >= 0 and we want to make x + y >= 2. We have:

>>> example
Got: (define-fun abd () Bool (= s1 2))
Got: (define-fun abd () Bool (<= 2 s1))
Got: (define-fun abd () Bool (= (+ s1 s0) 2))
Got: (define-fun abd () Bool (= (+ s0 2) s1))

Note that s0 refers to x and s1 refers to y above. You can verify that adding any of these will ensure x + y >= 2.