TaPAS  0.2
prestaf-formula.h
Go to the documentation of this file.
1 /*
2  * prestaf-formula.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 
43 #ifndef __PRESTAF_FORMULA_H__
44 # define __PRESTAF_FORMULA_H__
45 
46 # include <ccl/ccl-log.h>
47 # include <ccl/ccl-hash.h>
49 
50 BEGIN_C_DECLS
51 
73 typedef struct prestaf_formula_st prestaf_formula;
74 
85 typedef struct prestaf_linear_term_st prestaf_linear_term;
86 
87 
99 extern ccl_list *
101 
109 extern prestaf_formula *
111 
121 extern void
123 
129 extern void
131 
138 extern prestaf_predicate *
140 
141 
142 extern prestaf_formula *
143 prestaf_formula_create_from_file (const char *filename);
144 
145 extern prestaf_formula *
146 prestaf_formula_create_boolean_cst (int value);
147 
155 extern prestaf_formula *
157 
165 extern prestaf_formula *
167 
168 extern prestaf_formula *
169 prestaf_formula_create_xor (prestaf_formula *f1, prestaf_formula *f2);
170 
178 extern prestaf_formula *
180 
188 extern prestaf_formula *
190 
197 extern prestaf_formula *
199 
210 extern prestaf_formula *
212 
223 extern prestaf_formula *
225 
226 extern prestaf_formula *
227 prestaf_formula_create_single_exists (ccl_ustring v, prestaf_formula *f);
228 
237 extern prestaf_formula *
239 
248 extern prestaf_formula *
250 
259 extern prestaf_formula *
261 
270 extern prestaf_formula *
272 
281 extern prestaf_formula *
283 
292 extern prestaf_formula *
294 
310 extern prestaf_linear_term *
311 prestaf_linear_term_create (uint32_t n, int *a, ccl_ustring *x, int b);
312 
325 extern prestaf_linear_term *
327 
340 extern prestaf_linear_term *
342 
352 extern prestaf_linear_term *
354 
362 extern prestaf_linear_term *
364 
374 extern void
376 
388 extern int
390 
403 extern int
405 
414 extern void
416 
423 extern prestaf_formula *
425 
426 extern int
427 prestaf_formula_get_size (prestaf_formula *F);
428 
429 extern void
430 prestaf_formula_display_automaton (prestaf_formula *F, ccl_log_type log);
431 
432 END_C_DECLS
433 
434 #endif /* ! __PRESTAF_FORMULA_H__ */
prestaf_linear_term * prestaf_linear_term_add_reference(prestaf_linear_term *t)
Increments the reference counter of a linear term.
prestaf_linear_term * prestaf_linear_term_neg(prestaf_linear_term *t)
Negate a linear term.
prestaf_predicate * prestaf_formula_solutions(prestaf_formula *f)
Getting solutions of a Presbruger formula.
prestaf_formula * prestaf_formula_create_imply(prestaf_formula *f1, prestaf_formula *f2)
Formulae implication.
prestaf_formula * prestaf_formula_create_forall(ccl_list *variables, prestaf_formula *f)
Universal quantification of a formula.
struct prestaf_linear_term_st prestaf_linear_term
Pointers to linear terms.
prestaf_linear_term * prestaf_linear_term_create(uint32_t n, int *a, ccl_ustring *x, int b)
Constructor for linear terms.
prestaf_formula * prestaf_formula_create_not(prestaf_formula *f)
Formula negation.
prestaf_linear_term * prestaf_linear_term_plus(prestaf_linear_term *t1, prestaf_linear_term *t2)
Add two linear terms.
prestaf_formula * prestaf_formula_add_reference(prestaf_formula *f)
Increments the reference counter of a formula.
struct prestaf_predicate_st prestaf_predicate
Structure representing a predicate. The variables of the predicate take their value into ...
void prestaf_linear_term_del_reference(prestaf_linear_term *t)
Decrements the reference counter of a linear term.
prestaf_formula * prestaf_formula_create_equiv(prestaf_formula *f1, prestaf_formula *f2)
Formulae equivalence.
void prestaf_formula_statistics(prestaf_formula *F, ccl_log_type log)
Display informations about the sataf_msa encoding the solutions of Presburger formula.
prestaf_formula * prestaf_formula_create_lt(prestaf_linear_term *t1, prestaf_linear_term *t2)
Constructor for strict inferiority (&lt;) of linear terms.
prestaf_formula * prestaf_formula_linear_transform(prestaf_formula *F, ccl_hash *c, int a)
Replace each free variables by .
struct ccl_list_st ccl_list
Type of a generic list.
Definition: ccl-list.h:33
int prestaf_linear_term_get_coef(prestaf_linear_term *t, ccl_ustring x)
Getting coefficient of a linear term.
prestaf_linear_term * prestaf_linear_term_minus(prestaf_linear_term *t1, prestaf_linear_term *t2)
Substract two linear terms.
prestaf_formula * prestaf_formula_create_leq(prestaf_linear_term *t1, prestaf_linear_term *t2)
Constructor for large inferiority (&lt;=) of linear terms.
int prestaf_linear_term_get_ith_coef(prestaf_linear_term *t, uint32_t i)
Getting coefficient of a linear term.
ccl_list * prestaf_formula_get_variables(prestaf_formula *f)
Free variables of a formula.
prestaf_formula * prestaf_formula_create_or(prestaf_formula *f1, prestaf_formula *f2)
Formulae disjunction.
prestaf_formula * prestaf_formula_create_eq(prestaf_linear_term *t1, prestaf_linear_term *t2)
Constructor for equality (==) of linear terms.
char * ccl_ustring
Alias type for strings that are stored in an internal dictionary and then can be used as identifiers ...
Definition: ccl-string.h:34
prestaf_formula * prestaf_formula_create_and(prestaf_formula *f1, prestaf_formula *f2)
Formulae conjunction.
prestaf_formula * prestaf_formula_create_gt(prestaf_linear_term *t1, prestaf_linear_term *t2)
Constructor for strict superiority (&gt;) of linear terms.
enum ccl_log_type_enum ccl_log_type
Enum that indicates which kind of message has to be displayed. Each kind of message can be displayed ...
Definition: ccl-log.h:50
prestaf_formula * prestaf_formula_create_exists(ccl_list *variables, prestaf_formula *f)
Existential quantification of a formula.
struct prestaf_formula_st prestaf_formula
Pointers to Presburger formula.
prestaf_formula * prestaf_formula_create_neq(prestaf_linear_term *t1, prestaf_linear_term *t2)
Constructor for disequality (!=) of linear terms.
A dynamic association table implemented by hashing.
void prestaf_formula_display(ccl_log_type log, prestaf_formula *f)
Textual display of a Presburger formula.
struct ccl_hash_st ccl_hash
abstract type of an hash table.
Definition: ccl-hash.h:57
Message displayer.
void prestaf_formula_del_reference(prestaf_formula *f)
Decrements the reference counter of a a formula.
This module allows the manipulation of predicates for which variables take their value into ...
prestaf_formula * prestaf_formula_create_geq(prestaf_linear_term *t1, prestaf_linear_term *t2)
Constructor for weak superiority (&gt;=) of linear terms.