TaPAS  0.2
Typedefs | Functions
prestaf-predicate.h File Reference

This module allows the manipulation of predicates for which variables take their value into ${\cal N}$. The relation underlying a predicate is encoded using a sataf_msa. More...

#include <ccl/ccl-list.h>
#include <ccl/ccl-string.h>
#include <sataf/sataf.h>

Go to the source code of this file.

Typedefs

typedef struct prestaf_predicate_st prestaf_predicate
 Structure representing a predicate. The variables of the predicate take their value into ${\cal N}$. More...
 

Functions

prestaf_predicateprestaf_predicate_create (ccl_list *vars, sataf_msa *rel)
 Contructor of predicates. More...
 
prestaf_predicateprestaf_predicate_add_reference (prestaf_predicate *P)
 Increments the counter of reference of P. More...
 
void prestaf_predicate_del_reference (prestaf_predicate *P)
 Decrements the counter of reference of P. More...
 
ccl_listprestaf_predicate_get_variables (prestaf_predicate *P)
 Variables of a predicate. More...
 
sataf_msaprestaf_predicate_get_relation (prestaf_predicate *P)
 Relation of a predicate. More...
 
void prestaf_predicate_rename (prestaf_predicate *P, ccl_list *vars)
 Relabelling of the variables. More...
 
prestaf_predicateprestaf_predicate_not (prestaf_predicate *P)
 Compute the complement of a predictate P More...
 
prestaf_predicateprestaf_predicate_or (prestaf_predicate *P1, prestaf_predicate *P2)
 Binary disjunction. More...
 
prestaf_predicateprestaf_predicate_and (prestaf_predicate *P1, prestaf_predicate *P2)
 Binary conjunction. More...
 
prestaf_predicateprestaf_predicate_multi_or (ccl_list *predicates)
 N-ary disjunction. More...
 
prestaf_predicateprestaf_predicate_multi_and (ccl_list *predicates)
 N-ary conjunction. More...
 
prestaf_predicateprestaf_predicate_imply (prestaf_predicate *P1, prestaf_predicate *P2)
 Logical implication. More...
 
prestaf_predicateprestaf_predicate_equiv (prestaf_predicate *P1, prestaf_predicate *P2)
 Logical equality. More...
 
prestaf_predicateprestaf_predicate_exists (ccl_ustring v, prestaf_predicate *P)
 Existential projection. More...
 
prestaf_predicateprestaf_predicate_forall (ccl_ustring v, prestaf_predicate *P)
 Universal projection. More...
 
int prestaf_predicate_display_vectors (ccl_log_type log, prestaf_predicate *P)
 Display the assignments belonging to the predicate ::P. More...
 

Detailed Description

This module allows the manipulation of predicates for which variables take their value into ${\cal N}$. The relation underlying a predicate is encoded using a sataf_msa.

The module offers Boolean operations over these predicates and a pretty printer of the elements of the relation (in the finite case). When applying a binary operation on predicates (e.g prestaf_predicate_or()), the operands are considered to be defined over the same set of variables; if this is not the case they are extended to fit this requirement.

Definition in file prestaf-predicate.h.

Typedef Documentation

typedef struct prestaf_predicate_st prestaf_predicate

Structure representing a predicate. The variables of the predicate take their value into ${\cal N}$.

This structure associates a relation encoded using a marked-shared automaton (see sataf_msa) and a list of names. The width of the relation is the size of the list and the ith column is labelled by the name with the index i in then list.

Definition at line 54 of file prestaf-predicate.h.

Function Documentation

prestaf_predicate* prestaf_predicate_add_reference ( prestaf_predicate P)

Increments the counter of reference of P.

Parameters
Pthe referenced predicate
Precondition
P != NULL
Returns
the argument P
prestaf_predicate* prestaf_predicate_and ( prestaf_predicate P1,
prestaf_predicate P2 
)

Binary conjunction.

Parameters
P1first operand of the conjunction.
P2second operand of the conjunction.
Precondition
P1 != NULL && P2 != NULL
Returns
A predicate representing the intersection of the two sets represented by P1 and P2.
prestaf_predicate* prestaf_predicate_create ( ccl_list vars,
sataf_msa rel 
)

Contructor of predicates.

This function associates a list of names and a relation encoded with a sataf_msa automaton.

Parameters
varsis a list of ccl_ustring. These names label the columns of the relation rel.
relis the relation encoding the assignments satisfying the predicate.
Precondition
vars != NULL && rel != NULL
Returns
The newly allocated predicate.
void prestaf_predicate_del_reference ( prestaf_predicate P)

Decrements the counter of reference of P.

If the counter becomes 0 then the structure is deallocated.

Parameters
Pthe dereferenced predicate
Precondition
P != NULL && the number of reference to P is > 0
int prestaf_predicate_display_vectors ( ccl_log_type  log,
prestaf_predicate P 
)

Display the assignments belonging to the predicate ::P.

This function works only for finite subsets of ${\cal N}^n$; if the set represented by P is infinite then nothing is displayed.

The displayed verctors are mappings from the variables of P into $\cal N$.

Parameters
Pthe predicate to be displayed.
Precondition
P != NULL
Returns
1 if the set has been correctly displayed; 0 if the set is infinite.
Bug:
this procedure doesn't properly for infinite sets.
prestaf_predicate* prestaf_predicate_equiv ( prestaf_predicate P1,
prestaf_predicate P2 
)

Logical equality.

This operation computes $P1\cap P2 \cup \overline{P1}\cap \overline{P2}$

Parameters
P1first operand of the equality
P2first operand of the equality
Precondition
P1 != NULL && P2 != NULL
Returns
The predicate encoding the equality
prestaf_predicate* prestaf_predicate_exists ( ccl_ustring  v,
prestaf_predicate P 
)

Existential projection.

Parameters
vthe name of then variable removed from the predicate.
Pthe predicate that is projected.
Precondition
v != NULL && P != NULL
Returns
The predicate equal to P existentially projected on variables of P without v
prestaf_predicate* prestaf_predicate_forall ( ccl_ustring  v,
prestaf_predicate P 
)

Universal projection.

Parameters
vthe name of variable removed from the predicate.
Pthe predicate that is projected.
Precondition
v != NULL && P != NULL
Returns
The predicate equal to P universally projected on variables of P without v
sataf_msa* prestaf_predicate_get_relation ( prestaf_predicate P)

Relation of a predicate.

Precondition
P != NULL
Returns
The sataf_msa encoding the set of vectors represented by P
ccl_list* prestaf_predicate_get_variables ( prestaf_predicate P)

Variables of a predicate.

Precondition
P != NULL
Returns
The (internal) ordered list of variables of P
prestaf_predicate* prestaf_predicate_imply ( prestaf_predicate P1,
prestaf_predicate P2 
)

Logical implication.

This operation computes $\overline{P1}\cup P2$

Parameters
P1first operand of the implication
P2first operand of the implication
Precondition
P1 != NULL && P2 != NULL
Returns
The predicate encoding $\overline{P1}\cup P2$
prestaf_predicate* prestaf_predicate_multi_and ( ccl_list predicates)

N-ary conjunction.

Parameters
predicatesthe list of predicates on which the conjunction is applied.
Precondition
predicates != NULL && ccl_list_size(predicates) >= 1
Returns
The conjunction of elements in predicates.
prestaf_predicate* prestaf_predicate_multi_or ( ccl_list predicates)

N-ary disjunction.

Parameters
predicatesthe list of predicates on which the disjunction is applied.
Precondition
predicates != NULL && ccl_list_size(predicates) >= 1
Returns
The disjunction of elements in predicates.
prestaf_predicate* prestaf_predicate_not ( prestaf_predicate P)

Compute the complement of a predictate P

Parameters
Pthe predicate to be complemented.
Precondition
P != NULL
Returns
The complement of P
prestaf_predicate* prestaf_predicate_or ( prestaf_predicate P1,
prestaf_predicate P2 
)

Binary disjunction.

Parameters
P1first operand of the disjunction.
P2second operand of the disjunction.
Precondition
P1 != NULL && P2 != NULL
Returns
A predicate representing the union of the two sets represented by P1 and P2.
void prestaf_predicate_rename ( prestaf_predicate P,
ccl_list vars 
)

Relabelling of the variables.

This function simply replaces the list of variables of the predicate P by the list vars.

Parameters
Pthe relabelled predicate.
varsthe new labelling list.
Precondition
P != NULL && vars != NULL