| 
    TaPAS
    0.2
    
   | 
 
This module implements an encoding of Presburger formulae. It computes also for a given formula its set of solutions using Shared Automata. More...
Go to the source code of this file.
Typedefs | |
| typedef struct prestaf_formula_st | prestaf_formula | 
| Pointers to Presburger formula.  More... | |
| typedef struct  prestaf_linear_term_st  | prestaf_linear_term | 
| Pointers to linear terms.  More... | |
This module implements an encoding of Presburger formulae. It computes also for a given formula its set of solutions using Shared Automata.
Presburger formulae are syntactically defined by:
F ::= T == T | T != T | T < T | T <= T | T > T | T >= T | -F | F \/ F | F /\ F | F => F | F <=> F | E.x F | A.x F
E. and A. operators are respectively existential and universal quantification. T represents a linear term defined syntactically by:
T ::= c | a.x | T+T | T-T | -T
where c and a are an integers and x is a variable taken its value into natural numbers 
. 
Definition in file prestaf-formula.h.
| typedef struct prestaf_formula_st prestaf_formula | 
Pointers to Presburger formula.
This type defines pointers to structures encoding Presburger formulae. These formula are syntactically defined by:
F ::= T == T | T != T | T < T | T <= T | T > T | T >= T | -F | F \/ F | F /\ F | F => F | F <=> F | E.x F | A.x F
E. and A. operators are respectively existential and universal quantification. T represents a linear term defined syntactically by:
T ::= c | a.x | T+T | T-T | -T
where c and a are an integers and x is a variable taken its value into natural numbers 
.
prestaf_formula uses a counter of references.
Definition at line 73 of file prestaf-formula.h.
| typedef struct prestaf_linear_term_st prestaf_linear_term | 
Pointers to linear terms.
This type defines pointers to structures encoding linear terms of the form a0.x0+...+an.xn+ b where ai and b are integers and xi are variables.
prestaf_linear_term uses a counter of references.
Definition at line 85 of file prestaf-formula.h.
| prestaf_formula* prestaf_formula_add_reference | ( | prestaf_formula * | f | ) | 
Increments the reference counter of a formula.
| f | the formual to be referenced | 
| prestaf_formula* prestaf_formula_create_and | ( | prestaf_formula * | f1, | 
| prestaf_formula * | f2 | ||
| ) | 
Formulae conjunction.
| f1 | first operand | 
| f2 | second operand | 
| prestaf_formula* prestaf_formula_create_eq | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Constructor for equality (==) of linear terms.
| t1 | first operand | 
| t2 | second operand | 
| prestaf_formula* prestaf_formula_create_equiv | ( | prestaf_formula * | f1, | 
| prestaf_formula * | f2 | ||
| ) | 
Formulae equivalence.
| f1 | first operand | 
| f2 | second operand | 
| prestaf_formula* prestaf_formula_create_exists | ( | ccl_list * | variables, | 
| prestaf_formula * | f | ||
| ) | 
Existential quantification of a formula.
| variables | the list of quantified variables | 
| f | the formula to quantify | 
| prestaf_formula* prestaf_formula_create_forall | ( | ccl_list * | variables, | 
| prestaf_formula * | f | ||
| ) | 
Universal quantification of a formula.
| variables | the list of quantified variables | 
| f | the formula to quantify | 
| prestaf_formula* prestaf_formula_create_geq | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Constructor for weak superiority (>=) of linear terms.
| t1 | first operand | 
| t2 | second operand | 
| prestaf_formula* prestaf_formula_create_gt | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Constructor for strict superiority (>) of linear terms.
| t1 | first operand | 
| t2 | second operand | 
| prestaf_formula* prestaf_formula_create_imply | ( | prestaf_formula * | f1, | 
| prestaf_formula * | f2 | ||
| ) | 
Formulae implication.
| f1 | first operand | 
| f2 | second operand | 
| prestaf_formula* prestaf_formula_create_leq | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Constructor for large inferiority (<=) of linear terms.
| t1 | first operand | 
| t2 | second operand | 
| prestaf_formula* prestaf_formula_create_lt | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Constructor for strict inferiority (<) of linear terms.
| t1 | first operand | 
| t2 | second operand | 
| prestaf_formula* prestaf_formula_create_neq | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Constructor for disequality (!=) of linear terms.
| t1 | first operand | 
| t2 | second operand | 
| prestaf_formula* prestaf_formula_create_not | ( | prestaf_formula * | f | ) | 
Formula negation.
| f | first operand | 
| prestaf_formula* prestaf_formula_create_or | ( | prestaf_formula * | f1, | 
| prestaf_formula * | f2 | ||
| ) | 
Formulae disjunction.
| f1 | first operand | 
| f2 | second operand | 
| void prestaf_formula_del_reference | ( | prestaf_formula * | f | ) | 
Decrements the reference counter of a a formula.
When the reference counter of the object falls to 0 then the memory allocated for the formula is released.
| f | the formula to be dereferenced | 
| void prestaf_formula_display | ( | ccl_log_type | log, | 
| prestaf_formula * | f | ||
| ) | 
Textual display of a Presburger formula.
| f | the formula to be displayed | 
| ccl_list* prestaf_formula_get_variables | ( | prestaf_formula * | f | ) | 
Free variables of a formula.
This function returns a list containing all the variables appearing in the given formula f.
| f | the formula | 
| prestaf_formula* prestaf_formula_linear_transform | ( | prestaf_formula * | F, | 
| ccl_hash * | c, | ||
| int | a | ||
| ) | 
Replace each free variables 
 by 
. 
| prestaf_predicate* prestaf_formula_solutions | ( | prestaf_formula * | f | ) | 
Getting solutions of a Presbruger formula.
| void prestaf_formula_statistics | ( | prestaf_formula * | F, | 
| ccl_log_type | log | ||
| ) | 
Display informations about the sataf_msa encoding the solutions of Presburger formula.
| F | a Presburger formula. | 
| log | the log-stream where informations are displayed. | 
| prestaf_linear_term* prestaf_linear_term_add_reference | ( | prestaf_linear_term * | t | ) | 
Increments the reference counter of a linear term.
| t | the term to be referenced | 
| prestaf_linear_term* prestaf_linear_term_create | ( | uint32_t | n, | 
| int * | a, | ||
| ccl_ustring * | x, | ||
| int | b | ||
| ) | 
Constructor for linear terms.
This function allocates a structure encoding a linear term of the form a[0]*x[0]+...+a[n-1]*x[n-1]+b.
| n | the number of variables in this term. | 
| a | the coefficient of each sub-term. | 
| x | the names of variables. | 
| b | the constant of the term? | 
| void prestaf_linear_term_del_reference | ( | prestaf_linear_term * | t | ) | 
Decrements the reference counter of a linear term.
When the reference counter of the object falls to 0 then the memory allocated for the term is released.
| t | the term to be dereferenced | 
| int prestaf_linear_term_get_coef | ( | prestaf_linear_term * | t, | 
| ccl_ustring | x | ||
| ) | 
Getting coefficient of a linear term.
This function returns the coefficient of the variable x in t.
| t | the considered term. | 
| x | the variable for which one want to get the coefficent.. | 
| int prestaf_linear_term_get_ith_coef | ( | prestaf_linear_term * | t, | 
| uint32_t | i | ||
| ) | 
Getting coefficient of a linear term.
This function returns the ith coefficient in t (the constant is not considered here). The subterms are ordered using the address of the variable names.
| t | the considered term. | 
| i | the index for which one want to get the coefficent. | 
| prestaf_linear_term* prestaf_linear_term_minus | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Substract two linear terms.
This operation computes the substraction of its two arguments. The set of variables of the two terms are merged before the operation.
| t1 | the first linear term. | 
| t2 | the second linear term. | 
| prestaf_linear_term* prestaf_linear_term_neg | ( | prestaf_linear_term * | t | ) | 
Negate a linear term.
This operation negates its two arguments.
| t | the first linear term | 
| prestaf_linear_term* prestaf_linear_term_plus | ( | prestaf_linear_term * | t1, | 
| prestaf_linear_term * | t2 | ||
| ) | 
Add two linear terms.
This operation computes the sum of its two arguments. The set of variables of the two terms are merged before the operation.
| t1 | the first linear term | 
| t2 | the second linear term | 
 1.8.5