From 1e9e4ac17898de9a8772445de5fb78fddce93d1a Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Tue, 17 Dec 2024 14:15:20 -0800
Subject: [PATCH] examples

---
 solutions/src/2024/17.hs | 40 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 38 insertions(+), 2 deletions(-)

diff --git a/solutions/src/2024/17.hs b/solutions/src/2024/17.hs
index 6998ede..ab43f18 100644
--- a/solutions/src/2024/17.hs
+++ b/solutions/src/2024/17.hs
@@ -8,11 +8,33 @@ Maintainer  : emertens@gmail.com
 
 <https://adventofcode.com/2024/day/17>
 
+>>> :{
+:main + "Register A: 729
+Register B: 0
+Register C: 0
+\&
+Program: 0,1,5,4,3,0
+"
+:}
+4,6,3,5,6,3,5,2,1,0
+no part 2
+
+>>> :{
+:main + "Register A: 2024
+Register B: 0
+Register C: 0
+\&
+Program: 0,3,5,4,3,0
+"
+:}
+5,7,3,0
+117440
+
 -}
 module Main (main) where
 
 import Advent (format)
-import Data.List (intercalate)
+import Data.List (intercalate, isSuffixOf)
 import Data.SBV
     (Word64, SWord64, SBool,
      (.==), (.&.), (.&&), sShiftRight, shiftR, xor,
@@ -30,14 +52,19 @@ main =
       %n
       Program: %u&,%n|]
 
+    -- Run with given input register A
     putStrLn (intercalate "," (map show (run (Machine a1 b c) program)))
+    
+    -- Search specific to the kinds of problems we get
+    --print (search program b c)
 
+    -- Search using Z3
     res <- optLexicographic \a2 ->
      do minimize "smallest a" a2
         constrain (sRun (SMachine program a2 (fromIntegral b) (fromIntegral c)) program)
     case getModelValue "smallest a" res of
       Just x -> print (x :: Word64)
-      Nothing -> fail "no solution"
+      Nothing -> putStrLn "no part 2"
 
 data Machine = Machine { rA, rB, rC :: !Int }
 
@@ -83,3 +110,12 @@ sRun m0 pgm = go m0 pgm
           0 -> 0; 1 -> 1; 2 -> 2; 3 -> 3
           4 -> sA m; 5 -> sB m; 6 -> sC m
           _ -> error "invalid combo operand"
+
+search :: [Int] -> Int -> Int -> Int
+search pgm b c = head (go =<< [0 .. 7])
+  where
+    go a =
+      case run (Machine a 0 0) pgm of
+        out | out == pgm           -> [a]
+            | out `isSuffixOf` pgm -> go =<< take 8 [8 * a ..]
+            | otherwise            -> []