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

Copyright (c) Levent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV.Examples.Queries.Interpolants

Description

Demonstrates extraction of interpolants via queries.

Synopsis

# Documentation

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:

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


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:

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


This establishes that we indeed have an interpolant!