{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Uninterpreted.Shannon where
import Data.SBV
type Ternary = SBool -> SBool -> SBool -> SBool
type Binary = SBool -> SBool-> SBool
pos :: (SBool -> a) -> a
pos :: forall a. (SBool -> a) -> a
pos SBool -> a
f = SBool -> a
f SBool
sTrue
neg :: (SBool -> a) -> a
neg :: forall a. (SBool -> a) -> a
neg SBool -> a
f = SBool -> a
f SBool
sFalse
shannon :: IO ThmResult
shannon :: IO ThmResult
shannon = Ternary -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (Ternary -> IO ThmResult) -> Ternary -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
x SBool
y SBool
z -> Ternary
f SBool
x SBool
y SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBool
x SBool -> SBool -> SBool
.&& Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
.|| SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.&& Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z)
where f :: Ternary
f :: Ternary
f = String -> Ternary
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
shannon2 :: IO ThmResult
shannon2 :: IO ThmResult
shannon2 = Ternary -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (Ternary -> IO ThmResult) -> Ternary -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
x SBool
y SBool
z -> Ternary
f SBool
x SBool
y SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== ((SBool
x SBool -> SBool -> SBool
.|| Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z) SBool -> SBool -> SBool
.&& (SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.|| Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z))
where f :: Ternary
f :: Ternary
f = String -> Ternary
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
derivative :: Ternary -> Binary
derivative :: Ternary -> SBool -> SBool -> SBool
derivative Ternary
f SBool
y SBool
z = Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
.<+> Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z
noWiggle :: IO ThmResult
noWiggle :: IO ThmResult
noWiggle = (SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
y SBool
z -> SBool -> SBool
sNot (SBool -> SBool -> SBool
f' SBool
y SBool
z) SBool -> SBool -> SBool
.<=> Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z
where f :: Ternary
f :: Ternary
f = String -> Ternary
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
f' :: SBool -> SBool -> SBool
f' = Ternary -> SBool -> SBool -> SBool
derivative Ternary
f
universal :: Ternary -> Binary
universal :: Ternary -> SBool -> SBool -> SBool
universal Ternary
f SBool
y SBool
z = Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
.&& Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z
univOK :: IO ThmResult
univOK :: IO ThmResult
univOK = (SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
y SBool
z -> SBool -> SBool -> SBool
f' SBool
y SBool
z SBool -> SBool -> SBool
.=> Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
.&& Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z
where f :: Ternary
f :: Ternary
f = String -> Ternary
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
f' :: SBool -> SBool -> SBool
f' = Ternary -> SBool -> SBool -> SBool
universal Ternary
f
existential :: Ternary -> Binary
existential :: Ternary -> SBool -> SBool -> SBool
existential Ternary
f SBool
y SBool
z = Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
.|| Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z
existsOK :: IO ThmResult
existsOK :: IO ThmResult
existsOK = (SBool -> SBool -> SBool) -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove ((SBool -> SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
y SBool
z -> SBool -> SBool -> SBool
f' SBool
y SBool
z SBool -> SBool -> SBool
.=> Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
pos Ternary
f SBool
y SBool
z SBool -> SBool -> SBool
.|| Ternary -> SBool -> SBool -> SBool
forall a. (SBool -> a) -> a
neg Ternary
f SBool
y SBool
z
where f :: Ternary
f :: Ternary
f = String -> Ternary
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
f' :: SBool -> SBool -> SBool
f' = Ternary -> SBool -> SBool -> SBool
existential Ternary
f