ajet/advent-of-code
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

use java deps for z3

Browse Source
This commit is contained in:
Adam Jeniski 2025-12-22 17:55:11 -05:00
parent d55ca4c019
commit 8fa11862e1
2 changed files with 51 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
2025/project.clj
View File

@ -10,5 +10,6 @@
[babashka/fs "0.5.23"] [babashka/fs "0.5.23"]
[org.babashka/http-client "0.4.22"] [org.babashka/http-client "0.4.22"]
[org.clojure/core.match "1.1.0"] [org.clojure/core.match "1.1.0"]
[clj-python/libpython-clj "2.026"]] [clj-python/libpython-clj "2.025"]
:source-paths ["src" "../shared/clj/src"]) [tools.aqua/z3-turnkey "4.14.1"]]
:source-paths ["src" "../shared/clj/src"])

102
2025/src/day10.clj
View File

@ -1,26 +1,23 @@
(ns day10 (ns day10
(:require input-manager (:require [clojure.math.combinatorics :as combo]
[core :refer [dbg]] [input-manager])
[clojure.math.combinatorics :as combo] (:import (com.microsoft.z3 BoolExpr Context Expr IntNum Optimize Optimize$Handle)))
[clojure.string :as str]
[libpython-clj2.require :refer [require-python]]
[libpython-clj2.python :as py]))
(defn parse-line [line] (defn parse-line [line]
{:indicators (->> line {:indicators (->> line
(drop 1) (drop 1)
(take-while (complement #{\]})) (take-while (complement #{\]}))
(mapv (partial = \#))) (mapv (partial = \#)))
:buttons (->> line :buttons (->> line
(re-seq #"\([\d,]+\)") (re-seq #"\([\d,]+\)")
(map #(map parse-long (re-seq #"\d+" %)))) (map #(map parse-long (re-seq #"\d+" %))))
:joltages (->> line :joltages (->> line
(drop-while #(not= % \{)) (drop-while #(not= % \{))
(drop 1) (drop 1)
(take-while #(not= % \})) (take-while #(not= % \}))
(apply str) (apply str)
(re-seq #"\d+") (re-seq #"\d+")
(mapv parse-long))}) (mapv parse-long))})
(def input (map parse-line (input-manager/get-input 2025 10))) (def input (map parse-line (input-manager/get-input 2025 10)))
@ -39,51 +36,48 @@
;; part 1 ;; part 1
(apply + (map minimum-button-mashing input)) (apply + (map minimum-button-mashing input))
;; clj-python setup
(defmacro ! [self method & args] `(py/call-attr ~method ~self ~@args))
(defmacro py= [self & args] `(! "__eq__" ~self ~@args))
(defmacro py>= [self & args] `(! "__ge__" ~self ~@args))
(defmacro pysubscript [self & args] `(! "__getitem__" ~self ~@args))
;; z3 stuff
(require-python :from (str (System/getenv "HOME") "/.local/lib/python3.13/site-packages/") '[z3 :as z3])
(def Int z3/Int)
(def Optimize z3/Optimize)
(def Sum z3/Sum)
(defn add-formulas! [opt [f & fs]]
(when f
(! "add" opt f)
(recur opt fs)))
;; part 2 ;; part 2
(->> input (->> input
(map (fn [{:keys [joltages buttons]}] (map (fn [{:keys [joltages buttons]}]
(let [opt (Optimize) (let [ctx (Context.)
^Optimize opt (.mkOptimize ctx)
bs (->> buttons bs (->> buttons
count count
range range
(map #(Int (str "b" %)))) (map #(.mkIntConst ctx (str "b" %))))
js (->> joltages js (->> joltages
count count
range range
(map #(Int (str "j" %))))] (map #(.mkIntConst ctx (str "j" %))))]
(add-formulas! opt (for [idx (range (count joltages))] (.Add
(let [jn (nth js idx) opt
summation-args (->> buttons (into-array
(map set) BoolExpr
(map-indexed vector) (for [idx (range (count joltages))]
(filter #(contains? (second %) idx)) (let [jn (nth js idx)
(map first) summation-args (->> buttons
(map #(nth bs %)))] (map set)
(py= jn (apply Sum summation-args))))) (map-indexed vector)
(add-formulas! opt (for [[idx joltage] (map-indexed vector joltages)] (filter #(contains? (second %) idx))
(let [jn (nth js idx)] (map first)
(py= jn joltage)))) (map #(nth bs %))
(add-formulas! opt (for [b bs] (py>= b 0))) (into-array Expr)
(! "minimize" opt (apply Sum bs)) (.mkAdd ctx))]
(! "check" opt) (.mkEq ctx jn summation-args)))))
(let [model (! "model" opt)] (.Add
(->> (for [b bs] (! "as_long" (pysubscript model b))) opt
(apply +)))))) (into-array
Expr
(for [[idx joltage] (map-indexed vector joltages)]
(let [jn (nth js idx)]
(.mkEq ctx jn (.mkInt ctx (long joltage)))))))
(.Add
opt
(into-array
Expr
(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 []))
(.getInt ^IntNum (.getLower mx))))))
(apply +)) (apply +))