Skip to content

Commit

Permalink
improve bottom_up_reduce(...) to stop earlier if there is no more mer…
Browse files Browse the repository at this point in the history 
…ging possible.
  • Loading branch information
@alan23273850
alan23273850 committed Nov 14, 2024
1 parent d061025 commit ae5117d
Show file tree
Hide file tree
Showing 2 changed files with 77 additions and 58 deletions.
2 changes: 1 addition & 1 deletion include/autoq/aut_description.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ public: // methods
/********************************************/
/* reduce.cc: applying reduction algorithms */
void sim_reduce();
void bottom_up_reduce();
void bottom_up_reduce(int starts_from_depth=INT_MAX);
void union_all_colors_for_a_given_transition();
bool light_reduce_up(); /// lightweight size reduction, done upwards; returns @p true iff the automaton changed
bool light_reduce_up_iter(); /// lightweight upwareds size reduction, iterated until change happens, returns @p true iff the automaton changed
Expand Down
133 changes: 76 additions & 57 deletions src/reduce.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -525,91 +525,110 @@ struct HASH {
}
};
template <typename Symbol>
void AUTOQ::Automata<Symbol>::bottom_up_reduce() {
void AUTOQ::Automata<Symbol>::bottom_up_reduce(int starts_from_depth) {
TopDownTransitions transitions2; // the resulting transitions
auto it = transitions.rbegin(); // global pointer
std::map<State, std::map<Symbol, std::map<StateVector, Tag>>> qfic;
// std::map<std::map<Symbol, std::map<StateVector, Tag>>, State> repr; // 9.9 sec in make test
std::unordered_map<std::map<Symbol, std::map<StateVector, Tag>>, State, HASH<Symbol>> repr; // 9.6 sec in make test
std::map<State, State> rewrite;
bool may_be_merged_furthermore = true;

/* Convert leaf transitions into the new data structure. */
for (; it != transitions.rend(); it++) { // iterate over all leaf transitions
if (it->first.is_internal()) break; // assert leaf transitions
const auto &symbol = it->first.symbol();
const auto &tag = it->first.tag();
for (const auto &out_ins : it->second) {
for (const auto &in : out_ins.second) {
qfic[out_ins.first][symbol][in] |= tag;
if (may_be_merged_furthermore && starts_from_depth >= qubitNum + 1) {
const auto &symbol = it->first.symbol();
const auto &tag = it->first.tag();
for (const auto &out_ins : it->second) {
for (const auto &in : out_ins.second) {
qfic[out_ins.first][symbol][in] |= tag;
}
}
} else {
transitions2.insert(*it);
}
}

/* Construct equivalent classes of top states. */
assert(repr.empty());
for (const auto &top_ : qfic) {
const auto &top = top_.first;
auto it = repr.find(top_.second);
if (it != repr.end()) {
rewrite[top] = it->second;
} else { // create a new class
rewrite[top] = top;
repr[top_.second] = top;
for (const auto &f_ : top_.second) {
const auto &f = f_.first;
for (const auto &ic : f_.second) {
const auto &in = ic.first;
const auto &c = ic.second;
/* Put the non-redundant transitions into the resulting automaton. */
transitions2[SymbolTag(f, c)][top].insert(in);
if (may_be_merged_furthermore && starts_from_depth >= qubitNum + 1) {
may_be_merged_furthermore = false;
assert(repr.empty());
for (const auto &top_ : qfic) {
const auto &top = top_.first;
auto it = repr.find(top_.second);
if (it != repr.end()) {
rewrite[top] = it->second;
may_be_merged_furthermore = true;
} else { // create a new class
rewrite[top] = top;
repr[top_.second] = top;
for (const auto &f_ : top_.second) {
const auto &f = f_.first;
for (const auto &ic : f_.second) {
const auto &in = ic.first;
const auto &c = ic.second;
/* Put the non-redundant transitions into the resulting automaton. */
transitions2[SymbolTag(f, c)][top].insert(in);
}
}
}
}
qfic.clear();
repr.clear();
}
qfic.clear();
repr.clear();

/* Convert internal transitions into the new data structure. */
for (; it != transitions.rend(); it++) { // iterate over all internal transitions
auto qubit = it->first.symbol().qubit();
const auto &symbol = it->first.symbol();
const auto &tag = it->first.tag();
/* Collect all internal transitions at this layer into the new data structure. */
for (const auto &out_ins : it->second) {
const auto &out = out_ins.first;
for (auto in : out_ins.second) {
// rewrite the input states according to the equivalence classes previously computed
for_each(in.begin(), in.end(), [&rewrite](State &s) { s = rewrite.at(s); });
qfic[out][symbol][in] |= tag;
if (may_be_merged_furthermore && starts_from_depth >= qubit) {
const auto &symbol = it->first.symbol();
const auto &tag = it->first.tag();
/* Collect all internal transitions at this layer into the new data structure. */
for (const auto &out_ins : it->second) {
const auto &out = out_ins.first;
for (auto in : out_ins.second) {
// rewrite the input states according to the equivalence classes previously computed
for_each(in.begin(), in.end(), [&rewrite](State &s) {
auto it = rewrite.find(s);
if (it != rewrite.end())
s = it->second;
});
qfic[out][symbol][in] |= tag;
}
}
}
/*******************************************************************************/
if (std::next(it) == transitions.rend()
|| qubit != std::next(it)->first.symbol().qubit()) { // to change layer or already the end of the first layer
rewrite.clear();
/* Construct equivalent classes of top states. */
assert(repr.empty());
for (const auto &top_ : qfic) {
const auto &top = top_.first;
auto it = repr.find(top_.second);
if (it != repr.end()) {
rewrite[top] = it->second;
} else { // create a new class
rewrite[top] = top;
repr[top_.second] = top;
for (const auto &f_ : top_.second) {
const auto &f = f_.first;
for (const auto &ic : f_.second) {
const auto &in = ic.first;
const auto &c = ic.second;
/* Put the non-redundant transitions into the resulting automaton. */
transitions2[SymbolTag(f, c)][top].insert(in);
/*******************************************************************************/
if (std::next(it) == transitions.rend()
|| qubit != std::next(it)->first.symbol().qubit()) { // to change layer or already the end of the first layer
rewrite.clear();
/* Construct equivalent classes of top states. */
may_be_merged_furthermore = false;
assert(repr.empty());
for (const auto &top_ : qfic) {
const auto &top = top_.first;
auto it = repr.find(top_.second);
if (it != repr.end()) {
rewrite[top] = it->second;
may_be_merged_furthermore = true;
} else { // create a new class
rewrite[top] = top;
repr[top_.second] = top;
for (const auto &f_ : top_.second) {
const auto &f = f_.first;
for (const auto &ic : f_.second) {
const auto &in = ic.first;
const auto &c = ic.second;
/* Put the non-redundant transitions into the resulting automaton. */
transitions2[SymbolTag(f, c)][top].insert(in);
}
}
}
}
qfic.clear();
repr.clear();
}
qfic.clear();
repr.clear();
} else {
transitions2.insert(*it);
}
}
transitions = transitions2;
Expand Down

0 comments on commit ae5117d

Please sign in to comment.