Added initial Z3 solvers for defining circuits.

This allows for constraint-based circuit design using
Z3's solvers and optimizers. This is a starting point
and I plan to expand.

This introduces `lbstanza-z3` as a git submodule because I
don't know what the best way to package stanza modules is
yet.

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "lbstanza-z3"]
+	path = lbstanza-z3
+	url = ssh://callendorph-github/callendorph/lbstanza-z3

.vscode/tasks.json

@@ -13,6 +13,7 @@
                 "${workspaceFolder}/tests/TolMath_tests.stanza",
                 "${workspaceFolder}/tests/NumTools_tests.stanza",
                 "${workspaceFolder}/tests/Geometry_tests.stanza",
+                "${workspaceFolder}/tests/Solvers.stanza",
             ],
             "group": "test",
             "presentation": {

src/Solvers/SeriesSets.stanza

@@ -0,0 +1,40 @@
+defpackage etools/Solvers/SeriesSets :
+  import core
+  import collections
+  import etools/ESeries
+  import etools/Errors
+  import z3/Context
+  import z3/AST/AST
+  import z3/AST/Sets
+
+; Resistor/Capacitor/Inductor Sets
+;  The following functions are used to create
+; Z3 set that can be used to limit the solution
+; space to only available resistor values.
+
+public defn ESeries-set (ctx:Context, series:ESeries, exp:Double) -> AST :
+  val values = map(scaled-series{_, exp}, get-series(series))
+  create-real-set(ctx, values)
+
+public defn ESeries-set (ctx:Context, series:ESeries, minV:Double, maxV:Double) -> AST :
+  ; Create a Real-valued set sort that contains the ESeries values between
+  ;  the min and max values provided.
+  val values = find-in-range(series, minV, maxV)
+  create-real-set(ctx, values)
+
+public defn OpAmp-set (ctx:Context, series:ESeries) -> AST :
+  ; For opamps, because of the range of currents and the input
+  ;   and output impedances, we want particular ranges of
+  ;   resistor values used.
+  ESeries-set(ctx, series, 10.0e3, 600.0e3)
+
+
+; Existing Set - We use a HashSet to contain the
+;   values and then convert to an AST because the Z3
+;   Set AST, while impemented as an array, is not easy to
+;   interrogate for values.
+
+public defn to-Z3-set (ctx:Context, hset:HashSet<Double>) -> AST :
+  val values = to-tuple(to-seq(hset))
+  create-real-set(ctx, values)
+

src/Solvers/Utils.stanza

@@ -0,0 +1,18 @@
+defpackage etools/Solvers/Utils :
+  import core
+  import z3/AST/AST
+  import z3/AST/Operators
+
+public defn parallel-R (r1:Double|AST, r2:Double|AST) -> Double|AST :
+  ; Compute equivalent resistance of two parallel resistors
+  (r1 * r2) / (r1 + r2)
+
+public defn parallel-R (Rs:Tuple<AST>) -> AST :
+  ; Compute the equivalent resistance of multiple parallel
+  ;   resistors as AST in a solver equation.
+  1.0 / sum(map({ 1.0 / _ }, Rs))
+
+public defn sq-error-ast (obs:AST, exp:AST) -> AST :
+  ; Compute the squared error between the observed and the
+  ;  expected value.
+  pow((exp - obs) / exp, 2.0)

src/Solvers/VoltageDivider.stanza

@@ -0,0 +1,248 @@
+defpackage etools/Solvers/VoltageDivider :
+  import core
+  import collections
+  import etools/ESeries
+  import etools/Errors
+  import z3/Context
+  import z3/AST/AST
+  import z3/AST/Vector
+  import z3/Model
+  import z3/Solver
+  import z3/Optimize
+  import z3/Tactics
+  import z3/Shellable
+  import z3/Constrainable
+  import z3/AST/Functions
+  import z3/AST/Numerals
+  import z3/AST/Sets
+  import z3/AST/Operators
+  import z3/Enums/Z3_lbool
+  import etools/Solvers/Utils
+  import etools/Solvers/SeriesSets
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Solvers
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+public defstruct VoltageDivider:
+  ; Vin ---
+  ;        |
+  ;        R1
+  ;        |
+  ;        ---- Vout
+  ;        |
+  ;        R2
+  ;        |
+  ;       GND
+  Vin : Double
+  TargetVout : Double
+  R1 : False|Double
+  R2 : False|Double
+  MaxCurr : Double
+
+  ; Value Set from which the resistor solution
+  ;   will be chosen.
+  ValueSet : AST
+
+public defn VoltageDivider (Vin:Double, TargetVout:Double, MaxCurr:Double, ValueSet:AST) -> VoltageDivider :
+  VoltageDivider(Vin, TargetVout, false, false, MaxCurr, ValueSet)
+
+
+public defn target-ratio (d:VoltageDivider) -> Double:
+  TargetVout(d) / Vin(d)
+
+public defn min-R (d:VoltageDivider) -> Double :
+  Vin(d) / MaxCurr(d)
+
+public defstruct DividerSolution :
+  R1 : Double
+  R2 : Double
+
+public defn ratio (s:DividerSolution) -> Double :
+  R2(s) / (R1(s) + R2(s))
+
+public defn vout (s:DividerSolution, vin:Double) -> Double :
+  vin * ratio(s)
+
+public defmethod print (o:OutputStream, s:DividerSolution):
+  print(o, "R1: %~   R2: %~" % [R1(s), R2(s)])
+
+
+public defn set-divider-constraints (ctx:Context, c:Constrainable, state:VoltageDivider) -> Tuple<AST> :
+
+  val [r1, r2] = to-tuple(RealVars(ctx, ["R1", "R2"])) as [AST, AST]
+  val [vin, vout] = to-tuple(RealVars(ctx, ["Vin", "Vout"])) as [AST, AST]
+  val targ = RealVar(ctx, "TargetVout")
+
+  val Rset = ValueSet(state)
+  val minR = min-R(state)
+
+  match(R1(state), R2(state)):
+    (x:Double, y:False):
+      ; Peg R1
+      assert-on(c, z-equal?(r1, x))
+      ; Let R2 float inside out value set
+      assert-on(c, mk-set-member?(r2, Rset))
+    (x:False, y:Double):
+      ; Peg R2
+      assert-on(c, z-equal?(r2, y))
+      ; Let R1 float inside out value set
+      assert-on(c, mk-set-member?(r1, Rset))
+    (x:Double, y:Double): throw(InvalidValue("Either R1 or R2 must be False"))
+    (x:False, y:False):
+      ; Bootstrap by picking a range of values for R2 that
+      ;   should work.
+      val ratio = target-ratio(state)
+      val TargR2 = ratio * minR
+      println("Min R: %~   Target R2: %~" % [minR, TargR2])
+      assert-on(c, r2 > (TargR2 * 0.8))
+      ; The Algorithm will pick both R1 and R2 but we want it
+      ;  restricted to the available set of resistor values.
+      assert-on(c, mk-set-member?(r2, Rset))
+      assert-on(c, mk-set-member?(r1, Rset))
+
+  assert-on(c, z-equal?(vin, Vin(state)))
+  assert-on(c, z-equal?(targ, TargetVout(state)))
+
+  assert-on(c, r1 > 0.0)
+  assert-on(c, r2 > 0.0)
+
+  assert-on(c, (r1 + r2) > minR)
+  assert-on(c, z-equal?(vout, vin * (r2 / (r1 + r2))))
+
+  [vin, vout, targ, r1, r2]
+
+
+public defn get-solution (s:Constrainable, r1:AST, r2:AST) -> DividerSolution :
+  val m = get-model(s)
+  println("%~" % [m])
+  val R1Val = to-double(m[r1])
+  val R2Val = to-double(m[r2])
+  val sol = DividerSolution(R1Val, R2Val)
+  sol
+
+public defn create-scenarios (ctx:Context, state:VoltageDivider, Existing:HashSet<Double>, r1:AST, r2:AST) -> List<Scenario> :
+  ; There are a few different scenarios of floating resistor values
+  ;  1. If R1 or R2 is pegged - then we just check
+  ;     the other one can be solved from the existing set.
+  ;  2. If R1 & R2 are floating - then we need to check:
+  ;     1.  Check if we can select both from the existing set.
+  ;     2.  If that fails - check if R1 can be selected from the existing set
+  ;     3.  Else check if R2 can be selected from the existing set.
+  val ExistingSet = to-Z3-set(ctx, Existing)
+  var scenarios = List()
+  ; Base Case - We let the resistors that aren't pegged float
+  ;   and find a solution.
+  scenarios = cons(Scenario("R1 and/or R2 Float", ASTVector(ctx)), scenarios)
+  ; Under different states, we want to set a different set of
+  ;   constraints by which we attempt to solve from the existing
+  ;   resistor set.
+  match(R1(state), R2(state)):
+    (x:Double, y:False):
+      val scene = Scenario(
+        "Select R2 from Existing",
+        ASTVector(ctx, [
+          mk-set-member?(r2, ExistingSet)
+        ]))
+      scenarios = cons(scene, scenarios)
+
+    (x:False, y:Double):
+      val scene = Scenario(
+        "Select R1 from Existing",
+        ASTVector(ctx, [
+          mk-set-member?(r1, ExistingSet)
+        ]))
+      scenarios = cons(scene, scenarios)
+
+    (x:False, y:False):
+
+      val scenes = [
+        Scenario(
+          "Select R1 & R2 from Existing Set",
+          ASTVector(ctx, [
+            mk-set-member?(r1, ExistingSet),
+            mk-set-member?(r2, ExistingSet),
+          ])
+        ),
+        Scenario(
+          "Select R1 from Existing Set & R2 Floats",
+          ASTVector(ctx, [
+            mk-set-member?(r1, ExistingSet),
+          ])
+        ),
+        Scenario(
+          "Select R2 from Existing Set & R1 Floats",
+          ASTVector(ctx, [
+            mk-set-member?(r2, ExistingSet),
+          ])
+        ),
+      ]
+      scenarios = append(scenes, scenarios)
+  scenarios
+
+public defn solve (ctx:Context, state:VoltageDivider, accuracy:Double, Existing:HashSet<Double>) -> Maybe<DividerSolution> :
+  ; Solver a voltage divider equation using the passed existing set of resistors.
+  ; @param state voltage divider goals
+  ; @parram accuracy percent error that we are willing to accept.
+  ; @param Existing available resistors already in the design.
+  if accuracy <= 0.0 :
+    fatal("Accuracy must be percentage greater than zero")
+
+  val s = Solver(ctx)
+
+  val [vin, vout, targ, r1, r2] = set-divider-constraints(ctx, s, state) as [AST, AST, AST, AST, AST]
+
+  ; Use a squared error as our target constraint
+  val err = sq-error-ast(vout, targ)
+  val acc = accuracy / 100.0
+  assert-on(s, err < (acc * acc))
+
+  val scenarios = create-scenarios(ctx, state, Existing, r1, r2)
+
+  val [r, idx] = solve-scenarios(s, to-tuple(scenarios))
+  if r is Z3_L_TRUE:
+    val sol = get-solution(s, r1, r2)
+    One(sol)
+  else:
+    None()
+
+
+public defn optimize (ctx:Context, state:VoltageDivider, Existing:HashSet<Double>) -> Maybe<DividerSolution> :
+  ; Optimize a voltage divider equation using the passed existing set of resistors.
+  ; @NOTE - This will select resistors only from the existing set when applicable.
+  ;   This means that this function may not give you great accuracy depending on what
+  ;   resistance values are in your design at this point.
+  ;   Best to use this function last and only for "Best Effort" where you don't
+  ;   care about accuracy - you just need something, the cheaper the better.
+  ;
+  ; @param state voltage divider goals
+  ; @param Existing available resistors already in the design.
+
+  val s = Optimizer(ctx)
+
+  val [vin, vout, targ, r1, r2] = set-divider-constraints(ctx, s, state) as [AST, AST, AST, AST, AST]
+
+  ; Use a squared error as our target constraint
+  val err = sq-error-ast(vout, targ)
+  minimize(s, err)
+
+  val scenarios = create-scenarios(ctx, state, Existing, r1, r2)
+  val [r, idx] = solve-scenarios(s, to-tuple(scenarios))
+  if r is Z3_L_TRUE:
+    val sol = get-solution(s, r1, r2)
+    One(sol)
+  else:
+    None()
+
+
+
+
+
+
+
+
+
+
+

stanza.proj

@@ -1,3 +1,4 @@
+include "lbstanza-z3/stanza.proj"
 packages etools/* defined-in "src/"
 import etools/jitx/ESeries when-imported (etools/ESeries, jitx)
 import etools/jitx/TolMath when-imported (jitx)

tests/Solvers.stanza

@@ -0,0 +1,70 @@
+#use-added-syntax(tests)
+defpackage etools/Solvers-tests :
+  import core
+  import collections
+  import etools/Solvers/VoltageDivider
+  import etools/Solvers/SeriesSets
+  import etools/ESeries
+  import z3/Context
+  import z3/Solver
+
+deftest(solvers) test-solve-with-existing :
+
+  val cfg = Config()
+  val ctx = Context(cfg)
+
+  val series = E96()
+  val Rset = ESeries-set(ctx, series, 10.0e3, 400.0e3)
+
+  val Existing = HashSet<Double>()
+  add(Existing, 47.0e3)
+  add(Existing, 4.7e3)
+  ; We expect the solver to use R1 as this value
+  add(Existing, 54.9e3)
+
+  val div = VoltageDivider(24.0, 6.0, 500.0e-6, Rset)
+
+  val out = solve(ctx, div, 1.0, Existing)
+
+  match(out):
+    (_:None):
+      println("Failed to Find Solution")
+      #EXPECT(1 == 0)
+    (o:One<DividerSolution>):
+      val x = value(o)
+      println("Solution: %~" % [x])
+      println("Vout=%~" % [vout(x, Vin(div))])
+      #EXPECT(R1(x) == 54900.0)
+      #EXPECT(R2(x) == 18200.0)
+
+
+deftest(solvers) test-optim-with-existing :
+
+  val cfg = Config()
+  val ctx = Context(cfg)
+
+  val series = E96()
+  val Rset = ESeries-set(ctx, series, 10.0e3, 400.0e3)
+
+  val Existing = HashSet<Double>()
+  ; add(Existing, 100.0e3)
+  add(Existing, 47.0e3)
+  add(Existing, 4.7e3)
+  add(Existing, 18.2e3)
+  add(Existing, 54.9e3)
+
+  val div = VoltageDivider(24.0, 6.0, 500.0e-6, Rset)
+
+  val out = optimize(ctx, div, Existing)
+
+  match(out):
+    (_:None):
+      println("Failed to Find Solution")
+      #EXPECT(1 == 0)
+    (o:One<DividerSolution>):
+      val x = value(o)
+      println("Solution: %~" % [x])
+      println("Vout=%~" % [vout(x, Vin(div))])
+      #EXPECT(R1(x) == 54900.0)
+      #EXPECT(R2(x) == 18200.0)
+