>>> intersection (fromList [1..10]) (fromList [5..15]) .== (fromList [5..10] :: SSet Integer) True >>> prove $ \(a :: SSet Integer) b -> a `intersection` b .== b `intersection` a Q.E.D. >>> prove $ \(a :: SSet Integer) b c -> a `intersection` (b `intersection` c) .== (a `intersection` b) `intersection` c Q.E.D. >>> prove $ \(a :: SSet Integer) -> a `intersection` full .== a Q.E.D. >>> prove $ \(a :: SSet Integer) -> a `intersection` empty .== empty Q.E.D. >>> prove $ \(a :: SSet Integer) -> a `intersection` complement a .== empty Q.E.D. >>> prove $ \(a :: SSet Integer) b -> a `disjoint` b .=> a `intersection` b .== empty Q.E.D.
>>> prove $ intersections [] .== (full :: SSet Integer) Q.E.D.
>>> interleaveLen Inductive lemma (strong): interleaveLen Step: Measure is non-negative Q.E.D. Step: 1 (2 way full case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.2.3 Q.E.D. Result: Q.E.D. [Proven] interleaveLen
>>> interleaveRoundTrip Lemma: revCons Q.E.D. Inductive lemma (strong): roundTripGen Step: Measure is non-negative Q.E.D. Step: 1 (4 way full case split) Step: 1.1 Q.E.D. Step: 1.2 Q.E.D. Step: 1.3 Q.E.D. Step: 1.4.1 Q.E.D. Step: 1.4.2 Q.E.D. Step: 1.4.3 Q.E.D. Step: 1.4.4 Q.E.D. Step: 1.4.5 Q.E.D. Step: 1.4.6 Q.E.D. Step: 1.4.7 Q.E.D. Step: 1.4.8 Q.E.D. Result: Q.E.D. Lemma: interleaveRoundTrip Step: 1 Q.E.D. Step: 2 Q.E.D. Result: Q.E.D. [Proven] interleaveRoundTrip
runSMTWith z3 $ do let f = uninterpret "f" :: SInteger -> SInteger query $ do constrain $ \(Forall (b :: SInteger)) -> f b .== f b checkSatThe solver will complain about the unknown constant f (Int). A workaround of this is to explicit register them with registerUISMTFunction:
runSMTWith z3 $ do let f = uninterpret "f" :: SInteger -> SInteger registerUISMTFunction f query $ do constrain $ \(Forall (b :: SInteger)) -> f b .== f b checkSatSee https://github.com/LeventErkok/sbv/issues/711 for more info.
setOption $ ProduceInterpolants Truefor this call to not error out! To get an interpolant for a pair of formulas A and B, use a constrainWithAttribute call to attach interplation groups to A and B. Then call getInterpolantMathSAT ["A"], assuming those are the names you gave to the formulas in the A group. An interpolant for A and B is a formula I such that:
A .=> I and B .=> sNot IThat is, it's evidence that A and B cannot be true together since A implies I but B implies not I; establishing that A and B cannot be satisfied at the same time. Furthermore, I will have only the symbols that are common to A and B. NB. Interpolant extraction isn't standardized well in SMTLib. Currently both MathSAT and Z3 support them, but with slightly differing APIs. So, we support two APIs with slightly differing types to accommodate both. See Documentation.SBV.Examples.Queries.Interpolants for example usages in these solvers. NB. For a version which generalizes over the underlying monad, see getInterpolantMathSAT
A ==> I and B ==> not IThat is, it's evidence that A and B cannot be true together since A implies I but B implies not I; establishing that A and B cannot be satisfied at the same time. Furthermore, I will have only the symbols that are common to A and B. In Z3, interpolants generalize to sequences: If you pass more than two formulas, then you will get a sequence of interpolants. In general, for N formulas that are not satisfiable together, you will be returned N-1 interpolants. If formulas are A1 .. An, then interpolants will be I1 .. I(N-1), such that A1 ==> I1, A2 /\ I1 ==> I2, A3 /\ I2 ==> I3, ..., and finally AN ===> not I(N-1). Currently, SBV only returns simple and sequence interpolants, and does not support tree-interpolants. If you need these, please get in touch. Furthermore, the result will be a list of mere strings representing the interpolating formulas, as opposed to a more structured type. Please get in touch if you use this function and can suggest a better API. NB. Interpolant extraction isn't standardized well in SMTLib. Currently both MathSAT and Z3 support them, but with slightly differing APIs. So, we support two APIs with slightly differing types to accommodate both. See Documentation.SBV.Examples.Queries.Interpolants for example usages in these solvers. NB. For a version which generalizes over the underlying monad, see getInterpolantZ3