-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Enumerate
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how enumerations can be translated to their SMT-Lib
-- counterparts, without losing any information content. Also see
-- "Documentation.SBV.Examples.Puzzles.U2Bridge" for a more detailed
-- example involving enumerations.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.Enumerate where

import Data.SBV

-- | A simple enumerated type, that we'd like to translate to SMT-Lib intact;
-- i.e., this type will not be uninterpreted but rather preserved and will
-- be just like any other symbolic type SBV provides.
--
-- Also note that we need to have the following @LANGUAGE@ options defined:
-- @TemplateHaskell@, @StandaloneDeriving@, @DeriveDataTypeable@, @DeriveAnyClass@ for
-- this to work.
data E = A | B | C
       deriving (Int -> E
E -> Int
E -> [E]
E -> E
E -> E -> [E]
E -> E -> E -> [E]
(E -> E)
-> (E -> E)
-> (Int -> E)
-> (E -> Int)
-> (E -> [E])
-> (E -> E -> [E])
-> (E -> E -> [E])
-> (E -> E -> E -> [E])
-> Enum E
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: E -> E
succ :: E -> E
$cpred :: E -> E
pred :: E -> E
$ctoEnum :: Int -> E
toEnum :: Int -> E
$cfromEnum :: E -> Int
fromEnum :: E -> Int
$cenumFrom :: E -> [E]
enumFrom :: E -> [E]
$cenumFromThen :: E -> E -> [E]
enumFromThen :: E -> E -> [E]
$cenumFromTo :: E -> E -> [E]
enumFromTo :: E -> E -> [E]
$cenumFromThenTo :: E -> E -> E -> [E]
enumFromThenTo :: E -> E -> E -> [E]
Enum, E
E -> E -> Bounded E
forall a. a -> a -> Bounded a
$cminBound :: E
minBound :: E
$cmaxBound :: E
maxBound :: E
Bounded, E -> E -> Bool
(E -> E -> Bool) -> (E -> E -> Bool) -> Eq E
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: E -> E -> Bool
== :: E -> E -> Bool
$c/= :: E -> E -> Bool
/= :: E -> E -> Bool
Eq, Eq E
Eq E =>
(E -> E -> Ordering)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> E)
-> (E -> E -> E)
-> Ord E
E -> E -> Bool
E -> E -> Ordering
E -> E -> E
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
$ccompare :: E -> E -> Ordering
compare :: E -> E -> Ordering
$c< :: E -> E -> Bool
< :: E -> E -> Bool
$c<= :: E -> E -> Bool
<= :: E -> E -> Bool
$c> :: E -> E -> Bool
> :: E -> E -> Bool
$c>= :: E -> E -> Bool
>= :: E -> E -> Bool
$cmax :: E -> E -> E
max :: E -> E -> E
$cmin :: E -> E -> E
min :: E -> E -> E
Ord)

-- | Make 'E' a symbolic value.
mkSymbolicEnumeration ''E

-- | Have the SMT solver enumerate the elements of the domain. We have:
--
-- >>> elts
-- Solution #1:
--   s0 = C :: E
-- Solution #2:
--   s0 = A :: E
-- Solution #3:
--   s0 = B :: E
-- Found 3 different solutions.
elts :: IO AllSatResult
elts :: IO AllSatResult
elts = (SE -> SBool) -> IO AllSatResult
forall a. Satisfiable a => a -> IO AllSatResult
allSat ((SE -> SBool) -> IO AllSatResult)
-> (SE -> SBool) -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ \(SE
x::SE) -> SE
x SE -> SE -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SE
x

-- | Shows that if we require 4 distinct elements of the type 'E', we shall fail; as
-- the domain only has three elements. We have:
--
-- >>> four
-- Unsatisfiable
four :: IO SatResult
four :: IO SatResult
four = (SE -> SE -> SE -> SE -> SBool) -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat ((SE -> SE -> SE -> SE -> SBool) -> IO SatResult)
-> (SE -> SE -> SE -> SE -> SBool) -> IO SatResult
forall a b. (a -> b) -> a -> b
$ \SE
a SE
b SE
c (SE
d::SE) -> [SE] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct [SE
a, SE
b, SE
c, SE
d]

-- | Enumerations are automatically ordered, so we can ask for the maximum
-- element. Note the use of quantification. We have:
--
-- >>> maxE
-- Satisfiable. Model:
--   maxE = C :: E
maxE :: IO SatResult
maxE :: IO SatResult
maxE = SymbolicT IO () -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO () -> IO SatResult)
-> SymbolicT IO () -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SE
mx :: SE <- String -> Symbolic SE
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"maxE"
                (Forall Any E -> SBool) -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any E -> SBool) -> SymbolicT IO ())
-> (Forall Any E -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SE
e) -> SE
mx SE -> SE -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SE
e

-- | Similarly, we get the minimum element. We have:
--
-- >>> minE
-- Satisfiable. Model:
--   minE = A :: E
minE :: IO SatResult
minE :: IO SatResult
minE = SymbolicT IO () -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO () -> IO SatResult)
-> SymbolicT IO () -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SE
mn :: SE <- String -> Symbolic SE
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"minE"
                (Forall Any E -> SBool) -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any E -> SBool) -> SymbolicT IO ())
-> (Forall Any E -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SE
e) -> SE
mn SE -> SE -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SE
e