Skip to content

Instantly share code, notes, and snippets.

@LeventErkok

LeventErkok/ALU.hs

Last active January 27, 2022 09:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LeventErkok/d8d6855a92783df115abd52d702d9496 to your computer and use it in GitHub Desktop.
Save LeventErkok/d8d6855a92783df115abd52d702d9496 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ALU.hs
{-# OPTIONS_GHC -Wall -Werror #-}
-- | Solve the Advent-of-code, 2021, day 24: https://adventofcode.com/2021/day/24
--
-- Load it to ghci as:
-- ghci -package mtl ALU.hs
--
-- Boolean specifies if we maximize (True) or minimize (False)
--
-- >>> puzzle True
-- 96918996924991
-- >>> puzzle False
-- 91811241911641
module ALU where
import Control.Monad.State.Lazy
import Data.Maybe
import Data.List
import Data.SBV
import Data.SBV.Internals (cvVal, CVal(CInteger))
import qualified Data.Map.Strict as M
import Prelude hiding (read, mod, div)
type Register = String
type Value = SInt64
data Data = Reg Register | Imm Integer
type Env = M.Map Register Value
type ALU = StateT Env Symbolic
w, x, y, z, c :: Data
w = Reg "w"
x = Reg "x"
y = Reg "y"
z = Reg "z"
c = Reg "c"
read :: Data -> ALU Value
read (Reg r) = get >>= \env -> pure $ fromJust (r `M.lookup` env)
read (Imm i) = pure $ literal (fromIntegral i)
write :: Data -> Value -> ALU ()
write (Reg r) v = modify' $ M.insert r v
write Imm{} _ = error "Writing to an immediate!"
input :: Bool -> Data -> ALU ()
input shouldMaximize a = do
cnt <- read c
let sh2 i | i < 10 = '0' : show i
| True = show i
v <- lift $ free $ "d" ++ sh2 (fromJust (unliteral cnt))
write c (1+cnt)
lift $ constrain $ inRange v (1, 9)
lift $ (if shouldMaximize then maximize else minimize) "goal" v
write a v
instance Num Data where
fromInteger = Imm
(+) = error "+ : unimplemented"
(*) = error "* : unimplemented"
negate (Imm i) = Imm (-i)
negate Reg{} = error "negate: unimplemented"
abs = error "abs : unimplemented"
signum = error "signum: unimplemented"
add, mul, div, mod, eql :: Data -> Data -> ALU ()
add a b = write a =<< (+) <$> read a <*> read b
mul a b = write a =<< (*) <$> read a <*> read b
div a b = write a =<< sDiv <$> read a <*> read b
mod a b = write a =<< sMod <$> read a <*> read b
eql a b = write a . oneIf =<< (.==) <$> read a <*> read b
run :: ALU () -> Symbolic Value
run pgm = evalStateT (pgm >> read z) (M.fromList [(r, 0) | Reg r <- [w, x, y, z, c]])
puzzle :: Bool -> IO ()
puzzle shouldMaximize = do
LexicographicResult r <- optimizeWith z3{isNonModelVar = ("goal" `isPrefixOf`)}
Lexicographic $ do zVal <- run (monad shouldMaximize)
constrain $ zVal .== 0
let sh (CInteger i) = show i
sh _ = error "unexpected output"
putStrLn $ concatMap (sh . cvVal . snd) $ sort $ M.toList (getModelDictionary r)
monad :: Bool -> ALU ()
monad shouldMaximize = do
let inp = input shouldMaximize
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment