-----------------------------------------------------------------------------
-- |
-- 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 = 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 mx :: SE <- String -> Symbolic SE
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"maxE"
                constrain $ \(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 mn :: SE <- String -> Symbolic SE
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"minE"
                constrain $ \(Forall SE
e) -> SE
mn SE -> SE -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SE
e