Vcsn  2.3
Be Rational
are-equivalent.hh
Go to the documentation of this file.
1 #pragma once
2 
3 #include <vcsn/algos/accessible.hh> // is_useless
5 #include <vcsn/algos/complete.hh>
8 #include <vcsn/algos/weight.hh>
9 #include <vcsn/algos/letterize.hh> // rea
10 #include <vcsn/algos/conjunction.hh> // conjunction
11 #include <vcsn/algos/reduce.hh>
12 #include <vcsn/algos/strip.hh>
13 #include <vcsn/algos/add.hh>
14 #include <vcsn/dyn/automaton.hh>
15 #include <vcsn/dyn/value.hh>
16 
17 namespace vcsn
18 {
19 
20  /*---------------------------------------.
21  | are_equivalent(automaton, automaton). |
22  `---------------------------------------*/
23 
25  template <Automaton Aut1, Automaton Aut2>
26  auto
27  are_equivalent(const Aut1& a1, const Aut2& a2)
28  -> std::enable_if_t<(std::is_same<weightset_t_of<Aut1>, b>::value
29  && std::is_same<weightset_t_of<Aut2>, b>::value),
30  bool>
31  {
32  const auto& l = realtime(a1);
33  const auto& r = realtime(a2);
34  return (is_useless(difference(l, r))
35  && is_useless(difference(r, l)));
36  }
37 
38 
40  template <Automaton Aut1, Automaton Aut2>
41  auto
42  are_equivalent(const Aut1& a1, const Aut2& a2)
43  -> decltype((std::enable_if_t<!std::is_same<weightset_t_of<Aut1>, b>()>(),
44  a2->weightset()->sub(a2->weightset()->zero(),
45  a2->weightset()->one()),
46  true))
47  {
48  const auto& ws2 = *a2->weightset();
49  const auto& l = realtime(a1);
50  const auto& r = realtime(a2);
51  // d = l + -r.
52  auto d = add(l,
53  lweight(ws2.sub(ws2.zero(), ws2.one()),
54  r));
55  return is_empty(reduce(d));
56  }
57 
58 
59  namespace dyn
60  {
61  namespace detail
62  {
64  template <Automaton Aut1, Automaton Aut2>
65  bool
66  are_equivalent(const automaton& aut1, const automaton& aut2)
67  {
68  const auto& a1 = aut1->as<Aut1>();
69  const auto& a2 = aut2->as<Aut2>();
71  }
72  }
73  }
74 
75 
76  /*-----------------------------------------.
77  | are_equivalent(expression, expression). |
78  `-----------------------------------------*/
79 
81  template <typename ExpSet1, typename ExpSet2>
82  auto
83  are_equivalent(const ExpSet1& rs1,
84  const typename ExpSet1::value_t r1,
85  const ExpSet2& rs2,
86  const typename ExpSet2::value_t r2)
87  -> bool
88  {
89  // We use derived-term because it supports all our operators.
90  // FIXME: bench to see if standard would not be a better bet in
91  // the other cases.
92  return are_equivalent(strip(derived_term(rs1, r1)),
93  strip(derived_term(rs2, r2)));
94  }
95 
96 
97  namespace dyn
98  {
99  namespace detail
100  {
102  template <typename ExpSet1, typename ExpSet2>
103  bool
105  {
106  const auto& l = r1->as<ExpSet1>();
107  const auto& r = r2->as<ExpSet2>();
108  return ::vcsn::are_equivalent(l.valueset(), l.value(),
109  r.valueset(), r.value());
110  }
111  }
112  }
113 
114 
115  /*-----------------------------------.
116  | difference(automaton, automaton). |
117  `-----------------------------------*/
118 
120  template <Automaton Lhs, Automaton Rhs>
121  fresh_automaton_t_of<Lhs>
122  difference(const Lhs& lhs, const Rhs& rhs)
123  {
124  // Meet complement()'s requirements.
125  auto r = strip(rhs);
126  if (!is_deterministic(r))
128  else if (!is_complete(r))
129  r = complete(r);
130  return strip(conjunction(lhs, complement(r)));
131  }
132 
133  namespace dyn
134  {
135  namespace detail
136  {
138  template <Automaton Lhs, Automaton Rhs>
139  automaton
140  difference(const automaton& lhs, const automaton& rhs)
141  {
142  const auto& l = lhs->as<Lhs>();
143  const auto& r = rhs->as<Rhs>();
145  }
146  }
147  }
148 
149  /*--------------------------------------.
150  | difference(expression, expression). |
151  `--------------------------------------*/
152 
154  template <typename ExpSet>
155  typename ExpSet::value_t
156  difference(const ExpSet& rs,
157  const typename ExpSet::value_t& lhs,
158  const typename ExpSet::value_t& rhs)
159  {
160  return rs.conjunction(lhs, rs.complement(rhs));
161  }
162 
163  namespace dyn
164  {
165  namespace detail
166  {
168  template <typename ExpSetLhs, typename ExpSetRhs>
169  expression
171  {
172  const auto& l = lhs->as<ExpSetLhs>();
173  const auto& r = rhs->as<ExpSetLhs>();
174  return {l.valueset(), ::vcsn::difference(l.valueset(),
175  l.value(),
176  r.value())};
177  }
178  }
179  }
180 }
auto complete(const Aut &aut) -> decltype(::vcsn::copy(aut))
Definition: complete.hh:61
bool is_complete(const Aut &aut)
Whether aut is complete.
Definition: is-complete.hh:13
automaton difference(const automaton &lhs, const automaton &rhs)
Bridge.
bool is_empty(const Aut &a) ATTRIBUTE_PURE
Whether has no states.
Definition: accessible.hh:192
bool is_useless(const Aut &a)
Whether all no state is useful.
Definition: accessible.hh:168
ExpSet::value_t difference(const ExpSet &rs, const typename ExpSet::value_t &lhs, const typename ExpSet::value_t &rhs)
Difference of expressions.
expression difference_expression(const expression &lhs, const expression &rhs)
Bridge (difference).
bool is_deterministic(const Aut &aut, state_t_of< Aut > s)
Whether state s is deterministic in aut.
auto rs
Definition: lift.hh:152
auto add(const Aut1 &lhs, const Aut2 &rhs, deterministic_tag)
Definition: add.hh:71
Definition: a-star.hh:8
A dyn automaton.
Definition: automaton.hh:17
auto determinize(const Aut &a, Tag={}, bool_constant< Lazy >={})
Definition: determinize.hh:247
auto lweight(const weight_t_of< Aut > &w, const Aut &aut, Tag tag={}) -> fresh_automaton_t_of< Aut >
Left-multiplication of an automaton by a weight.
Definition: weight.hh:126
bool are_equivalent(const automaton &aut1, const automaton &aut2)
Bridge.
bool are_equivalent_expression(const expression &r1, const expression &r2)
Bridge (are_equivalent).
std::enable_if_t< labelset_t_of< ExpSet >::is_free(), expression_automaton< mutable_automaton< typename ExpSet::context_t > > > derived_term(const ExpSet &rs, const typename ExpSet::value_t &r, const std::string &algo="auto")
The derived-term automaton, for free labelsets.
auto are_equivalent(const ExpSet1 &rs1, const typename ExpSet1::value_t r1, const ExpSet2 &rs2, const typename ExpSet2::value_t r2) -> bool
Check equivalence between two expressions.
auto conjunction(const Aut &aut, to exp) -> fresh_automaton_t_of< Aut >
Repeated conjunction of a automaton.
Definition: conjunction.hh:947
auto realtime(const Aut &aut) -> decltype(proper(::vcsn::letterize(aut)))
Split the word transitions in the input automaton into letter ones, and remove the spontaneous transi...
Definition: letterize.hh:219
auto reduce(const Aut &input) -> decltype(copy(input))
Definition: reduce.hh:608
fresh_automaton_t_of< Lhs > difference(const Lhs &lhs, const Rhs &rhs)
An automaton that computes weights of lhs, but not by rhs.
weightset_mixin< detail::b_impl > b
Definition: fwd.hh:48
auto & as()
Extract wrapped typed automaton.
Definition: automaton.hh:37
auto strip(const Aut &aut)
Remove (all) the decorations from a decorated automaton.
Definition: strip.hh:34
Provide a variadic mul on top of a binary mul(), and one().
Definition: fwd.hh:46
auto are_equivalent(const Aut1 &a1, const Aut2 &a2) -> std::enable_if_t<(std::is_same< weightset_t_of< Aut1 >, b >::value &&std::is_same< weightset_t_of< Aut2 >, b >::value), bool >
Check equivalence between Boolean automata on a free labelset.
value_impl< detail::expression_tag > expression
Definition: fwd.hh:25
auto complement(const Aut &aut) -> decltype(copy(aut))
Definition: complement.hh:48
weightset_mixin< detail::r_impl > r
Definition: fwd.hh:54