-----------------------------------------------------------------------------
-- |
-- 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 x <- String -> Symbolic SInteger
sInteger String
"x"
                            let 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
                            mapM_ notEq disallow
                            return $ x .>= 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 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 "x" `getModelValue` 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