This commit is contained in:
Adam Jeniski 2025-12-12 12:21:02 -10:00
parent 50e6464eba
commit 9ea11f35c9

View File

@ -50,7 +50,7 @@
(def Int z3/Int) (def Int z3/Int)
(def Optimize z3/Optimize) (def Optimize z3/Optimize)
(def Sum z3/Sum) (def Sum z3/Sum)
(defn apply-formulas! [opt [f & fs]] (defn add-formulas! [opt [f & fs]]
(when f (when f
(! "add" opt f) (! "add" opt f)
(recur opt fs))) (recur opt fs)))
@ -67,19 +67,19 @@
count count
range range
(map #(Int (str "j" %))))] (map #(Int (str "j" %))))]
(apply-formulas! opt (for [idx (range (count joltages))] (add-formulas! opt (for [idx (range (count joltages))]
(let [jn (nth js idx) (let [jn (nth js idx)
summation-args (->> buttons summation-args (->> buttons
(map set) (map set)
(map-indexed vector) (map-indexed vector)
(filter #(contains? (second %) idx)) (filter #(contains? (second %) idx))
(map first) (map first)
(map #(nth bs %)))] (map #(nth bs %)))]
(py= jn (apply Sum summation-args))))) (py= jn (apply Sum summation-args)))))
(apply-formulas! opt (for [[idx joltage] (map-indexed vector joltages)] (add-formulas! opt (for [[idx joltage] (map-indexed vector joltages)]
(let [jn (nth js idx)] (let [jn (nth js idx)]
(py= jn joltage)))) (py= jn joltage))))
(apply-formulas! opt (for [b bs] (py>= b 0))) (add-formulas! opt (for [b bs] (py>= b 0)))
(! "minimize" opt (apply Sum bs)) (! "minimize" opt (apply Sum bs))
(! "check" opt) (! "check" opt)
(let [model (! "model" opt)] (let [model (! "model" opt)]