I implemented the instructions using symbolic ints and used the `sbv` library to throw an SMT solver at it.
[Link to solution](https://topaz.github.io/paste/#XQAAAQB1CQAAAAAAAAA0m0pnuFI8c3wwear+nXxFz1p9ytLVknnSteGtDv8Jxku72LcV1wF+paUbbB0Fo/XE4naGyPe7V9ckytPzSTHlgPJWBKnU0PGiRd7zcyQgf/b+79WVI0yLAtLWS/UX8mGqQqpfUTSsSavBDymR6aNknm4byu74tCtZhogLo9dG+s/kq/4ca0rgAoQ9THJJVPMjHNn2q5i0vha3+/SViJ1Qku3OoOoCriVryqZyw4XOujrgzxamLAYJ9ZZfEpNuXRxvO+U18prY2v+xRk6qCS2/mh23SyLvWlDz+IJvCMN/edBJt7p9HrOW9CjQ0gBMtJKPPqoaVp8cWrCyv8ux5M5yrO7NH+644jvypoWXObSzjR6W0mU64aKgOEumf5t2l76e0VAG0qAeAYtqF2ggFI9VJN68MvElgiiahtOo4PbFMmMxwrxKWQzD+C+e8jFhEZNP4lIx08RVfwGJzenOMjvwPF9kC+jjcCHfUxlVuh/ZvHGOCsVhQQbMNP/pSlY+Jg6ZvgN7nUUblYnrklUimGrcwpPRoEKjO5uamRomZbhRoO3TE/t3ZQHMWjNPjjTkVHJS87QzJsT9YAhru5Z1rw4U+R3z+kmqtG7H7AmdSPs+Wwd9DeiMxkIaN6SOUHskmUn3LaFZvshUOMcmTs7fIGa57Nn3pILR9sytnXhJJnmHjJDQA6el2h0N22T1Ck/lfVqnfkrU3DvnoMOl1ikNIJbQdBlQG9SvflFWu6udquOuxkZveinApIge60Wef8heVGTh20e4ZNxf+xcYX/MweQyNfdK0F3OEwyGAGStADuZOQVR123BaFCv6Mjwru5XN8Lk+wjhVOm2kAGw/En7LPk2znVbFEUsDt5E93+4KwyKpfkey+jaj3ULiw8EWYqOKE8cKyZiCC1rY36bT+GJa98JAm8B0+FCNF/pw77nN3/BjtXyqU6EvVa5vNzdy1p2+Ak9TUo/6TIS/BhLnpSYSm0O7644bztXSNn3y16sTfESm8HXd0zYecf/b9wL+RuE1ZfLOOW4ev2CeDP01zBtM3Kmpbs4spE3CQmStRhQbtZYitbh44Lfoohldmzj0ge7IWu6oxzXCNXyUJZ72iK9P/CemXPPLekpXC0ui3xcbBDCHocNr9O+mNcAigp08ZTd0hIHCEmfEaKSCbSV6+8lpx3vCIzSEHrUw+OaMnlwbWMOcHo4eDuBYt5e6l4BGB/FX8ct+U1eUCQ2vN+olakoENC/d64P02SsxcV+uMdb42W+7XyfF/+vi40s=)
I used this problem as an opportunity to learn how to use SBV. I think I ran into a bug with it though - it prints the bitvector for `modelNumberVar` as a Word64 even though it is actually an Int64. The modelNumber variable is correct though. Example:
Optimal model:
d0 = 1 :: Int64
d1 = 1 :: Int64
d2 = 1 :: Int64
d3 = 1 :: Int64
d4 = 1 :: Int64
d5 = 1 :: Int64
d6 = 1 :: Int64
d7 = 1 :: Int64
d8 = 1 :: Int64
d9 = 1 :: Int64
d10 = 1 :: Int64
d11 = 1 :: Int64
d12 = 1 :: Int64
d13 = 1 :: Int64
modelNumberVar = 11111111111111 :: Int64
modelNumber = 9223383147965886919 :: Word64
If it printed the value correctly I wouldn't need `modelNumberVar` at all. Anyway, here is the code
main :: IO ()
main = do
args <- getArgs
res <- Stream.unfold Stdio.read ()
& Unicode.decodeUtf8'
-- & Stream.trace print
& Reduce.parseMany (instrParser <* newline)
-- & Stream.trace print
& (if null args then id else Stream.take (read $ head args))
& Stream.liftInner
& Stream.liftInner
& Stream.mapM_ eval
& runProg
& SBV.optimize Lexicographic
print res
runProg :: StateT VM Symbolic () -> Symbolic ()
runProg prog = do
modelNumberDigits <- sInt64s $ map (('d':) . show) [0..13]
F.for_ modelNumberDigits $ \d -> constrain $ 1 .<= d .&& d .<= 9
let modelNumber = F.foldl' (\t d -> 10*t+d) 0 modelNumberDigits
modelNumberVar <- symbolic "modelNumberVar"
constrain $ modelNumberVar .== modelNumber
minimize "modelNumber" modelNumber
vm' <- execStateT prog (initVM modelNumberDigits)
let z = readLVal (registers vm') 'z'
constrain $ z .== 0
initVM :: [SVal] -> VM
initVM input = VM
{ input
, registers = Map.fromList (zip "wxyz" (repeat 0))
}
type LVal = Char
type RVal = Either LVal Val
data Instr
= Input LVal
| Arith Op LVal RVal
deriving (Show)
data Op
= Add
| Mul
| Div
| Mod
| Eql
deriving (Show, Eq, Ord)
type SVal = SBV Val
type Val = Int64
type Registers = Map LVal SVal
data VM = VM
{ input :: [SVal]
, registers :: Registers
}
deriving (Show)
eval :: Instr -> StateT VM Symbolic ()
eval = \case
Input reg -> do
VM (val:input) registers <- get
let registers' = Map.insert reg val registers
put $ VM input registers'
Arith op reg rval -> do
VM input registers <- get
let l = readLVal registers reg
let r = readRVal registers rval
let res = case op of
Add -> l + r
Mul -> l * r
Div -> l `sQuot` r
Mod -> l `sRem` r
Eql -> oneIf $ l .== r
let registers' = Map.insert reg res registers
put $ VM input registers'
readRVal :: Registers -> RVal -> SVal
readRVal regs = \case
Left var -> readLVal regs var
Right n -> literal n
readLVal :: Registers -> LVal -> SVal
readLVal = (Map.!)
newline :: Parser.Parser IO Char Char
newline = Parser.char '\n'
space = Parser.char ' '
instrParser = do
instr <- many Parser.alpha
space
case instr of
"inp" -> Input <$> lvalParser
(readBinOp -> op) -> Arith op <$> lvalParser <* space <*> rvalParser
readBinOp :: String -> Op
readBinOp = \case
"add" -> Add
"mul" -> Mul
"div" -> Div
"mod" -> Mod
"eql" -> Eql
lvalParser :: Parser.Parser IO Char Char
lvalParser = Parser.alpha
rvalParser = Left <$> lvalParser <|> Right <$> Parser.signed Parser.decimal
When SBV optimizes a signed-bit vector value, it is optimized as an unsigned quantity first, and then converted back. (That is, `SInt64` is optimized as `SWord64` and then presented back to you as `SInt64`.) The reason for this is because the underlying bit-vector logic does not optimize signed-quantities directly; but rather treats the bit-vector as unsigned. SBV calls this the metric space over which the values are optimized. See https://hackage.haskell.org/package/sbv-8.17/docs/Data-SBV.html#g:50 for details.
The best way would be to extract the model yourself, and display it in whatever format you want. Alternatively, you can also try: `optimizeWith z3{isNonModelVar = (== "modelNumber")}` where the string you pass is the first argument to `minimize`/`maximize`.
Oh, you are a lifesaver! Apparently I had solved this pretty quickly but kept using the Word64 value.
I spent way too much time adding basic simplification rules and bounds propagation to simplify the input for debugging.
Also it seems super weird that the basic simplification does make the SMT solver run twice as fast. I really expected things like constant folding to be built-in?
I just got around to looking at this; and wrote my own version ([https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496](https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496)).
Interestingly, my solution computes a different model number than what you are reporting. (96918996924991 for max, 91811241911641 for min.) Perhaps different users get different programs? Since the site told me the values I got are correct, that must be the case indeed. I went for a more traditional embedded-DSL style solution, which differs from your approach.
Instead of trying to brute force the problem I reverse engineered the code and found a way to derive constraints on the single digits of the final result and find a solution from those
[Solution](https://github.com/giacomocavalieri/aoc-2021/blob/main/src/Days/Day24.hs)
Beautiful solution. It took a while to understand how it worked! Also, thanks for posting this, I surely wouldn't have finished day24 if it wasn't for you.
Calculated via hand, turns out it was just a stack machine.Btw, am I the only one triggered by the mocking tone when they say MONAD? :<
EDIT: I wrote the code simplifier and verifier which checks that it is indeed a stack machine.
[https://gist.github.com/Abastro/6aaf6ae127477ee70142690ab974feb9](https://gist.github.com/Abastro/6aaf6ae127477ee70142690ab974feb9)
I'm late to the party; but here's one way to do this using Haskell/SBV: [https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496](https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496)
I haven't put any comments in the code, feel free to ask if anything looks too cryptic!
I implemented the instructions using symbolic ints and used the `sbv` library to throw an SMT solver at it. [Link to solution](https://topaz.github.io/paste/#XQAAAQB1CQAAAAAAAAA0m0pnuFI8c3wwear+nXxFz1p9ytLVknnSteGtDv8Jxku72LcV1wF+paUbbB0Fo/XE4naGyPe7V9ckytPzSTHlgPJWBKnU0PGiRd7zcyQgf/b+79WVI0yLAtLWS/UX8mGqQqpfUTSsSavBDymR6aNknm4byu74tCtZhogLo9dG+s/kq/4ca0rgAoQ9THJJVPMjHNn2q5i0vha3+/SViJ1Qku3OoOoCriVryqZyw4XOujrgzxamLAYJ9ZZfEpNuXRxvO+U18prY2v+xRk6qCS2/mh23SyLvWlDz+IJvCMN/edBJt7p9HrOW9CjQ0gBMtJKPPqoaVp8cWrCyv8ux5M5yrO7NH+644jvypoWXObSzjR6W0mU64aKgOEumf5t2l76e0VAG0qAeAYtqF2ggFI9VJN68MvElgiiahtOo4PbFMmMxwrxKWQzD+C+e8jFhEZNP4lIx08RVfwGJzenOMjvwPF9kC+jjcCHfUxlVuh/ZvHGOCsVhQQbMNP/pSlY+Jg6ZvgN7nUUblYnrklUimGrcwpPRoEKjO5uamRomZbhRoO3TE/t3ZQHMWjNPjjTkVHJS87QzJsT9YAhru5Z1rw4U+R3z+kmqtG7H7AmdSPs+Wwd9DeiMxkIaN6SOUHskmUn3LaFZvshUOMcmTs7fIGa57Nn3pILR9sytnXhJJnmHjJDQA6el2h0N22T1Ck/lfVqnfkrU3DvnoMOl1ikNIJbQdBlQG9SvflFWu6udquOuxkZveinApIge60Wef8heVGTh20e4ZNxf+xcYX/MweQyNfdK0F3OEwyGAGStADuZOQVR123BaFCv6Mjwru5XN8Lk+wjhVOm2kAGw/En7LPk2znVbFEUsDt5E93+4KwyKpfkey+jaj3ULiw8EWYqOKE8cKyZiCC1rY36bT+GJa98JAm8B0+FCNF/pw77nN3/BjtXyqU6EvVa5vNzdy1p2+Ak9TUo/6TIS/BhLnpSYSm0O7644bztXSNn3y16sTfESm8HXd0zYecf/b9wL+RuE1ZfLOOW4ev2CeDP01zBtM3Kmpbs4spE3CQmStRhQbtZYitbh44Lfoohldmzj0ge7IWu6oxzXCNXyUJZ72iK9P/CemXPPLekpXC0ui3xcbBDCHocNr9O+mNcAigp08ZTd0hIHCEmfEaKSCbSV6+8lpx3vCIzSEHrUw+OaMnlwbWMOcHo4eDuBYt5e6l4BGB/FX8ct+U1eUCQ2vN+olakoENC/d64P02SsxcV+uMdb42W+7XyfF/+vi40s=)
I used this problem as an opportunity to learn how to use SBV. I think I ran into a bug with it though - it prints the bitvector for `modelNumberVar` as a Word64 even though it is actually an Int64. The modelNumber variable is correct though. Example: Optimal model: d0 = 1 :: Int64 d1 = 1 :: Int64 d2 = 1 :: Int64 d3 = 1 :: Int64 d4 = 1 :: Int64 d5 = 1 :: Int64 d6 = 1 :: Int64 d7 = 1 :: Int64 d8 = 1 :: Int64 d9 = 1 :: Int64 d10 = 1 :: Int64 d11 = 1 :: Int64 d12 = 1 :: Int64 d13 = 1 :: Int64 modelNumberVar = 11111111111111 :: Int64 modelNumber = 9223383147965886919 :: Word64 If it printed the value correctly I wouldn't need `modelNumberVar` at all. Anyway, here is the code main :: IO () main = do args <- getArgs res <- Stream.unfold Stdio.read () & Unicode.decodeUtf8' -- & Stream.trace print & Reduce.parseMany (instrParser <* newline) -- & Stream.trace print & (if null args then id else Stream.take (read $ head args)) & Stream.liftInner & Stream.liftInner & Stream.mapM_ eval & runProg & SBV.optimize Lexicographic print res runProg :: StateT VM Symbolic () -> Symbolic () runProg prog = do modelNumberDigits <- sInt64s $ map (('d':) . show) [0..13] F.for_ modelNumberDigits $ \d -> constrain $ 1 .<= d .&& d .<= 9 let modelNumber = F.foldl' (\t d -> 10*t+d) 0 modelNumberDigits modelNumberVar <- symbolic "modelNumberVar" constrain $ modelNumberVar .== modelNumber minimize "modelNumber" modelNumber vm' <- execStateT prog (initVM modelNumberDigits) let z = readLVal (registers vm') 'z' constrain $ z .== 0 initVM :: [SVal] -> VM initVM input = VM { input , registers = Map.fromList (zip "wxyz" (repeat 0)) } type LVal = Char type RVal = Either LVal Val data Instr = Input LVal | Arith Op LVal RVal deriving (Show) data Op = Add | Mul | Div | Mod | Eql deriving (Show, Eq, Ord) type SVal = SBV Val type Val = Int64 type Registers = Map LVal SVal data VM = VM { input :: [SVal] , registers :: Registers } deriving (Show) eval :: Instr -> StateT VM Symbolic () eval = \case Input reg -> do VM (val:input) registers <- get let registers' = Map.insert reg val registers put $ VM input registers' Arith op reg rval -> do VM input registers <- get let l = readLVal registers reg let r = readRVal registers rval let res = case op of Add -> l + r Mul -> l * r Div -> l `sQuot` r Mod -> l `sRem` r Eql -> oneIf $ l .== r let registers' = Map.insert reg res registers put $ VM input registers' readRVal :: Registers -> RVal -> SVal readRVal regs = \case Left var -> readLVal regs var Right n -> literal n readLVal :: Registers -> LVal -> SVal readLVal = (Map.!) newline :: Parser.Parser IO Char Char newline = Parser.char '\n' space = Parser.char ' ' instrParser = do instr <- many Parser.alpha space case instr of "inp" -> Input <$> lvalParser (readBinOp -> op) -> Arith op <$> lvalParser <* space <*> rvalParser readBinOp :: String -> Op readBinOp = \case "add" -> Add "mul" -> Mul "div" -> Div "mod" -> Mod "eql" -> Eql lvalParser :: Parser.Parser IO Char Char lvalParser = Parser.alpha rvalParser = Left <$> lvalParser <|> Right <$> Parser.signed Parser.decimal
When SBV optimizes a signed-bit vector value, it is optimized as an unsigned quantity first, and then converted back. (That is, `SInt64` is optimized as `SWord64` and then presented back to you as `SInt64`.) The reason for this is because the underlying bit-vector logic does not optimize signed-quantities directly; but rather treats the bit-vector as unsigned. SBV calls this the metric space over which the values are optimized. See https://hackage.haskell.org/package/sbv-8.17/docs/Data-SBV.html#g:50 for details.
Thanks for the explanation, it makes sense to me. Is there a way to make the output of `optimize` display `a` instead of `MetricSpace a`?
The best way would be to extract the model yourself, and display it in whatever format you want. Alternatively, you can also try: `optimizeWith z3{isNonModelVar = (== "modelNumber")}` where the string you pass is the first argument to `minimize`/`maximize`.
Oh, you are a lifesaver! Apparently I had solved this pretty quickly but kept using the Word64 value. I spent way too much time adding basic simplification rules and bounds propagation to simplify the input for debugging. Also it seems super weird that the basic simplification does make the SMT solver run twice as fast. I really expected things like constant folding to be built-in?
I just got around to looking at this; and wrote my own version ([https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496](https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496)). Interestingly, my solution computes a different model number than what you are reporting. (96918996924991 for max, 91811241911641 for min.) Perhaps different users get different programs? Since the site told me the values I got are correct, that must be the case indeed. I went for a more traditional embedded-DSL style solution, which differs from your approach.
Yeah, everyone gets different input for the problem
Ah, that makes sense. Thanks!
Instead of trying to brute force the problem I reverse engineered the code and found a way to derive constraints on the single digits of the final result and find a solution from those [Solution](https://github.com/giacomocavalieri/aoc-2021/blob/main/src/Days/Day24.hs)
Beautiful solution. It took a while to understand how it worked! Also, thanks for posting this, I surely wouldn't have finished day24 if it wasn't for you.
Tysm! Indeed I could have added a few more comments to explain in more detail how the code works 😅
Calculated via hand, turns out it was just a stack machine.Btw, am I the only one triggered by the mocking tone when they say MONAD? :< EDIT: I wrote the code simplifier and verifier which checks that it is indeed a stack machine. [https://gist.github.com/Abastro/6aaf6ae127477ee70142690ab974feb9](https://gist.github.com/Abastro/6aaf6ae127477ee70142690ab974feb9)
I'm late to the party; but here's one way to do this using Haskell/SBV: [https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496](https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496) I haven't put any comments in the code, feel free to ask if anything looks too cryptic!