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>

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_predicate *	prestaf_predicate_create (ccl_list vars, sataf_msa rel)
	Contructor of predicates. More...

prestaf_predicate *	prestaf_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_list *	prestaf_predicate_get_variables (prestaf_predicate *P)
	Variables of a predicate. More...

sataf_msa *	prestaf_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_predicate *	prestaf_predicate_not (prestaf_predicate *P)
	Compute the complement of a predictate P More...

prestaf_predicate *	prestaf_predicate_or (prestaf_predicate P1, prestaf_predicate P2)
	Binary disjunction. More...

prestaf_predicate *	prestaf_predicate_and (prestaf_predicate P1, prestaf_predicate P2)
	Binary conjunction. More...

prestaf_predicate *	prestaf_predicate_multi_or (ccl_list *predicates)
	N-ary disjunction. More...

prestaf_predicate *	prestaf_predicate_multi_and (ccl_list *predicates)
	N-ary conjunction. More...

prestaf_predicate *	prestaf_predicate_imply (prestaf_predicate P1, prestaf_predicate P2)
	Logical implication. More...

prestaf_predicate *	prestaf_predicate_equiv (prestaf_predicate P1, prestaf_predicate P2)
	Logical equality. More...

prestaf_predicate *	prestaf_predicate_exists (ccl_ustring v, prestaf_predicate *P)
	Existential projection. More...

prestaf_predicate *	prestaf_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 i^th 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

P	the referenced predicate

Precondition: P != NULL

Returns: the argument P

prestaf_predicate* prestaf_predicate_and	(	prestaf_predicate *	P1,
		prestaf_predicate *	P2
	)

Binary conjunction.

Parameters

P1	first operand of the conjunction.
P2	second 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

vars	is a list of ccl_ustring. These names label the columns of the relation rel.
rel	is 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

P	the 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

P	the 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

P1	first operand of the equality
P2	first 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

v	the name of then variable removed from the predicate.
P	the 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

v	the name of variable removed from the predicate.
P	the 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

P1	first operand of the implication
P2	first 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

predicates the 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

predicates the 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

P	the 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

P1	first operand of the disjunction.
P2	second 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

P	the relabelled predicate.
vars	the new labelling list.

Precondition: P != NULL && vars != NULL

Typedefs

Functions

Detailed Description

Typedef Documentation

Function Documentation