Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Demonstrates extraction of abducts via queries.
N.B. Interpolants are only supported by CVC5 currently.
Documentation
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
.