    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Uninterpreted.Deduce
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates uninterpreted sorts and how they can be used for deduction.
    -- This example is inspired by the discussion at <http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3>,
    -- essentially showing how to show the required deduction using SBV.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.Deduce where

    import Data.Generics
    import Data.SBV

    -- we will have our own "uninterpreted" functions corresponding
    -- to not/or/and, so hide their Prelude counterparts.
    import Prelude hiding (not, or, and)

    -----------------------------------------------------------------------------
    -- * Representing uninterpreted booleans
    -----------------------------------------------------------------------------

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

    -- | Handy shortcut for the type of symbolic values over 'B'
    type SB = SBV B

    -----------------------------------------------------------------------------
    -- * Uninterpreted connectives over 'B'
    -----------------------------------------------------------------------------

    -- | Uninterpreted logical connective 'and'
    and :: SB -> SB -> SB
    and :: SBV B -> SBV B -> SBV B
    and = String -> SBV B -> SBV B -> SBV B
    forall a. Uninterpreted a => String -> a
    uninterpret "AND"

    -- | Uninterpreted logical connective 'or'
    or :: SB -> SB -> SB
    or :: SBV B -> SBV B -> SBV B
    or  = String -> SBV B -> SBV B -> SBV B
    forall a. Uninterpreted a => String -> a
    uninterpret "OR"

    -- | Uninterpreted logical connective 'not'
    not :: SB -> SB
    not :: SBV B -> SBV B
    not = String -> SBV B -> SBV B
    forall a. Uninterpreted a => String -> a
    uninterpret "NOT"

    -----------------------------------------------------------------------------
    -- * Axioms of the logical system
    -----------------------------------------------------------------------------

    -- | Distributivity of OR over AND, as an axiom in terms of
    -- the uninterpreted functions we have introduced. Note how
    -- variables range over the uninterpreted sort 'B'.
    ax1 :: [String]
    ax1 :: [String]
    ax1 = [ "(assert (forall ((p B) (q B) (r B))"
          , "   (= (AND (OR p q) (OR p r))"
          , "      (OR p (AND q r)))))"
          ]

    -- | One of De Morgan's laws, again as an axiom in terms
    -- of our uninterpeted logical connectives.
    ax2 :: [String]
    ax2 :: [String]
    ax2 = [ "(assert (forall ((p B) (q B))"
          , "   (= (NOT (OR p q))"
          , "      (AND (NOT p) (NOT q)))))"
          ]

    -- | Double negation axiom, similar to the above.
    ax3 :: [String]
    ax3 :: [String]
    ax3 = ["(assert (forall ((p B)) (= (NOT (NOT p)) p)))"]

    -----------------------------------------------------------------------------
    -- * Demonstrated deduction
    -----------------------------------------------------------------------------

    -- | Proves the equivalence @NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r)@,
    -- following from the axioms we have specified above. We have:
    --
    -- >>> test
    -- Q.E.D.
    test :: IO ThmResult
    test :: IO ThmResult
    test = SymbolicT IO SBool -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove (SymbolicT IO SBool -> IO ThmResult)
    -> SymbolicT IO SBool -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ do String -> [String] -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
    addAxiom "OR distributes over AND" [String]
    ax1
                      String -> [String] -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
    addAxiom "de Morgan"               [String]
    ax2
                      String -> [String] -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
    addAxiom "double negation"         [String]
    ax3
                      SBV B
    p <- String -> Symbolic (SBV B)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "p"
                      SBV B
    q <- String -> Symbolic (SBV B)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "q"
                      SBV B
    r <- String -> Symbolic (SBV B)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "r"
                      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 B -> SBV B
    not (SBV B
    p SBV B -> SBV B -> SBV B
    `or` (SBV B
    q SBV B -> SBV B -> SBV B
    `and` SBV B
    r))
                             SBV B -> SBV B -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SBV B -> SBV B
    not SBV B
    p SBV B -> SBV B -> SBV B
    `and` SBV B -> SBV B
    not SBV B
    q) SBV B -> SBV B -> SBV B
    `or` (SBV B -> SBV B
    not SBV B
    p SBV B -> SBV B -> SBV B
    `and` SBV B -> SBV B
    not SBV B
    r)