sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Queries.Abducts

Description

Demonstrates extraction of abducts via queries.

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

Synopsis

- example :: IO ()

# Documentation

example :: IO () Source #

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`.