    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.AOC_2021_24
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A solution to the advent-of-code problem, 2021, day 24: <http://adventofcode.com/2021/day/24>.
    --
    -- Here is a high-level summary: We are essentially modeling the ALU of a fictional
    -- computer with 4 integer registers (w, x, y, z), and 6 instructions (inp, add, mul, div, mod, eql).
    -- You are given a program (hilariously called "monad"), and your goal is to figure out what
    -- the maximum and minimum inputs you can provide to this program such that when it runs
    -- register z ends up with the value 1. Please refer to the above link for the full description.
    --
    -- While there are multiple ways to solve this problem in SBV, the solution here demonstrates
    -- how to turn programs in this fictional language into actual Haskell/SBV programs, i.e.,
    -- developing a little EDSL (embedded domain-specific language) for it. Hopefully this
    -- should provide a template for other similar programs.
    -----------------------------------------------------------------------------

    {-# LANGUAGE NamedFieldPuns   #-}
    {-# LANGUAGE NegativeLiterals #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.AOC_2021_24 where

    import Prelude hiding (read, mod, div)

    import Control.Monad (forM_)
    import Data.Maybe

    import qualified Data.Map.Strict          as M
    import qualified Control.Monad.State.Lazy as ST

    import Data.SBV

    -----------------------------------------------------------------------------------------------
    -- * Registers, values, and the ALU
    -----------------------------------------------------------------------------------------------

    -- | A Register in the machine, identified by its name.
    type Register = String

    -- | We operate on 64-bit signed integers. It is also possible to use the unbounded integers here
    -- as the problem description doesn't mention any size limitations. But performance isn't as good
    -- with unbounded integers, and 64-bit signed bit-vectors seem to fit the bill just fine, much
    -- like any other modern processor these days.
    type Value = SInt64

    -- | An item of data to be processed. We can either be referring to a named register, or an immediate value.
    data Data = Reg {Data -> Register
    register :: Register}
              | Imm Int64

    -- | 'Num' instance for 'Data'. This is merely there for us to be able to represent programs in a
    -- natural way, i.e, lifting integers (positive and negative). Other methods are neither implemented
    -- nor needed.
    instance Num Data where
      fromInteger :: Integer -> Data
    fromInteger    = Int64 -> Data
    Imm (Int64 -> Data) -> (Integer -> Int64) -> Integer -> Data
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int64
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      + :: Data -> Data -> Data
    (+)            = Register -> Data -> Data -> Data
    forall a. HasCallStack => Register -> a
    error Register
    "+     : unimplemented"
      * :: Data -> Data -> Data
    (*)            = Register -> Data -> Data -> Data
    forall a. HasCallStack => Register -> a
    error Register
    "*     : unimplemented"
      negate :: Data -> Data
    negate (Imm Int64
    i) = Int64 -> Data
    Imm (-Int64
    i)
      negate Reg{}   = Register -> Data
    forall a. HasCallStack => Register -> a
    error Register
    "negate: unimplemented"
      abs :: Data -> Data
    abs            = Register -> Data -> Data
    forall a. HasCallStack => Register -> a
    error Register
    "abs   : unimplemented"
      signum :: Data -> Data
    signum         = Register -> Data -> Data
    forall a. HasCallStack => Register -> a
    error Register
    "signum: unimplemented"

    -- | Shorthand for the @w@ register.
    w :: Data
    w :: Data
    w = Register -> Data
    Reg Register
    "w"

    -- | Shorthand for the @x@ register.
    x :: Data
    x :: Data
    x = Register -> Data
    Reg Register
    "x"

    -- | Shorthand for the @y@ register.
    y :: Data
    y :: Data
    y = Register -> Data
    Reg Register
    "y"

    -- | Shorthand for the @z@ register.
    z :: Data
    z :: Data
    z = Register -> Data
    Reg Register
    "z"

    -- | The state of the machine. We keep track of the data values, along with the input parameters.
    data State = State { State -> Map Register Value
    env    :: M.Map Register Value  -- ^ Values of registers
                       , State -> [Value]
    inputs :: [Value]               -- ^ Input parameters, stored in reverse.
                       }

    -- | The ALU is simply a state transformer, manipulating the state, wrapped around SBV's 'Symbolic' monad.
    type ALU = ST.StateT State Symbolic

    -----------------------------------------------------------------------------------------------
    -- * Operations
    -----------------------------------------------------------------------------------------------

    -- | Reading a value. For a register, we simply look it up in the environment.
    -- For an immediate, we simply return it.
    read :: Data -> ALU Value
    read :: Data -> ALU Value
    read (Reg Register
    r) = StateT State Symbolic State
    forall s (m :: * -> *). MonadState s m => m s
    ST.get StateT State Symbolic State -> (State -> ALU Value) -> ALU Value
    forall a b.
    StateT State Symbolic a
    -> (a -> StateT State Symbolic b) -> StateT State Symbolic b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \State
    st -> Value -> ALU Value
    forall a. a -> StateT State Symbolic a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> ALU Value) -> Value -> ALU Value
    forall a b. (a -> b) -> a -> b
    $ Maybe Value -> Value
    forall a. HasCallStack => Maybe a -> a
    fromJust (Register
    r Register -> Map Register Value -> Maybe Value
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` State -> Map Register Value
    env State
    st)
    read (Imm Int64
    i) = Value -> ALU Value
    forall a. a -> StateT State Symbolic a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> ALU Value) -> Value -> ALU Value
    forall a b. (a -> b) -> a -> b
    $ Int64 -> Value
    forall a. SymVal a => a -> SBV a
    literal Int64
    i

    -- | Writing a value. We update the registers.
    write :: Data -> Value -> ALU ()
    write :: Data -> Value -> ALU ()
    write Data
    d Value
    v = (State -> State) -> ALU ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    ST.modify' ((State -> State) -> ALU ()) -> (State -> State) -> ALU ()
    forall a b. (a -> b) -> a -> b
    $ \State
    st -> State
    st{env :: Map Register Value
    env = Register -> Value -> Map Register Value -> Map Register Value
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (Data -> Register
    register Data
    d) Value
    v (State -> Map Register Value
    env State
    st)}

    -- | Reading an input value. In this version, we simply write a free symbolic value
    -- to the specified register, and keep track of the inputs explicitly.
    inp :: Data -> ALU ()
    inp :: Data -> ALU ()
    inp Data
    a = do Value
    v <- Symbolic Value -> ALU Value
    forall (m :: * -> *) a. Monad m => m a -> StateT State m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    ST.lift Symbolic Value
    forall a. SymVal a => Symbolic (SBV a)
    free_
               Data -> Value -> ALU ()
    write Data
    a Value
    v
               (State -> State) -> ALU ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    ST.modify' ((State -> State) -> ALU ()) -> (State -> State) -> ALU ()
    forall a b. (a -> b) -> a -> b
    $ \State
    st -> State
    st{inputs :: [Value]
    inputs = Value
    v Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : State -> [Value]
    inputs State
    st}

    -- | Addition.
    add :: Data -> Data -> ALU ()
    add :: Data -> Data -> ALU ()
    add Data
    a Data
    b = Data -> Value -> ALU ()
    write Data
    a (Value -> ALU ()) -> ALU Value -> ALU ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Value -> Value -> Value
    forall a. Num a => a -> a -> a
    (+) (Value -> Value -> Value)
    -> ALU Value -> StateT State Symbolic (Value -> Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Data -> ALU Value
    read Data
    a StateT State Symbolic (Value -> Value) -> ALU Value -> ALU Value
    forall a b.
    StateT State Symbolic (a -> b)
    -> StateT State Symbolic a -> StateT State Symbolic b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Data -> ALU Value
    read Data
    b

    -- | Multiplication.
    mul :: Data -> Data -> ALU ()
    mul :: Data -> Data -> ALU ()
    mul Data
    a Data
    b = Data -> Value -> ALU ()
    write Data
    a (Value -> ALU ()) -> ALU Value -> ALU ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Value -> Value -> Value
    forall a. Num a => a -> a -> a
    (*) (Value -> Value -> Value)
    -> ALU Value -> StateT State Symbolic (Value -> Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Data -> ALU Value
    read Data
    a StateT State Symbolic (Value -> Value) -> ALU Value -> ALU Value
    forall a b.
    StateT State Symbolic (a -> b)
    -> StateT State Symbolic a -> StateT State Symbolic b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Data -> ALU Value
    read Data
    b

    -- | Division.
    div :: Data -> Data -> ALU ()
    div :: Data -> Data -> ALU ()
    div Data
    a Data
    b = Data -> Value -> ALU ()
    write Data
    a (Value -> ALU ()) -> ALU Value -> ALU ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Value -> Value -> Value
    forall a. SDivisible a => a -> a -> a
    sDiv (Value -> Value -> Value)
    -> ALU Value -> StateT State Symbolic (Value -> Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Data -> ALU Value
    read Data
    a StateT State Symbolic (Value -> Value) -> ALU Value -> ALU Value
    forall a b.
    StateT State Symbolic (a -> b)
    -> StateT State Symbolic a -> StateT State Symbolic b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Data -> ALU Value
    read Data
    b

    -- | Modulus.
    mod :: Data -> Data -> ALU ()
    mod :: Data -> Data -> ALU ()
    mod Data
    a Data
    b = Data -> Value -> ALU ()
    write Data
    a (Value -> ALU ()) -> ALU Value -> ALU ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Value -> Value -> Value
    forall a. SDivisible a => a -> a -> a
    sMod (Value -> Value -> Value)
    -> ALU Value -> StateT State Symbolic (Value -> Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Data -> ALU Value
    read Data
    a StateT State Symbolic (Value -> Value) -> ALU Value -> ALU Value
    forall a b.
    StateT State Symbolic (a -> b)
    -> StateT State Symbolic a -> StateT State Symbolic b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Data -> ALU Value
    read Data
    b

    -- | Equality.
    eql :: Data -> Data -> ALU ()
    eql :: Data -> Data -> ALU ()
    eql Data
    a Data
    b = Data -> Value -> ALU ()
    write Data
    a (Value -> ALU ()) -> (SBool -> Value) -> SBool -> ALU ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBool -> Value
    forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
    oneIf (SBool -> ALU ()) -> StateT State Symbolic SBool -> ALU ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Value -> Value -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    (.==) (Value -> Value -> SBool)
    -> ALU Value -> StateT State Symbolic (Value -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Data -> ALU Value
    read Data
    a StateT State Symbolic (Value -> SBool)
    -> ALU Value -> StateT State Symbolic SBool
    forall a b.
    StateT State Symbolic (a -> b)
    -> StateT State Symbolic a -> StateT State Symbolic b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Data -> ALU Value
    read Data
    b

    -----------------------------------------------------------------------------------------------
    -- * Running a program
    -----------------------------------------------------------------------------------------------

    -- | Run a given program, returning the final state. We simply start with the initial
    -- environment mapping all registers to zero, as specified in the problem specification.
    run :: ALU () -> Symbolic State
    run :: ALU () -> Symbolic State
    run ALU ()
    pgm = ALU () -> State -> Symbolic State
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    ST.execStateT ALU ()
    pgm State
    initState
     where initState :: State
    initState = State { env :: Map Register Value
    env    = [(Register, Value)] -> Map Register Value
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(Data -> Register
    register Data
    r, Value
    0) | Data
    r <- [Data
    w, Data
    x, Data
    y, Data
    z]]
                             , inputs :: [Value]
    inputs = []
                             }

    -----------------------------------------------------------------------------------------------
    -- * Solving the puzzle
    --
    -----------------------------------------------------------------------------------------------

    -- | We simply run the 'monad' program, and specify the constraints at the end. We take a boolean
    -- as a parameter, choosing whether we want to minimize or maximize the model-number. Note that this
    -- test takes rather long to run. We get:
    --
    -- @
    -- ghci> puzzle True
    -- Optimal model:
    --   Maximum model number = 96918996924991 :: Int64
    -- ghci> puzzle False
    -- Optimal model:
    --   Minimum model number = 91811241911641 :: Int64
    -- @
    puzzle :: Bool -> IO ()
    puzzle :: Bool -> IO ()
    puzzle Bool
    shouldMaximize = OptimizeResult -> IO ()
    forall a. Show a => a -> IO ()
    print (OptimizeResult -> IO ()) -> IO OptimizeResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SMTConfig -> OptimizeStyle -> SymbolicT IO () -> IO OptimizeResult
    forall a.
    Satisfiable a =>
    SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
    optimizeWith SMTConfig
    z3{isNonModelVar :: Register -> Bool
    isNonModelVar = (Register -> Register -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Register
    finalVar)}  OptimizeStyle
    Lexicographic SymbolicT IO ()
    problem
      where finalVar :: Register
    finalVar | Bool
    shouldMaximize = Register
    "Maximum model number"
                     | Bool
    True           = Register
    "Minimum model number"
            problem :: SymbolicT IO ()
    problem = do State{Map Register Value
    env :: State -> Map Register Value
    env :: Map Register Value
    env, [Value]
    inputs :: State -> [Value]
    inputs :: [Value]
    inputs} <- ALU () -> Symbolic State
    run ALU ()
    monad

                         -- The final z value should be 0
                         SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Maybe Value -> Value
    forall a. HasCallStack => Maybe a -> a
    fromJust (Data -> Register
    register Data
    z Register -> Map Register Value -> Maybe Value
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` Map Register Value
    env) Value -> Value -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Value
    0

                         -- Digits of the model number, stored in reverse
                         let digits :: [Value]
    digits = [Value] -> [Value]
    forall a. [a] -> [a]
    reverse [Value]
    inputs

                         -- Each digit is between 1-9
                         [Value] -> (Value -> SymbolicT IO ()) -> SymbolicT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Value]
    digits ((Value -> SymbolicT IO ()) -> SymbolicT IO ())
    -> (Value -> SymbolicT IO ()) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \Value
    d -> SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Value
    d Value -> (Value, Value) -> SBool
    forall a. OrdSymbolic a => a -> (a, a) -> SBool
    `inRange` (Value
    1, Value
    9)

                         -- Digits spell out the model number. We minimize/maximize this value as requested:
                         let modelNum :: Value
    modelNum = (Value -> Value -> Value) -> Value -> [Value] -> Value
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\Value
    sofar Value
    d -> Value
    10 Value -> Value -> Value
    forall a. Num a => a -> a -> a
    * Value
    sofar Value -> Value -> Value
    forall a. Num a => a -> a -> a
    + Value
    d) Value
    0 [Value]
    digits

                         -- maximize/minimize the digits as requested
                         if Bool
    shouldMaximize
                            then Register -> Value -> SymbolicT IO ()
    forall a. Metric a => Register -> SBV a -> SymbolicT IO ()
    maximize Register
    "goal" Value
    modelNum
                            else Register -> Value -> SymbolicT IO ()
    forall a. Metric a => Register -> SBV a -> SymbolicT IO ()
    minimize Register
    "goal" Value
    modelNum

                         -- For display purposes, create a variable to assign to modelNum
                         Value
    modelNumV <- Register -> Symbolic Value
    forall a. SymVal a => Register -> Symbolic (SBV a)
    free Register
    finalVar
                         SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Value
    modelNumV Value -> Value -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Value
    modelNum

    -- | The program we need to crack. Note that different users get different programs on the Advent-Of-Code site, so this is simply one example.
    -- You can simply cut-and-paste your version instead. (Don't forget the pragma @NegativeLiterals@ to GHC so @add x -1@ parses correctly as @add x (-1)@.)
    monad :: ALU ()
    monad :: ALU ()
    monad = do Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    11
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    5
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    13
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    5
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    12
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    15
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    15
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    10
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    2
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -1
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    2
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    14
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    5
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -8
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    8
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -7
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    14
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -8
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    12
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    1
               Data -> Data -> ALU ()
    add Data
    x Data
    11
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    7
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -2
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    14
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -2
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    13
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y
               Data -> ALU ()
    inp Data
    w
               Data -> Data -> ALU ()
    mul Data
    x Data
    0
               Data -> Data -> ALU ()
    add Data
    x Data
    z
               Data -> Data -> ALU ()
    mod Data
    x Data
    26
               Data -> Data -> ALU ()
    div Data
    z Data
    26
               Data -> Data -> ALU ()
    add Data
    x Data
    -13
               Data -> Data -> ALU ()
    eql Data
    x Data
    w
               Data -> Data -> ALU ()
    eql Data
    x Data
    0
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    25
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    y Data
    1
               Data -> Data -> ALU ()
    mul Data
    z Data
    y
               Data -> Data -> ALU ()
    mul Data
    y Data
    0
               Data -> Data -> ALU ()
    add Data
    y Data
    w
               Data -> Data -> ALU ()
    add Data
    y Data
    6
               Data -> Data -> ALU ()
    mul Data
    y Data
    x
               Data -> Data -> ALU ()
    add Data
    z Data
    y

    {- HLint ignore module "Reduce duplication" -}