Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Demonstrates extraction of interpolants via queries.

# Documentation

evenOdd :: Symbolic [String] Source #

Compute the interpolant for formulas `y = 2x`

and `y = 2z+1`

.
These formulas are not satisfiable together since it would mean
`y`

is both even and odd at the same time. An interpolant for
this pair of formulas is a formula that's expressed only in terms
of `y`

, which is the only common symbol among them. We have:

`>>>`

["(<= 0 (+ (div s1 2) (div (* (- 1) s1) 2)))"]`runSMT evenOdd`

This is a bit hard to read unfortunately, due to translation artifacts and use of strings. To analyze,
we need to know that `s1`

is `y`

through SBV's translation. Let's express it in
regular infix notation with `y`

for `s1`

:

0 <= (y`div`

2) + ((-y)`div`

2)

Notice that the only symbol is `y`

, as required. To establish that this is
indeed an interpolant, we should establish that when `y`

is even, this formula
is `True`

; and if `y`

is odd, then then it should be `False`

. You can argue
mathematically that this indeed the case, but let's just use SBV to prove these:

`>>>`

Q.E.D.`prove $ \y -> (y `sMod` 2 .== 0) ==> (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))`

And:

`>>>`

Q.E.D.`prove $ \y -> (y `sMod` 2 .== 1) ==> bnot (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))`

This establishes that we indeed have an interpolant!