37 namespace awali {
namespace sttc
43 template <
typename Context>
49 require_weightset_commutativity();
52 template <
typename Context>
55 require(identities_ != identities_t::series
57 "series (currently) depend on weightset commutativity");
61 template <typename Context> \
64 ratexpset_impl<Context>
69 return "ratexpset<" + context_t::sname() +
'>';
72 DEFINE::vname(
bool full)
const
79 case identities_t::trivial:
80 case identities_t::associativity:
83 case identities_t::series:
98 DEFINE::make(std::istream& is)
102 eat(is,
"ratexpset<");
103 auto ctx = Context::make(is);
106 if (is.peek() ==
'(')
115 DEFINE::open(
bool o)
const
118 return this->labelset()->open(o);
131 DEFINE::is_series() const ->
bool
133 return identities_ == identities_t::series;
138 return ctx_.labelset();
143 return ctx_.weightset();
149 if (labelset_t::is_one(v))
151 return std::make_shared<atom_t>(v);
157 return std::make_shared<zero_t>();
163 return std::make_shared<one_t>();
166 template <
typename Context>
167 template <exp::type_t Type>
173 switch(identities_) {
174 case identities_t::trivial :
178 auto variadic = std::dynamic_pointer_cast<const variadic_t<Type>>(v);
186 template <
typename Context>
187 template <exp::type_t Type>
194 gather<Type>(res, l);
195 gather<Type>(res,
r);
210 else if (is_series())
211 res = add_nonzero_series_(l,
r);
213 res = std::make_shared<sum_t>(gather<type_t::sum>(l,
r));
217 DEFINE::less_than_ignoring_weight_(value_t l, value_t
r)
const
220 return less_than(unwrap_possible_lweight_(l), unwrap_possible_lweight_(
r));
223 DEFINE::remove_from_sum_series_(ratexps_t addends,
224 typename ratexps_t::iterator i)
const
227 switch (addends.size())
238 return std::make_shared<sum_t>(std::move(addends));
242 DEFINE::insert_in_sum_series_(
const sum_t& addends, value_t r)
const
247 ratexps_t
copy = addends.subs();
248 assert(
copy.size() > 0);
252 auto rw = possibly_implicit_lweight_(r);
253 auto rn = unwrap_possible_lweight_(r);
255 [
this] (value_t left, value_t right)
257 return less_than_ignoring_weight_(left, right);
259 const auto i = std::lower_bound(
copy.begin(),
copy.end(), rn, closure);
261 &&
equals(unwrap_possible_lweight_(*i), rn))
264 const weight_t& iw = possibly_implicit_lweight_(*i);
267 return remove_from_sum_series_(std::move(
copy), i);
274 return std::make_shared<sum_t>(std::move(
copy));
277 DEFINE::merge_sum_series_(
const sum_t& addends1, value_t aa2)
const
281 for (
const auto& e: addends1)
282 res = add_nonzero_series_(res, e);
286 DEFINE::add_nonzero_series_(value_t l, value_t r)
const
289 assert(! is_zero(r));
292 const auto ls = down_pointer_cast<const sum_t>(l);
295 return merge_sum_series_(*ls, r);
297 return insert_in_sum_series_(*ls, r);
302 return add_nonzero_series_(r, l);
305 auto ls = std::make_shared<sum_t>(ratexps_t{l});
306 return insert_in_sum_series_(*ls, r);
310 DEFINE::type_ignoring_lweight_(value_t e)
const
313 return unwrap_possible_lweight_(e)->type();
316 DEFINE::possibly_implicit_lweight_(value_t e)
const
319 if (
auto lw = std::dynamic_pointer_cast<const lweight_t>(e))
325 DEFINE::unwrap_possible_lweight_(value_t e)
const
328 if (
auto lw = std::dynamic_pointer_cast<const lweight_t>(e))
338 return mul_series_(l,
r);
340 return mul_expressions_(l,
r);
343 DEFINE::mul_expressions_(value_t l, value_t
r)
const
346 return mul_(l,
r,
false);
349 DEFINE::mul_series_(value_t l, value_t
r)
const
352 return mul_(l,
r,
true);
355 DEFINE::mul_(value_t l, value_t r,
bool series)
const
358 value_t res =
nullptr;
367 res = rmul(l, possibly_implicit_lweight_(r));
370 res = lmul(possibly_implicit_lweight_(l), r);
373 res = nontrivial_mul_series_(l, r);
375 res = nontrivial_mul_expressions_(l, r);
379 DEFINE::is_unweighted_nonsum_(value_t v)
const
394 DEFINE::is_nonsum_(value_t v)
const
397 return is_unweighted_nonsum_(unwrap_possible_lweight_(v));
403 return mul_atoms_(a, b,
typename std::is_same<kind_t, labels_are_words>::type{});
406 DEFINE::mul_atoms_(
const label_t& a,
const label_t& b, std::true_type)
const
409 return std::make_shared<atom_t>(labelset()->concat(a, b));
412 DEFINE::mul_atoms_(
const label_t& a,
const label_t& b, std::false_type)
const
415 return std::make_shared<prod_t>(values_t{std::make_shared<atom_t>(a),
416 std::make_shared<atom_t>(b)});
419 DEFINE::mul_unweighted_nontrivial_products_(value_t a, value_t b)
const
422 assert(! is_zero(a));
423 assert(! is_zero(b));
426 assert(! std::dynamic_pointer_cast<const lweight_t>(a));
427 assert(! std::dynamic_pointer_cast<const lweight_t>(b));
436 DEFINE::mul_products_(value_t a, value_t b)
const
439 assert(! is_zero(a));
440 assert(! is_zero(b));
441 value_t na = unwrap_possible_lweight_(a), nb = unwrap_possible_lweight_(b);
446 return lmul(possibly_implicit_lweight_(a), b);
451 return lmul(
weightset()->mul(possibly_implicit_lweight_(a),
452 possibly_implicit_lweight_(b)),
455 return lmul(
weightset()->mul(possibly_implicit_lweight_(a),
456 possibly_implicit_lweight_(b)),
457 mul_unweighted_nontrivial_products_(na, nb));
462 DEFINE::nontrivial_mul_expressions_(value_t l, value_t r)
const
465 return std::make_shared<prod_t>(gather<type_t::prod>(l, r));
468 DEFINE::nontrivial_mul_series_(value_t l, value_t r)
const
474 const auto& lt = type_ignoring_lweight_(l), rt = type_ignoring_lweight_(r);
475 value_t res =
zero();
478 for (
const auto& la: *down_pointer_cast<const sum_t>(l))
479 res = add(res, mul(la, r));
483 for (
const auto& ra: *down_pointer_cast<const sum_t>(r))
484 res = add(res, mul(l, ra));
487 if (is_nonsum_(l) && is_nonsum_(r))
488 return mul_products_(l, r);
491 weight_t lw = possibly_implicit_lweight_(l)
492 , rw = possibly_implicit_lweight_(r);
493 value_t nl = unwrap_possible_lweight_(l)
494 , nr = unwrap_possible_lweight_(r);
496 std::make_shared<prod_t>(gather<type_t::prod>(nl, nr)));
516 res = lmul(
weightset()->mul(possibly_implicit_lweight_(l),
517 possibly_implicit_lweight_(
r)),
523 auto lhs = down_pointer_cast<const atom_t>(unwrap_possible_lweight_(l))->value();
524 auto rhs = down_pointer_cast<const atom_t>(unwrap_possible_lweight_(
r))->value();
525 if (labelset()->
equals(lhs, rhs))
526 res = rmul(l, possibly_implicit_lweight_(
r));
531 else if ( (type_ignoring_lweight_(l) ==
type_t::one
538 res = std::make_shared<conjunction_t>(gather<type_t::conjunction>(l,
r));
556 res = std::make_shared<ldiv_t>(
ratexps_t{l,
r});
584 res = std::make_shared<shuffle_t>(gather<type_t::shuffle>(l,
r));
591 return concat_(l,
r,
typename std::is_same<kind_t, labels_are_words>::type{});
595 DEFINE::concat_(value_t l, value_t
r, std::false_type)
const
598 return mul_expressions_(l,
r);
602 DEFINE::concat_(value_t l, value_t
r, std::true_type)
const
614 gather<type_t::prod>(ls, l);
617 gather<type_t::prod>(rs,
r);
622 auto lhs = std::dynamic_pointer_cast<const atom_t>(ls.back());
623 auto rhs = std::dynamic_pointer_cast<const atom_t>(rs.front());
624 ls.back() = atom(labelset()->concat(lhs->value(), rhs->value()));
625 ls.insert(ls.end(), rs.begin() + 1, rs.end());
628 ls.insert(ls.end(), rs.begin(), rs.end());
632 return std::make_shared<prod_t>(ls);
636 return mul_expressions_(l, r);
648 value_t res = std::make_shared<star_t>(e);
650 "star argument ", e,
" not starrable");
660 if (
auto wl = std::dynamic_pointer_cast<const lweight_t>(e))
662 else if (
auto wr = std::dynamic_pointer_cast<const rweight_t>(e))
665 return std::make_shared<complement_t>(e);
680 else if (
auto l = std::dynamic_pointer_cast<const atom_t>(e))
684 res = std::make_shared<transposition_t>(e);
702 else if (
auto lw = std::dynamic_pointer_cast<const lweight_t>(e))
703 return lmul(
weightset()->mul(w, lw->weight()), lw->sub());
705 else if (is_series())
706 return nontrivial_lmul_series_(w, e);
708 return nontrivial_lmul_expression_(w, e);
711 DEFINE::nontrivial_lmul_expression_(
const weight_t& w, value_t s)
const
714 return std::make_shared<lweight_t>(w, s);
717 DEFINE::nontrivial_lmul_series_(
const weight_t& w, value_t s)
const
721 return nontrivial_lmul_expression_(w, s);
724 const auto& ss = down_pointer_cast<const sum_t>(s);
729 addends.emplace_back(lmul(w, a));
730 return std::make_shared<sum_t>(std::move(addends));
747 else if (
auto lw = std::dynamic_pointer_cast<const lweight_t>(e))
748 return lmul(lw->weight(), rmul(lw->sub(), w));
750 else if (
auto rw = std::dynamic_pointer_cast<const rweight_t>(e))
751 return rmul(rw->sub(),
weightset()->mul(rw->weight(), w));
753 else if (is_series())
754 return nontrivial_rmul_series_(e, w);
756 return nontrivial_rmul_expression_(e, w);
759 DEFINE::nontrivial_rmul_expression_(value_t e,
const weight_t& w)
const
762 return std::make_shared<rweight_t>(w, e);
765 DEFINE::nontrivial_rmul_series_(value_t s,
const weight_t& w)
const
769 return nontrivial_rmul_expression_(s, w);
772 const auto& ss = down_pointer_cast<const sum_t>(s);
776 value_t res =
zero();
778 res = add(res, rmul(a, w));
786 std::ostringstream o;
811 size_t l = sizer(lhs),
r = sizer(rhs);
827 if(lhs.get()==rhs.get())
846 return copy(rs, *
this, v);
849 template <
typename Context>
850 template <
typename GenSet>
857 return atom(labelset()->
conv(ls, v));
886 template <
typename Context>
887 template <
typename Ctx2>
894 return copy(rs, *
this, v);
906 const std::string& )
const
919 template <
typename Context>
920 template <
typename... Args>
926 return letter_class_<labelset_t>(std::forward<Args>(args)...,
927 std::is_same<labelset_t, oneset>{});
930 template <
typename Context>
931 template <
typename LabelSet_>
935 (std::set<
std::pair<
typename LabelSet_::letter_t,
936 typename LabelSet_::letter_t>> ccs,
938 std::false_type)
const
942 auto gens = labelset()->genset();
949 for (
const auto& cc: ccs)
951 auto i =
std::find(std::begin(gens), std::end(gens), cc.first);
952 auto end =
std::find(i, std::end(gens), cc.second);
954 "invalid letter interval: ",
955 format(*labelset(), labelset()->
value(std::get<0>(cc))),
957 format(*labelset(), labelset()->
value(std::get<1>(cc))));
958 for (end = std::next(end); i != end; ++i)
959 res = add(res,
atom(labelset()->
value(*i)));
962 else if (ccs.empty())
964 res = add(res,
atom(labelset()->
value(l)));
969 std::set<typename LabelSet_::letter_t> accepted;
970 for (
const auto& cc: ccs)
972 auto i =
std::find(std::begin(gens), std::end(gens), cc.first);
973 auto end =
std::find(i, std::end(gens), cc.second);
975 "invalid letter interval: ",
976 format(*labelset(), labelset()->
value(std::get<0>(cc))),
978 format(*labelset(), labelset()->
value(std::get<1>(cc))));
979 for (end = std::next(end); i != end; ++i)
980 accepted.emplace(*i);
983 if (!
has(accepted,
c))
987 "invalid empty letter class");
991 template <
typename Context>
992 template <
typename LabelSet_,
typename... Args>
996 std::true_type)
const
Definition: qfraction.hh:26
The Boolean semring.
Definition: b.hh:38
bool value_t
Definition: b.hh:56
The semiring of complex numbers.
Definition: c.hh:44
carries the algebraic settings of automata
Definition: context.hh:40
std::string vname(bool full=true) const
Definition: context.hh:137
Definition: transpose.hh:36
Implementation of labels are letters.
Definition: letterset.hh:43
letter_t value_t
Definition: letterset.hh:53
The semiring of rational numbers.
Definition: q.hh:42
The semiring of floating Numbers.
Definition: r.hh:35
double value_t
Definition: r.hh:56
Definition: ratexp.hh:280
Definition: equal_visit.hh:34
rat::type_t type_t
The possible types of ratexps.
Definition: ratexp.hh:43
Definition: less_than.hh:34
A typed ratexp set.
Definition: ratexpset.hh:46
typename node_t::value_t value_t
The value this is a set of: typeful shared pointers.
Definition: ratexpset.hh:93
typename context_t::weightset_ptr weightset_ptr
Definition: ratexpset.hh:54
value_t letter_class(Args &&... chars) const
A ratexp matching one character amongst chars.
label_t_of< context_t > label_t
Definition: ratexpset.hh:55
typename context_t::labelset_ptr labelset_ptr
Definition: ratexpset.hh:53
Context context_t
Definition: ratexpset.hh:49
ratexpset_impl(const context_t &ctx, identities_t identities)
Constructor.
Definition: ratexpset.hxx:44
value_t conv(std::istream &is) const
Definition: ratexpset.hxx:897
typename node_t::ratexps_t ratexps_t
Definition: ratexpset.hh:90
typename weightset_t::value_t weight_t
Definition: ratexpset.hh:56
An inner node with multiple children.
Definition: ratexp.hh:115
The semiring of Integers.
Definition: z.hh:35
int value_t
Definition: z.hh:56
weightset_description weightset(const std::string &k)
any_t label_t
Type for (transition) labels; it is an alias to any_t since its precise type depends on the weightset...
Definition: typedefs.hh:48
any_t weight_t
Type for (transition) weights; it is an alias to any_t since the its precise type depends on the weig...
Definition: typedefs.hh:61
automaton_t transpose(automaton_t aut, options_t opts={})
Transposes aut or returns a transposed copy of aut.
std::ostream & print(const std::tuple< Args... > &args, std::ostream &o)
Definition: tuple.hh:254
static constexpr TOP< void > value
Definition: priority.hh:93
ATTRIBUTE_PURE auto find(const std::vector< T, Alloc > &s, const T &e) -> typename std::vector< T, Alloc >::const_iterator
Convenience wrapper around std::find.
Definition: vector.hh:81
bool has(const std::map< Key, Value, Compare, Alloc > &s, const Key &e)
Definition: map.hh:53
unary< type_t::star, Label, Weight > star
Definition: fwd.hh:129
constant< type_t::zero, Label, Weight > zero
Definition: fwd.hh:113
variadic< type_t::ldiv, Label, Weight > ldiv
Definition: fwd.hh:148
variadic< type_t::conjunction, Label, Weight > conjunction
Definition: fwd.hh:145
variadic< type_t::shuffle, Label, Weight > shuffle
Definition: fwd.hh:151
OutRatExpSet::value_t copy(const InRatExpSet &in_rs, const OutRatExpSet &out_rs, const typename InRatExpSet::value_t &v)
Definition: copy.hh:147
unary< type_t::transposition, Label, Weight > transposition
Definition: fwd.hh:132
constant< type_t::one, Label, Weight > one
Definition: fwd.hh:116
unary< type_t::complement, Label, Weight > complement
Definition: fwd.hh:126
identities
A ratexpset can implement several different sets of identities on expressions.
Definition: identities.hh:32
@ trivial
Trivial identities only.
std::string to_string(identities i)
void eat(std::istream &is, char c)
Check lookahead character and advance.
Definition: stream.hh:62
RatExpSet::ratexp_t less_than(const RatExpSet &rs, const typename RatExpSet::ratexp_t &v)
Definition: less_than.hh:166
RatExpSet::ratexp_t equals(const RatExpSet &rs, const typename RatExpSet::ratexp_t &v)
Definition: equal_visit.hh:153
RatExpSet::ratexp_t parse_exp(const RatExpSet &ratexpset, const std::string &s, bool check_complete=true, bool strict_alphabet=true)
parser of rational expressions
Definition: exp_parser.hh:438
AutOut transpose(Aut &aut, bool keep_history=true)
Definition: transpose.hh:79
auto format(const ValueSet &vs, const typename ValueSet::value_t &v, Args &&... args) -> std::string
Format v via vs.print.
Definition: stream.hh:109
bool is_valid(const Aut &aut)
Tests if aut is valid.
Definition: is_valid.hh:162
std::ostream & print(const RatExpSet &rs, const typename RatExpSet::ratexp_t &e, std::ostream &o, bool with_dot=false)
Definition: print_exp.hh:201
void require(bool b, Args &&... args)
If b is not verified, raise an error with args as message.
Definition: raise.hh:55
pair_automaton< Aut > pair(const Aut &aut, bool keep_initials=false)
Definition: synchronizing_word.hh:266
auto conv(const ValueSet &vs, const std::string &str, Args &&... args) -> decltype(vs.conv(std::declval< std::istream & >(), std::forward< Args >(args)...))
Parse str via vs.conv.
Definition: stream.hh:45
typename internal::weightset_t_of_impl< internal::base_t< ValueSet > >::type weightset_t_of
Helper to retrieve the type of the weightset of a value set.
Definition: traits.hh:86
static const std::string full
Completely version of Awali as a std::string.
Definition: version.hh:42
Main namespace of Awali.
Definition: ato.hh:22
Provide a variadic mul on top of a binary mul(), and one().
Definition: weightset.hh:38