resistors.csv

z3-resistor-combinatorics.clj

(ns z3-resistor-combinatorics
  (:require [clojure.java.jdbc :as jdbc]
            [clojure.edn :as edn]
            [clojure.java.shell :refer [sh]]
            [backtick :refer [template]]
            [lonocloud.synthread :as ->])
  (:import (java.io File)))


(defn z3->str
  [forms]
  (with-out-str
    (doseq [l forms]
      (prn l))))


(defn z3
  [s]
  (let [f (File/createTempFile "foo" ".z3")]
    (spit f (if (string? s) s (z3->str s)))
    (time
      (:out (sh "z3" (.getAbsolutePath f))))))


(def db
  {:classname   "org.sqlite.JDBC"
   :subprotocol "sqlite"
   :subname     "/Users/dev/Dropbox/jlc_2020_oct.db"})


(def re-resistor-description
  #"(?i)[^0-9]*([0-9]+\.?[0-9]*)(.*)Ohms.*±([0-9]+\.?[0-9]*)% ([0-9/\.]+)(.*)W.*")

(defn parse-si-prefix
  [prefix]
  (case prefix
    "K" 1e3
    "M" 1e6
    "m" 1e-3
    "" 1))

(def resistors
  (->> (jdbc/query db ["SELECT LCSCPart, Description, LibraryType, Package FROM parts WHERE FirstCategory = 'Resistors' AND SolderJoint = '2' AND Stock != 0"])
       (map (fn [m]
              (merge m (when-let [[_ r r-prefix tolerance power power-prefix] (re-matches re-resistor-description (:description m))]
                         (try
                           {:val (-> (* (Double/parseDouble r)
                                        (parse-si-prefix r-prefix)
                                        ;;TODO: don't actually round to 1ohm --- this is hack to workaround printing in scientific notation
                                        )
                                     long)
                            :tolerance (Double/parseDouble tolerance)
                            :power (double (* (edn/read-string power) ;;parsing a ratio
                                              (parse-si-prefix power-prefix)))}
                           (catch Exception e
                             (dbg (:description m))
                             nil))))))))

(println (z3 (template (

                        (define-fun abs ((x Real)) Real
                          (ite (>= x 0) x (- x)))


                        (define-fun in-catalog ((id String) (val Real)) Bool
                          (or

                           ;;special case for "no resistor"
                           (and (= id "0") (= val 0))

                           ~@(->> resistors
                                  ;;(take 3000)
                                  (keep (fn [{:keys [lcscpart val]}]
                                          (when val
                                            (template (and (= id ~lcscpart)
                                                           (= val ~val)))))))))


                        (define-fun combine ((r1 Real) (r2 Real) (series Bool)) Real
                          (ite series
                               (+ r1 r2)
                               ;;parallel
                               (ite (= r1 0)
                                    r2
                                    (ite (= r2 0)
                                         r1
                                         (/ 1 (+ (/ 1 r1) (/ 1 r2)))))))


                        (declare-const target-val Real)
                        (declare-const tolerance Real)
                        (declare-const result-val Real)
                        (declare-const abs-error Real)

                        (declare-const series Bool)

                        (declare-const a-id String)
                        (declare-const a-val Real)

                        (declare-const b-id String)
                        (declare-const b-val Real)

                        (assert (in-catalog a-id a-val))
                        (assert (in-catalog b-id b-val))

                        (assert (= result-val (combine a-val b-val series)))

                        (assert (= abs-error (/ (abs (- result-val target-val))
                                                target-val)))

                        (assert (< abs-error (* tolerance target-val)))


                        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                        ;;inputs

                        (assert (= tolerance 0.01))
                        (assert (= target-val 101.0))
                        
                        (check-sat)
                        ;;(check-sat-using smt) ;;sometimes this helps w/ "unknown", othertimes not so much
                        ;;(check-sat-using qfnra-nlsat)
                        ;;(set-option :timeout 15000)
                        (get-model)))))

;;z3 takes about 1s on my laptop to parse 3500 resistors; takes about 10s to solve a 2-resistor problem.
;;but seems to work intermittently. cannot find solution w/ 3000 resistors but works fine with 2000.