Dumping Z3 code from IR (IR --> Z3 converter)

[dassbrothers]

I want to dump the Z3 equivalent code from the IR that is being generated. Is there any tutorial regarding that? I can see "xls/xls/solvers/z3_ir_translator.cc", "xls/xls/solvers/z3_lec.cc" and other relevant files, but I am unsure which functions to invoke or how to invoke them in which order. Any help would be appreciated.

[cdleary]

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]

Thanks, @cdleary, for the prompt response. That helped me understand how the transformation works and the Z3 output of the IR in the SMTLIB format. But one doubt is that the Z3 output only has the functionality captured, and the variable declarations and other suffs are missing. Moreover, none of the assert statements got boiled down in Z3 as well. Another question is that currently, the conversion only supports conversion of IR "functions" I guess and not "procs" right? Thanks for the help.

[cdleary]

@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 IR nodes also flag a "not yet implemented error", though I think there's not a big conceptual hurdle to add them to the proven assertion set instead of flagging them as unimplemented. I filed #1346 to track the latter one as an enhancement, thanks for pointing it out. LMK if you have any other questions.

[cdleary]

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 thinking it'd just make the SMTLib more readable (vs a large expression tree) or is there some other concern you had in mind?

[dassbrothers]

Thank you for clarifying my doubts. Please feel free to close this issue because you have already created an enhancement ticket. I will let you know if I have any other doubts. For the SMTLib part, I thought that emitting a code of this form "(bvadd (concat #b0 x) (concat #b0 y))" from a simple 1-bit adder would cause any error or not in the Z3 code as x and y are never declared anywhere. Originally x and y are 1 bit variables defined in the DSLX code

[cdleary]

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 << Z3_ast_to_string(translator->ctx(), translator->GetReturnNode())
            << '\n';

The API docs don't mention anything explicitly about params: https://z3prover.github.io/api/html/group__capi.html#ga3975f8427c68d0a938834afd78ccef4d

But it seems like they're declared outside that "ast_to_string" call so we should see if there's a better call to be doing for that tool.