API to access Init/Next formula before SMT cell encoding?

[ak24-ho]

Hi Apalache team,

I’m working on a research project using Apalache and I’m trying to extract the logical formula corresponding to a TLA+ specification before it is lowered into the SMT cell encoding ($C$0, $C$1, ...).

I know Apalache produces log0.smt, but at that stage the formula is already encoded over arena cells, which is difficult to relate back to the original TLA+ operators.

My goal is to access something closer to the parsed/typed representation of operators such as Init and Next (for example as TlaEx / TlaOperDecl, or another IR), ideally before SMT translation.

I wanted to ask:

1. Is there an existing API, CLI flag, or internal utility in Apalache to export or print the IR of Init / Next before SMT encoding?
2. Is there a recommended way to access the generated symbolic formula before it becomes arena-cell based SMT?
3. If not, which part of the codebase would you recommend extending to extract this representation?

Any pointers would be greatly appreciated.

Thanks a lot!