module Data.SBV.Program.Examples(
  -- * Reset most significant set bit
  paperRunningExampleSpec,
  paperRunningExample,
  -- * Quadratic equation
  quadEquExampleSpec,
  quadEquExample
) 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 - 2*x + 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