-----------------------------------------------------------------------------
-- |
-- 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)