-----------------------------------------------------------------------------
-- |
-- 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 = forall a. Provable a => a -> IO SatResult
sat forall a b. (a -> b) -> a -> b
$ do SInteger
x <- String -> Symbolic SInteger
sInteger String
"x"
                            let notEq :: Integer -> m ()
notEq Integer
i = forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SInteger
x forall a. EqSymbolic a => a -> a -> SBool
./= forall a. SymVal a => a -> SBV a
literal Integer
i
                            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. SolverContext m => Integer -> m ()
notEq [Integer]
disallow
                            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SInteger
x 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
         | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Integer]
model forall a. Ord a => a -> a -> Bool
>= Int
10 = 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" forall a b. (Modelable a, SymVal b) => String -> a -> Maybe b
`getModelValue` SatResult
res of
                 Just Integer
c -> [Integer] -> [Integer] -> IO [Integer]
go ([Integer
cforall a. Num a => a -> a -> a
-Integer
4 .. Integer
cforall a. Num a => a -> a -> a
+Integer
4] forall a. [a] -> [a] -> [a]
++ [Integer]
disallow) (Integer
c forall a. a -> [a] -> [a]
: [Integer]
model)
                 Maybe Integer
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return [Integer]
model