-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Set
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
--
-- __A note on cardinality__: You can indirectly talk about cardinality: 'Data.SBV.Set.hasSize'
-- can be used to state that the set is finite and has size @k@ for a user-specified symbolic
-- integer @k@.
-----------------------------------------------------------------------------

{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Set (
        -- * Constructing sets
          empty, full, universal, singleton, fromList, complement

        -- * Equality of sets
        -- $setEquality

        -- * Insertion and deletion
        , insert, delete

        -- * Query
        , member, notMember, null, isEmpty, isFull, isUniversal, hasSize, isSubsetOf, isProperSubsetOf, disjoint

        -- * Combinations
        , union, unions, intersection, intersections, difference, (\\)

        ) where

import Prelude hiding (null)

import Data.Proxy (Proxy(Proxy))
import qualified Data.Set as Set

import Data.SBV.Core.Data
import Data.SBV.Core.Model    ((.==), (./=))
import Data.SBV.Core.Symbolic (SetOp(..))

import qualified Data.Generics.Uniplate.Data as G

-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Prelude hiding(null)
-- >>> import Data.SBV hiding(complement)
-- >>> :set -XScopedTypeVariables

-- | Empty set.
--
-- >>> empty :: SSet Integer
-- {} :: {SInteger}
empty :: forall a. HasKind a => SSet a
empty :: forall a. HasKind a => SSet a
empty = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a. Set a
Set.empty
  where k :: Kind
k = Kind -> Kind
KSet forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)

-- | Full set.
--
-- >>> full :: SSet Integer
-- U :: {SInteger}
--
-- Note that the universal set over a type is represented by the letter @U@.
full :: forall a. HasKind a => SSet a
full :: forall a. HasKind a => SSet a
full = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
ComplementSet forall a. Set a
Set.empty
  where k :: Kind
k = Kind -> Kind
KSet forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)

-- | Synonym for 'full'.
universal :: forall a. HasKind a => SSet a
universal :: forall a. HasKind a => SSet a
universal = forall a. HasKind a => SSet a
full

-- | Singleton list.
--
-- >>> singleton 2 :: SSet Integer
-- {2} :: {SInteger}
singleton :: forall a. (Ord a, SymVal a) => SBV a -> SSet a
singleton :: forall a. (Ord a, SymVal a) => SBV a -> SSet a
singleton = (forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
`insert` (forall a. HasKind a => SSet a
empty :: SSet a))

-- | 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}
fromList :: forall a. (Ord a, SymVal a) => [a] -> SSet a
fromList :: forall a. (Ord a, SymVal a) => [a] -> SSet a
fromList = forall a. SymVal a => a -> SBV a
literal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> RCSet a
RegularSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList

-- | 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.
complement :: forall a. (Ord a, SymVal a) => SSet a -> SSet a
complement :: forall a. (Ord a, SymVal a) => SSet a -> SSet a
complement SSet a
ss
  | Kind
KChar forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall on. Uniplate on => on -> [on]
G.universe Kind
k
  = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"*** Data.SBV: Set.complement is not available for the type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Kind
k
                    , [Char]
"***"
                    , [Char]
"*** See: https://github.com/LeventErkok/sbv/issues/601 for a discussion"
                    , [Char]
"*** on why SBV does not support this operation at this type."
                    , [Char]
"***"
                    , [Char]
"*** Alternative: Use sets of strings instead, though the match isn't perfect."
                    , [Char]
"*** If you run into this issue, please comment on the above ticket for"
                    , [Char]
"*** possible improvements."
                    ]
  | Just (RegularSet Set a
rs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
ComplementSet Set a
rs
  | Just (ComplementSet Set a
cs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet Set a
cs
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = Kind -> Kind
KSet (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a))

        r :: State -> IO SV
r State
st = do SV
svs <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
ss
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetComplement) [SV
svs]

-- | 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 =   2 :: Integer
--   s1 = {2} :: {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.
insert :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
insert :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
insert SBV a
se SSet a
ss
  -- Case 1: Constant regular set, just add it:
  | Just a
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
se, Just (RegularSet Set a
rs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a b. (a -> b) -> a -> b
$ a
e forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set a
rs

  -- Case 2: Constant complement set, with element in the complement, just remove it:
  | Just a
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
se, Just (ComplementSet Set a
cs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss, a
e forall a. Ord a => a -> Set a -> Bool
`Set.member` Set a
cs
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
ComplementSet forall a b. (a -> b) -> a -> b
$ a
e forall a. Ord a => a -> Set a -> Set a
`Set.delete` Set a
cs

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where ka :: Kind
ka = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)
        k :: Kind
k  = Kind -> Kind
KSet Kind
ka

        r :: State -> IO SV
r State
st = do SV
svs <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
ss
                  SV
sve <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
se
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetInsert) [SV
sve, SV
svs]

-- | 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 =  2 :: 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.
delete :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
delete :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
delete SBV a
se SSet a
ss
  -- Case 1: Constant regular set, just remove it:
  | Just a
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
se, Just (RegularSet Set a
rs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a b. (a -> b) -> a -> b
$ a
e forall a. Ord a => a -> Set a -> Set a
`Set.delete` Set a
rs

  -- Case 2: Constant complement set, with element missing in the complement, just add it:
  | Just a
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
se, Just (ComplementSet Set a
cs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss, a
e forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set a
cs
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
ComplementSet forall a b. (a -> b) -> a -> b
$ a
e forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set a
cs

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where ka :: Kind
ka = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)
        k :: Kind
k  = Kind -> Kind
KSet Kind
ka

        r :: State -> IO SV
r State
st = do SV
svs <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
ss
                  SV
sve <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
se
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetDelete) [SV
sve, SV
svs]

-- | 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.
member :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool
member :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SBool
member SBV a
se SSet a
ss
  -- Case 1: Constant regular set, just check:
  | Just a
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
se, Just (RegularSet Set a
rs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ a
e forall a. Ord a => a -> Set a -> Bool
`Set.member` Set a
rs

  -- Case 2: Constant complement set, check for non-member
  | Just a
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
se, Just (ComplementSet Set a
cs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
ss
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ a
e forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set a
cs

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where r :: State -> IO SV
r State
st = do SV
svs <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
ss
                  SV
sve <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
se
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetMember) [SV
sve, SV
svs]

-- | 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.
notMember :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool
notMember :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SBool
notMember SBV a
se SSet a
ss = SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SBool
member SBV a
se SSet a
ss

-- | 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 `Data.SBV.prove` in the last case since dealing
-- with infinite sets requires a call to the solver and cannot be
-- constant folded.
null :: HasKind a => SSet a -> SBool
null :: forall a. HasKind a => SSet a -> SBool
null = (forall a. EqSymbolic a => a -> a -> SBool
.== forall a. HasKind a => SSet a
empty)

-- | Synonym for 'Data.SBV.Set.null'.
isEmpty :: HasKind a => SSet a -> SBool
isEmpty :: forall a. HasKind a => SSet a -> SBool
isEmpty = forall a. HasKind a => SSet a -> SBool
null

-- | 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 - {2} :: {Integer}
--   s0  =       2 :: Integer
--
-- >>> isFull (full :: SSet Integer)
-- True
--
-- Note how we have to call `Data.SBV.prove` in the first case since dealing
-- with infinite sets requires a call to the solver and cannot be
-- constant folded.
isFull :: HasKind a => SSet a -> SBool
isFull :: forall a. HasKind a => SSet a -> SBool
isFull = (forall a. EqSymbolic a => a -> a -> SBool
.== forall a. HasKind a => SSet a
full)

-- | Synonym for 'Data.SBV.Set.isFull'.
isUniversal :: HasKind a => SSet a -> SBool
isUniversal :: forall a. HasKind a => SSet a -> SBool
isUniversal = forall a. HasKind a => SSet a -> SBool
isFull

-- | Does the set have the given size? It implicitly asserts that the set
-- it is operating on is finite. NB. Only z3 supported this call, and as
-- discussed in http://github.com/Z3Prover/z3/issues/3854, recent versions
-- of z3 doesn't support size calls either. So, you can only use this if you have
-- a sufficiently old version of z3.
--
-- >>> prove $ \i -> hasSize (empty :: SSet Integer) i .== (i .== 0)
-- Q.E.D.
--
-- >>> sat $ \i -> hasSize (full :: SSet Integer) i
-- Unsatisfiable
--
-- The following tests are commented out since z3 no longer supports size:
--
-- > >>> prove $ \a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a `union` b) k .=> k .>= i `smax` j
-- > Q.E.D.
--
-- > >>> prove $ \a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a `intersection` b) k .=> k .<= i `smin` j
-- > Q.E.D.
--
-- > >>> prove $ \a k -> hasSize (a :: SSet Integer) k .=> k .>= 0
-- > Q.E.D.
hasSize :: (Ord a, SymVal a) => SSet a -> SInteger -> SBool
hasSize :: forall a. (Ord a, SymVal a) => SSet a -> SInteger -> SBool
hasSize SSet a
sa SInteger
si
  -- Case 1: Constant regular set, see if the size matches
  | Just (RegularSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa
  = forall a. SymVal a => a -> SBV a
literal (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Set a -> Int
Set.size Set a
a)) forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
si

  -- Case 2: Constant complement set, will never have finite size
  | Just (ComplementSet Set a
_) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa
  = SBool
sFalse

  -- Case 3: Integer is constant, and is negative:
  | Just Integer
i <- forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
si, Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0
  = SBool
sFalse

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sa
                  SV
svi <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SInteger
si
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetHasSize) [SV
sva, SV
svi]

-- | 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.
isSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool
isSubsetOf :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SBool
isSubsetOf SSet a
sa SSet a
sb
  -- Case 1: Constant regular sets, just check:
  | Just (RegularSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (RegularSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
b

  -- Case 2: Constant complement sets, check in the reverse direction:
  | Just (ComplementSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (ComplementSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ Set a
b forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
a

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sa
                  SV
svb <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sb
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetSubset) [SV
sva, SV
svb]

-- | 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 = 2 :: Integer
--   s1 = U :: {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 =         2 :: Integer
--   s1 = U - {2,3} :: {Integer}
--
-- >>> prove $ \x (s :: SSet Integer) -> x `member` s .=> (x `delete` s) `isProperSubsetOf` s
-- Q.E.D.
isProperSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool
isProperSubsetOf :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SBool
isProperSubsetOf SSet a
a SSet a
b = SSet a
a forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SBool
`isSubsetOf` SSet a
b SBool -> SBool -> SBool
.&& SSet a
a forall a. EqSymbolic a => a -> a -> SBool
./= SSet a
b

-- | 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!
disjoint :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool
disjoint :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SBool
disjoint SSet a
a SSet a
b = SSet a
a forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
`intersection` SSet a
b forall a. EqSymbolic a => a -> a -> SBool
.== forall a. HasKind a => SSet a
empty

-- | 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.
union :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
union :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
union SSet a
sa SSet a
sb
  -- Case 1: Constant regular sets, just compute
  | Just (RegularSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (RegularSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set a
b

  -- Case 2: Constant complement sets, complement the intersection:
  | Just (ComplementSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (ComplementSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
ComplementSet forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set a
b

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf SSet a
sa
        r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sa
                  SV
svb <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sb
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetUnion) [SV
sva, SV
svb]

-- | Unions. Equivalent to @'foldr' 'union' 'empty'@.
--
-- >>> prove $ unions [] .== (empty :: SSet Integer)
-- Q.E.D.
unions :: (Ord a, SymVal a) => [SSet a] -> SSet a
unions :: forall a. (Ord a, SymVal a) => [SSet a] -> SSet a
unions = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
union forall a. HasKind a => SSet a
empty

-- | 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.
intersection :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
intersection :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
intersection SSet a
sa SSet a
sb
  -- Case 1: Constant regular sets, just compute
  | Just (RegularSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (RegularSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set a
b

  -- Case 2: Constant complement sets, complement the union:
  | Just (ComplementSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (ComplementSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
ComplementSet forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set a
b

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf SSet a
sa
        r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sa
                  SV
svb <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sb
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetIntersect) [SV
sva, SV
svb]

-- | Intersections. Equivalent to @'foldr' 'intersection' 'full'@. Note that
-- Haskell's 'Data.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.
intersections :: (Ord a, SymVal a) => [SSet a] -> SSet a
intersections :: forall a. (Ord a, SymVal a) => [SSet a] -> SSet a
intersections = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
intersection forall a. HasKind a => SSet a
full

-- | 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.
difference :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
difference :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
difference SSet a
sa SSet a
sb
  -- Only constant fold the regular case, others are left symbolic
  | Just (RegularSet Set a
a) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sa, Just (RegularSet Set a
b) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SSet a
sb
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
b

  -- Otherwise, go symbolic
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf SSet a
sa
        r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sa
                  SV
svb <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SSet a
sb
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (SetOp -> Op
SetOp SetOp
SetDifference) [SV
sva, SV
svb]

-- | Synonym for 'Data.SBV.Set.difference'.
infixl 9 \\
(\\) :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
\\ :: forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
(\\) = forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
difference

{- $setEquality
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 = {Just 3} :: {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!
-}