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

-- | 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 = B :: E
-- Solution #3:
--   s0 = A :: E
-- Found 3 different solutions.
elts :: IO AllSatResult
elts :: IO AllSatResult
elts = (SBV E -> SBool) -> IO AllSatResult
forall a. Provable a => a -> IO AllSatResult
allSat ((SBV E -> SBool) -> IO AllSatResult)
-> (SBV E -> SBool) -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ \(SBV E
x::SE) -> SBV E
x SBV E -> SBV E -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV E
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 = (SBV E -> SBV E -> SBV E -> SBV E -> SBool) -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat ((SBV E -> SBV E -> SBV E -> SBV E -> SBool) -> IO SatResult)
-> (SBV E -> SBV E -> SBV E -> SBV E -> SBool) -> IO SatResult
forall a b. (a -> b) -> a -> b
$ \SBV E
a SBV E
b SBV E
c (SBV E
d::SE) -> [SBV E] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct [SBV E
a, SBV E
b, SBV E
c, SBV E
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 SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV E
mx <- String -> Symbolic (SBV E)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"maxE"
                SBV E
e  <- String -> Symbolic (SBV E)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"e"
                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 E
mx SBV E -> SBV E -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= (SBV E
e::SE)

-- | Similarly, we get the minimum element. We have:
--
-- >>> minE
-- Satisfiable. Model:
--   minE = A :: E
minE :: IO SatResult
minE :: IO SatResult
minE = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV E
mx <- String -> Symbolic (SBV E)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"minE"
                SBV E
e  <- String -> Symbolic (SBV E)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"e"
                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 E
mx SBV E -> SBV E -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= (SBV E
e::SE)