--
-- | These examples can from GHCi by importing this module.
-- To get a human-readable pseudocode for the solution use
--
-- @
-- ghci> Right res <- someExample
-- ghci> putStrLn $ writePseudocode res
-- @
module Data.SBV.Program.Examples(
  -- * Reset most significant set bit
  paperRunningExampleSpec,
  paperRunningExample,
  -- * Quadratic equation
  quadEquExampleSpec,
  quadEquExample,
  -- * Transform boolean formula into NAND-only expression
  nandifyExample
) where

import Data.List

import Data.SBV
import Data.SBV.Program
import Data.SBV.Program.SimpleLibrary as Lib

-- | A running example from the original paper. The function should reset the
-- least significant set bit of a 8-byte word:
-- >>> 0001 0010 -> 0000 0010
paperRunningExampleSpec :: SimpleSpec Word8
paperRunningExampleSpec :: SimpleSpec Word8
paperRunningExampleSpec = forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
1 forall a b. (a -> b) -> a -> b
$ \[SBV Word8
i] SBV Word8
o -> [SBool] -> SBool
sAnd forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map [Int
7,Int
6..Int
0] forall a b. (a -> b) -> a -> b
$ \Int
t ->
          (forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV Word8
i Int
t SBool -> SBool -> SBool
.&& [SBool] -> SBool
sAnd (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map [Int
tforall a. Num a => a -> a -> a
-Int
1,Int
tforall a. Num a => a -> a -> a
-Int
2..Int
0] forall a b. (a -> b) -> a -> b
$ \Int
j -> SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV Word8
i Int
j))
          SBool -> SBool -> SBool
.=>
          (SBool -> SBool
sNot (forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV Word8
o Int
t) SBool -> SBool -> SBool
.&& [SBool] -> SBool
sAnd (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map (Int
t forall a. Eq a => a -> [a] -> [a]
`delete` [Int
7,Int
6..Int
0]) forall a b. (a -> b) -> a -> b
$ \Int
j -> forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV Word8
i Int
j forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV Word8
o Int
j))

paperRunningExample :: IO
  (Either SynthesisError (Program Location (SimpleComponent Word8)))
paperRunningExample = forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a]
-> spec a -> IO (Either SynthesisError (Program Location (comp a)))
refinedExAllProcedure [forall a. (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
Lib.and, forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
Lib.dec] SimpleSpec Word8
paperRunningExampleSpec

-- | Synthesizes a formula for the quadratic equation \(x^2 - 2x + 1 = 0\)
quadEquExampleSpec :: SimpleSpec Int32
quadEquExampleSpec :: SimpleSpec Int32
quadEquExampleSpec = forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
1 forall a b. (a -> b) -> a -> b
$ \[SBV Int32
i] SBV Int32
o -> [SBool] -> SBool
sAnd [
    SBV Int32
i forall a. EqSymbolic a => a -> a -> SBool
.== SBV Int32
1 SBool -> SBool -> SBool
.=> SBV Int32
o forall a. EqSymbolic a => a -> a -> SBool
.== SBV Int32
0,
    SBV Int32
i forall a. EqSymbolic a => a -> a -> SBool
.== SBV Int32
4 SBool -> SBool -> SBool
.=> SBV Int32
o forall a. EqSymbolic a => a -> a -> SBool
.== SBV Int32
9
  ]

quadEquExample :: IO
  (Either SynthesisError (Program Location (SimpleComponent Int32)))
quadEquExample = forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a]
-> spec a -> IO (Either SynthesisError (Program Location (comp a)))
refinedExAllProcedure [forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
Lib.mul, forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
Lib.add, forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
Lib.sub, forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
Lib.inc] SimpleSpec Int32
quadEquExampleSpec

-- | Reimplement arbitrary boolean formula with only NAND components.
-- Example usage:
--
-- @
-- nandifyExample 2 (SimpleSpec 2 $ \[i1, i2] o -> o .== (i1 .&& i2))
-- @
nandifyExample ::
    Int -- ^ Amount of NAND components available
  -> SimpleSpec Bool -- ^ Specification of the desired function
  -> IO (Either SynthesisError (Program Location (SimpleComponent Bool)))
nandifyExample :: Int
-> SimpleSpec Bool
-> IO
     (Either SynthesisError (Program Location (SimpleComponent Bool)))
nandifyExample Int
size = forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a]
-> spec a -> IO (Either SynthesisError (Program Location (comp a)))
refinedExAllProcedure [SimpleComponent Bool]
library
  where
    library :: [SimpleComponent Bool]
library = [forall {a}. SimpleComponent a
Lib.const, forall {a}. SimpleComponent a
Lib.const] forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate Int
size SimpleComponent Bool
Lib.bNand