    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Uninterpreted.Sort
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates uninterpreted sorts, together with axioms.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass     #-}
    {-# LANGUAGE DeriveDataTypeable #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.Sort where

    import Data.Generics
    import Data.SBV

    -- | A new data-type that we expect to use in an uninterpreted fashion
    -- in the backend SMT solver. Note the custom @deriving@ clause, which
    -- takes care of most of the boilerplate. The () field is needed so
    -- SBV will not translate it to an enumerated data-type
    newtype Q = Q () deriving (Q -> Q -> Bool
    (Q -> Q -> Bool) -> (Q -> Q -> Bool) -> Eq Q
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Q -> Q -> Bool
    $c/= :: Q -> Q -> Bool
    == :: Q -> Q -> Bool
    $c== :: Q -> Q -> Bool
    Eq, Eq Q
    Eq Q =>
    (Q -> Q -> Ordering)
    -> (Q -> Q -> Bool)
    -> (Q -> Q -> Bool)
    -> (Q -> Q -> Bool)
    -> (Q -> Q -> Bool)
    -> (Q -> Q -> Q)
    -> (Q -> Q -> Q)
    -> Ord Q
    Q -> Q -> Bool
    Q -> Q -> Ordering
    Q -> Q -> Q
    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 :: Q -> Q -> Q
    $cmin :: Q -> Q -> Q
    max :: Q -> Q -> Q
    $cmax :: Q -> Q -> Q
    >= :: Q -> Q -> Bool
    $c>= :: Q -> Q -> Bool
    > :: Q -> Q -> Bool
    $c> :: Q -> Q -> Bool
    <= :: Q -> Q -> Bool
    $c<= :: Q -> Q -> Bool
    < :: Q -> Q -> Bool
    $c< :: Q -> Q -> Bool
    compare :: Q -> Q -> Ordering
    $ccompare :: Q -> Q -> Ordering
    $cp1Ord :: Eq Q
    Ord, Typeable Q
    DataType
    Constr
    Typeable Q =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Q -> c Q)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Q)
    -> (Q -> Constr)
    -> (Q -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Q))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q))
    -> ((forall b. Data b => b -> b) -> Q -> Q)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Q -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Q -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Q -> m Q)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Q -> m Q)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Q -> m Q)
    -> Data Q
    Q -> DataType
    Q -> Constr
    (forall b. Data b => b -> b) -> Q -> Q
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Q -> c Q
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Q
    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) -> Q -> u
    forall u. (forall d. Data d => d -> u) -> Q -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Q -> m Q
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Q -> m Q
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Q
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Q -> c Q
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Q)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q)
    $cQ :: Constr
    $tQ :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Q -> m Q
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Q -> m Q
    gmapMp :: (forall d. Data d => d -> m d) -> Q -> m Q
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Q -> m Q
    gmapM :: (forall d. Data d => d -> m d) -> Q -> m Q
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Q -> m Q
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Q -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Q -> u
    gmapQ :: (forall d. Data d => d -> u) -> Q -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Q -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r
    gmapT :: (forall b. Data b => b -> b) -> Q -> Q
    $cgmapT :: (forall b. Data b => b -> b) -> Q -> Q
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Q)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Q)
    dataTypeOf :: Q -> DataType
    $cdataTypeOf :: Q -> DataType
    toConstr :: Q -> Constr
    $ctoConstr :: Q -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Q
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Q
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Q -> c Q
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Q -> c Q
    $cp1Data :: Typeable Q
    Data, ReadPrec [Q]
    ReadPrec Q
    Int -> ReadS Q
    ReadS [Q]
    (Int -> ReadS Q)
    -> ReadS [Q] -> ReadPrec Q -> ReadPrec [Q] -> Read Q
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    readListPrec :: ReadPrec [Q]
    $creadListPrec :: ReadPrec [Q]
    readPrec :: ReadPrec Q
    $creadPrec :: ReadPrec Q
    readList :: ReadS [Q]
    $creadList :: ReadS [Q]
    readsPrec :: Int -> ReadS Q
    $creadsPrec :: Int -> ReadS Q
    Read, Int -> Q -> ShowS
    [Q] -> ShowS
    Q -> String
    (Int -> Q -> ShowS) -> (Q -> String) -> ([Q] -> ShowS) -> Show Q
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Q] -> ShowS
    $cshowList :: [Q] -> ShowS
    show :: Q -> String
    $cshow :: Q -> String
    showsPrec :: Int -> Q -> ShowS
    $cshowsPrec :: Int -> Q -> ShowS
    Show, Typeable Q
    HasKind Q
    (HasKind Q, Typeable Q) =>
    (forall (m :: * -> *).
     MonadSymbolic m =>
     Maybe Quantifier -> Maybe String -> m (SBV Q))
    -> (Q -> SBV Q)
    -> (CV -> Q)
    -> (SBV Q -> (Q -> Bool) -> Bool)
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q])
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q])
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q])
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q))
    -> (forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV Q])
    -> (SBV Q -> Maybe Q)
    -> (SBV Q -> Bool)
    -> (SBV Q -> Bool)
    -> SymVal Q
    CV -> Q
    SBV Q -> Bool
    SBV Q -> Maybe Q
    SBV Q -> (Q -> Bool) -> Bool
    Q -> SBV Q
    forall a.
    (HasKind a, Typeable a) =>
    (forall (m :: * -> *).
     MonadSymbolic m =>
     Maybe Quantifier -> Maybe String -> m (SBV a))
    -> (a -> SBV a)
    -> (CV -> a)
    -> (SBV a -> (a -> Bool) -> Bool)
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV a])
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV a])
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV a])
    -> (forall (m :: * -> *). MonadSymbolic m => String -> m (SBV a))
    -> (forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV a])
    -> (SBV a -> Maybe a)
    -> (SBV a -> Bool)
    -> (SBV a -> Bool)
    -> SymVal a
    forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
    forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
    forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV Q]
    forall (m :: * -> *).
    MonadSymbolic m =>
    Maybe Quantifier -> Maybe String -> m (SBV Q)
    isSymbolic :: SBV Q -> Bool
    $cisSymbolic :: SBV Q -> Bool
    isConcrete :: SBV Q -> Bool
    $cisConcrete :: SBV Q -> Bool
    unliteral :: SBV Q -> Maybe Q
    $cunliteral :: SBV Q -> Maybe Q
    symbolics :: [String] -> m [SBV Q]
    $csymbolics :: forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBV Q]
    symbolic :: String -> m (SBV Q)
    $csymbolic :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
    mkFreeVars :: Int -> m [SBV Q]
    $cmkFreeVars :: forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
    free_ :: m (SBV Q)
    $cfree_ :: forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
    free :: String -> m (SBV Q)
    $cfree :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
    mkExistVars :: Int -> m [SBV Q]
    $cmkExistVars :: forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
    exists_ :: m (SBV Q)
    $cexists_ :: forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
    exists :: String -> m (SBV Q)
    $cexists :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
    mkForallVars :: Int -> m [SBV Q]
    $cmkForallVars :: forall (m :: * -> *). MonadSymbolic m => Int -> m [SBV Q]
    forall_ :: m (SBV Q)
    $cforall_ :: forall (m :: * -> *). MonadSymbolic m => m (SBV Q)
    forall :: String -> m (SBV Q)
    $cforall :: forall (m :: * -> *). MonadSymbolic m => String -> m (SBV Q)
    isConcretely :: SBV Q -> (Q -> Bool) -> Bool
    $cisConcretely :: SBV Q -> (Q -> Bool) -> Bool
    fromCV :: CV -> Q
    $cfromCV :: CV -> Q
    literal :: Q -> SBV Q
    $cliteral :: Q -> SBV Q
    mkSymVal :: Maybe Quantifier -> Maybe String -> m (SBV Q)
    $cmkSymVal :: forall (m :: * -> *).
    MonadSymbolic m =>
    Maybe Quantifier -> Maybe String -> m (SBV Q)
    $cp2SymVal :: Typeable Q
    $cp1SymVal :: HasKind Q
    SymVal, Q -> Bool
    Q -> Int
    Q -> String
    Q -> Kind
    (Q -> Kind)
    -> (Q -> Bool)
    -> (Q -> Int)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> Bool)
    -> (Q -> String)
    -> HasKind Q
    forall a.
    (a -> Kind)
    -> (a -> Bool)
    -> (a -> Int)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> Bool)
    -> (a -> String)
    -> HasKind a
    showType :: Q -> String
    $cshowType :: Q -> String
    isEither :: Q -> Bool
    $cisEither :: Q -> Bool
    isMaybe :: Q -> Bool
    $cisMaybe :: Q -> Bool
    isTuple :: Q -> Bool
    $cisTuple :: Q -> Bool
    isSet :: Q -> Bool
    $cisSet :: Q -> Bool
    isList :: Q -> Bool
    $cisList :: Q -> Bool
    isString :: Q -> Bool
    $cisString :: Q -> Bool
    isChar :: Q -> Bool
    $cisChar :: Q -> Bool
    isUninterpreted :: Q -> Bool
    $cisUninterpreted :: Q -> Bool
    isUnbounded :: Q -> Bool
    $cisUnbounded :: Q -> Bool
    isDouble :: Q -> Bool
    $cisDouble :: Q -> Bool
    isFloat :: Q -> Bool
    $cisFloat :: Q -> Bool
    isReal :: Q -> Bool
    $cisReal :: Q -> Bool
    isBounded :: Q -> Bool
    $cisBounded :: Q -> Bool
    isBoolean :: Q -> Bool
    $cisBoolean :: Q -> Bool
    intSizeOf :: Q -> Int
    $cintSizeOf :: Q -> Int
    hasSign :: Q -> Bool
    $chasSign :: Q -> Bool
    kindOf :: Q -> Kind
    $ckindOf :: Q -> Kind
    HasKind)

    -- | Declare an uninterpreted function that works over Q's
    f :: SBV Q -> SBV Q
    f :: SBV Q -> SBV Q
    f = String -> SBV Q -> SBV Q
    forall a. Uninterpreted a => String -> a
    uninterpret "f"

    -- | A satisfiable example, stating that there is an element of the domain
    -- 'Q' such that 'f' returns a different element. Note that this is valid only
    -- when the domain 'Q' has at least two elements. We have:
    --
    -- >>> t1
    -- Satisfiable. Model:
    --   x = Q!val!0 :: Q
    -- <BLANKLINE>
    --   f :: Q -> Q
    --   f _ = Q!val!1
    t1 :: IO SatResult
    t1 :: IO SatResult
    t1 = SymbolicT IO SBool -> IO SatResult
    forall a. Provable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do SBV Q
    x <- String -> Symbolic (SBV Q)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "x"
                  SBool -> SymbolicT IO SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SBV Q -> SBV Q
    f SBV Q
    x SBV Q -> SBV Q -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SBV Q
    x

    -- | This is a variant on the first example, except we also add an axiom
    -- for the sort, stating that the domain 'Q' has only one element. In this case
    -- the problem naturally becomes unsat. We have:
    --
    -- >>> t2
    -- Unsatisfiable
    t2 :: IO SatResult
    t2 :: IO SatResult
    t2 = SymbolicT IO SBool -> IO SatResult
    forall a. Provable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do SBV Q
    x <- String -> Symbolic (SBV Q)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "x"
                  String -> [String] -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
    addAxiom "Q" ["(assert (forall ((x Q) (y Q)) (= x y)))"]
                  SBool -> SymbolicT IO SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SBV Q -> SBV Q
    f SBV Q
    x SBV Q -> SBV Q -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SBV Q
    x