I'm trying to use Z3 to solve a logic puzzle, mostly as a chance to learn more about Z3. I'm stuck on a couple of things out of the gate:

How do people usually interact with Z3 in practice? Manually writing smtlib doesn't seem like it would scale. Do people use the Z3 bindings to Python, Java, etc. or are people using libraries to generate smtlib syntax which then gets fed in?

I'm looking at the TypeScript bindings. There's a "high level" set of bindings which seems incomplete (no support for datatype declarations, for example) and a "low level" set of bindings that seems more featureful. I get the vibe that the high level bindings aren't getting a lot of usage or maintenance. Can anyone confirm or give background here? Is TS simply the wrong language to use, or am I still likely to be writing Z3 in a modern-ish way by using the low level bindings?

#z3 #smt #smtlib #TheoremProvers #TheoremProving

I just published a tool called smatch that I've wanted for a while now. A grep-like tool to do pattern matching on S-expressions (#lisp) using #regex-like syntax for trees.

It also has recursive patterns, so you can pattern match with patterns that look like grammars.

My end goal is to use them for #SMTLIB but it should still work for most lisps (clojure being an exception).

The code and an x86_64-linux static binary are here: https://github.com/geezee/smatch