-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Enumerate
  Copyright : ( c )  
-- License   : BSD3
-- Maintainer: 
-- 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@ ,  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 = allSat $ \(x::SE) -> x .== 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 = sat $ \a b c (d::SE) -> distinct [a, b, c, 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 = sat $ do mx <- sbvExists "maxE"
                e  <- sbvForall "e"
                return $ mx .>= (e::SE)

-- | Similarly, we get the minimum element. We have:
--
-- >>> minE
-- Satisfiable. Model:
--   minE = A :: E
minE :: IO SatResult
minE = sat $ do mx <- sbvExists "minE"
                e  <- sbvForall "e"
                return $ mx .<= (e::SE)

---------------------------------------------------------------------------
 |
 Module    : Documentation.SBV.Examples.Misc.Enumerate
 License   : BSD3
 Maintainer: 
 Stability : experimental

 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 StandaloneDeriving  #
# OPTIONS_GHC -Wall -Werror #
 i.e., this type will not be uninterpreted but rather preserved and will

 Also note that we need to have the following @LANGUAGE@ options defined:
 this to work.
 | Make 'E' a symbolic value.

 >>> elts
 Solution #1:
   s0 = C :: E
 Solution #2:
   s0 = B :: E
 Solution #3:
   s0 = A :: E

 Unsatisfiable
 | 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
 | Similarly, we get the minimum element. We have:

 >>> minE
 Satisfiable. Model:
   minE = A :: E
  Copyright : ( c )  
  Demonstrates how enumerations can be translated to their SMT - Lib

# LANGUAGE ScopedTypeVariables #
# LANGUAGE TemplateHaskell      #


module Documentation.SBV.Examples.Misc.Enumerate where

import Data.SBV

  | A simple enumerated type , that we 'd like to translate to SMT - Lib intact ;
  be just like any other symbolic type SBV provides .
  @TemplateHaskell@ , @StandaloneDeriving@ , @DeriveDataTypeable@ ,  for
data E = A | B | C

mkSymbolicEnumeration ''E

  | Have the SMT solver enumerate the elements of the domain . We have :
  Found 3 different solutions .
elts :: IO AllSatResult
elts = allSat $ \(x::SE) -> x .== 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
four :: IO SatResult
four = sat $ \a b c (d::SE) -> distinct [a, b, c, d]

maxE :: IO SatResult
maxE = sat $ do mx <- sbvExists "maxE"
                e  <- sbvForall "e"
                return $ mx .>= (e::SE)

minE :: IO SatResult
minE = sat $ do mx <- sbvExists "minE"
                e  <- sbvForall "e"
                return $ mx .<= (e::SE)
