TaPAS  0.2
prestaf-batof.h
Go to the documentation of this file.
1 /*
2  * prestaf-batof.h -- add a comment about this file
3  *
4  * This file is a part of the PresTAF project.
5  *
6  * Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
7  *
8  * This program is free software; you can redistribute it and/or modify
9  * it under the terms of the GNU General Public License as published by
10  * the Free Software Foundation; either version 2 of the License, or
11  * (at your option) any later version.
12  *
13  * This program is distributed in the hope that it will be useful,
14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16  * GNU General Public License for more details.
17  *
18  * You should have received a copy of the GNU General Public License
19  * along with this program; if not, write to the Free Software
20  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
21  * 02110-1301 USA
22  */
23 
29 #ifndef __PRESTAF_BATOF_H__
30 # define __PRESTAF_BATOF_H__
31 
32 # include <gmp.h>
33 # include <ccl/ccl-common.h>
34 # include <ccl/ccl-log.h>
35 # include <ccl/ccl-string.h>
36 # include <sataf/sataf.h>
37 # include <armoise/armoise-tree.h>
38 # include <talalib/talalib.h>
39 
40 # define BTF_MAX_NUMBER_OF_VARIABLES 256
41 
42 BEGIN_C_DECLS
43 
44 typedef struct btf_bound_st {
45  tla_vsp_t V;
46  tla_saff_t B;
47 } btf_bound;
48 
49 /*
50  * EXIT AUTOMATON TO ASP
51  * @pre ea->nb_local_states > 1 || exit_automaton_is_zero_or_one(ea)
52  @ @pre ea->alphabet_size == 2
53  */
54 extern int
55 btf_ea_to_vsp (tla_vsp_t res, sataf_ea *ea, int s);
56 
57 extern void
58 btf_msa_to_saff (tla_saff_t saff, sataf_msa *msa);
59 
60 extern armoise_tree *
61 btf_msa_to_formula (int m, sataf_msa *msa, const char * const *varnames,
62  int with_prefix);
63 
64 extern armoise_tree *
65 btf_msa_to_convex_hull (int m, sataf_msa *msa, const char * const *varnames);
66 
67 END_C_DECLS
68 
69 #endif /* ! __PRESTAF_BATOF_H__ */
struct sataf_ea_st sataf_ea
Type for the data structure encoding Exit Automata.
Definition: sataf.h:99
Syntactic tree for the Armoise language.
Structure encoding of a parse-tree node.
Some useful and common macros.
Module gathering routines frequently used for the manipulation of string.
Message displayer.
struct sataf_msa_st sataf_msa
Type for the data structure encoding Marked Shared Automata.
Definition: sataf.h:81