[schoen]

> Operator overloading allowed me to define joules like so: `J = KG * M*-1 * S*-2`. Then I could define grays (a radiation-related unit) like `Gy = J/KG`. Repeat for hundreds of units.

Presumably exponentiation rather than multiplication by a constant, right?

This is cool and reminds me of how the Python Z3 binding uses operator overloading to let you express arithmetic and logical constraints

  >>> import z3
  >>> s = z3.Solver()
  >>> a, b, c, d = (z3.Int(x) for x in "abcd")
  >>> s.add(a*b == c+d)
  >>> s.add(a+b == c+d)
  >>> s.add(a!=0,b!=0,c!=0,d!=0)
  >>> s.check()
  sat
  >>> s.model()
  [d = 6, c = -2, b = 2, a = 2]
  >>> s.reset()
  >>> s.add(a>1, b>1, c>1)
  >>> s.add(a*a + b*b == c*c)
  >>> s.check()
  sat
  >>> s.model()
  [c = 17, b = 8, a = 15]

(It's limited in some ways for some reasons, like for some types and relations you may have to use a Z3 function to express a relation even though Python has syntax for it -- the example that I know of is that you have to use z3.Or(), z3.And(), etc., with boolean variables instead of Python's builtin boolean operators. Not sure why.)*

[kpgiskpg]

Oh wait, Hackernews seems to have removed one of the astericks symbols. It should be Python's exponentiation operator (2 astericks symbols), ya. (edit: fixed now).

That's cool too! How do you define the variables?

[schoen]

Oh wait, I left that part out! I'll edit my post.

... there we go.

You use Z3 objects that represent unknowns of particular types, like Z3.Int, Z3.Bool, etc. Each one returns an object representing a variable of that type, which can then be used in (Python-formatted!) expressions that you give to a solver.