Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Verifier] Verify each circuit transformation step #176

Merged
merged 4 commits into from
Jun 12, 2024
Merged

Conversation

xumingkuan
Copy link
Collaborator

This PR adds a function to verify circuit transformations. It first removes the common first/last gates from each circuit transformation step, then uses Z3 to verify if the remaining parts are equivalent. If the hash values differ by more than 1, it will not invoke Z3 and report they are not equivalent directly. Assuming the code is implemented correctly, it guarantees that the two circuits are equivalent if it returns true.

Example potential output of test_optimization_steps:

...
Verifying circuit 4 -> circuit 5
Checking Verifier::equivalent() on:
CircuitSeq {
0: Q0 = t(Q0)
1: Q0 = tdg(Q0)
}

CircuitSeq {
}

Considering a total of 2 circuits split into 1 hash values...
Processed 0 hash values that had only 1 circuit sequence, now processing the remaining 1 ones with 2 or more circuit sequences...
Start checking equivalence with different hash...
Solver invoked 0 times to find 0 equivalences with different hash, including 0 out of 0 possible equivalences under phase shift.
1 equivalences found in 1.078999999910593 seconds (solver invoked 1 times for 2 DAGs with 1 different hash values and 1 potential equivalences), output 1 equivalence classes.       
Json saved in 0.0 seconds.
5 transformations verified.
All transformations are verified.

This PR also combines the quartz_root_path in multiple files into a constant variable in utils.h. It also adds helper functions remove_gate_near_end(), get_suffix_seq(), and is_one_of_last_gates().

@xumingkuan xumingkuan merged commit 0934472 into master Jun 12, 2024
2 checks passed
@xumingkuan xumingkuan deleted the verify-opt2 branch June 12, 2024 21:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant