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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.Sort where

    import Data.SBV

    -- | A new data-type that we expect to use in an uninterpreted fashion
    -- in the backend SMT solver.
    data Q

    -- | Make 'Q' an uinterpreted sort. This will automatically introduce the
    -- type 'SQ' into our environment, which is the symbolic version of the
    -- carrier type 'Q'.
    mkUninterpretedSort ''Q

    -- | Declare an uninterpreted function that works over Q's
    f :: SQ -> SQ
    f :: SQ -> SQ
    f = String -> SQ -> SQ
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "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. Satisfiable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do SQ
    x <- String -> Symbolic SQ
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "x"
                  SBool -> SymbolicT IO SBool
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SQ -> SQ
    f SQ
    x SQ -> SQ -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SQ
    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. Satisfiable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do SQ
    x <- String -> Symbolic SQ
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "x"
                  (Forall Any Q -> Forall Any Q -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Q -> Forall Any Q -> SBool) -> SymbolicT IO ())
    -> (Forall Any Q -> Forall Any Q -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SQ
    a) (Forall SQ
    b) -> SQ
    a SQ -> SQ -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SQ
    b :: SQ)
                  SBool -> SymbolicT IO SBool
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SQ -> SQ
    f SQ
    x SQ -> SQ -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SQ
    x