TaPAS  0.2
Macros | Typedefs | Functions
genepi-plugin.h File Reference

Specification of Plugin Prototypes. More...

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

Go to the source code of this file.

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_implgenepi_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_implgenepi_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_implgenepi_plugin_top (genepi_plugin_impl *plugin, int n)
 Computes the complete relation of arity n. More...
 
genepi_set_implgenepi_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_implgenepi_plugin_top_Z (genepi_plugin_impl *plugin, int n)
 Computes the complete relation of arity n restricted integers. More...
 
genepi_set_implgenepi_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_implgenepi_plugin_top_R (genepi_plugin_impl *plugin, int n)
 Computes the complete relation of arity n restricted to reals. More...
 
genepi_set_implgenepi_plugin_bot (genepi_plugin_impl *plugin, int n)
 Computes the empty relation of arity n. More...
 
genepi_set_implgenepi_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_implgenepi_plugin_set_union (genepi_plugin_impl *plugin, genepi_set_impl *X1, genepi_set_impl *X2)
 Computes the union of two relations. More...
 
genepi_set_implgenepi_plugin_set_intersection (genepi_plugin_impl *plugin, genepi_set_impl *X1, genepi_set_impl *X2)
 Computes the intersection of two relations. More...
 
genepi_set_implgenepi_plugin_set_complement (genepi_plugin_impl *plugin, genepi_set_impl *X)
 Computes the complement of the set X. More...
 
genepi_set_implgenepi_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_implgenepi_plugin_invproject (genepi_plugin_impl *plugin, genepi_set_impl *X, const int *selection, int size)
 Adds columns to the relation X. More...
 
genepi_set_implgenepi_plugin_apply (genepi_plugin_impl *plugin, genepi_set_impl *R, genepi_set_impl *A)
 Computes post (R, A) More...
 
genepi_set_implgenepi_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 */

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_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
Xa 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
Rthe transition relation
Athe 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
Rthe transition relation;
Athe 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
nthe 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
X1first operand of the comparison
X2second 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
Xthe 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
X1first operand of the comparison
oppredicate over X1 and X2 to test
X2second 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
Xa 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
Xthe relation on which we check dependency.
selan array of Booleans identifying the columns on which the dependency is checked.
selsizethe 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
Xthe set to display
outputthe stream on which the result is displayed
varnamesthe 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
Xthe set to display
outputthe 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
Xthe 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
Xthe considered relation
xthe vector receiving the element of X
x_sizethe size of x
Precondition
X != NULL
x != NULL
x_size == GENEPI_PLUGIN_FUNC (get_width) (X)
Postcondition
result >= 0
Return values
0if X is empty.
thecommon 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
Xthe set X
psolutionsthe address where the vectors are stored
psizethe address of the integer receiving the number of solution
maxthe 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
Xthe 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
Xthe relation where new columns are added
selectionthe specification of new columns
sizenumber 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
Xthe 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
Xthe 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
Xthe 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
Xthe considered relation
vthe vector whose belonging is tested.
v_sizethe size of v
vdenthe 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
alphathe array of coefficient of the linear operation
alpha_sizethe number of coefficients
cthe constant term of the operation
opthe 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
X1first operand
X2second 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
Xthe relation to project
selectionthe selection of columns of X which must be kept by the projection.
sizethe 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
inputthe stream where the set is loaded
pseta 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
Xthe 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
X1the first operand of the intersection
X2the 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
X1the first operand of the union
X2the 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
nthe 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
nthe 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
nthe 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
nthe 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
nthe 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
outputthe stream where data are written.
setthe 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.