Skip to content

Instantly share code, notes, and snippets.

@burke
Created December 4, 2022 00:26
Show Gist options
  • Save burke/cdf5c59e6e15ea7812229523eee116e3 to your computer and use it in GitHub Desktop.
Save burke/cdf5c59e6e15ea7812229523eee116e3 to your computer and use it in GitHub Desktop.
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)
(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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment