    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Uninterpreted.UISortAllSat
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates uninterpreted sorts and how all-sat behaves for them.
    -- Thanks to Eric Seidel for the idea.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveDataTypeable #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.UISortAllSat where

    import Data.Generics
    import Data.SBV

    -- | A "list-like" data type, but one we plan to uninterpret at the SMT level.
    -- The actual shape is really immaterial for us, but could be used as a proxy
    -- to generate test cases or explore data-space in some other part of a program.
    -- Note that we neither rely on the shape of this data, nor need the actual
    -- constructors.
    data L = Nil
           | Cons Int L
           deriving (L -> L -> Bool
    (L -> L -> Bool) -> (L -> L -> Bool) -> Eq L
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: L -> L -> Bool
    $c/= :: L -> L -> Bool
    == :: L -> L -> Bool
    $c== :: L -> L -> Bool
    Eq, Eq L
    Eq L =>
    (L -> L -> Ordering)
    -> (L -> L -> Bool)
    -> (L -> L -> Bool)
    -> (L -> L -> Bool)
    -> (L -> L -> Bool)
    -> (L -> L -> L)
    -> (L -> L -> L)
    -> Ord L
    L -> L -> Bool
    L -> L -> Ordering
    L -> L -> L
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: L -> L -> L
    $cmin :: L -> L -> L
    max :: L -> L -> L
    $cmax :: L -> L -> L
    >= :: L -> L -> Bool
    $c>= :: L -> L -> Bool
    > :: L -> L -> Bool
    $c> :: L -> L -> Bool
    <= :: L -> L -> Bool
    $c<= :: L -> L -> Bool
    < :: L -> L -> Bool
    $c< :: L -> L -> Bool
    compare :: L -> L -> Ordering
    $ccompare :: L -> L -> Ordering
    $cp1Ord :: Eq L
    Ord, Int -> L -> ShowS
    [L] -> ShowS
    L -> String
    (Int -> L -> ShowS) -> (L -> String) -> ([L] -> ShowS) -> Show L
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [L] -> ShowS
    $cshowList :: [L] -> ShowS
    show :: L -> String
    $cshow :: L -> String
    showsPrec :: Int -> L -> ShowS
    $cshowsPrec :: Int -> L -> ShowS
    Show, ReadPrec [L]
    ReadPrec L
    Int -> ReadS L
    ReadS [L]
    (Int -> ReadS L)
    -> ReadS [L] -> ReadPrec L -> ReadPrec [L] -> Read L
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    readListPrec :: ReadPrec [L]
    $creadListPrec :: ReadPrec [L]
    readPrec :: ReadPrec L
    $creadPrec :: ReadPrec L
    readList :: ReadS [L]
    $creadList :: ReadS [L]
    readsPrec :: Int -> ReadS L
    $creadsPrec :: Int -> ReadS L
    Read, Typeable L
    DataType
    Constr
    Typeable L =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> L -> c L)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c L)
    -> (L -> Constr)
    -> (L -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c L))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L))
    -> ((forall b. Data b => b -> b) -> L -> L)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r)
    -> (forall u. (forall d. Data d => d -> u) -> L -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> L -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> L -> m L)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> L -> m L)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> L -> m L)
    -> Data L
    L -> DataType
    L -> Constr
    (forall b. Data b => b -> b) -> L -> L
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> L -> c L
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c L
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> L -> u
    forall u. (forall d. Data d => d -> u) -> L -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> L -> m L
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> L -> m L
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c L
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> L -> c L
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c L)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)
    $cCons :: Constr
    $cNil :: Constr
    $tL :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> L -> m L
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> L -> m L
    gmapMp :: (forall d. Data d => d -> m d) -> L -> m L
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> L -> m L
    gmapM :: (forall d. Data d => d -> m d) -> L -> m L
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> L -> m L
    gmapQi :: Int -> (forall d. Data d => d -> u) -> L -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> L -> u
    gmapQ :: (forall d. Data d => d -> u) -> L -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> L -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r
    gmapT :: (forall b. Data b => b -> b) -> L -> L
    $cgmapT :: (forall b. Data b => b -> b) -> L -> L
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c L)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c L)
    dataTypeOf :: L -> DataType
    $cdataTypeOf :: L -> DataType
    toConstr :: L -> Constr
    $ctoConstr :: L -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c L
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c L
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> L -> c L
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> L -> c L
    $cp1Data :: Typeable L
    Data)

    -- | Declare instances to make 'L' a usable uninterpreted sort. First we need the
    -- 'SymVal' instance, with the default definition sufficing.
    instance SymVal L

    -- | Similarly, 'HasKind's default implementation is sufficient.
    instance HasKind L

    -- | An uninterpreted "classify" function. Really, we only care about
    -- the fact that such a function exists, not what it does.
    classify :: SBV L -> SInteger
    classify :: SBV L -> SInteger
    classify = String -> SBV L -> SInteger
    forall a. Uninterpreted a => String -> a
    uninterpret "classify"

    -- | Formulate a query that essentially asserts a cardinality constraint on
    -- the uninterpreted sort 'L'. The goal is to say there are precisely 3
    -- such things, as it might be the case. We manage this by declaring four
    -- elements, and asserting that for a free variable of this sort, the
    -- shape of the data matches one of these three instances. That is, we
    -- assert that all the instances of the data 'L' can be classified into
    -- 3 equivalence classes. Then, allSat returns all the possible instances,
    -- which of course are all uninterpreted.
    --
    -- As expected, we have:
    --
    -- >>> allSat genLs
    -- Solution #1:
    --   l  = L!val!0 :: L
    --   l0 = L!val!0 :: L
    --   l1 = L!val!1 :: L
    --   l2 = L!val!2 :: L
    -- <BLANKLINE>
    --   classify :: L -> Integer
    --   classify L!val!2 = 2
    --   classify L!val!1 = 1
    --   classify _       = 0
    -- Solution #2:
    --   l  = L!val!1 :: L
    --   l0 = L!val!0 :: L
    --   l1 = L!val!1 :: L
    --   l2 = L!val!2 :: L
    -- <BLANKLINE>
    --   classify :: L -> Integer
    --   classify L!val!2 = 2
    --   classify L!val!1 = 1
    --   classify _       = 0
    -- Solution #3:
    --   l  = L!val!2 :: L
    --   l0 = L!val!0 :: L
    --   l1 = L!val!1 :: L
    --   l2 = L!val!2 :: L
    -- <BLANKLINE>
    --   classify :: L -> Integer
    --   classify L!val!2 = 2
    --   classify L!val!1 = 1
    --   classify _       = 0
    -- Found 3 different solutions.
    genLs :: Predicate
    genLs :: Predicate
    genLs = do [l :: SBV L
    l, l0 :: SBV L
    l0, l1 :: SBV L
    l1, l2 :: SBV L
    l2] <- [String] -> Symbolic [SBV L]
    forall a. SymVal a => [String] -> Symbolic [SBV a]
    symbolics ["l", "l0", "l1", "l2"]
               SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV L -> SInteger
    classify SBV L
    l0 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 0
               SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV L -> SInteger
    classify SBV L
    l1 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 1
               SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV L -> SInteger
    classify SBV L
    l2 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 2
               SBool -> Predicate
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Predicate) -> SBool -> Predicate
    forall a b. (a -> b) -> a -> b
    $ SBV L
    l SBV L -> SBV L -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV L
    l0 SBool -> SBool -> SBool
    .|| SBV L
    l SBV L -> SBV L -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV L
    l1 SBool -> SBool -> SBool
    .|| SBV L
    l SBV L -> SBV L -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV L
    l2