Awali
Another Weighted Automata library
reduce.hh
Go to the documentation of this file.
1 // This file is part of Awali.
2 // Copyright 2016-2022 Sylvain Lombardy, Victor Marsault, Jacques Sakarovitch
3 //
4 // Awali is a free software: you can redistribute it and/or modify
5 // it under the terms of the GNU General Public License as published by
6 // the Free Software Foundation, either version 3 of the License, or
7 // (at your option) any later version.
8 //
9 // This program is distributed in the hope that it will be useful,
10 // but WITHOUT ANY WARRANTY; without even the implied warranty of
11 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 // GNU General Public License for more details.
13 //
14 // You should have received a copy of the GNU General Public License
15 // along with this program. If not, see <http://www.gnu.org/licenses/>.
16 
17 
18 #ifndef AWALI_ALGOS_REDUCE_HH
19 # define AWALI_ALGOS_REDUCE_HH
20 
21 # include <map>
22 # include <unordered_map>
23 # include <vector>
24 # include <cmath>
25 
26 #include <awali/sttc/algos/copy.hh>
32 
33 namespace awali { namespace sttc {
34 
35  namespace internal
36  {
37  /*
38  The core algorithm computes a scaled basis from a list of
39  vectors. There is a permutation on entries in such a way that
40  the first non-zero entry of the i-th vector of the basis has
41  index i. (in the field case, this entry is equal to 1)
42 
43  If v is a new vector, for every vector b_i of the bases:
44 
45  - either v[i] is zero and there is nothing to do
46 
47  - or v[i] is different from 0 in this case, v is modified as v:=
48  v - v[i].b which makes v[i]=0 (in the Z case, b may also be
49  modified) This is performed by the reduce_vector method
50 
51  After the iteration, if v is null, it means that the vector was in the
52  vector space (or the Z-module) generated by the basis.
53  Otherwise, a non zero entry of v is selected (find_pivot),
54  v is normalized (normalization_vector) and the permutation is
55  updated in such a way that the pivot becomes the first non zero
56  entry of v, which is inserted in the basis.
57 
58  Once the basis is stabilized, a bottom-up reduction is applied
59  to the scaled basis in order to make it more "diagonal".
60  Finally, the new automaton is built w.r.t. the computed basis.
61  The construction of the automaton can not be done on-the-fly due
62  to both the Z case where the basis is modified and the bottom-up
63  reduction.
64  */
65 
66 
67  /*
68 
69  The implementation of elementary methods slightly differ
70  w.r.t. the weightset.
71 
72  Generically,
73 
74  find_pivot returns the first non zero entry
75 
76  reduce_vector computes current := current - current[i].b_i
77 
78  normalisation_vector applied a ratio in such a way that
79  the pivot is 1
80 
81  bottom_up_reduction applies, for each vector of the
82  basis, reduce_vector to every preceding vector in the
83  basis.
84 
85 
86  In Q : find_pivot searchs for the entry where
87  |numerator|+|denominator| is minimal
88 
89  In R : find_pivot searchs for the entry x where |x|+1/|x|
90  is minimal
91 
92  In Z : find_pivot searchs for the (non zero) entry x where
93  |x| is minimal
94  reduce_vector both reduce the current and the basis vector
95  (w.r.t. the gcd of current[i] and b_i[i])
96  normalisation_vector does not apply
97  bottom_up_reduction does not apply
98 
99  */
100 
101  template<typename Weightset>
102  struct select
103  {
104  template<typename Reduc, typename Vector>
105  static unsigned
106  find_pivot(Reduc* that, const Vector& v,
107  unsigned begin, unsigned* permutation)
108  {
109  return that->find_pivot(v, begin, permutation);
110  }
111 
112  template<typename Reduc, typename Vector>
113  static void
114  reduce_vector(Reduc* that, Vector& vbasis,
115  Vector& current, unsigned b, unsigned* permutation)
116  {
117  that->reduce_vector(vbasis, current, b, permutation);
118  }
119 
120  template<typename Reduc, typename Vector>
121  static void
122  normalisation_vector(Reduc* that, Vector& v,
123  unsigned pivot, unsigned* permutation)
124  {
125  that->normalisation_vector(v, pivot, permutation);
126  }
127 
128  template<typename Reduc, typename Basis>
129  static void
130  bottom_up_reduction(Reduc* that, Basis& basis, unsigned* permutation)
131  {
132  that->bottom_up_reduction(basis, permutation);
133  }
134 
135  template<typename Reduc, typename Basis, typename Vector>
136  static void
137  vector_in_new_basis(Reduc* that, Basis& basis,
138  Vector& current, Vector& new_vector,
139  unsigned* permutation)
140  {
141  that->vector_in_new_basis(basis, current, new_vector, permutation);
142  }
143  };
144 
145  template <>
146  struct select<q> : select<void>
147  {
148  template<typename Reduc, typename Vector>
149  static unsigned
150  find_pivot(Reduc* that, const Vector& v,
151  unsigned begin, unsigned* permutation)
152  {
153  return that->find_pivot_by_norm(v, begin, permutation);
154  }
155  };
156 
157  template <>
158  struct select<r> : select<void>
159  {
160  template<typename Reduc, typename Vector>
161  static unsigned
162  find_pivot(Reduc* that, const Vector& v,
163  unsigned begin, unsigned* permutation)
164  {
165  return that->find_pivot_by_norm(v, begin, permutation);
166  }
167  };
168 
169  template <>
170  struct select<z> : select<void>
171  {
172  template<typename Reduc, typename Vector>
173  static unsigned
174  find_pivot(Reduc* that, const Vector& v,
175  unsigned begin, unsigned* permutation)
176  {
177  return that->find_pivot_by_norm(v, begin, permutation);
178  }
179 
180  template <typename Reduc, typename Vector>
181  static void
182  reduce_vector(Reduc* that, Vector& vbasis,
183  Vector& current, unsigned b, unsigned* permutation)
184  {
185  that->z_reduce_vector(vbasis, current, b, permutation);
186  }
187 
188  template <typename Reduc, typename Vector>
189  static void normalisation_vector(Reduc*, Vector&, unsigned, unsigned*)
190  {}
191 
192  template<typename Reduc, typename Basis>
193  static void bottom_up_reduction(Reduc*, Basis&, unsigned*)
194  {}
195 
196  template<typename Reduc, typename Basis, typename Vector>
197  static void
198  vector_in_new_basis(Reduc* that, Basis& basis,
199  Vector& current, Vector& new_vector,
200  unsigned* permutation)
201  {
202  that->z_vector_in_new_basis(basis, current, new_vector, permutation);
203  }
204  };
205 
206  template <typename Aut, typename AutOutput>
208  {
209  static_assert(context_t_of<Aut>::is_lal,
210  "requires free labelset");
211 
212  using automaton_t = Aut;
213  using context_t = context_t_of<automaton_t>;
214  using weightset_t = typename context_t::weightset_t;
215  using output_automaton_t = AutOutput;
216  using label_t = label_t_of<automaton_t>;
217  using weight_t = typename context_t::weight_t;
218  using vector_t = std::vector<weight_t>;
219  using matrix_t = std::vector<std::map<std::size_t, weight_t> > ;
220  using matrix_set_t = std::map<label_t, matrix_t>;
221 
222  public:
223  reductioner(const automaton_t& input)
224  : input_(input)
225  , res_(make_shared_ptr<output_automaton_t>(input_->context()))
226  {}
227 
230  {
231  std::unordered_map<state_t, unsigned> state_to_index;
232  unsigned i = 0;
233  for (auto s: input_->states())
234  state_to_index[s] = i++;
235  dimension = i;
236  if (dimension == 0)
237  return;
238  init.resize(i);
239  final.resize(i);
240  // Computation of the initial vector.
241  for (auto t : input_->initial_transitions())
242  init[state_to_index[input_->dst_of(t)]] = input_->weight_of(t);
243  // Computation of the final vector.
244  for (auto t : input_->final_transitions())
245  final[state_to_index[input_->src_of(t)]] = input_->weight_of(t);
246  // For each letter, we define an adjency matrix.
247  for (auto t : input_->transitions())
248  {
249  auto it = letter_matrix_set.find(input_->label_of(t));
250  if (it == letter_matrix_set.end())
251  it = letter_matrix_set.emplace(input_->label_of(t),
252  matrix_t(dimension)).first;
253  it->second[state_to_index[input_->src_of(t)]]
254  [state_to_index[input_->dst_of(t)]] = input_->weight_of(t);
255  }
256  }
257 
258  //utility methods
259 
261  void product_vector_matrix(const vector_t& v,
262  const matrix_t& m,
263  vector_t& res)
264  {
265  for (unsigned i = 0; i < dimension; i++)
266  for (auto it : m[i])
267  {
268  unsigned j = it.first;
269  res[j] = ws_.add(res[j], ws_.mul(v[i], it.second));
270  }
271  }
272 
274  weight_t scalar_product(const vector_t& v,
275  const vector_t& w)
276  {
277  weight_t res = ws_.zero();
278  for (unsigned i = 0; i < dimension; ++i)
279  res = ws_.add(res, ws_.mul(v[i], w[i]));
280  return res;
281  }
282 
284  using z_weight_t = sttc::z::value_t; // int or long
286  using r_weight_t = sttc::r::value_t; // = double
287 
288  /*
289  The pivot is the entry x of the vector such that norm(x) is minimal.
290  This "norm" highly depends on the semiring.
291 
292  For rational numbers, it is the sum of the numerator and the
293  denominator (absolute value)
294 
295  For "real" numbers, it is |x|+|1/x| .
296  */
297 
298  static unsigned norm(const q_weight_t& w)
299  {
300  return w.den+abs(w.num);
301  }
302 
304  static double norm(const r_weight_t& w)
305  {
306  return std::fabs(w)+std::fabs(1/w);
307  }
308 
310  static unsigned norm(const z_weight_t& w)
311  {
312  return abs(w);
313  }
314 
315  // Works for both Q and R.
316  unsigned
317  find_pivot_by_norm(const vector_t& v, unsigned begin,
318  unsigned* permutation)
319  {
320  unsigned i=begin;
321  for(; i < dimension && ws_.is_zero(v[permutation[i]]); ++i)
322  ;
323  if(i==dimension)
324  return dimension;
325  unsigned pivot=i;
326  auto min = norm(v[permutation[i++]]);
327  for (; i < dimension; ++i)
328  if (!ws_.is_zero(v[permutation[i]])
329  && (pivot == dimension
330  || norm(v[permutation[i]])<min))
331  {
332  pivot = i;
333  min = norm(v[permutation[i]]);
334  }
335 // std::cerr << v[permutation[pivot]] << std::endl;
336  return pivot;
337  }
338 
339  // End of Q/R specializations.
340 
341 
342  // Specialization for Z.
343 
344  // Gcd function that also computes the Bezout coefficients.
345  // Used in the z reduction.
346  static z_weight_t
348  {
349  //z_weight_t res = 0;
350  //gcd = ax + by
351  int sx=(x<0)?-1:1, sy=(y<0)?-1:1;
352  bool inv=false;
353  if(x<0) x=-x;
354  if(y<0) y=-y;
355  if(x>y){
356  z_weight_t t=x; x=y; y=t;
357  inv=true;
358  }
359  a=1; b=0;
360  int a0=0, b0=1;
361  while(y!=0) {
362  z_weight_t q=x/y, r=x%y;
363  z_weight_t a1=a0, b1=b0;
364  a0=a-q*a0; b0=b-q*b0;
365  a=a1; b=b1;
366  x=y; y=r;
367  }
368  if(inv) {
369  int c=a; a=b; b=c;
370  }
371  a*=sx; b*=sy;
372  return x;
373  }
374 
375  /*
376  gcd= a.vbasis[pivot] + b.current[pivot]
377  current[pivot] is made zero with a unimodular linear transformation
378  This also modifies the basis vector
379  [ vbasis ] := [ a b ] . [ vbasis ]
380  [ current ] [-current[pivot]/gcd vbasis[pivot]/gcd] [ current ]
381  */
382  void z_reduce_vector(vector_t& vbasis, vector_t& current,
383  unsigned nb, unsigned* permutation)
384  {
385  unsigned pivot = permutation[nb]; //pivot of vector vbasis
386  if (ws_.is_zero(current[pivot]))
387  return;
388  weight_t bp = vbasis[pivot];
389  weight_t cp = current[pivot];
390  weight_t a,b;
391  weight_t g = gcd(bp, cp, a, b);
392  bp /= g;
393  cp /= g;
394  for (unsigned i = nb; i < dimension; ++i)
395  {
396  weight_t tmp = current[permutation[i]];
397  current[permutation[i]] = bp*tmp - cp*vbasis[permutation[i]];
398  vbasis[permutation[i]] = a*vbasis[permutation[i]] + b*tmp;
399  }
400  }
401 
402  void z_vector_in_new_basis(std::vector<vector_t>& basis,
403  vector_t& current, vector_t& new_vector,
404  unsigned* permutation)
405  {
406  for (unsigned b = 0; b < basis.size(); ++b)
407  {
408  vector_t& vbasis = basis[b];
409  unsigned pivot = permutation[b]; //pivot of vector vbasis
410  new_vector[b] = current[pivot] / vbasis[pivot];
411  if (!ws_.is_zero(new_vector[b]))
412  {
413  current[pivot] = ws_.zero();
414  for (unsigned i = b+1; i < dimension; ++i)
415  current[permutation[i]]
416  -= new_vector[b] * vbasis[permutation[i]];
417  }
418  }
419  }
420  // End of Z specializations.
421 
422  /* Generic subroutines.
423  These methods are written for any (skew) field.
424  Some are specialized for Q and R for stability issues.
425  Some are specialized for Z which is an Euclidean domain.
426  */
427 
430  unsigned find_pivot(const vector_t& v, unsigned begin,
431  unsigned* permutation)
432  {
433  for (unsigned i = begin; i < dimension; ++i)
434  if (!ws_.is_zero(v[permutation[i]]))
435  return i;
436  return dimension;
437  }
438 
447  weight_t reduce_vector(vector_t& vbasis,
448  vector_t& current, unsigned b,
449  unsigned* permutation)
450  {
451  unsigned pivot = permutation[b]; //pivot of vector vbasis
452  weight_t ratio = current[pivot];// vbasis[pivot] is one
453  if (ws_.is_zero(ratio))
454  return ratio;
455  // This is safer than current[p] = current[p]-ratio*vbasis[p];
456  current[pivot] = ws_.zero();
457  for (unsigned i = b+1; i < dimension; ++i)
458  current[permutation[i]]
459  = ws_.sub(current[permutation[i]],
460  ws_.mul(ratio, vbasis[permutation[i]]));
461  return ratio;
462  }
463 
465  void normalisation_vector(vector_t& v, unsigned pivot,
466  unsigned* permutation)
467  {
468  weight_t k = v[permutation[pivot]];
469  if (!ws_.is_one(k))
470  {
471  v[permutation[pivot]] = ws_.one();
472  for (unsigned r = pivot + 1; r < dimension; ++r)
473  v[permutation[r]] = ws_.rdiv(v[permutation[r]], k);
474  }
475  }
476 
479  void bottom_up_reduction(std::vector<vector_t>& basis,
480  unsigned* permutation)
481  {
482  for (unsigned b = basis.size()-1; 0 < b; --b)
483  for (unsigned c = 0; c < b; ++c)
484  reduce_vector(basis[b], basis[c], b, permutation);
485  }
486 
488  void vector_in_new_basis(std::vector<vector_t>& basis,
489  vector_t& current, vector_t& new_vector,
490  unsigned* permutation)
491  {
492  for (unsigned b = 0; b < basis.size(); ++b)
493  new_vector[b] = reduce_vector(basis[b], current, b, permutation);
494  }
495 
501  public:
502  void left_reduce()
503  {
504  // Used to select the proper overload depending on weightset_t.
505  using type_t = select<weightset_t>;
506 
508  // The basis is a list of vectors, each vector is associated with
509  // a state of the output
510  std::vector<vector_t> basis;
511  // The permutation array corresponds to a permutation of the indices
512  // (i.e. the columns of the matrices)
513  // such that permtuation[k] is the pivot of the k-th vector of the basis.
514  unsigned* permutation = new unsigned[dimension];
515  for (unsigned i = 0; i < dimension; ++i)
516  permutation[i] = i;
517  // If the initial vector is null, the function immediatly returns
518 
519  // A non zero entry is chosen as pivot
520  unsigned pivot = type_t::find_pivot(this, init, 0, permutation);
521  if (pivot == dimension) //all components of init are 0
522  return;
523  // The pivot of the first basis vector is permutation[0];
524  permutation[0] = pivot;
525  permutation[pivot] = 0;
526  // The initial vector is the first element of the new basis
527  // (up to the normalisation w.r.t the pivot)
528  vector_t first(init);
529  type_t::normalisation_vector(this, first, 0, permutation);
530  basis.push_back(first);
531  // To each vector of the basis, all the successor vectors are
532  // computed, reduced to respect to the basis, and finally, if
533  // linearly independant, pushed at the end of the basis
534  // itself.
535  for (unsigned nb = 0; nb < basis.size(); ++nb)
536  // All the vectors basis[nb].mu(a) are processed
537  for (auto mu : letter_matrix_set) //mu is a pair (letter,matrix)
538  {
539  vector_t current(dimension);
540  product_vector_matrix(basis[nb], mu.second, current);
541  //reduction of current w.r.t each basis vector;
542  for (unsigned b = 0; b < basis.size(); ++b)
543  type_t::reduce_vector(this, basis[b],
544  current, b, permutation);
545  // After reduction, we put current in the basis if it is
546  // not null and we search for the pivot of current.
547  pivot = type_t::find_pivot(this, current, basis.size(),
548  permutation);
549  if (pivot != dimension) //otherwise, current is null
550  {
551  if (pivot != basis.size())
552  std::swap(permutation[pivot], permutation[basis.size()]);
553  type_t::normalisation_vector(this, current,
554  basis.size(), permutation);
555  basis.push_back(current);
556  }
557  }
558 
559  // now, we use each vector to reduce the preceding vectors in
560  // the basis. If weightset=Z we do not do it.
561  type_t::bottom_up_reduction(this, basis, permutation);
562 
563  // Construction of the output automaton
564  // 1. States
565  std::vector<state_t> states(basis.size());
566  for (unsigned b = 0; b < basis.size(); ++b)
567  states[b] = res_->add_state();
568  // 2. Initial vector
569  vector_t vect_new_basis(basis.size());
570  type_t::vector_in_new_basis(this, basis, init,
571  vect_new_basis, permutation);
572  for (unsigned b = 0; b < basis.size(); ++b)
573  res_->set_initial(states[b], vect_new_basis[b]);
574  // 3. Each vector of the basis is a state; computation of the
575  // final function and the successor function
576  for (unsigned v = 0; v < basis.size(); ++v)
577  {
578  weight_t k = scalar_product(basis[v],final);
579  if(!ws_.is_zero(k))
580  res_->set_final(states[v],k);
581  for (auto mu : letter_matrix_set)
582  {
583  // mu is a pair (letter,matrix).
584  vector_t current(dimension);
585  product_vector_matrix(basis[v], mu.second, current);
586  type_t::vector_in_new_basis(this, basis, current,
587  vect_new_basis, permutation);
588  for (unsigned b = 0; b < basis.size(); ++b)
589  res_->new_transition(states[v], states[b],
590  mu.first, vect_new_basis[b]);
591  }
592  }
593  delete[] permutation;
594  }
595 
596 
597  output_automaton_t get_output() const
598  {
599  return res_;
600  }
601 
602  private:
603  automaton_t input_;
604  const weightset_t_of<automaton_t> ws_ = *input_->weightset();
605 
606  output_automaton_t res_;
607 
608  // Linear representation of the input.
609  unsigned dimension;
610  vector_t init;
611  vector_t final;
612  matrix_set_t letter_matrix_set;
613 
614  };
615 
616  }
617 
618  template<typename Aut>
619  Aut reduce(const Aut& input)
620  {
621  auto tmp = transpose_view(input);
622  internal::reductioner<decltype(tmp), Aut> algo(tmp);
623  algo.left_reduce();
624  auto tmp2=transpose_view(algo.get_output());
625  internal::reductioner<decltype(tmp2), Aut> algo2(tmp2);
626  algo2.left_reduce();
627  auto ret=copy(algo2.get_output());
628  if(ret->num_states() >= input->num_states())
629  ret= copy(input);
630  if(!input->get_name().empty()) {
631  ret->set_desc("Reduction of "+input->get_name());
632  ret->set_name("red-"+input->get_name());
633  }
634  else {
635  ret->set_desc("Reduction");
636  ret->set_name("red");
637  }
638  return ret;
639  }
640 
641  template<typename Aut>
642  Aut left_reduce(const Aut& input)
643  {
644  internal::reductioner<decltype(input), Aut> algo(input);
645  algo.left_reduce();
646  return copy(algo.get_output());
647  }
648 
649 }}//end of ns awali::stc
650 
651 #endif
Definition: qfraction.hh:26
den_t den
Definition: qfraction.hh:32
num_t num
Definition: qfraction.hh:31
The Boolean semring.
Definition: b.hh:38
The semiring of complex numbers.
Definition: c.hh:44
carries the algebraic settings of automata
Definition: context.hh:40
Definition: reduce.hh:208
sttc::r::value_t r_weight_t
Definition: reduce.hh:286
static unsigned norm(const z_weight_t &w)
Norm for integers.
Definition: reduce.hh:310
void z_reduce_vector(vector_t &vbasis, vector_t &current, unsigned nb, unsigned *permutation)
Definition: reduce.hh:382
void left_reduce()
Core algorithm This algorithm computes a basis of I.mu(w).
Definition: reduce.hh:502
void vector_in_new_basis(std::vector< vector_t > &basis, vector_t &current, vector_t &new_vector, unsigned *permutation)
Compute the coordinate of a vector in the new basis.
Definition: reduce.hh:488
unsigned find_pivot_by_norm(const vector_t &v, unsigned begin, unsigned *permutation)
Definition: reduce.hh:317
unsigned find_pivot(const vector_t &v, unsigned begin, unsigned *permutation)
Return the first (w.r.t the column permutation) non zero element as pivot.
Definition: reduce.hh:430
weight_t scalar_product(const vector_t &v, const vector_t &w)
Computes the scalar product of two vectors.
Definition: reduce.hh:274
static z_weight_t gcd(z_weight_t x, z_weight_t y, z_weight_t &a, z_weight_t &b)
Definition: reduce.hh:347
reductioner(const automaton_t &input)
Definition: reduce.hh:223
sttc::z::value_t z_weight_t
Specializations for Q and R.
Definition: reduce.hh:284
weight_t reduce_vector(vector_t &vbasis, vector_t &current, unsigned b, unsigned *permutation)
Reduce a vector w.r.t.
Definition: reduce.hh:447
void linear_representation()
Create the linear representation of the input.
Definition: reduce.hh:229
void normalisation_vector(vector_t &v, unsigned pivot, unsigned *permutation)
Normalize the basis vector such that its pivot is equal to 1.
Definition: reduce.hh:465
output_automaton_t get_output() const
Definition: reduce.hh:597
void bottom_up_reduction(std::vector< vector_t > &basis, unsigned *permutation)
Apply reduction to vectors of the basis to maximize the number of zeros.
Definition: reduce.hh:479
void z_vector_in_new_basis(std::vector< vector_t > &basis, vector_t &current, vector_t &new_vector, unsigned *permutation)
Definition: reduce.hh:402
static unsigned norm(const q_weight_t &w)
Definition: reduce.hh:298
void product_vector_matrix(const vector_t &v, const matrix_t &m, vector_t &res)
Computes the product of a row vector with a matrix.
Definition: reduce.hh:261
static double norm(const r_weight_t &w)
Norm for real numbers; a "stable" pivot should minimize this norm.
Definition: reduce.hh:304
The semiring of rational numbers.
Definition: q.hh:42
q_fraction_t value_t
Definition: q.hh:63
The semiring of floating Numbers.
Definition: r.hh:35
double value_t
Definition: r.hh:56
The semiring of Integers.
Definition: z.hh:35
int value_t
Definition: z.hh:56
std::vector< state_t > states(abstract_automaton_t const *aut, bool all)
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
type_t
The possible types of ratexps.
Definition: fwd.hh:48
typename internal::label_t_of_impl< internal::base_t< ValueSet > >::type label_t_of
Helper to retrieve the type of the labels of a value set.
Definition: traits.hh:71
Aut left_reduce(const Aut &input)
Definition: reduce.hh:642
SharedPtr make_shared_ptr(Args &&... args)
Same as std::make_shared, but parameterized by the shared_ptr type, not the (pointed to) element_type...
Definition: memory.hh:29
typename internal::context_t_of_impl< internal::base_t< ValueSet > >::type context_t_of
Helper to retrieve the type of the context of a value set.
Definition: traits.hh:66
AutOut copy(const AutIn &input, Pred keep_state, bool keep_history=true, bool transpose=false)
A copy of input keeping only its states that are accepted by keep_state.
Definition: copy.hh:189
Aut reduce(const Aut &input)
Definition: reduce.hh:619
std::shared_ptr< internal::transpose_view_impl< Aut > > transpose_view(std::shared_ptr< Aut > aut)
Definition: transpose_view.hh:265
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
ATTRIBUTE_CONST int min(int a, int b)
Definition: arith.hh:48
Main namespace of Awali.
Definition: ato.hh:22
static unsigned find_pivot(Reduc *that, const Vector &v, unsigned begin, unsigned *permutation)
Definition: reduce.hh:150
static unsigned find_pivot(Reduc *that, const Vector &v, unsigned begin, unsigned *permutation)
Definition: reduce.hh:162
static void normalisation_vector(Reduc *, Vector &, unsigned, unsigned *)
Definition: reduce.hh:189
static void bottom_up_reduction(Reduc *, Basis &, unsigned *)
Definition: reduce.hh:193
static unsigned find_pivot(Reduc *that, const Vector &v, unsigned begin, unsigned *permutation)
Definition: reduce.hh:174
static void reduce_vector(Reduc *that, Vector &vbasis, Vector &current, unsigned b, unsigned *permutation)
Definition: reduce.hh:182
static void vector_in_new_basis(Reduc *that, Basis &basis, Vector &current, Vector &new_vector, unsigned *permutation)
Definition: reduce.hh:198
Definition: reduce.hh:103
static void normalisation_vector(Reduc *that, Vector &v, unsigned pivot, unsigned *permutation)
Definition: reduce.hh:122
static void vector_in_new_basis(Reduc *that, Basis &basis, Vector &current, Vector &new_vector, unsigned *permutation)
Definition: reduce.hh:137
static unsigned find_pivot(Reduc *that, const Vector &v, unsigned begin, unsigned *permutation)
Definition: reduce.hh:106
static void bottom_up_reduction(Reduc *that, Basis &basis, unsigned *permutation)
Definition: reduce.hh:130
static void reduce_vector(Reduc *that, Vector &vbasis, Vector &current, unsigned b, unsigned *permutation)
Definition: reduce.hh:114