-----------------------------------------------------------------------------
-- |
-- 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 :: SSet a
empty = 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
$ 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 (Proxy a
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 :: SSet a
full = 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
$ 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 (Proxy a
forall k (t :: k). Proxy t
Proxy @a)

-- | Synonym for 'full'.
universal :: forall a. HasKind a => SSet a
universal :: 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 :: 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 :: [a] -> SSet a
fromList = RCSet a -> SSet a
forall a. SymVal a => a -> SBV a
literal (RCSet a -> SSet a) -> ([a] -> RCSet a) -> [a] -> SSet 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 :: SSet a -> SSet a
complement SSet a
ss
  | Kind
KChar Kind -> [Kind] -> 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 (Proxy a
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 = {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 :: 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 (Proxy a
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 = {} :: {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 :: 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 (Proxy a
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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: [SSet a] -> SSet a
unions = (SSet a -> SSet a -> SSet a) -> SSet a -> [SSet a] -> SSet a
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 :: 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 :: [SSet a] -> SSet a
intersections = (SSet a -> SSet a -> SSet a) -> SSet a -> [SSet a] -> SSet a
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 :: 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
\\ :: 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 =            U :: {Maybe Integer}
  s1 = U - {Just 3} :: {Maybe Integer}
  s2 =           {} :: {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!
-}