sbv-14.4: Documentation/SBV/Examples/Puzzles/AOC_2021_24.hs
-----------------------------------------------------------------------------
-- |
-- 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 0. 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 {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 = Imm . fromIntegral
(+) = error "+ : unimplemented"
(*) = error "* : unimplemented"
negate (Imm i) = Imm (-i)
negate Reg{} = error "negate: unimplemented"
abs = error "abs : unimplemented"
signum = error "signum: unimplemented"
-- | Shorthand for the @w@ register.
w :: Data
w = Reg "w"
-- | Shorthand for the @x@ register.
x :: Data
x = Reg "x"
-- | Shorthand for the @y@ register.
y :: Data
y = Reg "y"
-- | Shorthand for the @z@ register.
z :: Data
z = Reg "z"
-- | The state of the machine. We keep track of the data values, along with the input parameters.
data State = State { env :: M.Map Register Value -- ^ Values of registers
, 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 (Reg r) = ST.get >>= \st -> pure $ fromJust (r `M.lookup` env st)
read (Imm i) = pure $ literal i
-- | Writing a value. We update the registers.
write :: Data -> Value -> ALU ()
write d v = ST.modify' $ \st -> 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 a = do v <- ST.lift free_
write a v
ST.modify' $ \st -> st{inputs = v : inputs st}
-- | Addition.
add :: Data -> Data -> ALU ()
add a b = write a =<< (+) <$> read a <*> read b
-- | Multiplication.
mul :: Data -> Data -> ALU ()
mul a b = write a =<< (*) <$> read a <*> read b
-- | Division.
div :: Data -> Data -> ALU ()
div a b = write a =<< sDiv <$> read a <*> read b
-- | Modulus.
mod :: Data -> Data -> ALU ()
mod a b = write a =<< sMod <$> read a <*> read b
-- | Equality.
eql :: Data -> Data -> ALU ()
eql a b = write a . oneIf =<< (.==) <$> read a <*> read 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 pgm = ST.execStateT pgm initState
where initState = State { env = M.fromList [(register r, 0) | r <- [w, x, y, z]]
, 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 shouldMaximize = print =<< optimizeWith z3{isNonModelVar = (/= finalVar)} Lexicographic problem
where finalVar | shouldMaximize = "Maximum model number"
| True = "Minimum model number"
problem = do State{env, inputs} <- run 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 = reverse inputs
-- Each digit is between 1-9
forM_ digits $ \d -> constrain $ d `inRange` (1, 9)
-- Digits spell out the model number. We minimize/maximize this value as requested:
let modelNum = foldl (\sofar d -> 10 * sofar + d) 0 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 = do inp w
mul x 0
add x z
mod x 26
div z 1
add x 11
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 5
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 1
add x 13
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 5
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 1
add x 12
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 1
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 1
add x 15
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 15
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 1
add x 10
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 2
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -1
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 2
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 1
add x 14
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 5
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -8
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 8
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -7
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 14
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -8
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 12
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 1
add x 11
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 7
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -2
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 14
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -2
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 13
mul y x
add z y
inp w
mul x 0
add x z
mod x 26
div z 26
add x -13
eql x w
eql x 0
mul y 0
add y 25
mul y x
add y 1
mul z y
mul y 0
add y w
add y 6
mul y x
add z y
{- HLint ignore module "Reduce duplication" -}