Elektrine lite

← Feed

@thalia@discuss.systems

Post #1750297

2026-04-15 19:12 UTC

@dougmerritt @j2kun In my current research project, which involves implementing a stripped down LLVM IR, I implemented the parser first, which was a bad idea. I don't want both an AST and IR, so I'm iteratively refactoring my AST into an IR. I also already built an SMT IR with backends for Z3 and SMT-LIB, making this the opposite of my usual approach.

Replies (2)

  • @dougmerritt@mathstodon.xyz 2026-04-15 19:14

    @thalia @j2kun Hmm, why was it worthwhile to do the effort, did it obscure things, or are you space or time limited? > SMT-LIB I keep hearing about that usage more and more and more.

    Open ##1750298

  • @j2kun@mathstodon.xyz 2026-04-15 19:40

    @thalia @dougmerritt have you heard of the SMT backend added to MLIR? (Or maybe you were involved in that?)

    Open ##1750301