    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Misc.ModelExtract
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates use of programmatic model extraction. When programming with
    -- SBV, we typically use `sat`/`allSat` calls to compute models automatically.
    -- In more advanced uses, however, the user might want to use programmable
    -- extraction features to do fancier programming. We demonstrate some of
    -- these utilities here.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Misc.ModelExtract where

    import Data.SBV

    -- | A simple function to generate a new integer value, that is not in the
    -- given set of values. We also require the value to be non-negative
    outside :: [Integer] -> IO SatResult
    outside :: [Integer] -> IO SatResult
    outside [Integer]
    disallow = SymbolicT IO SBool -> IO SatResult
    forall a. Satisfiable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do SInteger
    x <- String -> Symbolic SInteger
    sInteger String
    "x"
                                let notEq :: Integer -> m ()
    notEq Integer
    i = SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    x SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    i
                                (Integer -> SymbolicT IO ()) -> [Integer] -> SymbolicT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Integer -> SymbolicT IO ()
    forall {m :: * -> *}. SolverContext m => Integer -> m ()
    notEq [Integer]
    disallow
                                SBool -> SymbolicT IO SBool
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0

    -- | We now use "outside" repeatedly to generate 10 integers, such that we not only disallow
    -- previously generated elements, but also any value that differs from previous solutions
    -- by less than 5.  Here, we use the `getModelValue` function. We could have also extracted the dictionary
    -- via `getModelDictionary` and did fancier programming as well, as necessary. We have:
    --
    -- >>> genVals
    -- [45,40,35,30,25,20,15,10,5,0]
    genVals :: IO [Integer]
    genVals :: IO [Integer]
    genVals = [Integer] -> [Integer] -> IO [Integer]
    go [] []
      where go :: [Integer] -> [Integer] -> IO [Integer]
    go [Integer]
    _ [Integer]
    model
             | [Integer] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Integer]
    model Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    10 = [Integer] -> IO [Integer]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Integer]
    model
            go [Integer]
    disallow [Integer]
    model
              = do SatResult
    res <- [Integer] -> IO SatResult
    outside [Integer]
    disallow
                   -- Look up the value of "x" in the generated model
                   -- Note that we simply get an integer here; but any
                   -- SBV known type would be OK as well.
                   case String
    "x" String -> SatResult -> Maybe Integer
    forall b. SymVal b => String -> SatResult -> Maybe b
    forall a b. (Modelable a, SymVal b) => String -> a -> Maybe b
    `getModelValue` SatResult
    res of
                     Just Integer
    c -> [Integer] -> [Integer] -> IO [Integer]
    go ([Integer
    cInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    4 .. Integer
    cInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    4] [Integer] -> [Integer] -> [Integer]
    forall a. [a] -> [a] -> [a]
    ++ [Integer]
    disallow) (Integer
    c Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [Integer]
    model)
                     Maybe Integer
    _      -> [Integer] -> IO [Integer]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Integer]
    model