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().
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:This PR also combines the
quartz_root_pathin multiple files into a constant variable inutils.h. It also adds helper functionsremove_gate_near_end(),get_suffix_seq(), andis_one_of_last_gates().