search

statusfailed / catgrad

a categorical deep learning compiler
MIT License
107 stars 2 forks source link

Single Static Assignment - MLIR and SMTLIB. #1

Open chadbrewbaker opened 10 months ago

chadbrewbaker commented 10 months ago

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 commented 10 months ago

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?