diff --git a/algorithms/qubit swapping.JPG b/algorithms/qubit swapping.JPG new file mode 100644 index 0000000000..b9968ba833 Binary files /dev/null and b/algorithms/qubit swapping.JPG differ diff --git a/include/autoq/aut_description.hh b/include/autoq/aut_description.hh index ada67acca9..b3b21fb0ff 100644 --- a/include/autoq/aut_description.hh +++ b/include/autoq/aut_description.hh @@ -231,6 +231,8 @@ public: #pragma GCC diagnostic ignored "-Weffc++" Automata operator||(const Automata &o) const; // use the logical OR operator to denote "union" #pragma GCC diagnostic pop + void SwapDown(int q); + void SwapUp(int q); /**************************************************/ }; diff --git a/src/general.cc b/src/general.cc index 57eab66130..6f547e3ece 100644 --- a/src/general.cc +++ b/src/general.cc @@ -174,6 +174,79 @@ AUTOQ::Automata AUTOQ::Automata::operator||(const Automata +void AUTOQ::Automata::SwapDown(int q) { + assert(!hasLoop); + TopDownTransitions old_transitions_at_q; + std::map>> old_transitions_at_q_plus_1; + + // Step 1. Delete all old transitions at level (q) and (q+1). + Symbol sym_at_q, sym_at_q_plus_1; + auto transitions_copy = transitions; + for (const auto &tr : transitions_copy) { + if (tr.first.symbol().is_internal()) { + if (tr.first.symbol().qubit() == q) { + transitions.erase(tr.first); + old_transitions_at_q.insert(tr); + sym_at_q = tr.first.symbol(); // save the symbol at level (q) + } + if (tr.first.symbol().qubit() == q+1) { + transitions.erase(tr.first); + for (const auto &out_ins : tr.second) { + for (const auto &in : out_ins.second) { + old_transitions_at_q_plus_1[out_ins.first].insert({tr.first.tag(), in}); + } + } + sym_at_q_plus_1 = tr.first.symbol(); // save the symbol at level (q+1) + } + if (tr.first.symbol().qubit() >= q+2) { + break; + } + } else { + break; + } + } + + // Step 2. Rewrite the new transitions at level (q) and (q+1). + std::set states_has_appeared; + for (const auto &tr : old_transitions_at_q) { + for (const auto &out_ins : tr.second) { + for (const auto &in : out_ins.second) { + assert(in.size() == 2); + auto leftChild = in.at(0); + auto rightChild = in.at(1); + if (states_has_appeared.contains(in.at(0))) leftChild = stateNum++; + if (states_has_appeared.contains(in.at(1))) rightChild = stateNum++; + transitions[SymbolTag(sym_at_q, tr.first.tag())][out_ins.first].insert({leftChild, rightChild}); // rewrite at level (q) + states_has_appeared.insert(in.at(0)); + states_has_appeared.insert(in.at(1)); + for (const auto &c1in1 : old_transitions_at_q_plus_1.at(in.at(0))) { + const auto &c1 = c1in1.first; + const auto &in1 = c1in1.second; + for (const auto &c2in2 : old_transitions_at_q_plus_1.at(in.at(1))) { + const auto &c2 = c2in2.first; + const auto &in2 = c2in2.second; + const auto c = c1 & c2; + if (c) { + transitions[SymbolTag(sym_at_q_plus_1, c)][leftChild].insert({in1.at(0), in2.at(0)}); // rewrite at level (q+1) + transitions[SymbolTag(sym_at_q_plus_1, c)][rightChild].insert({in1.at(1), in2.at(1)}); // rewrite at level (q+1) + } + } + } + } + } + } + auto start = std::chrono::steady_clock::now(); + bottom_up_reduce(q+1); + auto duration = std::chrono::steady_clock::now() - start; + total_reduce_time += duration; + if (opLog) std::cout << __FUNCTION__ << ":" << stateNum << " states " << count_transitions() << " transitions\n"; +} +template +void AUTOQ::Automata::SwapUp(int q) { + SwapDown(q-1); +} + // https://bytefreaks.net/programming-2/c/c-undefined-reference-to-templated-class-function template struct AUTOQ::Automata; template struct AUTOQ::Automata; diff --git a/unit_tests/explicit_tree_aut_test.cc b/unit_tests/explicit_tree_aut_test.cc index af221bf189..09a2657031 100644 --- a/unit_tests/explicit_tree_aut_test.cc +++ b/unit_tests/explicit_tree_aut_test.cc @@ -1343,4 +1343,123 @@ BOOST_AUTO_TEST_CASE(benchmarks_BVBugSym) BOOST_REQUIRE_MESSAGE(spec == spec2, folder + " failed!"); // ensure the compilation from .hsl to .lsta is correct } +// BOOST_AUTO_TEST_CASE(star_notation_and_reordering) +// { +// std::string sss(__FILE__); +// std::string benchmarks = sss.substr(0, sss.find_last_of("\\/")) + "/../unit_tests/testcase/general_star_example/"; +// for (const auto &entry : fs::directory_iterator(benchmarks)) { +// if (!entry.is_directory()) continue; +// auto folder = entry.path().string(); +// //auto aut = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "/pre.lsta"); +// auto aut2 = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "/pre.hsl"); +// //BOOST_REQUIRE_MESSAGE(aut == aut2, folder + " failed!"); // ensure the compilation from .hsl to .lsta is correct +// //auto spec = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "/post.lsta"); +// //BOOST_REQUIRE_MESSAGE(aut <= spec, folder + " failed!"); +// auto spec2 = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "/post.hsl"); +// //aut2.execute(folder + "/circuit.qasm"); +// BOOST_REQUIRE_MESSAGE(aut2 == spec2, folder + " failed!"); +// //BOOST_REQUIRE_MESSAGE(aut2 <= spec2, folder + " failed!"); +// //BOOST_REQUIRE_MESSAGE(spec == spec2, folder + " failed!"); // ensure the compilation from .hsl to .lsta is correct +// } +// } + +BOOST_AUTO_TEST_CASE(qubit_reordering) +{ + for (int z=2; z<=5; z++) { + AUTOQ::TreeAutomata spec; + spec.qubitNum = z; + int pow_of_two = 1; + AUTOQ::TreeAutomata::State state_counter = 0; + for (int level=1; level<=z; level++) { + for (int i=0; i=2; j--) + aut.SwapUp(j); + // aut.print_language(); + // spec.print_language(); + BOOST_REQUIRE_MESSAGE(aut == spec, __LINE__); + } + for (int z=2; z<=6; z+=2) { + AUTOQ::TreeAutomata spec; + spec.qubitNum = z; + for (int level=1; level<=z; level++) { + if (level >= 2) + spec.transitions[{level, 0b11}][2*level - 3].insert({2*level - 1, 2*level - 1}); + if (level % 2) + spec.transitions[{level, 0b01}][2*level - 2].insert({2*level - 1, 2*level}); + spec.transitions[{level, 0b10}][2*level - 2].insert({2*level, 2*level - 1}); + } + spec.transitions[AUTOQ::TreeAutomata::SymbolTag(AUTOQ::Symbol::Concrete(Complex::One()), 1)][2*z].insert({{}}); + spec.transitions[AUTOQ::TreeAutomata::SymbolTag(AUTOQ::Symbol::Concrete(Complex::Zero()), 1)][2*z - 1].insert({{}}); + spec.finalStates.push_back(0); + spec.stateNum = 2*z + 1; + /************************/ + AUTOQ::TreeAutomata spec2; + spec2.qubitNum = z; + for (int level=1; level<=z; level++) { + if (level >= 2) + spec2.transitions[{level, 0b11}][2*level - 3].insert({2*level - 1, 2*level - 1}); + if ((level+1) % 2) + spec2.transitions[{level, 0b01}][2*level - 2].insert({2*level - 1, 2*level}); + spec2.transitions[{level, 0b10}][2*level - 2].insert({2*level, 2*level - 1}); + } + spec2.transitions[AUTOQ::TreeAutomata::SymbolTag(AUTOQ::Symbol::Concrete(Complex::One()), 1)][2*z].insert({{}}); + spec2.transitions[AUTOQ::TreeAutomata::SymbolTag(AUTOQ::Symbol::Concrete(Complex::Zero()), 1)][2*z - 1].insert({{}}); + spec2.finalStates.push_back(0); + spec2.stateNum = 2*z + 1; + /*****************************/ + AUTOQ::TreeAutomata aut = spec; + for (int j=1; j<=z; j+=2) + aut.SwapDown(j); + // aut.print_language(); + // spec2.print_language(); + BOOST_REQUIRE_MESSAGE(aut == spec2, __LINE__); + /*****************************/ + aut = spec2; + for (int j=1; j<=z; j+=2) + aut.SwapDown(j); + // aut.print_language(); + // spec.print_language(); + BOOST_REQUIRE_MESSAGE(aut == spec, __LINE__); + } +} + // BOOST_AUTO_TEST_SUITE_END()