6 #include <unordered_map>
7 #include <unordered_set>
9 #include <boost/range/algorithm/permutation.hpp>
10 #include <boost/range/algorithm/sort.hpp>
14 #include <vcsn/dyn/fwd.hh>
31 template <Automaton Aut1, Automaton Aut2>
58 static_assert(std::is_same<weightset1_t, weightset2_t>{},
59 "are_isomorphic: contexts must be equal");
64 using states_t = std::pair<state1_t, state2_t>;
70 template <Automaton Aut>
74 std::unordered_map<label_t_of<Aut>,
75 std::pair<weight_t_of<Aut>, state_t_of<Aut>>,
80 dout_t<automaton1_t> dout1_;
81 dout_t<automaton2_t> dout2_;
84 template <Automaton Aut>
90 std::unordered_map<weight_t_of<Aut>,
91 std::vector<state_t_of<Aut>>,
94 vcsn::hash<labelset_t_of<Aut>>,
95 vcsn::equal_to<labelset_t_of<Aut>>>>;
96 nout_t<automaton1_t> nout1_;
97 nout_t<automaton2_t> nout2_;
102 using pair_t = std::pair<state1_t, state2_t>;
103 using worklist_t = std::stack<pair_t>;
104 worklist_t worklist_;
107 using s1tos2_t = std::unordered_map<state1_t, state2_t>;
108 using s2tos1_t = std::unordered_map<state2_t, state1_t>;
124 nocounterexample = 2,
126 trivially_different = 3,
138 : response(tag::never_computed)
145 template <Automaton Aut>
146 bool is_sequential_filling(
const Aut& a,
151 const state_t_of<Aut>& src = a->src_of(t);
152 const label_t_of<Aut>& l = a->label_of(t);
153 auto& doutsrc = dout[src];
154 if (doutsrc.find(l) == doutsrc.end())
155 dout[src][l] = {a->weight_of(t), a->dst_of(t)};
168 nout1_[a1_->src_of(t1)][a1_->label_of(t1)][a1_->weight_of(t1)]
169 .emplace_back(a1_->dst_of(t1));
171 nout2_[a2_->src_of(t2)][a2_->label_of(t2)][a2_->weight_of(t2)]
172 .emplace_back(a2_->dst_of(t2));
183 bool trivially_different()
186 if (a1_->num_states() != a2_->num_states())
188 if (a1_->num_transitions() != a2_->num_transitions())
203 are_isomorphicer(
const Aut1 &a1,
const Aut2 &a2)
215 fr_.response = full_response::tag::trivially_different;
218 "are-isomorphic: lhs automaton must be accessible");
220 "are-isomorphic: rhs automaton must be accessible");
225 if (trivially_different())
228 if (is_sequential_filling(a1_, dout1_))
229 if (is_sequential_filling(a2_, dout2_))
230 return get_full_response_sequential();
234 if (is_sequential_filling(a2_, dout2_))
239 return get_full_response_nonsequential();
243 using states1_t = std::vector<state1_t>;
244 using states2_t = std::vector<state2_t>;
250 using class_id = std::size_t;
251 using class_pair_t = std::pair<states1_t, states2_t>;
252 using state_classes_t = std::vector<class_pair_t>;
253 state_classes_t state_classes_;
255 template <Automaton Aut>
256 class_id state_to_class(state_t_of<Aut> s, Aut& a)
263 const auto& ws = *a->weightset();
264 const auto& ls = *a->labelset();
266 using transition_t = std::pair<weight_t_of<Aut>,
270 [&](
const transition_t& t1,
const transition_t& t2)
272 if (ws.less(t1.first, t2.first))
274 else if (ws.less(t2.first, t1.first))
277 return ls.less(t1.second, t2.second);
280 #define HASH_TRANSITIONS(expression, endpoint_getter) \
282 std::unordered_set<state_t_of<Aut>> endpoint_states; \
284 for (auto& t: expression) \
286 tt.emplace_back(transition_t{a->weight_of(t), a->label_of(t)}); \
287 endpoint_states.emplace(a->endpoint_getter(t)); \
289 boost::sort(tt, less); \
290 for (const auto& t: tt) \
292 hash_combine(res, ws.hash(t.first)); \
293 hash_combine(res, ls.hash(t.second)); \
295 hash_combine(res, endpoint_states.size()); \
305 #undef HASH_TRANSITIONS
310 const state_classes_t make_state_classes()
313 std::unordered_map<class_id, std::pair<states1_t, states2_t>> table;
314 for (
auto s1: a1_->all_states())
315 table[state_to_class(s1, a1_)].first.emplace_back(s1);
316 for (
auto s2: a2_->all_states())
317 table[state_to_class(s2, a2_)].second.emplace_back(s2);
323 for (
const auto& c: table)
324 res.emplace_back(std::move(c.second.first), std::move(c.second.second));
326 [](
const class_pair_t& c1,
const class_pair_t& c2)
328 return c1.first.size() > c2.first.size();
347 void print_class_stats(
const state_classes_t& cs,
348 std::ostream& o = std::cerr)
const
350 size_t max = 0,
min = a1_->num_all_states();
351 long double sum = 0.0;
352 for (
const auto& c: cs)
354 max = std::max(max, c.first.size());
356 sum += c.first.size();
358 long state_no = a1_->num_all_states();
359 o <<
"State no: " << state_no <<
'\n'
360 <<
"Class no: " << cs.size() <<
'\n'
361 <<
"* min class size: " << min <<
'\n'
362 <<
"* avg class size: " << sum / cs.size() <<
'\n'
363 <<
"* max class size: " << max <<
'\n';
367 void print_classes(
const state_classes_t& cs,
368 std::ostream& o = std::cerr)
370 for (
const auto& c: cs)
373 for (
const auto& s1: c.first)
376 for (
const auto& s2: c.second)
382 bool is_isomorphism_valid()
386 return is_isomorphism_valid_throwing();
388 catch (
const std::out_of_range&)
393 bool is_isomorphism_valid_throwing()
395 std::unordered_set<state1_t> mss1;
396 std::unordered_set<state2_t> mss2;
397 std::stack<pair_t> worklist;
398 worklist.push({a1_->pre(), a2_->pre()});
399 worklist.push({a1_->post(), a2_->post()});
400 while (! worklist.empty())
402 const auto p = std::move(worklist.top()); worklist.pop();
409 if (fr_.s1tos2_.at(s1) != s2 || fr_.s2tos1_.at(s2) != s1)
411 const bool m1 = (mss1.find(s1) != mss1.end());
412 const bool m2 = (mss2.find(s2) != mss2.end());
423 if ((s1 == a1_->pre()) != (s2 == a2_->pre())
424 || (s1 == a1_->post()) != (s2 == a2_->post()))
427 int t1n = 0, t2n = 0;
428 for (
auto t1:
all_out(a1_, s1))
430 auto d1 = a1_->dst_of(t1);
431 const auto& w1 = a1_->weight_of(t1);
432 const auto& l1 = a1_->label_of(t1);
433 const auto& d2s = nout2_.at(s2).at(l1).at(w1);
434 auto d2 = fr_.s1tos2_.at(d1);
437 worklist.push({d1, d2});
440 for (
auto t2:
all_out(a2_, s2))
442 auto d2 = a2_->dst_of(t2);
443 const auto& w2 = a2_->weight_of(t2);
444 const auto& l2 = a2_->label_of(t2);
445 const auto& d1s = nout1_.at(s1).at(l2).at(w2);
446 auto d1 = fr_.s2tos1_.at(d2);
449 worklist.push({d1, d2});
458 void update_result_isomorphism()
460 for (
const auto& c: state_classes_)
461 for (
size_t i = 0; i < c.first.size(); ++ i)
465 fr_.s1tos2_[s1] = s2;
466 fr_.s2tos1_[s2] = s1;
470 long factorial(
long n)
473 for (
long i = 1; i <= n; ++ i)
480 std::vector<long> class_permutation_max_;
481 std::vector<long> class_permutation_generated_;
483 void initialize_next_class_combination_state()
485 class_permutation_max_.clear();
486 class_permutation_generated_.clear();
487 for (
const auto& c: state_classes_)
489 class_permutation_max_.emplace_back(factorial(c.second.size()) - 1);
490 class_permutation_generated_.emplace_back(0);
498 bool next_class_combination()
507 const int rightmost = int(state_classes_.size()) - 1;
510 if (boost::next_permutation(state_classes_[rightmost].second))
513 ++ class_permutation_generated_[rightmost];
525 assert(class_permutation_generated_[rightmost]
526 == class_permutation_max_[rightmost]);
527 class_permutation_generated_[rightmost] = 0;
529 for (i = rightmost - 1;
531 && class_permutation_generated_[i] == class_permutation_max_[i];
534 boost::next_permutation(state_classes_[i].second);
535 class_permutation_generated_[i] = 0;
541 boost::next_permutation(state_classes_[i].second);
542 ++ class_permutation_generated_[i];
547 get_full_response_nonsequential()
551 state_classes_ = make_state_classes();
555 for (
const auto& c: state_classes_)
556 if (c.first.size() != c.second.size())
558 fr_.response = full_response::tag::nocounterexample;
564 initialize_next_class_combination_state();
567 update_result_isomorphism();
568 if (is_isomorphism_valid())
570 fr_.response = full_response::tag::isomorphic;
574 while (next_class_combination());
577 fr_.response = full_response::tag::nocounterexample;
582 get_full_response_sequential()
586 fr_.response = full_response::tag::counterexample;
588 worklist_.push({a1_->pre(), a2_->pre()});
590 while (! worklist_.empty())
592 const states_t states = worklist_.top(); worklist_.pop();
598 fr_.counterexample = {s1, s2};
605 if (dout1_[s1].
size() != dout2_[s2].
size())
608 for (
const auto& l1_w1dst1 : dout1_[s1])
610 const label1_t& l1 = l1_w1dst1.first;
611 const weight1_t& w1 = l1_w1dst1.second.first;
612 const state1_t& dst1 = l1_w1dst1.second.second;
614 const auto& s2out = dout2_.find(s2);
615 if (s2out == dout2_.cend())
617 const auto& s2outl = s2out->second.find(l1);
618 if (s2outl == s2out->second.cend())
621 state2_t dst2 = s2outl->second.second;
623 if (! weightset_t::equal(w1, w2))
626 const auto& isomorphics_to_dst1 = fr_.s1tos2_.find(dst1);
627 const auto& isomorphics_to_dst2 = fr_.s2tos1_.find(dst2);
629 if (isomorphics_to_dst1 == fr_.s1tos2_.cend())
631 if (isomorphics_to_dst2 == fr_.s2tos1_.cend())
633 fr_.s1tos2_[dst1] = dst2;
634 fr_.s2tos1_[dst2] = dst1;
635 worklist_.push({dst1, dst2});
640 else if (isomorphics_to_dst1 == fr_.s1tos2_.cend()
641 || isomorphics_to_dst1->second != dst2
642 || isomorphics_to_dst2->second != dst1)
646 fr_.response = full_response::tag::isomorphic;
652 const full_response&
r = get_full_response();
653 return r.response == full_response::tag::isomorphic;
659 using origins_t = std::map<state2_t, state1_t>;
665 require(fr_.reponse == full_response::tag::isomorphic,
666 __func__,
": isomorphism-check not successfully performed");
668 for (
const auto& s2s1: fr_.s2tos1_)
669 res[s2s1.first] = s2s1.second;
676 print(
const origins_t& orig, std::ostream& o)
679 <<
" node [shape = box, style = rounded]\n";
680 for (
const auto& p : orig)
683 o <<
" " << p.first - 2
684 <<
" [label = \"" << p.second <<
"\"]\n";
692 template <Automaton Aut1, Automaton Aut2>
707 template <Automaton Aut1, Automaton Aut2>
711 const auto& a1 = aut1->
as<Aut1>();
712 const auto& a2 = aut2->
as<Aut2>();
ATTRIBUTE_PURE bool has(const boost::container::flat_set< Key, Compare, Allocator > &s, const Key &e)
Whether e is member of s.
label_t_of< automaton1_t > label1_t
bool are_isomorphic(const automaton &aut1, const automaton &aut2)
Bridge.
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
This is useful to make hashes with labels or weights as keys without using non-default constructors; ...
state_t_of< automaton1_t > state1_t
void hash_combine(std::size_t &seed, const T &v)
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
std::vector< std::pair< string_t, string_t >> transitions_t
weightset_t_of< automaton2_t > weightset2_t
auto sort(const Aut &a) -> permutation_automaton< Aut >
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
bool are_isomorphic(const Aut1 &a1, const Aut2 &a2)
typename detail::labelset_t_of_impl< base_t< ValueSet >>::type labelset_t_of
label_t_of< automaton2_t > label2_t
context_t_of< automaton1_t > context1_t
weightset_mixin< detail::r_impl > r
Request the unordered_map implementation.
labelset_t_of< context1_t > labelset1_t
auto all_in(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions entering state s.
transition_t_of< automaton2_t > transition2_t
context_t_of< automaton2_t > context2_t
#define HASH_TRANSITIONS(expression, endpoint_getter)
labelset_t_of< context2_t > labelset2_t
typename detail::weightset_t_of_impl< base_t< ValueSet >>::type weightset_t_of
This is useful to make hashes with labels or weights as keys without using non-default constructors; ...
auto all_transitions(const Aut &aut)
All the transition indexes between all states (including pre and post).
weight_t_of< automaton1_t > weight1_t
transition_t_of< automaton1_t > transition1_t
auto(const automaton &aut, bool keep_initials) -> automaton pair_t
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
typename detail::context_t_of_impl< base_t< ValueSet >>::type context_t_of
weightset_t_of< automaton1_t > weightset1_t
std::unordered_set< state_t_of< Aut >> states_t
std::ostream & print(const Aut &aut, std::ostream &out=std::cout, const std::string &fmt="default")
weight_t_of< automaton2_t > weight2_t
bool is_accessible(const Aut &a)
Whether all its states are accessible.
size_t size(const ExpSet &rs, const typename ExpSet::value_t &r)
auto & as()
Extract wrapped typed automaton.
state_t_of< automaton2_t > state2_t
typename detail::label_t_of_impl< base_t< ValueSet >>::type label_t_of