gen.rb

exprs = File.readlines('input')
  .map { |l| "    (seq.unit \"#{l.chomp}\")" }
  .join("\n")

smt2 = File.read('tpl.smt2')
  .sub('%EXPRS%', exprs)
File.write('out.smt2', smt2)

tpl.smt2

(set-logic QF_S)

(define-sort Prio () Int)
(define-sort PrioSeq () (Seq Prio))

(define-fun to_prio ((s String)) Prio
  (let ((code (str.to_code s)))
       (ite (>= code 97)
            (- code 96)    ; ?a.ord-96 => 1
            (- code 38)))) ; ?A.ord-38 => 27

(define-fun seq.half-len ((s PrioSeq)) Int
  (to_int (/ (seq.len s) 2)))

(define-fun seq.first-half ((s PrioSeq)) PrioSeq
  (seq.extract s 0 (seq.half-len s)))

(define-fun seq.second-half ((s PrioSeq)) PrioSeq
  (seq.extract s (seq.half-len s) (seq.half-len s)))

(define-fun seq.intersect ((a PrioSeq) (b PrioSeq)) PrioSeq
  (seq.foldl
    (lambda ((acc PrioSeq) (in Int))
      (ite (and (seq.contains b (seq.unit in))
                (not (seq.contains acc (seq.unit in))))
           (seq.++ acc (seq.unit in))
           acc))
    (as seq.empty PrioSeq)
    a))

(declare-const seq100 PrioSeq)
(assert (= (seq.len seq100) 100))

(define-fun seq.from_str ((str String)) PrioSeq
  (seq.foldl
      (lambda ((acc PrioSeq) (in Int))
         (seq.++ acc (seq.unit (to_prio (str.at str (seq.len acc))))))
      (as seq.empty PrioSeq)
      (seq.extract seq100 0 (str.len str))))

(define-fun priority-intersect ((str String)) PrioSeq
  (let ((as_seq (seq.from_str str)))
    (seq.intersect (seq.first-half as_seq)
                   (seq.second-half as_seq))))

(define-fun seq.nonlast ((s (Seq (Seq String)))) (Seq (Seq String))
  (seq.extract s 0 (- (seq.len s) 1)))

(define-fun seq.last ((s (Seq (Seq String)))) (Seq String)
  (seq.nth s (- (seq.len s) 1)))

(define-fun seq.slices ((n Int) (s (Seq String))) (Seq (Seq String))
  (seq.foldl
    (lambda ((acc (Seq (Seq String))) (el String))
      (ite
        (or (= 0 (seq.len acc))
            (= n (seq.len (seq.last acc))))
        (seq.++ acc (seq.unit (seq.unit el)))
        (let ((nonlast (seq.nonlast acc)) (last (seq.last acc)))
          (seq.++ nonlast
                  (seq.unit (seq.++ last (seq.unit el)))))))
    (as seq.empty (Seq (Seq String)))
    s))

(define-fun common-priority-in-group ((s (Seq String))) PrioSeq
  (seq.intersect (seq.from_str (seq.nth s 2))
                 (seq.intersect (seq.from_str (seq.nth s 0))
                                (seq.from_str (seq.nth s 1)))))

(define-fun priorities-to-sum ((strs (Seq String))) PrioSeq
  (seq.foldl
    (lambda ((acc PrioSeq) (in String))
      (seq.++ acc (priority-intersect in)))
    (as seq.empty PrioSeq)
    strs))

(define-fun total-priority ((strs (Seq String))) Prio
  (seq.foldl
    (lambda ((acc Prio) (in Prio))
      (+ acc in))
    0
    (priorities-to-sum strs)))

(define-fun badges-to-sum ((strs (Seq String))) PrioSeq
  (seq.foldl
    (lambda ((acc PrioSeq) (in (Seq String)))
      (seq.++ acc (common-priority-in-group in)))
    (as seq.empty PrioSeq)
    (seq.slices 3 strs)))

(define-fun total-badges ((strs (Seq String))) Prio
  (seq.foldl
    (lambda ((acc Prio) (in Prio))
      (+ acc in))
    0
    (badges-to-sum strs)))


(define-const strs (Seq String)
  (seq.++
%EXPRS%))

(declare-const part1 Prio)
(assert (= part1 (total-priority strs)))

(declare-const part2 Prio)
(assert (= part2 (total-badges strs)))

(declare-const xxx (Seq (Seq String)))
(assert (= xxx (seq.slices 3 strs)))

(declare-const yyy (Seq String))
(assert (= yyy (seq.nth xxx 0)))

(declare-const zzz PrioSeq)
(assert (= zzz (common-priority-in-group yyy)))

(check-sat)

(get-value (part1))
(get-value (part2))