-----------------------------------------------------------------------------
-- |
-- 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 CPP              #-}
{-# LANGUAGE NamedFieldPuns   #-}
{-# LANGUAGE NegativeLiterals #-}

#if __GLASGOW_HASKELL__ >= 913
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-record-selectors #-}
#else
{-# OPTIONS_GHC -Wall -Werror #-}
#endif

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 = M.insert (register d) v (env 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 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_
           write a v
           ST.modify' $ \State
st -> State
st{inputs = v : inputs 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 (SBV 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 = (/= 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{env, inputs} <- ALU () -> Symbolic State
run ALU ()
monad

                     -- The final z value should be 0
                     constrain $ fromJust (register z `M.lookup` env) .== 0

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

                     -- Each digit is between 1-9
                     forM_ digits $ \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 -> 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 shouldMaximize
                        then maximize "goal" modelNum
                        else minimize "goal" modelNum

                     -- For display purposes, create a variable to assign to modelNum
                     modelNumV <- free finalVar
                     constrain $ modelNumV .== 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" -}