Chris Leary

The binary to do this is called `smtlib_emitter_main` -- there's a mini tutorial in the tools documentation here: https://google.github.io/xls/tools/#smtlib_emitter_main Let us know how that works for your use case.

@dassbrothers I believe you are correct about both limitations. It currently supports functions (we'd want a bounded-model-checking-style unroller to deal with the consequences of time with procs). I believe `assert`...

Also note there's no need for "variable declarations" in the translation, values are immutable so `let` bindings are just a shorthand notation for the result of some expression. Are you...

Good point, maybe there's something additional we should do to print out the parameter declarations -- this is the code: https://github.com/google/xls/blob/main/xls/tools/smtlib_emitter_main.cc#L61 ``` Z3_set_ast_print_mode(translator->ctx(), Z3_PRINT_SMTLIB2_COMPLIANT); std::cout ctx(), translator->GetReturnNode())

@spurserh Are the synthesis targets required for what the user is trying to do? Could try commenting them out for now if you just want XLS targets to generate RTL...

@spurserh Also note to help with these we'd probably need more step by step instructions on how the environment got set up, because the nightly OS X build is looking...

We think this should be fixed by #1535

Just to note what's going on, the parser doesn't support reference to an instantiated parametric function like that, so as a workaround you'd need to make a wrapper that has...

As you mentioned I do this just by hacking it out in the release branch. I did try to find a more proper way of doing it back in May...

The let statement is what causes the RHS to be at the alignment of the `= ` -- I'm not sure if it makes sense to align all expressions that...