    -----------------------------------------------------------------------------
    -- |
    -- 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 () -- instances only
    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 = SVal -> SBV (RCSet a)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (RCSet a)) -> SVal -> SBV (RCSet a)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ RCSet CVal -> CVal
    CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    RegularSet Set CVal
    forall a. Set a
    Set.empty
      where k :: Kind
    k = Kind -> Kind
    KSet (Kind -> Kind) -> Kind -> Kind
    forall a b. (a -> b) -> a -> b
    $ Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    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 = SVal -> SBV (RCSet a)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (RCSet a)) -> SVal -> SBV (RCSet a)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ RCSet CVal -> CVal
    CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    ComplementSet Set CVal
    forall a. Set a
    Set.empty
      where k :: Kind
    k = Kind -> Kind
    KSet (Kind -> Kind) -> Kind -> Kind
    forall a b. (a -> b) -> a -> b
    $ Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    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 = SSet a
    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 = (SBV a -> SSet a -> SSet a
    forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
    `insert` (SSet a
    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 = RCSet a -> SBV (RCSet a)
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SBV (RCSet a))
    -> ([a] -> RCSet a) -> [a] -> SBV (RCSet a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet (Set a -> RCSet a) -> ([a] -> Set a) -> [a] -> RCSet a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> Set a
    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 Kind -> [Kind] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Kind -> [Kind]
    forall on. Uniplate on => on -> [on]
    G.universe Kind
    k
      = [Char] -> SSet a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> SSet a) -> [Char] -> SSet a
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    "*** Data.SBV: Set.complement is not available for the type " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Kind -> [Char]
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    ComplementSet Set a
    rs
      | Just (ComplementSet Set a
    cs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet Set a
    cs
      | Bool
    True
      = SVal -> SSet a
    forall a. SVal -> SBV a
    SBV (SVal -> SSet a) -> SVal -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Kind -> Kind
    KSet (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a))

            r :: State -> IO SV
    r State
    st = do SV
    svs <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    ss
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 = U :: {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 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    se, Just (RegularSet Set a
    rs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ a
    e a -> Set a -> Set a
    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 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    se, Just (ComplementSet Set a
    cs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss, a
    e a -> Set a -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set a
    cs
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    ComplementSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ a
    e a -> Set a -> Set a
    forall a. Ord a => a -> Set a -> Set a
    `Set.delete` Set a
    cs

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SSet a
    forall a. SVal -> SBV a
    SBV (SVal -> SSet a) -> SVal -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where ka :: Kind
    ka = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    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 <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    ss
                      SV
    sve <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    se
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 = U - {2} :: {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 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    se, Just (RegularSet Set a
    rs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ a
    e a -> Set a -> Set a
    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 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    se, Just (ComplementSet Set a
    cs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss, a
    e a -> Set a -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.notMember` Set a
    cs
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    ComplementSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ a
    e a -> Set a -> Set a
    forall a. Ord a => a -> Set a -> Set a
    `Set.insert` Set a
    cs

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SSet a
    forall a. SVal -> SBV a
    SBV (SVal -> SSet a) -> SVal -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where ka :: Kind
    ka = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    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 <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    ss
                      SV
    sve <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    se
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    se, Just (RegularSet Set a
    rs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal (Bool -> SBool) -> Bool -> SBool
    forall a b. (a -> b) -> a -> b
    $ a
    e a -> Set a -> Bool
    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 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    se, Just (ComplementSet Set a
    cs) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    ss
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal (Bool -> SBool) -> Bool -> SBool
    forall a b. (a -> b) -> a -> b
    $ a
    e a -> Set a -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.notMember` Set a
    cs

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where r :: State -> IO SV
    r State
    st = do SV
    svs <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    ss
                      SV
    sve <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    se
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> SSet a -> SBool
    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 = (SSet a -> SSet a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SSet a
    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 = SSet a -> SBool
    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 = (SSet a -> SSet a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SSet a
    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 = SSet a -> SBool
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa
      = Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Set a -> Int
    forall a. Set a -> Int
    Set.size Set a
    a)) SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    si

      -- Case 2: Constant complement set, will never have finite size
      | Just (ComplementSet Set a
    _) <- SSet a -> Maybe (RCSet 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 <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    si, Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0
      = SBool
    sFalse

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where r :: State -> IO SV
    r State
    st = do SV
    sva <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sa
                      SV
    svi <- State -> SInteger -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SInteger
    si
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (RegularSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal (Bool -> SBool) -> Bool -> SBool
    forall a b. (a -> b) -> a -> b
    $ Set a
    a Set a -> Set a -> Bool
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (ComplementSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal (Bool -> SBool) -> Bool -> SBool
    forall a b. (a -> b) -> a -> b
    $ Set a
    b Set a -> Set a -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `Set.isSubsetOf` Set a
    a

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where r :: State -> IO SV
    r State
    st = do SV
    sva <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sa
                      SV
    svb <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sb
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 SSet a -> SSet a -> SBool
    forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SBool
    `isSubsetOf` SSet a
    b SBool -> SBool -> SBool
    .&& SSet a
    a SSet a -> SSet a -> SBool
    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 SSet a -> SSet a -> SSet a
    forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
    `intersection` SSet a
    b SSet a -> SSet a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SSet a
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (RegularSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ Set a
    a Set a -> Set a -> Set 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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (ComplementSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    ComplementSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ Set a
    a Set a -> Set a -> Set a
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.intersection` Set a
    b

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SSet a
    forall a. SVal -> SBV a
    SBV (SVal -> SSet a) -> SVal -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = SSet a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SSet a
    sa
            r :: State -> IO SV
    r State
    st = do SV
    sva <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sa
                      SV
    svb <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sb
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 = (SSet a -> SSet a -> SSet a) -> SSet a -> [SSet a] -> SSet a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SSet a -> SSet a -> SSet a
    forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
    union SSet a
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (RegularSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ Set a
    a Set a -> Set a -> Set 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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (ComplementSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    ComplementSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ Set a
    a Set a -> Set a -> Set a
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set a
    b

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SSet a
    forall a. SVal -> SBV a
    SBV (SVal -> SSet a) -> SVal -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = SSet a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SSet a
    sa
            r :: State -> IO SV
    r State
    st = do SV
    sva <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sa
                      SV
    svb <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sb
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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 = (SSet a -> SSet a -> SSet a) -> SSet a -> [SSet a] -> SSet a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SSet a -> SSet a -> SSet a
    forall a. (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
    intersection SSet a
    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) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sa, Just (RegularSet Set a
    b) <- SSet a -> Maybe (RCSet a)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SSet a
    sb
      = RCSet a -> SSet a
    forall a. SymVal a => a -> SBV a
    literal (RCSet a -> SSet a) -> RCSet a -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Set a -> RCSet a
    forall a. Set a -> RCSet a
    RegularSet (Set a -> RCSet a) -> Set a -> RCSet a
    forall a b. (a -> b) -> a -> b
    $ Set a
    a Set a -> Set a -> Set a
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference` Set a
    b

      -- Otherwise, go symbolic
      | Bool
    True
      = SVal -> SSet a
    forall a. SVal -> SBV a
    SBV (SVal -> SSet a) -> SVal -> SSet a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = SSet a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SSet a
    sa
            r :: State -> IO SV
    r State
    st = do SV
    sva <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sa
                      SV
    svb <- State -> SSet a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SSet a
    sb
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    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
    (\\) = 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!
    -}