inter package:sbv

Intersection of regular expressions

Require a boolean condition to be true in the state. Only used for internal purposes.

Get an internal-variable

Intersection.

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

Intersections. Equivalent to foldr intersection full. Note that Haskell's Set does not support this operation as it does not have a way of representing universal sets.

>>> prove $ intersections [] .== (full :: SSet Integer)
Q.E.D.

Interleave the elements of two lists. If one ends, we take the rest from the other.

Prove that interleave preserves total length. The induction here is on the total length of the lists, and hence we use the generalized induction principle. We have:

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

The functions uninterleave and interleave are inverses so long as the inputs are of the same length. (The equality would even hold if the first argument has one extra element, but we keep things simple here.) We have:

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

Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module. NB. There are various coding invariants in SBV that are maintained throughout the code. Indiscriminate use of functions in this module can break those invariants. So, you are on your own if you do utilize the functions here. (Unfortunately, what exactly those invariants are is a very good but also a very difficult question to answer!)

Demonstrates extraction of interpolants via queries. N.B. Interpolants are supported by MathSAT and Z3. Unfortunately the extraction of interpolants is not standardized, and are slightly different for these two solvers. So, we have two separate examples to demonstrate the usage.

interval, with low and high bounds

Interval. Can be open/closed on both ends.

Uninterpret a value, only for the purposes of code-generation. For execution and verification the value is used as is. For code-generation, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.

Extract a representative name for the model value of an uninterpreted kind. This is supposed to correspond to the value as computed internally by the SMT solver; and is unportable from solver to solver. Also see getModelUninterpretedValues.

Extract value of an uninterpreted variable from an all-sat call. Similar to getModelUninterpretedValue.

Make an uninterpred sort.

Uninterpret a value, i.e., add this value as a completely undefined value/function that the solver is free to instantiate to satisfy other constraints. Known issues Usually using an uninterpret function will register itself to the solver, but sometimes the lazyness of the evaluation might render this unreliable. For example, when working with quantifiers and uninterpreted functions with the following code:

runSMTWith z3 $ do
let f = uninterpret "f" :: SInteger -> SInteger
query $ do
constrain $ \(Forall (b :: SInteger)) -> f b .== f b
checkSat

The 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
checkSat

See https://github.com/LeventErkok/sbv/issues/711 for more info.

Uninterpret a value, with named arguments in case of functions. SBV will use these names when it shows the values for the arguments. If the given names are more than needed we ignore the excess. If not enough, we add from a stock set of variables.

Interpolant extraction for MathSAT. Compare with getInterpolantZ3, which performs similar function (but with a different use model) in Z3. Retrieve an interpolant after an Unsat result is obtained. Note you must have arranged for interpolants to be produced first via

setOption $ ProduceInterpolants True

for 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 I

That 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

Interpolant extraction for z3. Compare with getInterpolantMathSAT, which performs similar function (but with a different use model) in MathSAT. Unlike the MathSAT variant, you should simply call getInterpolantZ3 on symbolic booleans to retrieve the interpolant. Do not call checkSat or create named constraints. This makes it harder to identify formulas, but the current state of affairs in interpolant API requires this kludge. An interpolant for A and B is a formula I such that:

A ==> I
and B ==> not I

That 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

Get the value of an uninterpreted sort, as a String NB. For a version which generalizes over the underlying monad, see getUninterpretedValue

Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.