Awali
Another Weighted Automata library
Public Types | Public Member Functions | Static Public Member Functions
awali::sttc::internal::reductioner< Aut, AutOutput > Class Template Reference

#include <reduce.hh>

Public Types

using q_weight_t = sttc::q::value_t
 
using r_weight_t = sttc::r::value_t
 
using z_weight_t = sttc::z::value_t
 Specializations for Q and R. More...
 

Public Member Functions

 reductioner (const automaton_t &input)
 
void bottom_up_reduction (std::vector< vector_t > &basis, unsigned *permutation)
 Apply reduction to vectors of the basis to maximize the number of zeros. More...
 
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. More...
 
unsigned find_pivot_by_norm (const vector_t &v, unsigned begin, unsigned *permutation)
 
output_automaton_t get_output () const
 
void left_reduce ()
 Core algorithm This algorithm computes a basis of I.mu(w). More...
 
void linear_representation ()
 Create the linear representation of the input. More...
 
void normalisation_vector (vector_t &v, unsigned pivot, unsigned *permutation)
 Normalize the basis vector such that its pivot is equal to 1. More...
 
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. More...
 
weight_t reduce_vector (vector_t &vbasis, vector_t &current, unsigned b, unsigned *permutation)
 Reduce a vector w.r.t. More...
 
weight_t scalar_product (const vector_t &v, const vector_t &w)
 Computes the scalar product of two vectors. More...
 
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. More...
 
void z_reduce_vector (vector_t &vbasis, vector_t &current, unsigned nb, unsigned *permutation)
 
void z_vector_in_new_basis (std::vector< vector_t > &basis, vector_t &current, vector_t &new_vector, unsigned *permutation)
 

Static Public Member Functions

static z_weight_t gcd (z_weight_t x, z_weight_t y, z_weight_t &a, z_weight_t &b)
 
static unsigned norm (const q_weight_t &w)
 
static double norm (const r_weight_t &w)
 Norm for real numbers; a "stable" pivot should minimize this norm. More...
 
static unsigned norm (const z_weight_t &w)
 Norm for integers. More...
 

Member Typedef Documentation

◆ q_weight_t

template<typename Aut , typename AutOutput >
using awali::sttc::internal::reductioner< Aut, AutOutput >::q_weight_t = sttc::q::value_t

◆ r_weight_t

template<typename Aut , typename AutOutput >
using awali::sttc::internal::reductioner< Aut, AutOutput >::r_weight_t = sttc::r::value_t

◆ z_weight_t

template<typename Aut , typename AutOutput >
using awali::sttc::internal::reductioner< Aut, AutOutput >::z_weight_t = sttc::z::value_t

Specializations for Q and R.

Constructor & Destructor Documentation

◆ reductioner()

template<typename Aut , typename AutOutput >
awali::sttc::internal::reductioner< Aut, AutOutput >::reductioner ( const automaton_t &  input)

Member Function Documentation

◆ bottom_up_reduction()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::bottom_up_reduction ( std::vector< vector_t > &  basis,
unsigned *  permutation 
)

Apply reduction to vectors of the basis to maximize the number of zeros.

◆ find_pivot()

template<typename Aut , typename AutOutput >
unsigned awali::sttc::internal::reductioner< Aut, AutOutput >::find_pivot ( const vector_t &  v,
unsigned  begin,
unsigned *  permutation 
)

Return the first (w.r.t the column permutation) non zero element as pivot.

◆ find_pivot_by_norm()

template<typename Aut , typename AutOutput >
unsigned awali::sttc::internal::reductioner< Aut, AutOutput >::find_pivot_by_norm ( const vector_t &  v,
unsigned  begin,
unsigned *  permutation 
)

◆ gcd()

template<typename Aut , typename AutOutput >
static z_weight_t awali::sttc::internal::reductioner< Aut, AutOutput >::gcd ( z_weight_t  x,
z_weight_t  y,
z_weight_t a,
z_weight_t b 
)
static

◆ get_output()

template<typename Aut , typename AutOutput >
output_automaton_t awali::sttc::internal::reductioner< Aut, AutOutput >::get_output ( ) const

◆ left_reduce()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::left_reduce ( )

Core algorithm This algorithm computes a basis of I.mu(w).

The basis is scaled. An automaton where states correspond to the vectors of this basis is built

◆ linear_representation()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::linear_representation ( )

Create the linear representation of the input.

◆ norm() [1/3]

template<typename Aut , typename AutOutput >
static unsigned awali::sttc::internal::reductioner< Aut, AutOutput >::norm ( const q_weight_t w)
static

◆ norm() [2/3]

template<typename Aut , typename AutOutput >
static double awali::sttc::internal::reductioner< Aut, AutOutput >::norm ( const r_weight_t w)
static

Norm for real numbers; a "stable" pivot should minimize this norm.

◆ norm() [3/3]

template<typename Aut , typename AutOutput >
static unsigned awali::sttc::internal::reductioner< Aut, AutOutput >::norm ( const z_weight_t w)
static

Norm for integers.

◆ normalisation_vector()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::normalisation_vector ( vector_t &  v,
unsigned  pivot,
unsigned *  permutation 
)

Normalize the basis vector such that its pivot is equal to 1.

◆ product_vector_matrix()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::product_vector_matrix ( const vector_t &  v,
const matrix_t &  m,
vector_t &  res 
)

Computes the product of a row vector with a matrix.

◆ reduce_vector()

template<typename Aut , typename AutOutput >
weight_t awali::sttc::internal::reductioner< Aut, AutOutput >::reduce_vector ( vector_t &  vbasis,
vector_t &  current,
unsigned  b,
unsigned *  permutation 
)

Reduce a vector w.r.t.

a vector of the basis.

When this method is called, in vbasis and current, all the entries that come before (w.r.t the permutation) the pivot are zero. Moreover, vbasis[pivot]=1 This method computes current := current - current[pivot].vbasis

◆ scalar_product()

template<typename Aut , typename AutOutput >
weight_t awali::sttc::internal::reductioner< Aut, AutOutput >::scalar_product ( const vector_t &  v,
const vector_t &  w 
)

Computes the scalar product of two vectors.

◆ vector_in_new_basis()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::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.

◆ z_reduce_vector()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::z_reduce_vector ( vector_t &  vbasis,
vector_t &  current,
unsigned  nb,
unsigned *  permutation 
)

◆ z_vector_in_new_basis()

template<typename Aut , typename AutOutput >
void awali::sttc::internal::reductioner< Aut, AutOutput >::z_vector_in_new_basis ( std::vector< vector_t > &  basis,
vector_t &  current,
vector_t &  new_vector,
unsigned *  permutation 
)

The documentation for this class was generated from the following file: