aoc2024-day17-p1.scm

(use-modules (srfi srfi-1)
	     (ice-9 match) (ice-9 peg)
	     (ice-9 textual-ports)
	     (ice-9 pretty-print)
	     (srfi srfi-43))

(define-peg-string-patterns
  "top <-- entry entry entry NL entry !.
entry <-- name COLON SPACE (number COMMA?)* NL
name <-- [A-Za-z ]+
number <-- [0-9]+
COLON < ':'
COMMA < ','
SPACE < ' '
NL < '\n'
")

(define (parse-number number)
  (string->number (second number)))

(define (parse-reg reg)
  (parse-number (third reg)))

(define (parse-program program)
  (list->vector (map parse-number (third program))))

(define (parse-top top)
  (list (parse-reg (second top))
	(parse-reg (third top))
	(parse-reg (fourth top))
	0
	'()
	(parse-program (fifth top))))


(define (next-state state)
  (match-let* ([(a b c pc out imem) state]
	       [opcode (vector-ref imem pc)]
	       [operand (vector-ref imem (1+ pc))])
    (define (combo)
      (match operand
	[4 a]
	[5 b]
	[6 c]
	[7 (error "Malformed combo" state opcode operand)]
	[x x]))
    (match opcode
      ;; adv combo
      [0 (list (ash a (- (combo))) b c (+ 2 pc) out imem)]
      ;; bxl literal
      [1 (list a (logxor b operand) c (+ 2 pc) out imem)]
      ;; bst combo
      [2 (list a (logand (combo) 7) c (+ 2 pc) out imem)]
      ;; jnz literal
      [3 (list a b c
	       (if (zero? a)
		   (+ 2 pc)
		   operand)
	       out imem)]
      ;; bxc
      [4 (list a (logxor b c) c (+ 2 pc) out imem)]
      ;; out combo
      [5 (list a b c (+ 2 pc) (cons (logand (combo) 7) out) imem)]
      ;; bdv combo
      [6 (list a (ash a (- (combo))) c (+ 2 pc) out imem)]
      ;; cdv combo
      [7 (list a b (ash a (- (combo))) (+ 2 pc) out imem)]
      [_ (error "Malformed program" state opcode operand)])))

(define (run initial-state)
  (let next ([state initial-state])
    (if (>= (fourth state) (vector-length (sixth state)))
	(fifth state)
	(next (next-state state)))))


(define (out-string out)
  (string-drop
   (fold-right
    (λ (v prev)
      (string-append prev "," (number->string v)))
    ""
    out)
   1))


(let* ([input (get-string-all (current-input-port))]
       [peg-tree (peg:tree (match-pattern top input))]
       [state (parse-top peg-tree)])
  (pretty-print (out-string (run state))))

aoc2024-day17-p2.smt2

(set-logic QF_ABV)
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)

(declare-fun A () (_ BitVec 64))

(declare-fun _x7 () (_ BitVec 64))
(assert (= _x7 #x0000000000000007))

(declare-fun _x2 () (_ BitVec 64))
(assert (= _x2 #x0000000000000002))

(declare-fun _s0 () (_ BitVec 64))
(assert (= _s0 #x0000000000000000))
(declare-fun _s1 () (_ BitVec 64))
(assert (= _s1 #x0000000000000003))
(declare-fun _s2 () (_ BitVec 64))
(assert (= _s2 #x0000000000000006))
(declare-fun _s3 () (_ BitVec 64))
(assert (= _s3 #x0000000000000009))
(declare-fun _s4 () (_ BitVec 64))
(assert (= _s4 #x000000000000000c))
(declare-fun _s5 () (_ BitVec 64))
(assert (= _s5 #x000000000000000f))
(declare-fun _s6 () (_ BitVec 64))
(assert (= _s6 #x0000000000000012))
(declare-fun _s7 () (_ BitVec 64))
(assert (= _s7 #x0000000000000015))
(declare-fun _s8 () (_ BitVec 64))
(assert (= _s8 #x0000000000000018))
(declare-fun _s9 () (_ BitVec 64))
(assert (= _s9 #x000000000000001b))
(declare-fun _s10 () (_ BitVec 64))
(assert (= _s10 #x000000000000001e))
(declare-fun _s11 () (_ BitVec 64))
(assert (= _s11 #x0000000000000021))
(declare-fun _s12 () (_ BitVec 64))
(assert (= _s12 #x0000000000000024))
(declare-fun _s13 () (_ BitVec 64))
(assert (= _s13 #x0000000000000027))
(declare-fun _s14 () (_ BitVec 64))
(assert (= _s14 #x000000000000002a))
(declare-fun _s15 () (_ BitVec 64))
(assert (= _s15 #x000000000000002d))


(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s0) _x7) _x2) _x7) (bvlshr (bvlshr A _s0) (bvxor (bvand (bvlshr A _s0) _x7) _x2))) _x7)
  #x0000000000000002))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s1) _x7) _x2) _x7) (bvlshr (bvlshr A _s1) (bvxor (bvand (bvlshr A _s1) _x7) _x2))) _x7)
  #x0000000000000004))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s2) _x7) _x2) _x7) (bvlshr (bvlshr A _s2) (bvxor (bvand (bvlshr A _s2) _x7) _x2))) _x7)
  #x0000000000000001))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s3) _x7) _x2) _x7) (bvlshr (bvlshr A _s3) (bvxor (bvand (bvlshr A _s3) _x7) _x2))) _x7)
  #x0000000000000002))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s4) _x7) _x2) _x7) (bvlshr (bvlshr A _s4) (bvxor (bvand (bvlshr A _s4) _x7) _x2))) _x7)
  #x0000000000000007))
  
(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s5) _x7) _x2) _x7) (bvlshr (bvlshr A _s5) (bvxor (bvand (bvlshr A _s5) _x7) _x2))) _x7)
  #x0000000000000005))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s6) _x7) _x2) _x7) (bvlshr (bvlshr A _s6) (bvxor (bvand (bvlshr A _s6) _x7) _x2))) _x7)
  #x0000000000000000))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s7) _x7) _x2) _x7) (bvlshr (bvlshr A _s7) (bvxor (bvand (bvlshr A _s7) _x7) _x2))) _x7)
  #x0000000000000003))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s8) _x7) _x2) _x7) (bvlshr (bvlshr A _s8) (bvxor (bvand (bvlshr A _s8) _x7) _x2))) _x7)
  #x0000000000000001))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s9) _x7) _x2) _x7) (bvlshr (bvlshr A _s9) (bvxor (bvand (bvlshr A _s9) _x7) _x2))) _x7)
  #x0000000000000007))

(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s10) _x7) _x2) _x7) (bvlshr (bvlshr A _s10) (bvxor (bvand (bvlshr A _s10) _x7) _x2))) _x7)
  #x0000000000000004))
  
(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s11) _x7) _x2) _x7) (bvlshr (bvlshr A _s11) (bvxor (bvand (bvlshr A _s11) _x7) _x2))) _x7)
  #x0000000000000001))
  
(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s12) _x7) _x2) _x7) (bvlshr (bvlshr A _s12) (bvxor (bvand (bvlshr A _s12) _x7) _x2))) _x7)
  #x0000000000000005))
  
(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s13) _x7) _x2) _x7) (bvlshr (bvlshr A _s13) (bvxor (bvand (bvlshr A _s13) _x7) _x2))) _x7)
  #x0000000000000005))
  
(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s14) _x7) _x2) _x7) (bvlshr (bvlshr A _s14) (bvxor (bvand (bvlshr A _s14) _x7) _x2))) _x7)
  #x0000000000000003))
  
(assert
 (= 
  (bvand (bvxor (bvxor (bvxor (bvand (bvlshr A _s15) _x7) _x2) _x7) (bvlshr (bvlshr A _s15) (bvxor (bvand (bvlshr A _s15) _x7) _x2))) _x7)
  #x0000000000000000))


; lowest bound A > (1 << (3 * 15 + 1))
(assert (bvugt A (bvshl #x0000000000000001 #x000000000000002e)))
; #x000052a2d906c3f0 found by binary searching through each digit
; left-to-right until i found the largest digits that still produce
; a result
(assert (bvult A (bvsub (bvshl #x0000000000000001 #x0000000000000030) #x000052a2d906c3f0)))


(check-sat)
(get-value (A))