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

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

Data.SBV.Set

Description

A collection of set utilities, useful when working with symbolic sets. To the extent possible, the functions in this module follow those of Data.Set so importing qualified is the recommended workflow.

Note that unlike Data.Set, SBV sets can be infinite, represented as a complement of some finite set. This means that a symbolic set is either finite, or its complement is finite. (If the underlying domain is finite, then obviously both the set itself and its complement will always be finite.) Therefore, there are some differences in the API from Haskell sets. For instance, you can take the complement of any set, which is something you cannot do in Haskell! Conversely, you cannot compute the size of a symbolic set (as it can be infinite!), nor you can turn it into a list or necessarily enumerate its elements.

Synopsis

# Constructing sets

empty :: forall a. HasKind a => SSet a Source #

Empty set.

>>> empty :: SSet Integer
{} :: {SInteger}


full :: forall a. HasKind a => SSet a Source #

Full set.

>>> full :: SSet Integer
U :: {SInteger}


Note that the universal set over a type is represented by the letter U.

universal :: forall a. HasKind a => SSet a Source #

Synonym for full.

singleton :: forall a. (Ord a, SymVal a) => SBV a -> SSet a Source #

Singleton list.

>>> singleton 2 :: SSet Integer
{2} :: {SInteger}


fromList :: forall a. (Ord a, SymVal a) => [a] -> SSet a Source #

Conversion from a list.

>>> fromList ([] :: [Integer])
{} :: {SInteger}
>>> fromList [1,2,3]
{1,2,3} :: {SInteger}
>>> fromList [5,5,5,12,12,3]
{3,5,12} :: {SInteger}


complement :: forall a. (Ord a, SymVal a) => SSet a -> SSet a Source #

Complement.

>>> empty .== complement (full :: SSet Integer)
True


Complementing twice gets us back the original set:

>>> prove \$ $$s :: SSet Integer) -> complement (complement s) .== s Q.E.D.  # Equality of sets We can compare sets for equality: >>> empty .== (empty :: SSet Integer) True >>> full .== (full :: SSet Integer) True >>> full ./= (full :: SSet Integer) False >>> sat  \(x::SSet (Maybe Integer)) y z -> distinct [x, y, z] Satisfiable. Model: s0 = U - {Nothing} :: {Maybe Integer} s1 = {} :: {Maybe Integer} s2 = U :: {Maybe Integer}  However, if we compare two sets that are constructed as regular or in the complement form, we have to use a proof to establish equality: >>> prove  full .== (empty :: SSet Integer) Falsifiable  The reason for this is that there is no way in Haskell to compare an infinite set to any other set, as infinite sets are not representable at all! So, we have to delay the judgment to the SMT solver. If you try to constant fold, you will get: >>> full .== (empty :: SSet Integer) <symbolic> :: SBool  indicating that the result is a symbolic value that needs a decision procedure to be determined! # Insertion and deletion insert :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a Source # Insert an element into a set. Insertion is order independent: >>> prove  \x y (s :: SSet Integer) -> x insert (y insert s) .== y insert (x insert s) Q.E.D.  Deletion after insertion is not necessarily identity: >>> prove  \x (s :: SSet Integer) -> x delete (x insert s) .== s Falsifiable. Counter-example: s0 = 0 :: Integer s1 = {0} :: {Integer}  But the above is true if the element isn't in the set to start with: >>> prove  \x (s :: SSet Integer) -> x notMember s .=> x delete (x insert s) .== s Q.E.D.  Insertion into a full set does nothing: >>> prove  \x -> insert x full .== (full :: SSet Integer) Q.E.D.  delete :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a Source # Delete an element from a set. Deletion is order independent: >>> prove  \x y (s :: SSet Integer) -> x delete (y delete s) .== y delete (x delete s) Q.E.D.  Insertion after deletion is not necessarily identity: >>> prove  \x (s :: SSet Integer) -> x insert (x delete s) .== s Falsifiable. Counter-example: s0 = 0 :: Integer s1 = {} :: {Integer}  But the above is true if the element is in the set to start with: >>> prove  \x (s :: SSet Integer) -> x member s .=> x insert (x delete s) .== s Q.E.D.  Deletion from an empty set does nothing: >>> prove  \x -> delete x empty .== (empty :: SSet Integer) Q.E.D.  # Query member :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool Source # Test for membership. >>> prove  \x -> x member singleton (x :: SInteger) Q.E.D.  >>> prove  \x (s :: SSet Integer) -> x member (x insert s) Q.E.D.  >>> prove  \x -> x member (full :: SSet Integer) Q.E.D.  notMember :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool Source # Test for non-membership. >>> prove  \x -> x notMember observe "set" (singleton (x :: SInteger)) Falsifiable. Counter-example: set = {0} :: {Integer} s0 = 0 :: Integer  >>> prove  \x (s :: SSet Integer) -> x notMember (x delete s) Q.E.D.  >>> prove  \x -> x notMember (empty :: SSet Integer) Q.E.D.  null :: HasKind a => SSet a -> SBool Source # Is this the empty set? >>> null (empty :: SSet Integer) True  >>> prove  \x -> null (x delete singleton (x :: SInteger)) Q.E.D.  >>> prove  null (full :: SSet Integer) Falsifiable  Note how we have to call prove in the last case since dealing with infinite sets requires a call to the solver and cannot be constant folded. isEmpty :: HasKind a => SSet a -> SBool Source # Synonym for null. isFull :: HasKind a => SSet a -> SBool Source # Is this the full set? >>> prove  isFull (empty :: SSet Integer) Falsifiable  >>> prove  \x -> isFull (observe "set" (x delete (full :: SSet Integer))) Falsifiable. Counter-example: set = U - {0} :: {Integer} s0 = 0 :: Integer  >>> isFull (full :: SSet Integer) True  Note how we have to call prove in the first case since dealing with infinite sets requires a call to the solver and cannot be constant folded. isUniversal :: HasKind a => SSet a -> SBool Source # Synonym for isFull. isSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool Source # Subset test. >>> prove  empty isSubsetOf (full :: SSet Integer) Q.E.D.  >>> prove  \x (s :: SSet Integer) -> s isSubsetOf (x insert s) Q.E.D.  >>> prove  \x (s :: SSet Integer) -> (x delete s) isSubsetOf s Q.E.D.  isProperSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool Source # Proper subset test. >>> prove  empty isProperSubsetOf (full :: SSet Integer) Q.E.D.  >>> prove  \x (s :: SSet Integer) -> s isProperSubsetOf (x insert s) Falsifiable. Counter-example: s0 = 0 :: Integer s1 = U - {1} :: {Integer}  >>> prove  \x (s :: SSet Integer) -> x notMember s .=> s isProperSubsetOf (x insert s) Q.E.D.  >>> prove  \x (s :: SSet Integer) -> (x delete s) isProperSubsetOf s Falsifiable. Counter-example: s0 = 0 :: Integer s1 = {1} :: {Integer}  >>> prove  \x (s :: SSet Integer) -> x member s .=> (x delete s) isProperSubsetOf s Q.E.D.  disjoint :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool Source # Disjoint test. >>> disjoint (fromList [2,4,6]) (fromList [1,3]) True >>> disjoint (fromList [2,4,6,8]) (fromList [2,3,5,7]) False >>> disjoint (fromList [1,2]) (fromList [1,2,3,4]) False >>> prove  \(s :: SSet Integer) -> s disjoint complement s Q.E.D. >>> allSat  \(s :: SSet Integer) -> s disjoint s Solution #1: s0 = {} :: {Integer} This is the only solution.  The last example is particularly interesting: The empty set is the only set where disjoint is not reflexive! Note that disjointness of a set from its complement is guaranteed by the fact that all types are inhabited; an implicit assumption we have in classic logic which is also enjoyed by Haskell due to the presence of bottom! # Combinations union :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a Source # Union. >>> union (fromList [1..10]) (fromList [5..15]) .== (fromList [1..15] :: SSet Integer) True >>> prove  \(a :: SSet Integer) b -> a union b .== b union a Q.E.D. >>> prove  \(a :: SSet Integer) b c -> a union (b union c) .== (a union b) union c Q.E.D. >>> prove  \(a :: SSet Integer) -> a union full .== full Q.E.D. >>> prove  \(a :: SSet Integer) -> a union empty .== a Q.E.D. >>> prove  \(a :: SSet Integer) -> a union complement a .== full Q.E.D.  unions :: (Ord a, SymVal a) => [SSet a] -> SSet a Source # Unions. Equivalent to foldr union empty. >>> prove  unions [] .== (empty :: SSet Integer) Q.E.D.  intersection :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a Source # 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 :: (Ord a, SymVal a) => [SSet a] -> SSet a Source # 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.  difference :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a Source # Difference. >>> prove  \(a :: SSet Integer) -> empty difference a .== empty Q.E.D. >>> prove  \(a :: SSet Integer) -> a difference empty .== a Q.E.D. >>> prove  \(a :: SSet Integer) -> full difference a .== complement a Q.E.D. >>> prove  \(a :: SSet Integer) -> a difference a .== empty Q.E.D.  (\$$ :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a infixl 9 Source #

Synonym for difference.