----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.Queries.Interpolants -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Demonstrates extraction of interpolants via queries. -- -- N.B. As of Z3 version 4.8.0; Z3 no longer supports interpolants. You need -- to use the MathSAT backend for this example to work. ----------------------------------------------------------------------------- module Documentation.SBV.Examples.Queries.Interpolants where import Data.SBV import Data.SBV.Control -- | Compute the interpolant for the following sets of formulas: -- -- @{x - 3y >= -1, x + y >= 0}@ -- -- AND -- -- @{z - 2x >= 3, 2z <= 1}@ -- -- where the variables are integers. Note that these sets of -- formulas are themselves satisfiable, but not taken all together. -- The pair @(x, y) = (0, 0)@ satisfies the first set. The pair @(x, z) = (-2, 0)@ -- satisfies the second. However, there's no triple @(x, y, z)@ that satisfies all -- these four formulas together. We can use SBV to check this fact: -- -- >>> sat \$ \x y z -> sAnd [x - 3*y .>= -1, x + y .>= 0, z - 2*x .>= 3, 2 * z .<= (1::SInteger)] -- Unsatisfiable -- -- An interpolant for these sets would only talk about the variable @x@ that is common -- to both. We have: -- -- >>> runSMTWith mathSAT example -- "(<= 0 s0)" -- -- Notice that we get a string back, not a term; so there's some back-translation we need to do. We -- know that @s0@ is @x@ through our translation mechanism, so the interpolant is saying that @x >= 0@ -- is entailed by the first set of formulas, and is inconsistent with the second. Let's use SBV -- to indeed show that this is the case: -- -- >>> prove \$ \x y -> (x - 3*y .>= -1 .&& x + y .>= 0) .=> (x .>= (0::SInteger)) -- Q.E.D. -- -- And: -- -- >>> prove \$ \x z -> (z - 2*x .>= 3 .&& 2 * z .<= 1) .=> sNot (x .>= (0::SInteger)) -- Q.E.D. -- -- This establishes that we indeed have an interpolant! example :: Symbolic String example = do x <- sInteger "x" y <- sInteger "y" z <- sInteger "z" -- tell the solver we want interpolants setOption \$ ProduceInterpolants True -- create interpolation constraints. MathSAT requires the relevant formulas -- to be marked with the attribute :interpolation-group constrainWithAttribute [(":interpolation-group", "A")] \$ x - 3*y .>= -1 constrainWithAttribute [(":interpolation-group", "A")] \$ x + y .>= 0 constrainWithAttribute [(":interpolation-group", "B")] \$ z - 2*x .>= 3 constrainWithAttribute [(":interpolation-group", "B")] \$ 2*z .<= 1 -- To obtain the interpolant, we run a query query \$ do cs <- checkSat case cs of Unsat -> getInterpolant ["A"] Sat -> error "Unexpected sat result!" Unk -> error "Unexpected unknown result!"