{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Uninterpreted.Deduce where
import Data.SBV
import Prelude hiding (not, or, and)
data B
mkUninterpretedSort ''B
and :: SB -> SB -> SB
and :: SB -> SB -> SB
and = String -> SB -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"AND"
or :: SB -> SB -> SB
or :: SB -> SB -> SB
or = String -> SB -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"OR"
not :: SB -> SB
not :: SB -> SB
not = String -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"NOT"
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 (Forall Any B -> Forall Any B -> Forall Any B -> SBool)
-> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any B -> Forall Any B -> Forall Any B -> SBool)
-> SymbolicT IO ())
-> (Forall Any B -> Forall Any B -> Forall Any B -> SBool)
-> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SB
p) (Forall SB
q) (Forall SB
r) -> (SB
p SB -> SB -> SB
`or` SB
q) SB -> SB -> SB
`and` (SB
p SB -> SB -> SB
`or` SB
r) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB
p SB -> SB -> SB
`or` (SB
q SB -> SB -> SB
`and` SB
r)
(Forall Any B -> Forall Any B -> SBool) -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any B -> Forall Any B -> SBool) -> SymbolicT IO ())
-> (Forall Any B -> Forall Any B -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SB
p) (Forall SB
q) -> SB -> SB
not (SB
p SB -> SB -> SB
`or` SB
q) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB -> SB
not SB
p SB -> SB -> SB
`and` SB -> SB
not SB
q
(Forall Any B -> SBool) -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any B -> SBool) -> SymbolicT IO ())
-> (Forall Any B -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SB
p) -> SB -> SB
not (SB -> SB
not SB
p) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB
p
SB
p <- String -> Symbolic SB
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"p"
SB
q <- String -> Symbolic SB
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"q"
SB
r <- String -> Symbolic SB
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"r"
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
$ SB -> SB
not (SB
p SB -> SB -> SB
`or` (SB
q SB -> SB -> SB
`and` SB
r))
SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SB -> SB
not SB
p SB -> SB -> SB
`and` SB -> SB
not SB
q) SB -> SB -> SB
`or` (SB -> SB
not SB
p SB -> SB -> SB
`and` SB -> SB
not SB
r)