golf
This commit is contained in:
parent
14ac947ae3
commit
e51b3296d6
@ -1,7 +1,7 @@
|
||||
(ns day10
|
||||
(:require [clojure.math.combinatorics :as combo]
|
||||
[input-manager])
|
||||
(:import (com.microsoft.z3 BoolExpr Context Expr IntNum Optimize Optimize$Handle)))
|
||||
(:import (com.microsoft.z3 Context Expr IntNum Optimize Optimize$Handle)))
|
||||
|
||||
(defn parse-line [line]
|
||||
{:indicators (->> line
|
||||
@ -37,8 +37,8 @@
|
||||
(apply + (map minimum-button-mashing input))
|
||||
|
||||
;; part 2
|
||||
(defn add-expressions [opt type expressions]
|
||||
(.Add opt (into-array type expressions)))
|
||||
(defn add-expressions [opt expressions]
|
||||
(.Add opt (into-array Expr expressions)))
|
||||
|
||||
(->> input
|
||||
(map (fn [{:keys [joltages buttons]}]
|
||||
@ -52,8 +52,7 @@
|
||||
count
|
||||
range
|
||||
(map #(.mkIntConst ctx (str "j" %))))]
|
||||
(add-expressions opt BoolExpr
|
||||
(for [idx (range (count joltages))]
|
||||
(add-expressions opt (for [idx (range (count joltages))]
|
||||
(let [jn (nth js idx)
|
||||
summation-args (->> buttons
|
||||
(map set)
|
||||
@ -64,12 +63,10 @@
|
||||
(into-array Expr)
|
||||
(.mkAdd ctx))]
|
||||
(.mkEq ctx jn summation-args))))
|
||||
(add-expressions opt Expr
|
||||
(for [[idx joltage] (map-indexed vector joltages)]
|
||||
(add-expressions opt (for [[idx joltage] (map-indexed vector joltages)]
|
||||
(let [jn (nth js idx)]
|
||||
(.mkEq ctx jn (.mkInt ctx (long joltage))))))
|
||||
(add-expressions opt Expr
|
||||
(for [b bs]
|
||||
(add-expressions opt (for [b bs]
|
||||
(.mkGe ctx b (.mkInt ctx (long 0)))))
|
||||
(let [^Optimize$Handle mx (.MkMinimize opt (.mkAdd ctx (into-array Expr bs)))]
|
||||
(.Check opt (into-array Expr []))
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user