Work over transpiler in z3

[jwoehr]

Abstract

Expand transpiler use of z3 Theorem Prover

Description

z3 is employed as declarative logic in a couple of transpiler optimization passes already:

• https://github.com/Qiskit/qiskit-terra/blob/master/qiskit/transpiler/passes/optimization/crosstalk_adaptive_schedule.py
• https://github.com/Qiskit/qiskit-terra/blob/master/qiskit/transpiler/passes/optimization/hoare_opt.py
  Expand the use of z3 in transpiler passes as a means of making the logical content clearer to read and maintain than hand-coding the logical content.

Deliverable

Ongoing effort to clarify the transpiler.

GitHub repo

??

[HuangJunye]

This is a really cool project. I am interested in working on it. However, I am working on projects #1, #2 and #3 at the moment so it will be a while before I will have time, probably in late Oct.

[jwoehr]

You may be more successful at getting Advocates to hack on the Qiskit code itself than I was when I tried last March.
I don't envision this as a separate project but more like a club of people who want to hack on the transpiler in qiskit-terra.

[aditya-giri]

This is cool and interests me too - like Junye said, I'd like to work on this after completing the other ones!

[jwoehr]

Z3 makes the intentions of the author clearer in complex logic situation, and it can help avoid mistakes when you code things by hand with if statements etc.

[HuangJunye]

You may be more successful at getting Advocates to hack on the Qiskit code itself than I was when I tried last March.
I don't envision this as a separate project but more like a club of people who want to hack on the transpiler in qiskit-terra.

Looks like we have hope this time round. Let's see how it goes!

[georgios-ts]

Definitely a project i would like to get involved! There are already some reported issues on HoareOptimizer (see 1, 2). Maybe it's a good place to start. Though some guidance (a mentor ?) could be helpful.

[jwoehr]

@georgios-ts you can fork qiskit-terra any time and work on it. Are you familiar with forks, branches, and pull requests?
I can mentor on this (since I wrote the z3 issue anyway :) )

[georgios-ts]

Yes, great! I will start working on it and i'll get in contact if needed. :)