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_boolean_cst (int value);
144 
152 extern prestaf_formula *
154 
162 extern prestaf_formula *
164 
165 extern prestaf_formula *
166 prestaf_formula_create_xor (prestaf_formula *f1, prestaf_formula *f2);
167 
175 extern prestaf_formula *
177 
185 extern prestaf_formula *
187 
194 extern prestaf_formula *
196 
207 extern prestaf_formula *
209 
220 extern prestaf_formula *
222 
223 extern prestaf_formula *
224 prestaf_formula_create_single_exists (ccl_ustring v, prestaf_formula *f);
225 
234 extern prestaf_formula *
236 
245 extern prestaf_formula *
247 
256 extern prestaf_formula *
258 
267 extern prestaf_formula *
269 
278 extern prestaf_formula *
280 
289 extern prestaf_formula *
291 
307 extern prestaf_linear_term *
308 prestaf_linear_term_create (uint32_t n, int *a, ccl_ustring *x, int b);
309 
322 extern prestaf_linear_term *
324 
337 extern prestaf_linear_term *
339 
349 extern prestaf_linear_term *
351 
359 extern prestaf_linear_term *
361 
371 extern void
373 
385 extern int
387 
400 extern int
402 
411 extern void
413 
420 extern prestaf_formula *
422 
423 extern int
424 prestaf_formula_get_size (prestaf_formula *F);
425 
426 END_C_DECLS
427 
428 #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.