Specification of Plugin Prototypes. More...

#include <genepi/genepi.h>
#include <genepi/genepi-plugin-config.h>

Macros
#define	GENEPI_PLUGIN_FUNC(_f) GENEPI_PLUGIN_PREFIX (_LTX_ ## _f)
	Macro used to prefix function symbols. More...

Typedefs
typedef struct genepi_plugin_impl_st	genepi_plugin_impl
	Abstraction of a GENEPI plugin instance.

typedef struct genepi_set_impl_st	genepi_set_impl
	Abstraction of a GENEPI set. More...

Functions
genepi_plugin_impl *	genepi_plugin_init (genepi_plugconf *conf)
	Initializes the plugin. More...

void	genepi_plugin_terminate (genepi_plugin_impl *plugin)
	Releases ressources allocated by the plugin. More...

int	genepi_plugin_autotest (genepi_plugin_impl *plugin)
	Self-test. More...

genepi_solver_type	genepi_plugin_get_solver_type (genepi_plugin_impl *plugin)
	Returns the domain of variables used by the solver. More...

genepi_set_impl *	genepi_plugin_add_reference (genepi_plugin_impl plugin, genepi_set_impl X)
	Adds a new reference to the set X. More...

void	genepi_plugin_del_reference (genepi_plugin_impl plugin, genepi_set_impl X)
	Removes a reference to the set X. More...

genepi_set_impl *	genepi_plugin_top (genepi_plugin_impl *plugin, int n)
	Computes the complete relation of arity n. More...

genepi_set_impl *	genepi_plugin_top_N (genepi_plugin_impl *plugin, int n)
	Computes the complete relation of arity n restricted to positive or null integers. More...

genepi_set_impl *	genepi_plugin_top_Z (genepi_plugin_impl *plugin, int n)
	Computes the complete relation of arity n restricted integers. More...

genepi_set_impl *	genepi_plugin_top_P (genepi_plugin_impl *plugin, int n)
	Computes the complete relation of arity n restricted to positive or null reals. More...

genepi_set_impl *	genepi_plugin_top_R (genepi_plugin_impl *plugin, int n)
	Computes the complete relation of arity n restricted to reals. More...

genepi_set_impl *	genepi_plugin_bot (genepi_plugin_impl *plugin, int n)
	Computes the empty relation of arity n. More...

genepi_set_impl *	genepi_plugin_linear_operation (genepi_plugin_impl plugin, const int alpha, int alpha_size, genepi_comparator op, int c)
	Computes the set of solutions of a linear operation. More...

genepi_set_impl *	genepi_plugin_set_union (genepi_plugin_impl plugin, genepi_set_impl X1, genepi_set_impl *X2)
	Computes the union of two relations. More...

genepi_set_impl *	genepi_plugin_set_intersection (genepi_plugin_impl plugin, genepi_set_impl X1, genepi_set_impl *X2)
	Computes the intersection of two relations. More...

genepi_set_impl *	genepi_plugin_set_complement (genepi_plugin_impl plugin, genepi_set_impl X)
	Computes the complement of the set X. More...

genepi_set_impl *	genepi_plugin_project (genepi_plugin_impl plugin, genepi_set_impl X, const int *selection, int size)
	Projects a relation on a subset of its columns. More...

genepi_set_impl *	genepi_plugin_invproject (genepi_plugin_impl plugin, genepi_set_impl X, const int *selection, int size)
	Adds columns to the relation X. More...

genepi_set_impl *	genepi_plugin_apply (genepi_plugin_impl plugin, genepi_set_impl R, genepi_set_impl *A)
	Computes `post (R, A)` More...

genepi_set_impl *	genepi_plugin_applyinv (genepi_plugin_impl plugin, genepi_set_impl R, genepi_set_impl *A)
	Computes `pre (R, A)` More...

int	genepi_plugin_compare (genepi_plugin_impl plugin, genepi_set_impl X1, genepi_comparator op, genepi_set_impl *X2)
	Checks inclusion relation between X1 and X2. More...

int	genepi_plugin_is_empty (genepi_plugin_impl plugin, genepi_set_impl X)
	Checks the emptiness of X. More...

int	genepi_plugin_is_full (genepi_plugin_impl plugin, genepi_set_impl X)
	Checks is X is the complete relation. More...

int	genepi_plugin_is_finite (genepi_plugin_impl plugin, genepi_set_impl X)
	Checks if the set is finite. More...

int	genepi_plugin_depend_on (genepi_plugin_impl plugin, genepi_set_impl X, const int *sel, int selsize)
	Checks if the relation X depends on a subset of its column. More...

void	genepi_plugin_get_solutions (genepi_plugin_impl plugin, genepi_set_impl X, int **psolutions, int psize, int max)
	Computes an explicit representation of X. More...

void	genepi_plugin_display_all_solutions (genepi_plugin_impl plugin, genepi_set_impl X, FILE output, const char const *varnames)
	Displays all elements of X. More...

void	genepi_plugin_display_data_structure (genepi_plugin_impl plugin, genepi_set_impl X, FILE *output)
	Displays the data structure used to encode X. More...

int	genepi_plugin_get_width (genepi_plugin_impl plugin, genepi_set_impl X)
	Arity of X. More...

int	genepi_plugin_get_data_structure_size (genepi_plugin_impl plugin, genepi_set_impl X)
	The size allocated to X. More...

int	genepi_plugin_is_solution (genepi_plugin_impl plugin, genepi_set_impl X, const int *v, int v_size, int vden)
	Checks if v/vden* belongs* to X. More...

int	genepi_plugin_get_one_solution (genepi_plugin_impl plugin, genepi_set_impl X, int *x, int x_size)
	Gets one element in X. More...

unsigned int	genepi_plugin_cache_hash (genepi_plugin_impl plugin, genepi_set_impl X)
	Computes an hash value for X. More...

int	genepi_plugin_cache_equal (genepi_plugin_impl plugin, genepi_set_impl X1, genepi_set_impl *X2)
	Checks that two sets are equal in the cache. More...

int	genepi_plugin_write_set (genepi_plugin_impl plugin, FILE output, genepi_set_impl *set)
	Dump the set X onto the output stream. More...

int	genepi_plugin_read_set (genepi_plugin_impl plugin, FILE input, genepi_set_impl **pset)
	Load on the input stream a serialized set. More...

int	genepi_plugin_preorder (genepi_plugin_impl plugin, genepi_set_impl X1, genepi_set_impl *X2)
	Evaluate the pre-order over sets. More...

Detailed Description

Specification of Plugin Prototypes.

This header file declares prototypes of functions that a plugin have to implement. Each prototype is declared using a macro GENEPI_PLUGIN_FUNC() whose aim is to prefix each function name with the name of the plugin. GENEPI Plugin implementors must use this macro to define or to call the functions of their plugin.

Attention: This documentation has been automatically generated using Doxygen (http://www/doxygen.org/) which does not support function prototypes built using a macro-function like GENEPI_PLUGIN_FUNC(). For sake of readability this documentation has been produced by defining this macro-function as genepi_plugin_ ## f i.e. it adds the prefix genepi_plugin to the given symbol f by . Thus, in this documentation, any function name of the form genepi_pluginsome_name has to be understood (and use) as GENEPI_PLUGIN_FUNC(some_name).

The plugins are loaded (cf. genepi-loader.h) using the LTDL library and the name of the generated .la file is used by the plugin loader. The name of the file is the (nick)name of the module that has to be used to prefix plugin exported functions (see GENEPI_PLUGIN_FUNC()). The template plugin is distributed with a configure.ac file and a Makefile.am which can be helpful to build the plugin; the subdirectory m4 contains a useful M4 macro for checking the existence of the GENEPI library on the system and to locate the directory where plugins are installed.

Definition in file genepi-plugin.h.

Macro Definition Documentation

#define GENEPI_PLUGIN_FUNC ( _f ) GENEPI_PLUGIN_PREFIX (_LTX_ ## _f)

Macro used to prefix function symbols.

This macro-function is used to prefix each declaration of a plugin's function by the name of the plugin. Indeed the actual symbol name of an implemented function follows the form plugin name_LTX_function name. For example, if the plugin will be used under the name myplugin then the function implementing the initialization of the plugin will be actually called myplugin_LTX_init.

GENEPI_PLUGIN_FUNC() macro uses another macro called GENEPI_PLUGIN_PREFIX(_f) which is defined by the developper of the plugin. This macro has to prefix the symbol specified by its argument _f with the name of the plugin. The following lines present the code defining this macro in the template plugin distributed with GENEPI:

#ifndef GENEPI_PLUGIN_PREFIX      
/* replace the 'template' prefix by the one of the module name */
# warning "GENEPI_PLUGIN_PREFIX is not defined"
# define GENEPI_PLUGIN_PREFIX(_f) template ## _f 
#endif /* ! GENEPI_PLUGIN_NAME */
#include <genepi/genepi-plugin.h>

In order to use the expect symbol name, the developper of a GENEPI plugin has to use the GENEPI_PLUGIN_FUNC() to write the prototype of its function. For example, the get_solver_type function of the template plugin is defined this way:

genepi_solver_type
GENEPI_PLUGIN_FUNC(get_solver_type) (genepi_plugin_impl *plugin)
{
  return GENEPI_N_SOLVER;
}

Examples:: examples/plugins/template-plugin.c.

Definition at line 96 of file genepi-plugin.h.

Typedef Documentation

typedef struct genepi_set_impl_st genepi_set_impl

Abstraction of a GENEPI set.

This is an abstraction of the implementation of the encoding of a Presburger definable set. GENEPI uses it via pointers and no constraint exists on the underlying data structure contained into a genepi_set_impl (except that it must permits the implementation of function manipulating specified by the API).

Definition at line 112 of file genepi-plugin.h.

Function Documentation

genepi_set_impl* genepi_plugin_add_reference	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Adds a new reference to the set X.

This function is called to indicate the plugin that the set X is referenced another time.

Parameters

X	a non null pointer to a set

Precondition: X != NULL

Returns: X in any case

Definition at line 100 of file template-plugin.c.

genepi_set_impl* genepi_plugin_apply	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	R,
		genepi_set_impl *	A
	)

Computes post (R, A)

This function applies the relation R to the set A. If n is the width of A, the function assumes that 2*n is the width of R. The function computes the set of vectors defined by:

$apply(R,A) = \{ (x_1,\dots, x_n)\in A \mid \exists x_1^\prime,\dots x_n^\prime, (x_1^\prime,x_1,\dots,x_n^\prime,x_n)\in R\}$

Note the interleaving of primed and not primed variables and also note that the primed variable precedes its non-primed version.

Remarks: If this function it is not implemented by the plugin, a generic function is used.

Parameters

R	the transition relation
A	the relation on which R is applied.

Precondition: GENEPI_PLUGIN_FUNC (get_width) (R) = 2 * GENEPI_PLUGIN_FUNC (get_width) (A)

Returns: a pointer to the structure encoding post(R,A)

Definition at line 245 of file template-plugin.c.

genepi_set_impl* genepi_plugin_applyinv	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	R,
		genepi_set_impl *	A
	)

Computes pre (R, A)

This function is similar to apply but instead of computing the image of A by the relation R, it computes the set whose image is A by R. Formally, the function computes the set:

$applyinv(R,A) = \{ (x_1,\dots, x_n)\in A \mid \exists x_1, \dots x_n, (x_1^\prime,x_1,\dots,x_n^\prime,x_n)\in R\}$

Note the interleaving of primed and not primed variables and also note that the primed variable precedes its non-primed version.

Remarks: If this function is not implemented by the plugin, the loader replaces it by a generic version.

Parameters

R	the transition relation;
A	the image by R of the computed relation.

Precondition: GENEPI_PLUGIN_FUNC (get_width) (R) = 2 * GENEPI_PLUGIN_FUNC (get_width) (A)

Returns: a pointer to the structure encoding pre(R,A)

Definition at line 256 of file template-plugin.c.

int genepi_plugin_autotest ( genepi_plugin_impl * plugin )

Self-test.

This function is called on-demand by GENEPI clients to execute tests validating the plugin.

Returns: a non null value if the test is passed

Definition at line 81 of file template-plugin.c.

genepi_set_impl* genepi_plugin_bot	(	genepi_plugin_impl *	plugin,
		int	n
	)

Computes the empty relation of arity n.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

n	the arity of the computed relation

Precondition: n > 0

Returns: the encoding of $\emptyset^n$

Definition at line 172 of file template-plugin.c.

int genepi_plugin_cache_equal	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X1,
		genepi_set_impl *	X2
	)

Checks that two sets are equal in the cache.

Remarks: This function is not mandatory but indicates to GENEPI whether the data structure used by the plugin supports cache facility.

Parameters

X1	first operand of the comparison
X2	second operand of the comparison

Precondition: X1 != NULL; X2 != NULL

Remarks: This function is not mandatory.

Definition at line 403 of file template-plugin.c.

unsigned int genepi_plugin_cache_hash	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Computes an hash value for X.

Remarks: This function is not mandatory but indicates to GENEPI whether the data structure used by the plugin supports cache facility.

Parameters

X	the considered set

Precondition: X != NULL

Returns: an hash value of X

Definition at line 393 of file template-plugin.c.

int genepi_plugin_compare	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X1,
		genepi_comparator	op,
		genepi_set_impl *	X2
	)

Checks inclusion relation between X1 and X2.

According to op the function returns a non null value if X1 and X2 satisfy X1 op X2 where op is interpreted on sets.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X1	first operand of the comparison
op	predicate over X1 and X2 to test
X2	second operand of the comparison

Precondition: X1 != NULL; X2 != NULL; GENEPI_PLUGIN_FUNC (get_width) (X1) == GENEPI_PLUGIN_FUNC (get_width) (X2)

Returns: a non null value if X1 op X2

Definition at line 266 of file template-plugin.c.

void genepi_plugin_del_reference	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Removes a reference to the set X.

This indicates the plugin that a reference has to be removed to X. GENEPI assumes that X is valid while its number of references is positive. When the number of references falls to zero the plugin should release or collect ressources allocated to X.

Parameters

X	a non null pointer to a set

Precondition: X != NULL

Definition at line 112 of file template-plugin.c.

int genepi_plugin_depend_on	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		const int *	sel,
		int	selsize
	)

Checks if the relation X depends on a subset of its column.

X is said to be dependent of columns $i_1, \dots, i_n$ (where $i_j$ is such that $sel[i_j] \not=0$ ) if the projection of X these columns is not the complete relation of arity n.

Remarks: This function is not mandatory. If it is not implemented GENEPI checks that $X \not= invproject(project(sel,selsize),sel,selsize)$ .

Parameters

X	the relation on which we check dependency.
sel	an array of Booleans identifying the columns on which the dependency is checked.
selsize	the number of cells in sel.

Precondition: X != NULL; sel != NULL; selsize == GENEPI_PLUGIN_FUNC(get_width) (X)

Returns: "a non null value" if X depends on selected columns.

Definition at line 306 of file template-plugin.c.

void genepi_plugin_display_all_solutions	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		FILE *	output,
		const char const	varnames
	)

Displays all elements of X.

This function displays all elements of X even if X is infinite. The representation used to display X is not specified.

Remarks: This function is not mandatory.

Parameters

X	the set to display
output	the stream on which the result is displayed
varnames	the names labelling the column of the relation; the size of this array must be equal to the arity of the relation.

Precondition: X != NULL; output != NULL; varnames != NULL

Definition at line 328 of file template-plugin.c.

void genepi_plugin_display_data_structure	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		FILE *	output
	)

Displays the data structure used to encode X.

Remarks: This function is not mandatory.

Parameters

X	the set to display
output	the stream on which the result is displayed

Precondition: X != NULL; output != NULL

Definition at line 339 of file template-plugin.c.

int genepi_plugin_get_data_structure_size	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

The size allocated to X.

This function returns the internal size allocated to the set X. The semantics of the integer returned by this function is not specified but must be consistent with size of the underlying data structure; it can be a number of nodes in a graph or the number of characters in a string conversion of the data structure.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X	the considered relation

Precondition: X != NULL

Returns: the size of the internal encoding of X

Definition at line 359 of file template-plugin.c.

int genepi_plugin_get_one_solution	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		int *	x,
		int	x_size
	)

Gets one element in X.

This function fills the vector x with an element of X. If the components of x are not integers then components are set to the same denominator d which is return by the function. The way the function selects x is not specified.

Remarks: This function is not mandatory.

Parameters

X	the considered relation
x	the vector receiving the element of X
x_size	the size of x

Precondition: X != NULL; x != NULL; x_size == GENEPI_PLUGIN_FUNC (get_width) (X)

Postcondition: result >= 0

Return values

0	if X is empty.
the	common denominator of the solution x

Definition at line 382 of file template-plugin.c.

void genepi_plugin_get_solutions	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		int ***	psolutions,
		int *	psize,
		int	max
	)

Computes an explicit representation of X.

This function computes an array of vectors representing elements of the set X. Each vector is an array of integers allocated by the function. If X is an infinite set then max parameter is used to indicate the maximal number of vectors to return. The way the function choose the vectors is not specifed.

The vectors are returned via the psolutions parameter and the number of vectors is set into the variable pointed by psize.

If the max if negative then all the solutions are returned; in this case the function can guess that X is finite.

Remarks: This function is not mandatory.

Parameters

X	the set X
psolutions	the address where the vectors are stored
psize	the address of the integer receiving the number of solution
max	the maximal number of solutions.

Precondition: X != NULL; psolutions != NULL; psize != NULL; max >= 0 || GENEPI_PLUGIN_FUNC(is_finite) (X)

Definition at line 317 of file template-plugin.c.

genepi_solver_type genepi_plugin_get_solver_type ( genepi_plugin_impl * plugin )

Returns the domain of variables used by the solver.

If this function is not implemented GENEPI assumes that the solver works on positive or null integers.

Returns: the domain of variables used by the solver.

See Also: genepi_solver_type, genepi_solver_get_solver_type()

Definition at line 90 of file template-plugin.c.

int genepi_plugin_get_width	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Arity of X.

This function returns the arity or width of the given X

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X	the considered relation

Precondition: X != NULL

Returns: the arity of X

Definition at line 349 of file template-plugin.c.

genepi_plugin_impl* genepi_plugin_init ( genepi_plugconf * conf )

Initializes the plugin.

This function is called just after the plugin is loaded. It has to initialize ressources of the plugin. If the initialization fail the loader unload the plugin.

This function is ignored if not implemented.

Warning: A plugin might be loaded several times this this function has to take care of that in order to not remove or reinitialize data.

Returns: a non null value if the plugin is successfully initialized.

See Also: terminate

Definition at line 57 of file template-plugin.c.

genepi_set_impl* genepi_plugin_invproject	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		const int *	selection,
		int	size
	)

Adds columns to the relation X.

This function add columns to X according to the array of Booleans selection. The arity of the resulting relation is size and the relation itself is defined by:

$invproject(X,selection,size) = \{ (x_1,\dots,x_{size}) | \exists v\in X, v[1] = x_{i_1}\wedge \dots\wedge v[n] = x_{i_n} \} \}$

where n is the arity of X, $0 \leq i_1 \leq\dots\leq i_n < size$ and for $j=1\dots n, selection[i_j] = 0$ .

Parameters

X	the relation where new columns are added
selection	the specification of new columns
size	number of column in the result.

Precondition: X != NULL; selection != NULL; size >= GENEPI_PLUGIN_FUNC(get_width) (X)

Returns: the encoding of X extended with additionnal columns specified in selection.

Definition at line 234 of file template-plugin.c.

int genepi_plugin_is_empty	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Checks the emptiness of X.

This function checks if the set represented by X is empty or not.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X	the checked relation

Precondition: X != NULL

Returns: a non null value if X is the empty relation

Definition at line 276 of file template-plugin.c.

int genepi_plugin_is_finite	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Checks if the set is finite.

Remarks: This function is not mandatory.

Parameters

X	the checked relation

Precondition: X != NULL

Returns: a non null value is the set is finite

Definition at line 296 of file template-plugin.c.

int genepi_plugin_is_full	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Checks is X is the complete relation.

This function checks if the set represented by X is the complete relation of arity GENEPI_PLUGIN_FUNC (get_width) (X).

Remarks: If it is not implemented by the plugin, the loader replaces it by a generic version checking the emptyness of the complement of X.

Parameters

X	the checked relation

Precondition: X != NULL

Returns: a non null value if X is the complete relation

Definition at line 286 of file template-plugin.c.

int genepi_plugin_is_solution	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		const int *	v,
		int	v_size,
		int	vden
	)

Checks if v/vden belongs to X.

Remarks: This function is not mandatory. If the function is not implemented then it is replaced by the checking of the non-emptiness of the intersection X with the solutions of $\bigwedge_{i=0}^{v\_size} vden\times x_i = v[i]$ .

Parameters

X	the considered relation
v	the vector whose belonging is tested.
v_size	the size of v
vden	the denominator of v

Precondition: X != NULL; v != NULL; vden > 0; v_size == GENEPI_PLUGIN_FUNC (get_width) (X)

Returns: a non null value if v /vden\ is an element of X.

Definition at line 370 of file template-plugin.c.

genepi_set_impl* genepi_plugin_linear_operation	(	genepi_plugin_impl *	plugin,
		const int *	alpha,
		int	alpha_size,
		genepi_comparator	op,
		int	c
	)

Computes the set of solutions of a linear operation.

According to the value of op this function returns the set of solutions of the linear operation:

$\Sigma_{i=0..alpha\_size} alpha[i]\times x_i\mbox{ op }c$

with op interpreted on integers.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

alpha	the array of coefficient of the linear operation
alpha_size	the number of coefficients
c	the constant term of the operation
op	the identifier of the operation

Precondition: alpha != NULL && alpha_size > 0

Returns: the solutions of the specified linear operation.

Definition at line 181 of file template-plugin.c.

int genepi_plugin_preorder	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X1,
		genepi_set_impl *	X2
	)

Evaluate the pre-order over sets.

This function implements the pre-order relation $\preceq$ such that for all sets $S_1$ , $S_2$ and $S_3$ :

$S_1\preceq S_2 \wedge S_2\preceq S_1 \iff S_1 \mbox{ and } S_2 \mbox{ represent the same set}$
$S_1\preceq S_2 \wedge S_2\preceq S_3 \Longrightarrow S_1\preceq S_3$
$S_1\preceq S_2 \vee S_1\preceq S_2$

Parameters

X1	first operand
X2	second operand

Precondition: X1 != NULL; X2 != NULL

Returns: a non null value of X1 $\preceq$ X2

Definition at line 436 of file template-plugin.c.

genepi_set_impl* genepi_plugin_project	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X,
		const int *	selection,
		int	size
	)

Projects a relation on a subset of its columns.

This function computes the projection of X on the columns selected by the array of Booleans selection. The function computes:

$project(X) = \{ (x_{i_1}, \dots, x_{i_n}) \mid \exists v\in X, v[i_1] = x_{i_1}\wedge \dots\wedge v[i_n] = x_{i_n} \}$

where $0 \leq i_1 \leq\dots\leq i_n \leq size$ and for $j=1\dots n, selection[i_j] = 0$ . The function may assumed that the arity of X is equal or greater than size.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X	the relation to project
selection	the selection of columns of X which must be kept by the projection.
size	the number of Booleans in selection.

Precondition: X != NULL; selection != NULL; size == GENEPI_PLUGIN_FUNC(get_width) (X)

Returns: the encoding of the projection of X according to the selected columns in selection.

Definition at line 223 of file template-plugin.c.

int genepi_plugin_read_set	(	genepi_plugin_impl *	plugin,
		FILE *	input,
		genepi_set_impl **	pset
	)

Load on the input stream a serialized set.

This function is used to reload a set serialized with the genepi_plugin_write_set write function. The loaded set is putted in *pset. The function returns the number of bytes actually readed. If a negative or null value is returned an error has occurred and the returned value has to be interpreted as genepi_io_error.

Parameters

input	the stream where the set is loaded
pset	a pointer to the variable receiving the loaded set.

read_set function.

Precondition: input != NULL; pset != NULL

Returns: the number of bytes read on input or an error code

See Also: genepi_plugin_write_set

Definition at line 425 of file template-plugin.c.

References GENEPI_RW_ERR_IO.

genepi_set_impl* genepi_plugin_set_complement	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X
	)

Computes the complement of the set X.

This function computes the completement of X in the domain of variables i.e. either $N$ or $Z$ .

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X	the set to complement.

Precondition: X != NULL

Returns: the encoding of $\overline{X}$

Definition at line 213 of file template-plugin.c.

genepi_set_impl* genepi_plugin_set_intersection	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X1,
		genepi_set_impl *	X2
	)

Computes the intersection of two relations.

This function has to compute $X_1 \cap X_2$ where relations $ X_i$ are assumed to be of same arity.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X1	the first operand of the intersection
X2	the second operand of the intersection

Precondition: GENEPI_PLUGIN_FUNC (get_width) (X1) = GENEPI_PLUGIN_FUNC (get_width) (X2)

Returns: the encoding of $X_1 \cap X_2$

Definition at line 203 of file template-plugin.c.

genepi_set_impl* genepi_plugin_set_union	(	genepi_plugin_impl *	plugin,
		genepi_set_impl *	X1,
		genepi_set_impl *	X2
	)

Computes the union of two relations.

This function has to compute $X_1 \cup X_2$ where relations $ X_i$ are assumed to be of same arity.

Warning: In order to be validated by the loader a plugin MUST implement this function.

Parameters

X1	the first operand of the union
X2	the second operand of the union

Precondition: GENEPI_PLUGIN_FUNC (get_width) (X1) = GENEPI_PLUGIN_FUNC (get_width) (X2)

Returns: the encoding of $X_1 \cup X_2$

Definition at line 192 of file template-plugin.c.

void genepi_plugin_terminate ( genepi_plugin_impl * plugin )

Releases ressources allocated by the plugin.

This function destroys the ressources allocated by the module since its initilization.

This function has to handle the case multi-initialization of the plugin.

This function is ignored if not implemented.

See Also: init

Definition at line 70 of file template-plugin.c.

genepi_set_impl* genepi_plugin_top	(	genepi_plugin_impl *	plugin,
		int	n
	)

Computes the complete relation of arity n.

This function has to return the complete relation of arity n. Depending on the type of solver variables the result is either ${\cal N}^n$ , ${\cal Z}^n$ , ${\cal R+}^n$ or ${\cal R}^n$ .

Parameters

n	the arity of the computed relation

Precondition: n > 0

Returns: the encoding of the complete relation of arity n.

get_solver_type.

Definition at line 126 of file template-plugin.c.

genepi_set_impl* genepi_plugin_top_N	(	genepi_plugin_impl *	plugin,
		int	n
	)

Computes the complete relation of arity n restricted to positive or null integers.

This function has to return the complete relation of arity n over positive or null integers ${\cal N}$ .

Parameters

n	the arity of the computed relation

Precondition: n > 0

Returns: ${\cal N}^n \cap \mbox{\tt top(solver,n)}$

Definition at line 135 of file template-plugin.c.

genepi_set_impl* genepi_plugin_top_P	(	genepi_plugin_impl *	plugin,
		int	n
	)

Computes the complete relation of arity n restricted to positive or null reals.

Parameters

n	the arity of the computed relation

Precondition: n > 0

Returns: ${\cal R^+}^n \cap \mbox{\tt top(solver,n)}$

Definition at line 154 of file template-plugin.c.

genepi_set_impl* genepi_plugin_top_R	(	genepi_plugin_impl *	plugin,
		int	n
	)

Computes the complete relation of arity n restricted to reals.

Parameters

n	the arity of the computed relation

Precondition: n > 0

Returns: ${\cal R}^n \cap \mbox{\tt top(solver,n)}$

Definition at line 164 of file template-plugin.c.

genepi_set_impl* genepi_plugin_top_Z	(	genepi_plugin_impl *	plugin,
		int	n
	)

Computes the complete relation of arity n restricted integers.

Parameters

n	the arity of the computed relation

Precondition: n > 0

Returns: ${\cal Z}^n \cap \mbox{\tt top(solver,n)}$

Definition at line 144 of file template-plugin.c.

int genepi_plugin_write_set	(	genepi_plugin_impl *	plugin,
		FILE *	output,
		genepi_set_impl *	set
	)

Dump the set X onto the output stream.

This function can be used to serialize a set oX nto an output stream. The function returns the number of bytes actually written on the stream. If the result is negative or null then an error has occured and the returned has to be interpreted as a genepi_io_error.

Parameters

output	the stream where data are written.
set	the dumped GENEPI set

Precondition: output != NULL; set != NULL

Returns: the number of bytes written on output or an error code

See Also: genepi_plugin_read_set

Definition at line 414 of file template-plugin.c.

References GENEPI_RW_ERR_IO.

Macros

Typedefs

Functions

Detailed Description

Macro Definition Documentation

Typedef Documentation

Function Documentation