genepi-trace.h File Reference

Trace commands used by DIJO. More...

Go to the source code of this file.

Enumerations
enum	genepi_trace_command {   GENEPI_TRACE_ADD_REF = 0,   GENEPI_TRACE_DEL_REF,   GENEPI_TRACE_TOP,   GENEPI_TRACE_BOT,   GENEPI_TRACE_LINEAR,   GENEPI_TRACE_UNION,   GENEPI_TRACE_INTERSECTION,   GENEPI_TRACE_COMPLEMENT,   GENEPI_TRACE_PROJECT,   GENEPI_TRACE_INVPROJECT,   GENEPI_TRACE_APPLY,   GENEPI_TRACE_APPLYINV,   GENEPI_TRACE_CHK_COMPARE,   GENEPI_TRACE_CHK_EMPTY,   GENEPI_TRACE_CHK_FULL,   GENEPI_TRACE_CHK_FINITE,   GENEPI_TRACE_CHK_WIDTH,   GENEPI_TRACE_CHK_DS_SIZE,   GENEPI_TRACE_CHK_NB_VARS,   GENEPI_TRACE_TOP_N,   GENEPI_TRACE_TOP_Z,   GENEPI_TRACE_TOP_P,   GENEPI_TRACE_TOP_R,   GENEPI_TRACE_CHK_SOLUTION }
	Identifier of DIJO commands. More...

Detailed Description

Trace commands used by DIJO.

DIJO is used to reinterpret traces generated by the GENEPI solvers. When the traces are activated (using genepi_solver_set_trace_file()), GENEPI generates a stream of lines. The very first line is the name of the plugin used to generate the trace. Then, following lines are lists of integers separated by white spaces. Each line is a command to be executed by DIJO and the first integer is the identifier of a command, following integers are its arguments. Variables are identified with integers.

Definition in file genepi-trace.h.

Enumeration Type Documentation

enum genepi_trace_command

Identifier of DIJO commands.

Enumerator
GENEPI_TRACE_ADD_REF	syntax: cmd id Apply genepi_set_add_reference to the variable id. The variable id must exist.
GENEPI_TRACE_DEL_REF	syntax: cmd id Apply genepi_set_del_reference to the variable id. The variable id must exist.
GENEPI_TRACE_TOP	syntax: cmd dest_id width Assign to the variable dest_id the result of genepi_set_top (width). If the variable does not exist then it is created.
GENEPI_TRACE_BOT	syntax: cmd dest_id width Assign to the variable dest_id the result of genepi_set_bot (width). If the variable does not exist then it is created.
GENEPI_TRACE_LINEAR	syntax: cmd dest_id cmp cst alpha_size alpha_1 ... Assign to the variable dest_id the result of genepi_set_linear_operation ([alpha_1,...,alpha_{alpha_size}], cmp, cst). If the variable does not exist then it is created.
GENEPI_TRACE_UNION	syntax: cmd dest_id idop1 idop2 Assign to the variable dest_id the result of genepi_set_union (idop1, idop2). Variables idop1 and idop2 must exist.
GENEPI_TRACE_INTERSECTION	syntax: cmd dest_id idop1 idop2 Assign to the variable dest_id the result of genepi_set_intersection (idop1, idop2). Variables idop1 and idop2 must exist.
GENEPI_TRACE_COMPLEMENT	syntax: cmd dest_id idop Assign to the variable dest_id the result of genepi_set_complement (idop1, idop2). Variables idop1 and idop2 must exist.
GENEPI_TRACE_PROJECT	syntax: cmd dest_id idop sel_size sel_1 ... Assign to the variable dest_id the result of genepi_set_project (idop, [sel_1, ..., sel_{sel_size}]). The variable idop must exist.
GENEPI_TRACE_INVPROJECT	syntax: cmd dest_id idop sel_size sel_1 ... Assign to the variable dest_id the result of genepi_set_invproject (idop, [sel_1, ..., sel_{sel_size}]). The variable idop must exist.
GENEPI_TRACE_APPLY	syntax: cmd dest_id idop1 idop2 Assign to the variable dest_id the result of genepi_set_apply (idop1, idop2). Variables idop1 and idop2 must exist.
GENEPI_TRACE_APPLYINV	syntax: cmd dest_id idop1 idop2 Assign to the variable dest_id the result of genepi_set_applyinv (idop1, idop2). Variables idop1 and idop2 must exist.
GENEPI_TRACE_CHK_COMPARE	syntax: cmd cmp idop1 idop2 result Check that the result of genepi_set_compare (idop1, cmp, idop2) is result. Variables idop1 and idop2 must exist. cmp is the integer value of an enumeration genepi_comparator.
GENEPI_TRACE_CHK_EMPTY	syntax: cmd idop result Check that the result of genepi_set_is_empty (idop) is result. The variable idop must exist.
GENEPI_TRACE_CHK_FULL	syntax: cmd idop result Check that the result of genepi_set_is_full (idop) is result. The variable idop must exist.
GENEPI_TRACE_CHK_FINITE	syntax: cmd idop result Check that the result of genepi_set_is_finite (idop) is result. The variable idop must exist.
GENEPI_TRACE_CHK_WIDTH	syntax: cmd idop result Check that the result of genepi_set_get_width (idop) is result. The variable idop must exist.
GENEPI_TRACE_CHK_DS_SIZE	syntax: cmd idop result Check that genepi_set_get_data_structure_size (idop) is result. This test is enabled only if the solver used by DIJO is the same than the one used by GENEPI. The variable idop must exist.
GENEPI_TRACE_CHK_NB_VARS	syntax: cmd result Check that the current number of created variable is result.
GENEPI_TRACE_TOP_N	syntax: cmd dest_id width Assign to the variable dest_id the result of genepi_set_top_N (width). If the variable dest_id does not exist then it is created.
GENEPI_TRACE_TOP_Z	syntax: cmd dest_id width Assign to the variable dest_id the result of genepi_set_top_Z (width). If the variable dest_id does not exist then it is created.
GENEPI_TRACE_TOP_P	syntax: cmd dest_id width Assign to the variable dest_id the result of genepi_set_top_P (width). If the variable dest_id does not exist then it is created.
GENEPI_TRACE_TOP_R	syntax: cmd dest_id width Assign to the variable dest_id the result of genepi_set_top_R (width). If the variable dest_id does not exist then it is created.
GENEPI_TRACE_CHK_SOLUTION	syntax: cmd idop result size xden x_1 ... Check the result of genepi_set_is_solution on idop and [x_1/xden, ..., x_{size}/xden]. The variable idop must exist.

Definition at line 43 of file genepi-trace.h.