    -----------------------------------------------------------------------------
    -- |
    -- 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 DeriveAnyClass     #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell    #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.UISortAllSat where

    import Data.SBV

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> 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.
    data L

    -- | Make 'L' into an uninterpreted sort, automatically introducing 'SL'
    -- as a synonym for 'SBV' 'L'.
    mkUninterpretedSort ''L

    -- | An uninterpreted "classify" function. Really, we only care about
    -- the fact that such a function exists, not what it does.
    classify :: SL -> SInteger
    classify :: SL -> SInteger
    classify = String -> SL -> SInteger
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "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!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
    -- 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!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
    -- Found 3 different solutions.
    genLs :: Predicate
    genLs :: Predicate
    genLs = do [SL
    l, SL
    l0, SL
    l1, SL
    l2] <- [String] -> Symbolic [SL]
    forall a. SymVal a => [String] -> Symbolic [SBV a]
    symbolics [String
    "l", String
    "l0", String
    "l1", String
    "l2"]
               SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SL -> SInteger
    classify SL
    l0 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    0
               SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SL -> SInteger
    classify SL
    l1 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    1
               SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SL -> SInteger
    classify SL
    l2 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    2
               SBool -> Predicate
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Predicate) -> SBool -> Predicate
    forall a b. (a -> b) -> a -> b
    $ SL
    l SL -> SL -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SL
    l0 SBool -> SBool -> SBool
    .|| SL
    l SL -> SL -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SL
    l1 SBool -> SBool -> SBool
    .|| SL
    l SL -> SL -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SL
    l2