sataf.h

/*
 * sataf.h -- SATAF library main header file
 * 
 * This file is a part of the SATAF library. 
 * 
 * Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
 * 
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 * 
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
 * 02110-1301  USA
 */

#ifndef __SATAF_H__
# define __SATAF_H__

# include <tapas-config.h>

# include <ccl/ccl-list.h>
# include <ccl/ccl-hash.h>
# include <ccl/ccl-log.h>

BEGIN_C_DECLS 

typedef struct sataf_mao_st sataf_mao;

typedef struct sataf_mao_methods_st sataf_mao_methods;
typedef struct sataf_msa_st sataf_msa;
typedef struct sataf_sa_st sataf_sa;
typedef struct sataf_ea_st sataf_ea;
struct sataf_mao_methods_st
{
  const char *type;

  size_t (*size) (sataf_mao *self);

  void (*destroy) (sataf_mao *self);

  int (*no_cache) (sataf_mao *self);

  void (*is_root_of_scc) (sataf_mao *self, sataf_sa *sa, int q0);

  sataf_msa *(*simplify) (sataf_mao *self);

  uint32_t (*get_alphabet_size) (sataf_mao *self);

  char *(*to_string) (sataf_mao *self);

  sataf_mao *(*succ) (sataf_mao *self, uint32_t a);

  int (*is_final) (sataf_mao *self);

  int (*equals) (sataf_mao *self, sataf_mao *other);

  unsigned int (*hashcode) (sataf_mao *self);

  void (*to_dot) (ccl_log_type log, sataf_mao *self, const char **alphabet,
                  const char *graph_name, const char *graph_type);
};
typedef struct 
{
  uint32_t nb_shared_automata; 

  uint32_t nb_exit_automata;

  uint32_t nb_states;

  uint32_t depth;
  uint32_t to0;

  uint32_t refcount;
} sataf_msa_info;
typedef void sataf_sa_transformer (sataf_ea *ea, sataf_sa **bind_sa,
                                   uint32_t *bind_init);
                        /* --------------- */

typedef struct sataf_mao_memorizer_st sataf_mao_memorizer;

typedef struct {
  sataf_mao *A;
} sataf_mao_memo;

typedef void sataf_mao_memo_init_proc (sataf_mao_memo *m, void *data);

typedef void sataf_mao_memo_clean_proc (sataf_mao_memo *m);

                        /* --------------- */

extern int
sataf_init (int msa_op_cache_size, int mao_sharing_cache_size, 
            int ea_ut_table_size, int ea_ut_max_fill_degree, 
            int sa_ut_table_size, int sa_ut_max_fill_degree,
            int msa_ut_table_size, int msa_ut_max_fill_degree);

extern void
sataf_terminate (void);

extern void
sataf_log_statistics (ccl_log_type log);

extern sataf_mao * 
sataf_mao_create (size_t size, const sataf_mao_methods *methods);

static inline sataf_mao *
sataf_mao_add_reference(sataf_mao *a);

static inline void
sataf_mao_del_reference(sataf_mao *a);

extern char * 
sataf_mao_to_string (sataf_mao *self);

static inline const char *
sataf_mao_get_type (sataf_mao *self);

extern void
sataf_mao_is_root_of_scc (sataf_mao *self, sataf_sa *sa, int q0);

extern int 
sataf_mao_no_cache (sataf_mao *self);

extern sataf_msa * 
sataf_mao_simplify (sataf_mao *self);

extern uint32_t 
sataf_mao_get_alphabet_size (sataf_mao *self);

extern sataf_mao * 
sataf_mao_succ (sataf_mao *self, uint32_t letter);

extern int 
sataf_mao_is_final (sataf_mao *self);

extern int 
sataf_mao_equals (sataf_mao *self, sataf_mao *other);

extern unsigned int 
sataf_mao_hashcode (sataf_mao *self);

extern void 
sataf_mao_to_dot (ccl_log_type log, sataf_mao *self, const char **alphabet,
                  const char *graph_name, const char *graph_type);

extern void 
sataf_mao_default_to_dot (ccl_log_type log, sataf_mao *self, 
                          const char **alphabet, const char *graph_name, 
                          const char *graph_type);

extern sataf_mao * 
sataf_mao_create_zero (uint32_t alphabet_size);

extern sataf_mao * 
sataf_mao_create_one (uint32_t alphabet_size);

extern sataf_mao * 
sataf_mao_create_epsilon (uint32_t alphabet_size);

extern sataf_mao * 
sataf_mao_create_letter (uint32_t alphabet_size, uint32_t a);

extern sataf_mao * 
sataf_mao_create_alphabet (uint32_t alphabet_size);

extern sataf_mao * 
sataf_mao_create_from_arrays (uint32_t nb_states, uint32_t alphabet_size,
                              uint32_t s0, const uint8_t *is_final,
                              const uint32_t *succ);

extern sataf_mao * 
sataf_mao_create_ite (sataf_mao *i, sataf_mao *t, sataf_mao *e);

extern sataf_mao * 
sataf_mao_create_not (sataf_mao *a);

extern sataf_mao * 
sataf_mao_create_or (sataf_mao *a1, sataf_mao *a2);

extern sataf_mao * 
sataf_mao_create_and (sataf_mao *a1, sataf_mao *a2);

extern sataf_mao * 
sataf_mao_create_multi_or (ccl_list *operands);

extern sataf_mao * 
sataf_mao_create_multi_and (ccl_list *operands);

extern sataf_mao * 
sataf_mao_create_imply (sataf_mao *a1, sataf_mao *a2);

extern sataf_mao * 
sataf_mao_create_equiv (sataf_mao *a1, sataf_mao *a2);

extern sataf_mao * 
sataf_mao_create_forall (sataf_mao *a);

extern sataf_mao * 
sataf_mao_create_exists (sataf_mao *a);


extern sataf_mao_memorizer *
sataf_mao_memorizer_create (size_t memo_size, sataf_mao_memo_init_proc *init,
                            void *init_data, sataf_mao_memo_clean_proc *clean);

extern void
sataf_mao_memorizer_delete (sataf_mao_memorizer *M);

extern sataf_mao_memo *
sataf_mao_memorizer_remind (sataf_mao_memorizer *M, sataf_mao *A);

extern sataf_mao_memo *
sataf_mao_memorizer_succ (sataf_mao_memorizer *M, sataf_mao *A, int a);

static inline uint32_t
sataf_ea_encode_succ_as_local_state (uint32_t index);


static inline uint32_t 
sataf_ea_encode_succ_as_exit_state (uint32_t index);

static inline uint32_t
sataf_ea_decode_succ_state (uint32_t index);

static inline int
sataf_ea_is_exit_state (uint32_t successor);


static inline int
sataf_ea_is_local_state (uint32_t successor);

static uint32_t
sataf_ea_get_alphabet_size (sataf_ea *ea);

static inline uint32_t
sataf_ea_get_nb_states (sataf_ea *ea);

static inline uint32_t
sataf_ea_get_nb_exits (sataf_ea *ea);

static inline int
sataf_ea_is_final (sataf_ea *ea, uint32_t s);

static inline uint32_t
sataf_ea_get_successor (sataf_ea *ea, uint32_t state, uint32_t a);

static inline int
sataf_ea_is_zero (sataf_ea *ea);

static inline int
sataf_ea_is_one (sataf_ea *ea);


static inline int
sataf_ea_is_zero_or_one (sataf_ea *ea);

extern sataf_ea *
sataf_ea_create (uint32_t nb_states, uint32_t nb_exits, 
                 uint32_t alphabet_size);

extern sataf_ea *
sataf_ea_complement (sataf_ea *ea);

extern sataf_ea *
sataf_ea_create_with_arrays (uint32_t nb_states, uint32_t nb_exits,
                             uint32_t alphabet_size, const uint8_t *is_final,
                             const uint32_t *succ);

extern sataf_ea *
sataf_ea_add_reference (sataf_ea *ea);

extern void
sataf_ea_del_reference (sataf_ea *ea);

extern void
sataf_ea_set_successor (sataf_ea *ea, uint32_t src, uint32_t a, uint32_t tgt, 
                        int is_exit);

static inline void
sataf_ea_set_final (sataf_ea *ea, uint32_t s, int is_final);

extern void
sataf_ea_display_as_dot (sataf_ea *ea, ccl_log_type log, 
                         const char **alphabet);

extern sataf_ea *
sataf_ea_minimize (sataf_ea *ea, uint32_t *h);

extern sataf_ea *
sataf_ea_find_or_add (sataf_ea *ea);

extern sataf_ea *
sataf_ea_find (sataf_ea *ea);

extern int
sataf_ea_equals (sataf_ea *ea1, sataf_ea *ea2);

extern unsigned int
sataf_ea_hashcode (sataf_ea *ea);

extern void
sataf_ea_ut_statistics (ccl_log_type log);

extern sataf_sa * 
sataf_sa_create_one (uint32_t alphabet_size);

extern sataf_sa * 
sataf_sa_create_zero (uint32_t alphabet_size);

static inline sataf_sa *
sataf_sa_add_reference (sataf_sa *sa);

static inline void
sataf_sa_del_reference (sataf_sa *sa);

extern sataf_sa * 
sataf_sa_find_or_add (sataf_ea *ea, sataf_sa **bind_sa, uint32_t *bind_init);

extern void
sataf_sa_display_as_dot (sataf_sa *sa, ccl_log_type log, int marked_state, 
                         const char **alphabet, int with_info);

extern void
sataf_sa_display_scc_as_dot (sataf_sa *sa, ccl_log_type log);

static inline int
sataf_sa_is_zero (sataf_sa *sa);

static inline uint32_t
sataf_sa_get_alphabet_size (sataf_sa *sa);

static inline int
sataf_sa_is_one (sataf_sa *sa);

static inline int
sataf_sa_is_zero_or_one (sataf_sa *sa);

extern void
sataf_sa_table_statistics (ccl_log_type log);

extern void
sataf_sa_exists_closure (sataf_ea *ea, sataf_sa **bind_sa, 
                         uint32_t *bind_init);

extern void
sataf_sa_forall_closure (sataf_ea *ea, sataf_sa **bind_sa, 
                         uint32_t *bind_init);
/* @} */

extern sataf_msa * 
sataf_msa_find_or_add (sataf_sa *sa, uint32_t initial);

static inline uint32_t
sataf_msa_get_state (sataf_msa *msa);

static inline sataf_sa *
sataf_msa_get_sa (sataf_msa *msa);

static inline sataf_sa *
sataf_msa_get_sa_no_ref (sataf_msa *msa);

static inline sataf_msa *
sataf_msa_compute (sataf_mao *A);

extern sataf_msa *
sataf_msa_compute_with_transformer (sataf_mao *A, sataf_sa_transformer *T);

extern sataf_mao *
sataf_msa_to_mao (sataf_msa * msa);

extern void
sataf_msa_log_info (ccl_log_type log, sataf_msa *msa);

extern void
sataf_msa_get_info (sataf_msa *msa, sataf_msa_info *info);

extern sataf_msa * 
sataf_msa_succ (sataf_msa *msa, uint32_t a);

static inline int
sataf_msa_is_final (sataf_msa *msa);

static inline uint32_t
sataf_msa_get_alphabet_size (sataf_msa *msa);

static inline sataf_msa *
sataf_msa_add_reference (sataf_msa *msa);

static inline void
sataf_msa_del_reference (sataf_msa *msa);

extern void
sataf_msa_display_as_dot (sataf_msa *msa, ccl_log_type log,
                          const char **alphabet, int with_info);

extern void
sataf_msa_display_as_olddot (sataf_msa *msa, ccl_log_type log,
                             const char **alphabet);

static inline int
sataf_msa_is_zero (sataf_msa *msa);

static inline int
sataf_msa_is_one (sataf_msa *msa);

static inline int
sataf_msa_is_zero_or_one (sataf_msa *msa);

extern int
sataf_msa_is_included_in (sataf_msa *a1, sataf_msa *a2);


extern sataf_msa * 
sataf_msa_zero (uint32_t alphabet_size);

# define sataf_msa_empty sataf_msa_zero

extern sataf_msa * 
sataf_msa_one (uint32_t alphabet_size);

# define sataf_msa_all sataf_msa_one

extern sataf_msa * 
sataf_msa_epsilon (uint32_t alphabet_size);

extern int
sataf_msa_is_epsilon (sataf_msa *msa);

extern sataf_msa * 
sataf_msa_letter (uint32_t alphabet_size, uint32_t a);

extern sataf_msa * 
sataf_msa_alphabet (uint32_t alphabet_size);

extern sataf_msa * 
sataf_msa_ite (sataf_msa *i, sataf_msa *t, sataf_msa *e);

extern sataf_msa * 
sataf_msa_not (sataf_msa *a);

extern sataf_msa * 
sataf_msa_or (sataf_msa *a1, sataf_msa *a2);

extern sataf_msa * 
sataf_msa_xor (sataf_msa *a1, sataf_msa *a2);

extern sataf_msa * 
sataf_msa_and (sataf_msa *a1, sataf_msa *a2);

extern sataf_msa * 
sataf_msa_imply (sataf_msa *a1, sataf_msa *a2);

extern sataf_msa * 
sataf_msa_equiv (sataf_msa *a1, sataf_msa *a2);

extern sataf_msa * 
sataf_msa_forall (sataf_msa *a);

extern sataf_msa * 
sataf_msa_exists (sataf_msa *a);

extern sataf_msa * 
sataf_msa_concat (sataf_msa *a1, sataf_msa *a2);

extern sataf_msa * 
sataf_msa_power (sataf_msa *a, int N);

extern sataf_msa * 
sataf_msa_star (sataf_msa *a);

extern sataf_msa *
sataf_msa_change_acceptance (sataf_msa *a, ccl_hash *cond);

extern int
sataf_msa_is_detectable (sataf_msa *a1, sataf_msa *a2, ccl_list *acc);

extern sataf_msa * 
sataf_msa_cache_get (sataf_msa *a1, sataf_msa *a2, sataf_msa *a3,
                     const void *aux);

extern void
sataf_msa_cache_put (sataf_msa *a1, sataf_msa *a2, sataf_msa *a3,
                     const void *aux, sataf_msa *R);

# include <sataf/sataf-inline.h>

extern int
sataf_msa_are_complements (sataf_msa *a1, sataf_msa *a2);

END_C_DECLS


#endif /* ! __SATAF_H__ */