[Question][Hw6] parameter "int list" to be passed to Z3.Fixedpoint.add_fact in case of "use"

[sjoon2455]

Hi, I have a question on hw 6.

As I recall the lecture, basic facts to be added to the solver is something like the following:

Here, for the case of def and use, we specify line number and variable that is related to.

When implementing extract_instr, I am confused of required parameter int list that should be passed to Z3.Fixedpint.add_fact.
What should the integer list consist of?
Could anyone give any hint?
Would appreciate any help!

Thank you.

[mekty2012]

Z3.Fixedpoint.add_fact requires FuncDecl, and its domain to be integral type (like as llvm_instr sort in our HW).
If you want Use(instr1, instr2), you can put [(integer corresponding to instr1), (integer corresponding to instr2)].
I'm not sure why Z3 requires as this, maybe it is uncomputable to treat arbitrary expression in add_fact, and non-integral (possibly infinite?) types.
I found this info in Z3 C binding's document.
https://z3prover.github.io/api/html/group__capi.html#ga5b58cbd37d07f3ecfcea6763d2fc037c

[sjoon2455]

@mekty2012, thanks for your answer!