Single Static Assignment - MLIR and SMTLIB.

[chadbrewbaker]

Any way you could output in Single Static Assignment for LLVM/MLIR and SSA SMTLIB lisp for solvers like Microsoft Z3/CVC5? You could then shell out to LLVM and Z3/CVC5 to make optimization passes, and give you an easy compile target for WASM with a little IO boilerplate.

%1 = ...
%2 = ...


(+ x3 x2 x1)

[statusfailed]

SSA is basically what the compiler backend works with, but you might have to unwrap tensor primitives (like tensordot) into lower level representations unless LLVM has builtin tensor ops (does it?)

Are there any SMT solvers which work with tensor primitives?