#include <limits.h>
#include <ccl/ccl-string.h>
#include <ccl/ccl-tree.h>
#include <ccl/ccl-hash.h>
#include <ccl/ccl-list.h>
#include <ccl/ccl-log.h>

Macros
#define	ARMOISE_DOMAIN_HAS_POSITIVES (((uint32_t)0x1) << 0)
	Attributes of an armoise_domain.

Typedefs
typedef struct armoise_context_st	armoise_context
	Abstract type representing the context of a predicate. More...

typedef struct armoise_predicate_st	armoise_predicate
	Abstract of an ARMOISE predicate.

typedef struct armoise_formula_st	armoise_formula
	Abstract type for a first-order formula.

typedef struct armoise_variable_st	armoise_variable
	Abstract type for a first-order variable.

typedef struct armoise_term_st	armoise_term
	Abstract type for a (first-order) term.

typedef struct armoise_type_st	armoise_type
	Abstract type for variable or predicate types. More...

typedef struct armoise_domain_st	armoise_domain
	Abstract type for domains of variables, terms and predicates.

typedef uint32_t	armoise_domain_attr
	Attributes of an armoise_domain.

Enumerations
enum	armoise_predicate_kind
	Kind of predicates. More...

enum	armoise_formula_kind
	Kind of formula. More...

enum	armoise_term_kind
	Kind of term. More...

Functions
int	armoise_init (void)
	ARMOISE library initializer. More...

void	armoise_terminate (void)
	ARMOISE library finalizer. More...

armoise_context *	armoise_context_create_for_predicates (armoise_context *parent)
	Constructor for contexts storing predicate symbols. More...

armoise_context *	armoise_context_create_for_variables (armoise_context *parent)
	Constructor for contexts storing first order symbols. More...

armoise_context *	armoise_context_add_reference (armoise_context *ctx)
	Adds a new reference to the context ctx. More...

void	armoise_context_del_reference (armoise_context *ctx)
	Suppresses a reference to the context ctx. More...

armoise_context *	armoise_context_get_parent (armoise_context *ctx)
	Returns the parent context of ctx. More...

int	armoise_context_has (armoise_context *ctx, ccl_ustring id)
	Checks if the symbol id exists in the context ctx. More...

int	armoise_context_has_locally (armoise_context *ctx, ccl_ustring id)
	Checks if the symbol id is defined in the context ctx. More...

void *	armoise_context_get (armoise_context *ctx, ccl_ustring id)
	Returns the object associated with the symbol id. More...

void	armoise_context_add (armoise_context ctx, ccl_ustring id, void object)
	Defines symbol id in the context ctx. More...

ccl_hash *	armoise_context_get_table (armoise_context *ctx)
	Returns the symbol table of ctx. More...

ccl_list *	armoise_context_get_ids (armoise_context *ctx)
	Returns the list of symbol locally defined in ctx. More...

int	armoise_context_has_predicate_tree (armoise_context *ctx, ccl_ustring id)
	Checks the existences of a predicate tree id in ctx. More...

ccl_tree *	armoise_context_get_predicate_tree (armoise_context *ctx, ccl_ustring id)
	Retrieves the predicate tree identified by id in ctx. More...

void	armoise_context_add_predicate_tree (armoise_context ctx, ccl_ustring id, ccl_tree tree)
	Associates in ctx the identifier id and the tree of predicates tree. A new reference is added to tree. More...

armoise_predicate *	armoise_context_get_predicate (armoise_context ctx, ccl_ustring id, int nb_indices, const int indices)
	Retrieve the predicate corresponding to a leaf of tree of predicates defined in ctx by the symbol id. More...

const armoise_predicate *	armoise_context_get_cst_predicate (armoise_context ctx, ccl_ustring id, int nb_indices, const int indices)
	Behaves like armoise_context_get_predicate but the result can not be changed by the client code.

int	armoise_context_has_variable (armoise_context *ctx, ccl_ustring id)
	Checks the existences of a first-order variable identified by id in ctx. More...

void	armoise_context_add_variable (armoise_context ctx, armoise_variable var)
	Associates in ctx the identifier armoise_variable_get_name(var) and the first-order variable var. A new reference is added to var. More...

armoise_variable *	armoise_context_get_variable (armoise_context *ctx, ccl_ustring id)
	Retrieves the variable identified by id in ctx. More...

armoise_variable *	armoise_variable_create (ccl_ustring name, armoise_type *type)
	Constructor for a first-order variable defined by its name and its type. More...

void	armoise_variable_del_reference (armoise_variable *variable)
	Suppresses a reference to variable. More...

ccl_ustring	armoise_variable_get_name (armoise_variable *variable)
	Returns the identifier of variable. More...

armoise_type *	armoise_variable_get_type (armoise_variable *variable)
	Returns the type of variable. More...

const armoise_domain *	armoise_variable_get_domain (armoise_variable *variable)
	Returns the domain of variable. More...

void	armoise_variable_set_domain (armoise_variable variable, const armoise_domain D)
	Change the domain D of variable. More...

void	armoise_variable_log (ccl_log_type log, armoise_variable *variable)
	Display the variable on the log stream. More...

armoise_predicate *	armoise_predicate_create_empty (armoise_context ctx, armoise_type type)
	Constructor for an empty and untyped relation. More...

armoise_predicate *	armoise_predicate_create_naturals (armoise_context *ctx)
	Constructor for the predicate representing natural numbers ( $\cal N$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar). More...

armoise_predicate *	armoise_predicate_create_integers (armoise_context *ctx)
	Constructor for the predicate representing integers ( $\cal Z$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar). More...

armoise_predicate *	armoise_predicate_create_positives (armoise_context *ctx)
	Constructor for the real numbers restricted to positive ( ${\cal R}^+$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar). More...

armoise_predicate *	armoise_predicate_create_reals (armoise_context *ctx)
	Constructor for the real numbers ( $\cal R$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar). More...

armoise_predicate *	armoise_predicate_create_indirection (armoise_context ctx, ccl_ustring name, int nb_indices, const int indices)
	Constructor for a predicate that is a reference to another predicate. More...

armoise_predicate *	armoise_predicate_create_union (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the union of relations P1 and P2. More...

armoise_predicate *	armoise_predicate_create_intersection (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the intersection of relations P1 and P2. More...

armoise_predicate *	armoise_predicate_create_delta (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the symetric difference of P1 and P2. More...

armoise_predicate *	armoise_predicate_create_diff (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the difference of P1 and P2. More...

armoise_predicate *	armoise_predicate_create_complement (armoise_context ctx, armoise_predicate P)
	Creates a predicate representing the complement of P. More...

armoise_predicate *	armoise_predicate_create_add (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the arithmetical addition of P1 and P2. More...

armoise_predicate *	armoise_predicate_create_sub (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the arithmetical difference of P1 and P2. More...

armoise_predicate *	armoise_predicate_create_mul (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the multiplicaton of P1 and P2. More...

armoise_predicate *	armoise_predicate_create_div (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the division of P1 by P2. More...

armoise_predicate *	armoise_predicate_create_mod (armoise_context ctx, armoise_predicate P1, armoise_predicate *P2)
	Creates a predicate representing the modulo of P1 by P2. More...

armoise_predicate *	armoise_predicate_create_neg (armoise_context ctx, armoise_predicate P)
	Creates a predicate representing the negation of P. More...

armoise_predicate *	armoise_predicate_create_product (armoise_context ctx, int nb_comp, armoise_predicate *comps)
	Creates a predicate representing the cartesian product comps[0] $\times\dots\times$ comps[nb_comp-1]. More...

armoise_predicate *	armoise_predicate_create_integer (armoise_context *ctx, int i)
	Creates the singleton predicate $\{ i \}$ . More...

armoise_predicate *	armoise_predicate_create_paren (armoise_context ctx, armoise_predicate P)
	Creates a predicate enclosed by parenthesis . More...

armoise_predicate *	armoise_predicate_create_finite_set (armoise_context ctx, int nb_terms, armoise_term *values)
	Creates a predicate encoding a finite set of values. More...

armoise_predicate *	armoise_predicate_create_simple_set (armoise_context ctx, armoise_term proto, armoise_predicate P, armoise_formula def)
	Creates a predicate encoding a set defined by a first-order formula. More...

armoise_predicate *	armoise_predicate_add_reference (armoise_predicate *P)
	Adds a new reference to the predicate P. More...

void	armoise_predicate_del_reference (armoise_predicate *P)
	Suppresses a reference to the predicate P. More...

armoise_domain_attr	armoise_predicate_get_largest_domain (const armoise_predicate *P)
	Computes the smallest reference set (i.e. $\cal N$ , $\cal Z$ , $\cal R^+$ , $\cal R$ ) that contains all elements of P. More...

int	armoise_predicate_get_arity (armoise_predicate *P)
	Returns the number of columns of P. More...

armoise_type *	armoise_predicate_get_type (const armoise_predicate *P)
	Returns the type of P. More...

armoise_context *	armoise_predicate_get_context (const armoise_predicate *P)
	Returns a new reference to the context of P. More...

void	armoise_predicate_log (ccl_log_type log, const armoise_predicate *P)
	Display the predicate P on the log stream. More...

void	armoise_predicate_log_tree (ccl_log_type log, ccl_tree *t)
	Display the tree of predicates t on the log stream. More...

void	armoise_predicate_compute_domain (armoise_predicate *P)
	Computes the domain of P. More...

void	armoise_predicate_get_variables (armoise_predicate P, ccl_list variables)
	Collects free and bound variables in P. More...

armoise_predicate_kind	armoise_predicate_get_kind (const armoise_predicate *P)
	Returns the kind of P. More...

const armoise_predicate *	armoise_predicate_get_operand (const armoise_predicate *P, int i)
	Returns the i th operand of P. More...

armoise_predicate *	armoise_predicate_get_operand_at (const armoise_predicate *P, int i)
	Similar to armoise_predicate_get_operand but the counter of references of the returned operand is incremented.

int	armoise_predicate_get_nb_operands (const armoise_predicate *P)
	Returns the number of operands used to build P. More...

armoise_domain *	armoise_predicate_get_domain (const armoise_predicate *P)
	Returns the domain of P. More...

int	armoise_predicate_get_nb_elements (const armoise_predicate *P)
	Returns the number of elements in a finite set P. More...

const armoise_term *	armoise_predicate_get_element (const armoise_predicate *P, int i)
	Returns the i th element of a finite set P. More...

const armoise_term *	armoise_predicate_get_set_proto (const armoise_predicate P, armoise_predicate *resultP)
	Returns the prototype of the relation P defined by a first-order formula. More...

const armoise_formula *	armoise_predicate_get_set_formula (const armoise_predicate *P)
	Returns the formula of the relation P defined by a first-order formula. More...

void	armoise_predicate_get_indirection (const armoise_predicate P, ccl_ustring p_name, int p_nb_indices, const int *p_indices)
	Retrieves indirection informations pointed by P. More...

armoise_formula *	armoise_formula_add_reference (armoise_formula *F)
	Adds a new reference to the formula F. More...

void	armoise_formula_del_reference (armoise_formula *F)
	Suppresses a reference to the formula F. More...

armoise_formula_kind	armoise_formula_get_kind (const armoise_formula *F)
	Returns the kind of formula is pointed by F. More...

armoise_formula *	armoise_formula_create_constant (int value)
	Creates a formula encoding the Boolean value. More...

armoise_formula *	armoise_formula_create_in (armoise_term t, armoise_predicate P)
	Creates a formula encoding membership checking of t in P. More...

armoise_formula *	armoise_formula_create_or (armoise_formula F1, armoise_formula F2)
	Creates a formula encoding the disjunction of F1 and F2. More...

armoise_formula *	armoise_formula_create_and (armoise_formula F1, armoise_formula F2)
	Creates a formula encoding the conjunction of F1 and F2. More...

armoise_formula *	armoise_formula_create_equiv (armoise_formula F1, armoise_formula F2)
	Creates a formula encoding the equivalence of F1 and F2. More...

armoise_formula *	armoise_formula_create_imply (armoise_formula F1, armoise_formula F2)
	Creates a formula encoding the implication of F2 by F1. More...

armoise_formula *	armoise_formula_create_not (armoise_formula *F)
	Creates a formula encoding the negation of F. More...

armoise_formula *	armoise_formula_create_eq (armoise_term t1, armoise_term t2)
	Creates a formula encoding the equality of t1 and t2. More...

armoise_formula *	armoise_formula_create_neq (armoise_term t1, armoise_term t2)
	Creates a formula encoding the not-equality of t1 and t2. More...

armoise_formula *	armoise_formula_create_leq (armoise_term t1, armoise_term t2)
	Creates a formula encoding the inequality of t1 <= t2. More...

armoise_formula *	armoise_formula_create_geq (armoise_term t1, armoise_term t2)
	Creates a formula encoding the inequality of t1 >= t2. More...

armoise_formula *	armoise_formula_create_lt (armoise_term t1, armoise_term t2)
	Creates a formula encoding the inequality of t1 < t2. More...

armoise_formula *	armoise_formula_create_gt (armoise_term t1, armoise_term t2)
	Creates a formula encoding the inequality of t1 < t2. More...

armoise_formula *	armoise_formula_create_paren (armoise_formula *F)
	Creates a formula enclosed with parenthesis (F). More...

armoise_formula *	armoise_formula_create_exists (armoise_term qvars, armoise_predicate dom, armoise_formula *F)
	Quantifies existentially the formula F by the nb_vars variables given in qvars. More...

armoise_formula *	armoise_formula_create_forall (armoise_term qvars, armoise_predicate dom, armoise_formula *F)
	Quantifies universally the formula F by the nb_vars variables given in qvars. More...

void	armoise_formula_log (ccl_log_type log, armoise_formula *F)
	Display the formula F on the log stream. More...

void	armoise_formula_get_variables (const armoise_formula F, ccl_list variables)
	Collects free and bound variables in F. More...

int	armoise_formula_get_value (const armoise_formula *F)
	Returns the value of the Boolean constant encoded by F. More...

const armoise_formula *	armoise_formula_get_operand (const armoise_formula *F, int i)
	Returns the i th operands of F. More...

int	armoise_formula_get_nb_operands (const armoise_formula *F)
	Returns the number of operands of F. More...

const armoise_formula *	armoise_formula_get_quantified_formula (const armoise_formula *F)
	Returns the formula part of a quantified formula F. More...

armoise_term *	armoise_formula_get_quantified_variables (const armoise_formula F, armoise_predicate *p_domain)
	Returns the quantified variables of the quantified formula pointed by F. More...

armoise_term *	armoise_formula_get_in_term (const armoise_formula *F)
	Returns the term of a membership formula F. More...

armoise_predicate *	armoise_formula_get_in_predicate (const armoise_formula *F)
	Returns the term of a membership checking formula F. More...

armoise_term *	armoise_formula_get_cmp_left_term (const armoise_formula *F)
	Returns the left operand of the comparison encoded by F. More...

armoise_term *	armoise_formula_get_cmp_right_term (const armoise_formula *F)
	Returns the righr operand of the comparison encoded by F. More...

armoise_term *	armoise_term_add_reference (armoise_term *t)
	Adds a new reference to the term t. More...

void	armoise_term_del_reference (armoise_term *t)
	Suppresses a reference to the term t. More...

armoise_term_kind	armoise_term_get_kind (const armoise_term *t)
	Returns the kind of t. More...

int	armoise_term_get_dim (const armoise_term *t)
	Returns the dimension of the term t. More...

int	armoise_term_get_arity (const armoise_term *t)
	Returns the number of operand of t. More...

int	armoise_term_is_constant (const armoise_term *t)
	Check if the t is constant or not. More...

armoise_type *	armoise_term_get_type (const armoise_term *t)
	Returns the type of t. More...

armoise_variable *	armoise_term_get_variable (const armoise_term *t)
	Returns the armoise_variable underlying t. More...

void	armoise_term_get_value (const armoise_term t, int num, int *den)
	Retrieves the value of the constant encoded by t. More...

armoise_term *	armoise_term_get_operand_at (armoise_term *t, int i)
	Returns a new reference to the i th operand of t. More...

armoise_term *	armoise_term_create_variable (armoise_variable *v)
	Creates a new term encoding the variable v. More...

armoise_term *	armoise_term_create_vector_element (armoise_term *variable, int index)
	Creates a new term encoding the index th element of the vector variable. More...

armoise_term *	armoise_term_create_constant (int num, int den)
	Creates a new term encoding the rational number num / den. More...

armoise_term *	armoise_term_create_vector (int width, armoise_term **terms)
	Creates a term encoding a vector of terms. More...

armoise_term *	armoise_term_create_neg (armoise_term *t)
	Creates a term encoding the opposite of t. More...

armoise_term *	armoise_term_create_mul (armoise_term t1, armoise_term t2)
	Creates a term encoding the multiplication of t1 and t2. More...

armoise_term *	armoise_term_create_div (armoise_term t1, armoise_term t2)
	Creates a term encoding the division of t1 by t2. More...

armoise_term *	armoise_term_create_mod (armoise_term t1, armoise_term t2)
	Creates a term encoding the modulo of t1 by t2. More...

armoise_term *	armoise_term_create_add (armoise_term t1, armoise_term t2)
	Creates a term encoding the addition of t1 and t2. More...

armoise_term *	armoise_term_create_sub (armoise_term t1, armoise_term t2)
	Creates a term encoding the difference of t1 and t2. More...

void	armoise_term_log (ccl_log_type log, armoise_term *t)
	Display the term t on the log stream. More...

void	armoise_term_get_variables (const armoise_term t, ccl_list variables)
	Collects free and bound variables in t. More...

int	armoise_term_get_nb_operands (const armoise_term *t)
	Returns the number of operands of t. More...

const armoise_term *	armoise_term_get_operand (const armoise_term *t, int i)
	Returns the i th operand of P. More...

const armoise_term *	armoise_term_get_vec_element_variable (const armoise_term *t)
	Returns the variable referenced by a vector element term t. More...

int	armoise_term_get_vec_element_index (const armoise_term *t)
	Returns the index used by a vector element term t. More...

armoise_type *	armoise_type_create_scalar (void)
	Creates the scalar type.

armoise_type *	armoise_type_create_product (int nb_subtypes, armoise_type **subtypes)
	Creates a composite type made of nb_subtypes subtypes. More...

int	armoise_type_is_scalar (const armoise_type *type)
	Returns a non-null value if type is scalar. More...

armoise_type *	armoise_type_add_reference (armoise_type *type)
	Adds a new reference to type. More...

void	armoise_type_del_reference (armoise_type *type)
	Suppresses a reference to type. More...

int	armoise_type_get_width (const armoise_type *type)
	Returns the number of component of type. More...

int	armoise_type_get_depth_width (const armoise_type *type)
	Returns the number of leaves composing type. More...

void	armoise_type_log (ccl_log_type log, const armoise_type *type)
	Display the type on the log stream. More...

int	armoise_type_equals (const armoise_type type, const armoise_type other)
	Check whether type and other are equal. More...

armoise_type **	armoise_type_get_subtype_ref (armoise_type *type, int i)
	Returns the reference of the i th subtype of type. More...

const armoise_type *	armoise_type_get_subtype (const armoise_type *type, int i)
	Returns the i th subtype of type. More...

armoise_type *	armoise_type_duplicate (const armoise_type *type)
	Creates a copy of type. More...

armoise_domain *	armoise_domain_create_with_attr (const armoise_domain_attr attr)
	Creates a domain with given attibutes attr. More...

armoise_domain *	armoise_domain_create (void)
	Creates a domain containing real numbers. More...

armoise_domain *	armoise_domain_create_empty (void)
	Creates an empty domain. More...

armoise_domain *	armoise_domain_create_compound_domain (int width, armoise_domain **domains)
	Creates a domain composed of width domains. More...

armoise_domain *	armoise_domain_add_reference (armoise_domain *d)
	Adds a new reference to the domain d. More...

void	armoise_domain_del_reference (armoise_domain *d)
	Suppresses a reference to the domain d. More...

int	armoise_domain_get_width (const armoise_domain *d)
	Returns the number of components of d. More...

int	armoise_domain_is_empty (const armoise_domain *d)
	Checks if d is empty. More...

const armoise_domain *	armoise_domain_get_component (const armoise_domain *d, int i)
	Returns the i th component of d. More...

void	armoise_domain_set_component (armoise_domain d, int i, const armoise_domain di)
	Changes the i th component of d with di. More...

int	armoise_domain_get_min (const armoise_domain *d)
	Returns the lower bound of d. More...

int	armoise_domain_get_max (const armoise_domain *d)
	Returns the upper bound of d. More...

void	armoise_domain_set_attr (armoise_domain *d, const armoise_domain_attr attr)
	Changes the attributes of d. More...

armoise_domain_attr	armoise_domain_get_attr (const armoise_domain *d)
	Returns attributes defining d. More...

int	armoise_domain_is_finite (const armoise_domain *d)
	Checks if d is finite. More...

int	armoise_domain_is_restricted_to_integers (const armoise_domain *d)
	Checks if d is a subset of integers. More...

void	armoise_domain_log (ccl_log_type log, const armoise_domain *d)
	Display the domain on the log stream. More...

armoise_domain *	armoise_domain_duplicate (const armoise_domain *d)
	Return a copy of d. More...

int	armoise_domain_equals (const armoise_domain d1, const armoise_domain d2)
	Checks if d1 and d2 are equal. More...

int	armoise_domain_is_singleton (const armoise_domain *d)
	Checks if d contains only one element. More...

Variables
const armoise_domain_attr	ARMOISE_DOMAIN_ATTR_FOR_REALS
	Attributes for the domain $\cal R$ .

const armoise_domain_attr	ARMOISE_DOMAIN_ATTR_FOR_INTEGERS
	Attributes for the domain $\cal Z$ .

const armoise_domain_attr	ARMOISE_DOMAIN_ATTR_FOR_POSITIVES
	Attributes for the domain ${\cal R}^+$ .

const armoise_domain_attr	ARMOISE_DOMAIN_ATTR_FOR_NATURALS
	Attributes for the domain ${\cal N}$ .

Typedef Documentation

typedef struct armoise_context_st armoise_context

Abstract type representing the context of a predicate.

An armoise_context of a predicate stores all definition usable by a predicate. It is mainly the "in" part of a predicate. It inherits definitions of parent contexts. A context can be used to store either predicate symbols or first-order variables. Predicates are stored has ccl_tree and first-order variables as armoise_variable.

See Also: armoise_context_create_for_predicates, armoise_context_create_for_variables

Definition at line 46 of file armoise.h.

typedef struct armoise_type_st armoise_type

Abstract type for variable or predicate types.

A type can be unknown, scalar or a vector of types. 0 for the scalar type and the number of sub-types for the others.

Definition at line 143 of file armoise.h.

Enumeration Type Documentation

enum armoise_formula_kind

Kind of formula.

See Also: armoise_formula_get_kind

Definition at line 91 of file armoise.h.

enum armoise_predicate_kind

Kind of predicates.

See Also: armoise_predicate_get_kind

Definition at line 58 of file armoise.h.

enum armoise_term_kind

Kind of term.

See Also: armoise_term_get_kind

Definition at line 124 of file armoise.h.

Function Documentation

void armoise_context_add	(	armoise_context *	ctx,
		ccl_ustring	id,
		void *	object
	)

Defines symbol id in the context ctx.

This function assaciates in the symbol table of ctx the symbol id and the object (predicate or variable) object. The symbol must not exists in the table (i.e. it can not be redefined locally) however it can exist a parent context of ctx (i.e. the definition locally replaces the one of the parent).

Parameters

ctx	the considered context
id	the defined symbol
object	the object associated with id.

Precondition: ! armoise_context_has_locally (ctx, id); object != NULL

void armoise_context_add_predicate_tree	(	armoise_context *	ctx,
		ccl_ustring	id,
		ccl_tree *	tree
	)

Associates in ctx the identifier id and the tree of predicates tree. A new reference is added to tree.

See Also: armoise_context_add

armoise_context* armoise_context_add_reference ( armoise_context * ctx )

Adds a new reference to the context ctx.

This function increments the counter of references to ctx.

Parameters

ctx	the context newly referenced

Precondition: ctx != NULL

Returns: the pointer to ctx

void armoise_context_add_variable	(	armoise_context *	ctx,
		armoise_variable *	var
	)

Associates in ctx the identifier armoise_variable_get_name(var) and the first-order variable var. A new reference is added to var.

See Also: armoise_context_add

armoise_context* armoise_context_create_for_predicates ( armoise_context * parent )

Constructor for contexts storing predicate symbols.

The context does not store predicates as armoise_predicate but as ccl_tree trees.

Parameters

parent the parent context from which the result inherits definitions. It can be NULL.

Returns: a newly created context

See Also: armoise_context_add_predicate

armoise_context* armoise_context_create_for_variables ( armoise_context * parent )

Constructor for contexts storing first order symbols.

Parameters

parent the parent context from which the result inherits definitions. It can be NULL.

Returns: a newly created context

See Also: armoise_context_add_variable

void armoise_context_del_reference ( armoise_context * ctx )

Suppresses a reference to the context ctx.

This function decrements the counter of references to ctx. If this counter falls to 0 then the ressources allocated to ctx are released.

Parameters

ctx	the unreferenced context

Precondition: ctx != NULL; the number of references to ctx > 0

void* armoise_context_get	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Returns the object associated with the symbol id.

The function looks for id in the symbol table of ctx and those of its parents. If id is found then the object associated with it is returned.

Parameters

ctx	the considered context
id	the looked for symbol.

Precondition: ctx != NULL

Returns: a pointer to the object defining the symbol id or NULL if id is not an existing symbol.

ccl_list* armoise_context_get_ids ( armoise_context * ctx )

Returns the list of symbol locally defined in ctx.

The returned ccl_list contains the identifiers locally defined in ctx in their definition order. This list must not be modified.

Parameters

ctx	the considered context

Precondition: ctx != NULL

Returns: the internal list of symbols of ctx

armoise_context* armoise_context_get_parent ( armoise_context * ctx )

Returns the parent context of ctx.

Parameters

ctx	the context

Precondition: ctx != NULL

Returns: a new reference to the parent context of ctx or NULL if ctx has no parent.

armoise_predicate* armoise_context_get_predicate	(	armoise_context *	ctx,
		ccl_ustring	id,
		int	nb_indices,
		const int *	indices
	)

Retrieve the predicate corresponding to a leaf of tree of predicates defined in ctx by the symbol id.

This function assumes that a tree corresponding to a parallel definition of predicates exists in ctx. Then the function searches through the tree according to indices which indicates the index of child nodes to follow.

Precondition: armoise_context_get_predicate_tree (ctx, id) != NULL

Returns: a new reference to the predicate associated with id [indices[0]] ... [indices[nb_indices-1]]

ccl_tree* armoise_context_get_predicate_tree	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Retrieves the predicate tree identified by id in ctx.

Returns: a new reference to the ccl_tree or NULL

See Also: armoise_context_get

ccl_hash* armoise_context_get_table ( armoise_context * ctx )

Returns the symbol table of ctx.

The returned ccl_hash table associates ccl_ustring identifiers and armoise_predicate or armoise_variable objects. This table must not be modified.

Parameters

ctx	the considered context

Precondition: ctx != NULL

Returns: the internal symbol table of ctx

armoise_variable* armoise_context_get_variable	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Retrieves the variable identified by id in ctx.

Returns: a new reference to the armoise_variable or NULL

See Also: armoise_context_get

int armoise_context_has	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Checks if the symbol id exists in the context ctx.

Parameters

ctx	the considered context
id	the looked for symbol

Precondition: ctx != NULL

Returns: "a non-null value" if id belongs to ctx or one of its parent contexts.

int armoise_context_has_locally	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Checks if the symbol id is defined in the context ctx.

The existence test is not propagate to parent contexts.

Parameters

ctx	the considered context
id	the looked for symbol.

Precondition: ctx != NULL

Returns: "a non-null value" if id is defined by ctx.

int armoise_context_has_predicate_tree	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Checks the existences of a predicate tree id in ctx.

See Also: armoise_context_has

int armoise_context_has_variable	(	armoise_context *	ctx,
		ccl_ustring	id
	)

Checks the existences of a first-order variable identified by id in ctx.

See Also: armoise_context_has

armoise_domain* armoise_domain_add_reference ( armoise_domain * d )

Adds a new reference to the domain d.

This function increments the counter of references to d.

Parameters

d	the domain newly referenced

Precondition: d != NULL

Returns: the pointer to d

armoise_domain* armoise_domain_create ( void )

Creates a domain containing real numbers.

Returns: a domain containing real numbers

armoise_domain* armoise_domain_create_compound_domain	(	int	width,
		armoise_domain **	domains
	)

Creates a domain composed of width domains.

Parameters

width	the number of components
domains	the components of the result

Precondition: width >= 1; domains != NULL

Returns: the compound domain $domains[0]\times\dots\times domains[width-1]$

armoise_domain* armoise_domain_create_empty ( void )

Creates an empty domain.

Returns: an empty domain

armoise_domain* armoise_domain_create_with_attr ( const armoise_domain_attr attr )

Creates a domain with given attibutes attr.

Parameters

attr	the attributes

Returns: a domain with given attibutes attr

void armoise_domain_del_reference ( armoise_domain * d )

Suppresses a reference to the domain d.

This function decrements the counter of references to d. If this counter falls to 0 then the ressources allocated to ctx are released.

Parameters

d	the unreferenced domain

Precondition: d != NULL; the number of references to d > 0

armoise_domain* armoise_domain_duplicate ( const armoise_domain * d )

Return a copy of d.

Parameters

d	the domain

Precondition: d != NULL

Returns: a copy of d

int armoise_domain_equals	(	const armoise_domain *	d1,
		const armoise_domain *	d2
	)

Checks if d1 and d2 are equal.

Parameters

d1	the first domain
d2	the second domain

Precondition: d1 != NULL; d2 != NULL

Returns: a non null value if d1 = d2

armoise_domain_attr armoise_domain_get_attr ( const armoise_domain * d )

Returns attributes defining d.

Parameters

d	the domain

Precondition: d != NULL

Returns: the attributes defining d

const armoise_domain* armoise_domain_get_component	(	const armoise_domain *	d,
		int	i
	)

Returns the i th component of d.

Parameters

d	the domain
i	the index of the component

Precondition: d != NULL; 0 <= i && i < armoise_domain_get_width (d)

Returns: the i th component of d

int armoise_domain_get_max ( const armoise_domain * d )

Returns the upper bound of d.

Parameters

d	the domain

Precondition: d != NULL

Returns: the upper bound of d

int armoise_domain_get_min ( const armoise_domain * d )

Returns the lower bound of d.

Parameters

d	the domain

Precondition: d != NULL

Returns: the lower bound of d

int armoise_domain_get_width ( const armoise_domain * d )

Returns the number of components of d.

Parameters

d	the domain

Precondition: d != NULL

Returns: the number of components of d

int armoise_domain_is_empty ( const armoise_domain * d )

Checks if d is empty.

Parameters

d	the domain

Precondition: d != NULL

Returns: a non null value if d contains no element.

int armoise_domain_is_finite ( const armoise_domain * d )

Checks if d is finite.

Parameters

d	the domain

Precondition: d != NULL

Returns: a non null value if d contains a finite number of elements

int armoise_domain_is_restricted_to_integers ( const armoise_domain * d )

Checks if d is a subset of integers.

Parameters

d	the domain

Precondition: d != NULL

Returns: a non null value if d is a subset of integers

int armoise_domain_is_singleton ( const armoise_domain * d )

Checks if d contains only one element.

Parameters

d	the domain

Precondition: d != NULL

Returns: a non null value if d is a singleton

void armoise_domain_log	(	ccl_log_type	log,
		const armoise_domain *	d
	)

Display the domain on the log stream.

Parameters

log	the stream where the domain is displayed
d	the domain send on log

Precondition: d != NULL

void armoise_domain_set_attr	(	armoise_domain *	d,
		const armoise_domain_attr	attr
	)

Changes the attributes of d.

Parameters

d	the domain
attr	the new attributes for d

Precondition: d != NULL

Returns: the attributes defining d

void armoise_domain_set_component	(	armoise_domain *	d,
		int	i,
		const armoise_domain *	di
	)

Changes the i th component of d with di.

Parameters

d	the domain
i	the index of the component
di	the new component

Precondition: d != NULL; di != NULL; 0 <= i && i <= armoise_domain_get_width (d)

armoise_formula* armoise_formula_add_reference ( armoise_formula * F )

Adds a new reference to the formula F.

This function increments the counter of references to F.

Parameters

F	the formula newly referenced

Precondition: F != NULL

Returns: the pointer to F

armoise_formula* armoise_formula_create_and	(	armoise_formula *	F1,
		armoise_formula *	F2
	)

Creates a formula encoding the conjunction of F1 and F2.

Parameters

F1	the first operand
F2	the second operand

Precondition: F1 != NULL; F2 != NULL

Returns: a formula of kind ARMOISE_F_AND encoding $F1 \wedge F2$

armoise_formula* armoise_formula_create_constant ( int value )

Creates a formula encoding the Boolean value.

The function creates a formula that encode either true if value is not 0 or false if value is null.

Parameters

value the Boolean value

Returns: a newly created formula encoding true or false of kind ARMOISE_F_CONSTANT

armoise_formula* armoise_formula_create_eq	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a formula encoding the equality of t1 and t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a formula of kind ARMOISE_F_EQ encoding $t1\Rightarrow t2$

armoise_formula* armoise_formula_create_equiv	(	armoise_formula *	F1,
		armoise_formula *	F2
	)

Creates a formula encoding the equivalence of F1 and F2.

Parameters

F1	the first operand
F2	the second operand

Precondition: F1 != NULL; F2 != NULL

Returns: a formula of kind ARMOISE_F_EQUIV encoding $f1\Leftrightarrow F2$

armoise_formula* armoise_formula_create_exists	(	armoise_term *	qvars,
		armoise_predicate *	dom,
		armoise_formula *	F
	)

Quantifies existentially the formula F by the nb_vars variables given in qvars.

Parameters

nb_qvars	the number of variables to quantify
qvars	the variables to quantify
F	the quantified formula

Precondition: nb_qvars > 0; qvars != NULL; F != NULL

Returns: a formula of kind ARMOISE_F_EXISTS encoding $\exists qvars[0], \dots, \exists qvars[nb\_qvars-1] F$

armoise_formula* armoise_formula_create_forall	(	armoise_term *	qvars,
		armoise_predicate *	dom,
		armoise_formula *	F
	)

Quantifies universally the formula F by the nb_vars variables given in qvars.

Parameters

nb_qvars	the number of variables to quantify
qvars	the variables to quantify
F	the quantified formula

Precondition: nb_qvars > 0; qvars != NULL; F != NULL

Returns: a formula of kind ARMOISE_F_FORALL encoding $\forall qvars[0], \dots, \forall qvars[nb\_qvars-1] F$

armoise_formula* armoise_formula_create_geq	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a formula encoding the inequality of t1 >= t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a formula of kind ARMOISE_F_GEQ encoding $t1\geq t2$

armoise_formula* armoise_formula_create_gt	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a formula encoding the inequality of t1 < t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a formula of kind ARMOISE_F_GT encoding

armoise_formula* armoise_formula_create_imply	(	armoise_formula *	F1,
		armoise_formula *	F2
	)

Creates a formula encoding the implication of F2 by F1.

Parameters

F1	the first operand
F2	the second operand

Precondition: F1 != NULL; F2 != NULL

Returns: a formula of kind ARMOISE_F_IMPLY encoding $F1\Rightarrow F2$

armoise_formula* armoise_formula_create_in	(	armoise_term *	t,
		armoise_predicate *	P
	)

Creates a formula encoding membership checking of t in P.

Parameters

P	the predicate.
t	the value that the membership is checked

Precondition: t != NUL; P != NUL

Returns: a formula of kind ARMOISE_F_IN encoding $t \in P$

armoise_formula* armoise_formula_create_leq	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a formula encoding the inequality of t1 <= t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a formula of kind ARMOISE_F_LEQ encoding $t1\leq t2$

armoise_formula* armoise_formula_create_lt	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a formula encoding the inequality of t1 < t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a formula of kind ARMOISE_F_LT encoding

armoise_formula* armoise_formula_create_neq	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a formula encoding the not-equality of t1 and t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a formula of kind ARMOISE_F_NEQ encoding $t1\not= t2$

armoise_formula* armoise_formula_create_not ( armoise_formula * F )

Creates a formula encoding the negation of F.

Parameters

F	the operand

Precondition: F != NULL

Returns: a formula of kind ARMOISE_F_NOT encoding $\neg F$

armoise_formula* armoise_formula_create_or	(	armoise_formula *	F1,
		armoise_formula *	F2
	)

Creates a formula encoding the disjunction of F1 and F2.

Parameters

F1	the first operand
F2	the second operand

Precondition: F1 != NULL; F2 != NULL

Returns: a formula of kind ARMOISE_F_OR encoding $F1 \vee F2$

armoise_formula* armoise_formula_create_paren ( armoise_formula * F )

Creates a formula enclosed with parenthesis (F).

Parameters

F	the operand

Precondition: F != NULL

Returns: a formula of kind ARMOISE_F_PAREN encoding

void armoise_formula_del_reference ( armoise_formula * F )

Suppresses a reference to the formula F.

This function decrements the counter of references to F. If this counter falls to 0 then the ressources allocated to f are released.

Parameters

F	the unreferenced formula

Precondition: F != NULL; the number of references to F > 0

armoise_term* armoise_formula_get_cmp_left_term ( const armoise_formula * F )

Returns the left operand of the comparison encoded by F.

Parameters

F	the comparison formula

Precondition: F != NULL

Returns: the left operand of F.

armoise_term* armoise_formula_get_cmp_right_term ( const armoise_formula * F )

Returns the righr operand of the comparison encoded by F.

Parameters

F	the comparison formula

Precondition: F != NULL

Returns: the right operand of F.

armoise_predicate* armoise_formula_get_in_predicate ( const armoise_formula * F )

Returns the term of a membership checking formula F.

Parameters

F	the formula

Precondition: armoise_formula_get_kind (F) == ARMOISE_F_IN

Returns: the term t of the membership checking formula F.

armoise_term* armoise_formula_get_in_term ( const armoise_formula * F )

Returns the term of a membership formula F.

Parameters

F	the formula

Precondition: armoise_formula_get_kind (F) == ARMOISE_F_IN

Returns: the term t of the membership encoded by F.

armoise_formula_kind armoise_formula_get_kind ( const armoise_formula * F )

Returns the kind of formula is pointed by F.

Parameters

F	the formula

Precondition: F != NULL

Returns: the kind of formula of F

int armoise_formula_get_nb_operands ( const armoise_formula * F )

Returns the number of operands of F.

Parameters

F	the formula

Precondition: F != NULL

Returns: the number of operands of F

const armoise_formula* armoise_formula_get_operand	(	const armoise_formula *	F,
		int	i
	)

Returns the i th operands of F.

Parameters

F	the formula
i	the index of the expected operand

Precondition: 0 <= i && i < armoise_formula_get_nb_operands (F)

Returns: a non null value if F encodes true

const armoise_formula* armoise_formula_get_quantified_formula ( const armoise_formula * F )

Returns the formula part of a quantified formula F.

Parameters

F	the formula

Precondition: (armoise_formula_get_kind (F) == ARMOISE_F_EXISTS || armoise_formula_get_kind (F) == ARMOISE_F_FORALL)

Returns: the sub-formula of F that is quantified

armoise_term* armoise_formula_get_quantified_variables	(	const armoise_formula *	F,
		armoise_predicate **	p_domain
	)

Returns the quantified variables of the quantified formula pointed by F.

Parameters

F	the formula
p_nb_vars	a pointer to the integer receiving the number of quantified variables of F

Precondition: (armoise_formula_get_kind (F) == ARMOISE_F_EXISTS || armoise_formula_get_kind (F) == ARMOISE_F_FORALL)

Returns: the quantified variables defining F

int armoise_formula_get_value ( const armoise_formula * F )

Returns the value of the Boolean constant encoded by F.

Parameters

F	the formula

Precondition: armoise_formula_get_kind (F) == ARMOISE_F_CONSTANT

Returns: a non null value if F encodes true

void armoise_formula_get_variables	(	const armoise_formula *	F,
		ccl_list *	variables
	)

Collects free and bound variables in F.

The function goes through the structure of F and collects encountered armoise_variable's. Each collected variable is added (once) to the list variables.

Parameters

F	the formula
variables	the list receiving the variables

Precondition: F != NULL; variables != NULL

void armoise_formula_log	(	ccl_log_type	log,
		armoise_formula *	F
	)

Display the formula F on the log stream.

Parameters

log	the stream where the formula is displayed
F	the formula send on log

Precondition: F != NULL

int armoise_init ( void )

ARMOISE library initializer.

This function must be call prior to any other ARMOISE function call.

Returns: a non-null value if the initialization process is successful.

armoise_predicate* armoise_predicate_add_reference ( armoise_predicate * P )

Adds a new reference to the predicate P.

This function increments the counter of references to P.

Parameters

P	the predicate newly referenced

Precondition: P != NULL

Returns: the pointer to P

void armoise_predicate_compute_domain ( armoise_predicate * P )

Computes the domain of P.

This function tries to determine the finest domain of columns of P

Parameters

P	the predicate

Precondition: P != NULL

See Also: armoise_domain

armoise_predicate* armoise_predicate_create_add	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the arithmetical addition of P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: the predicate of kind ARMOISE_P_ADD encoding $P1+P2 = \{ p \mid \exists p_1\in P1, \exists p_2\in P2, p = p_1+p_2 \}$

armoise_predicate* armoise_predicate_create_complement	(	armoise_context *	ctx,
		armoise_predicate *	P
	)

Creates a predicate representing the complement of P.

P is complemented relatively to $\cal R$ . The result inherits its type from P.

Parameters

ctx	the context of the newly created predicate
P	the complemented predicate

Precondition: P != NULL

Returns: the predicate of kind ARMOISE_P_COMPLEMENT encoding $\overline{P}$

armoise_predicate* armoise_predicate_create_delta	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the symetric difference of P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: a predicate of kind ARMOISE_P_DELTA encoding $P1\Delta P2 = P1\setminus P2 \cup P2\setminus P1$

armoise_predicate* armoise_predicate_create_diff	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the difference of P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: a predicate of kind ARMOISE_P_DIFF encoding $P1\setminus P2$

armoise_predicate* armoise_predicate_create_div	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the division of P1 by P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: the predicate of kind ARMOISE_P_DIV encoding $P1 \times P2 = \{ p \mid \exists p_1\in P1, \exists p_2\in P2\setminus \{ 0 \}, p = p_1 / p_2 \}$

armoise_predicate* armoise_predicate_create_empty	(	armoise_context *	ctx,
		armoise_type *	type
	)

Constructor for an empty and untyped relation.

The type of the predicate is set to unknown (cf. armoise_type_is_unknown).

Parameters

ctx	the context

Precondition: ctx != NULL

Returns: a predicate of kind ARMOISE_P_EMPTY

armoise_predicate* armoise_predicate_create_finite_set	(	armoise_context *	ctx,
		int	nb_terms,
		armoise_term **	values
	)

Creates a predicate encoding a finite set of values.

The result inherits its type from the first typed element in values.

Parameters

ctx	the context of the newly created predicate
nb_terms	the number of values in the set
values	the constant terms that define the values

Returns: the predicate of kind ARMOISE_P_ENUM encoding $\{ values[0], \dots, values[\mbox{nb\_terms}-1] \}$

armoise_predicate* armoise_predicate_create_indirection	(	armoise_context *	ctx,
		ccl_ustring	name,
		int	nb_indices,
		const int *	indices
	)

Constructor for a predicate that is a reference to another predicate.

The predicate returned by this function refers to name [indices[0]] ... [indices[nb_indices-1]] where name is the name of a parallel definition of predicates. Of course, nb_indices can be zero if name refers to simple predicate definition.

The newly created predicate inherits the type of the predicate it makes a reference. The array indices is duplicated.

Parameters

ctx	the context of the newly created predicate
name	the identifier of a predicate or ccl_tree defined in ctx.
nb_indices	depth of search the ccl_tree referred by name
indices	array of indices indicating the path to follow in the ccl_tree pointed by name.

Precondition: name != NULL; index >= 0

Returns: a predicate of kind ARMOISE_P_INDIRECTION equal to name [indices[0]] ... [indices[nb_indices-1]]

armoise_predicate* armoise_predicate_create_integer	(	armoise_context *	ctx,
		int	i
	)

Creates the singleton predicate $\{ i \}$ .

The type of the result is set to scalar.

Parameters

ctx	the context of the newly created predicate
i	the single element in the resulting predicate.

Returns: the predicate of kind ARMOISE_P_ENUM encoding $\{ i \}$

armoise_predicate* armoise_predicate_create_integers ( armoise_context * ctx )

Constructor for the predicate representing integers ( $\cal Z$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar).

Parameters

ctx	the context

Precondition: ctx != NULL

Returns: a predicate of kind ARMOISE_P_INT

armoise_predicate* armoise_predicate_create_intersection	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the intersection of relations P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: a predicate of kind ARMOISE_P_INTERSECTION encoding $P1\cap P2$

armoise_predicate* armoise_predicate_create_mod	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the modulo of P1 by P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: the predicate of kind ARMOISE_P_MOD encoding $P1 \times P2 = \{ p \mid \exists p_1\in P1, \exists p_2\in P2\setminus \{ 0 \}, p = p_1 \% p_2 \}$

armoise_predicate* armoise_predicate_create_mul	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the multiplicaton of P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: the predicate of kind ARMOISE_P_MUL encoding $P1 \times P2 = \{ p \mid \exists p_1\in P1, \exists p_2\in P2, p = p_1 \times p_2 \}$

armoise_predicate* armoise_predicate_create_naturals ( armoise_context * ctx )

Constructor for the predicate representing natural numbers ( $\cal N$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar).

Parameters

ctx	the context

Precondition: ctx != NULL

Returns: a predicate of kind ARMOISE_P_NAT

armoise_predicate* armoise_predicate_create_neg	(	armoise_context *	ctx,
		armoise_predicate *	P
	)

Creates a predicate representing the negation of P.

The result inherits its type from P.

Parameters

ctx	the context of the newly created predicate
P	the operand

Precondition: P != NULL

Returns: the predicate of kind ARMOISE_P_NEG encoding $-P = \{ p \mid \exists p^\prime\in P, p = -p^\prime \}$

armoise_predicate* armoise_predicate_create_paren	(	armoise_context *	ctx,
		armoise_predicate *	P
	)

Creates a predicate enclosed by parenthesis $(P)$ .

The result inherits its type from P.

Parameters

ctx	the context of the newly created predicate
P	the predicate

Returns: the predicate of kind ARMOISE_P_PAREN encoding

armoise_predicate* armoise_predicate_create_positives ( armoise_context * ctx )

Constructor for the real numbers restricted to positive ( ${\cal R}^+$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar).

Parameters

ctx	the context

Precondition: ctx != NULL

Returns: a predicate of kind ARMOISE_P_POSI

armoise_predicate* armoise_predicate_create_product	(	armoise_context *	ctx,
		int	nb_comp,
		armoise_predicate **	comps
	)

Creates a predicate representing the cartesian product comps[0] $\times\dots\times$ comps[nb_comp-1].

The type of the result is the product of types of comps[i]'s.

Parameters

ctx	the context of the newly created predicate
nb_comp	the number of components of the product
comps	the components

Returns: the predicate of kind ARMOISE_P_PRODUCT encoding comps[0] $\times\dots\times$ comps[nb_comp-1].

armoise_predicate* armoise_predicate_create_reals ( armoise_context * ctx )

Constructor for the real numbers ( $\cal R$ ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar).

Parameters

ctx	the context

Precondition: ctx != NULL

Returns: a predicate of kind ARMOISE_P_REAL

armoise_predicate* armoise_predicate_create_simple_set	(	armoise_context *	ctx,
		armoise_term *	proto,
		armoise_predicate *	P,
		armoise_formula *	def
	)

Creates a predicate encoding a set defined by a first-order formula.

The result inherits its type from the prototyping term proto. formula is a first-order formula over variables appearing in proto.

Parameters

ctx	the context of the newly created predicate
proto	a term encoding the prototype of the encoded relation
P	a predicate that is the domain of proto
def	the FO formula defining the elements of the relation

Returns: the predicate of kind ARMOISE_P_SET encoding $\{ proto | def \}$

armoise_predicate* armoise_predicate_create_sub	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the arithmetical difference of P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown if none is typed).

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: the predicate of kind ARMOISE_P_SUB encoding $P1-P2 = \{ p \mid \exists p_1\in P1, \exists p_2\in P2, p = p_1-p_2 \}$

armoise_predicate* armoise_predicate_create_union	(	armoise_context *	ctx,
		armoise_predicate *	P1,
		armoise_predicate *	P2
	)

Creates a predicate representing the union of relations P1 and P2.

The result inherits its type from P1 or P2 (or is set to unknown) if none is typed.

Parameters

ctx	the context of the newly created predicate
P1	first operand
P2	second operand

Precondition: P1 != NULL, P2 != NULL

Returns: a predicate of kind ARMOISE_P_UNION encoding $P1\cup P2$

void armoise_predicate_del_reference ( armoise_predicate * P )

Suppresses a reference to the predicate P.

This function decrements the counter of references to P. If this counter falls to 0 then the ressources allocated to P are released.

Parameters

P	the unreferenced predicate

Precondition: P != NULL; the number of references to P > 0

int armoise_predicate_get_arity ( armoise_predicate * P )

Returns the number of columns of P.

This function returns the width of the type of P.

Parameters

P	the predicate

Precondition: P != NULL

Returns: the width of the type of P

See Also: armoise_type, armoise_predicate_get_type

armoise_context* armoise_predicate_get_context ( const armoise_predicate * P )

Returns a new reference to the context of P.

Parameters

P	the predicate

Precondition: P != NULL

Postcondition: result != NULL

Returns: the context used to create P

armoise_domain* armoise_predicate_get_domain ( const armoise_predicate * P )

Returns the domain of P.

This function returns the domain of P computed by armoise_predicate_compute_domain. The domain of P is not defined until the call to armoise_predicate_compute_domain.

Parameters

P	the predicate

Precondition: P != NULL

Postcondition: result != NULL

Returns: the domain of P

const armoise_term* armoise_predicate_get_element	(	const armoise_predicate *	P,
		int	i
	)

Returns the i th element of a finite set P.

Parameters

P	the predicate
i	the index of the value

Precondition: 0 <= i && i < armoise_predicate_get_nb_elements (P)

Returns: the number of values used to build P.

void armoise_predicate_get_indirection	(	const armoise_predicate *	P,
		ccl_ustring *	p_name,
		int *	p_nb_indices,
		const int **	p_indices
	)

Retrieves indirection informations pointed by P.

Parameters

P	the predicate
p_name	the identifier of a ccl_tree definied in the context of P
p_nb_indices	the depth of indirection
p_indices	an array used to store the indices of nodes to visit in the ccl_tree.

Precondition: armoise_predocate_get_kind (P) == ARMOISE_P_INDIRECTION

armoise_predicate_kind armoise_predicate_get_kind ( const armoise_predicate * P )

Returns the kind of P.

This function returns an enumeration indicating what kind of predicate is pointed by P.

Parameters

P	the predicate

Precondition: P != NULL

Returns: the kind of P

armoise_domain_attr armoise_predicate_get_largest_domain ( const armoise_predicate * P )

Computes the smallest reference set (i.e. $\cal N$ , $\cal Z$ , $\cal R^+$ , $\cal R$ ) that contains all elements of P.

Parameters

P	the predicate

Precondition: P != NULL

Returns: the attributes of the reference set

int armoise_predicate_get_nb_elements ( const armoise_predicate * P )

Returns the number of elements in a finite set P.

If P is of kind ARMOISE_P_ENUM (i.e. has been built using armoise_predicate_create_finite_set), this function returns the number of terms used in the set defined by P.

Parameters

P	the predicate

Precondition: armoise_predicate_kind (P) == ARMOISE_P_ENUM

Returns: the number of values used to build P.

int armoise_predicate_get_nb_operands ( const armoise_predicate * P )

Returns the number of operands used to build P.

Parameters

P	the predicate

Precondition: P != NULL

Returns: the number of operands used to build P

const armoise_predicate* armoise_predicate_get_operand	(	const armoise_predicate *	P,
		int	i
	)

Returns the i th operand of P.

For predicates that are a composition of one or more predicates, this function returns the i th operand of the composition. In case of indirection, the predicate is considered to have one operand.

Parameters

P	the predicate
i	the index of the operand

Precondition: 0 <= i && i < armoise_predicate_get_nb_operands (P)

Returns: the i th operand of P

Remarks: The counter of references of the result is not increment. Use armoise_predicate_get_operand in this case.

const armoise_formula* armoise_predicate_get_set_formula ( const armoise_predicate * P )

Returns the formula of the relation P defined by a first-order formula.

Parameters

P	the predicate

Precondition: armoise_predicate_get_kind (P) == ARMOISE_P_SET

Returns: proto if P is defined by { proto | formula }

const armoise_term* armoise_predicate_get_set_proto	(	const armoise_predicate *	P,
		armoise_predicate **	resultP
	)

Returns the prototype of the relation P defined by a first-order formula.

Parameters

P	the predicate

Precondition: armoise_predicate_get_kind (P) == ARMOISE_P_SET

Returns: proto if P is defined by { proto | formula }

armoise_type* armoise_predicate_get_type ( const armoise_predicate * P )

Returns the type of P.

Parameters

P	the predicate

Precondition: P != NULL

Returns: the width of the type of P

See Also: armoise_type

void armoise_predicate_get_variables	(	armoise_predicate *	P,
		ccl_list *	variables
	)

Collects free and bound variables in P.

The function goes through the structure of P and collects encountered armoise_variable's. Each collected variable is added (once) to the list variables.

Parameters

P	the predicate
variables	the list receiving the variables

Precondition: P != NULL; variables != NULL

void armoise_predicate_log	(	ccl_log_type	log,
		const armoise_predicate *	P
	)

Display the predicate P on the log stream.

Parameters

log	the stream where the predicate is displayed
P	the predicate send on log

Precondition: P != NULL

void armoise_predicate_log_tree	(	ccl_log_type	log,
		ccl_tree *	t
	)

Display the tree of predicates t on the log stream.

Parameters

log	the stream where the variable is displayed
t	the predicate tree send on log

Precondition: t != NULL

armoise_term* armoise_term_add_reference ( armoise_term * t )

Adds a new reference to the term t.

This function increments the counter of references to t.

Parameters

t	the term newly referenced

Precondition: t != NULL

Returns: the pointer to t

armoise_term* armoise_term_create_add	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a term encoding the addition of t1 and t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a term of kind ARMOISE_T_ADD encoding the

armoise_term* armoise_term_create_constant	(	int	num,
		int	den
	)

Creates a new term encoding the rational number num / den.

Remarks: the fration num / den is reduced in such a way that the denominator becomes > 0.

Parameters

num	the numerator
den	the denominator

Precondition: den != 0

Returns: a term of kind ARMOISE_T_CONSTANT encoding the num / den

armoise_term* armoise_term_create_div	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a term encoding the division of t1 by t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a term of kind ARMOISE_T_DIV encoding the

armoise_term* armoise_term_create_mod	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a term encoding the modulo of t1 by t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a term of kind ARMOISE_T_MOD encoding the $t1 \% t2$

armoise_term* armoise_term_create_mul	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a term encoding the multiplication of t1 and t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a term of kind ARMOISE_T_MUL encoding the $t1 \times t2$

armoise_term* armoise_term_create_neg ( armoise_term * t )

Creates a term encoding the opposite of t.

Parameters

t the term

Precondition: t != NULL

Returns: a term of kind ARMOISE_T_NEG encoding the

armoise_term* armoise_term_create_sub	(	armoise_term *	t1,
		armoise_term *	t2
	)

Creates a term encoding the difference of t1 and t2.

Parameters

t1	the first operand
t2	the second operand

Precondition: t1 != NULL; t2 != NULL

Returns: a term of kind ARMOISE_T_SUB encoding the

armoise_term* armoise_term_create_variable ( armoise_variable * v )

Creates a new term encoding the variable v.

Parameters

v	the variable

Precondition: v != NULL

Returns: a term of kind ARMOISE_T_VARIABLE encoding the variable v

armoise_term* armoise_term_create_vector	(	int	width,
		armoise_term **	terms
	)

Creates a term encoding a vector of terms.

If width == 1 then terms[0] is returned.

Parameters

width	the number of components of the vector
terms	the components of the vector

Precondition: width >= 1

Returns: a term of kind ARMOISE_T_VECTOR encoding the vector (terms[0], ..., terms[width-1])

armoise_term* armoise_term_create_vector_element	(	armoise_term *	variable,
		int	index
	)

Creates a new term encoding the index th element of the vector variable.

Parameters

variable	the vectorial variable
index	the index in the vector

Precondition: variable != NULL

Returns: a term of kind ARMOISE_T_ELEMENT encoding the variable[index]

void armoise_term_del_reference ( armoise_term * t )

Suppresses a reference to the term t.

This function decrements the counter of references to t. If this counter falls to 0 then the ressources allocated to t are released.

Parameters

t	the unreferenced term

Precondition: t != NULL; the number of references to t > 0

int armoise_term_get_arity ( const armoise_term * t )

Returns the number of operand of t.

The function returns the number of operands of t. If t is a constant or a variable then the result is 0.

Parameters

t the term

Precondition: t != NULL return the number of operand of t

int armoise_term_get_dim ( const armoise_term * t )

Returns the dimension of the term t.

Parameters

t the term

Precondition: t != NULL return the width of the type of t

See Also: armoise_type, armoise_type_get_width

armoise_term_kind armoise_term_get_kind ( const armoise_term * t )

Returns the kind of t.

This function returns an enumeration indicating what kind of term is pointed by t.

Parameters

t the term

Precondition: t != NULL

Returns: the kind of t

int armoise_term_get_nb_operands ( const armoise_term * t )

Returns the number of operands of t.

Parameters

t the term

Precondition: t != NULL

Returns: the number of operands of t

const armoise_term* armoise_term_get_operand	(	const armoise_term *	t,
		int	i
	)

Returns the i th operand of P.

For terms that are a composition of one or more terms, this function returns the i th operand of the composition.

Parameters

t	the term
i	the index of the operand

Precondition: 0 <= i && i < armoise_term_get_nb_operands (P)

Returns: the i th operand of P

Remarks: The counter of references of the result is not increment. Use armoise_predicate_get_operand in this case.

armoise_term* armoise_term_get_operand_at	(	armoise_term *	t,
		int	i
	)

Returns a new reference to the i th operand of t.

For terms that are a composition of one or more terms, this function returns the i th operand of the composition.

Parameters

t	the term
i	the index of the operand

Precondition: 0 <= i && i < armoise_term_get_nb_operands (t)

Returns: a new reference to the i th operand of P

armoise_type* armoise_term_get_type ( const armoise_term * t )

Returns the type of t.

Parameters

t the term

Precondition: t!= NULL

Returns: the type of t

void armoise_term_get_value	(	const armoise_term *	t,
		int *	num,
		int *	den
	)

Retrieves the value of the constant encoded by t.

Parameters

t	the term
num	the address of the integer receiving the numerator
den	the address of the integer receiving the denominator

Precondition: armoise_term_get_kind (t) == ARMOISE_T_CONSTANT

armoise_variable* armoise_term_get_variable ( const armoise_term * t )

Returns the armoise_variable underlying t.

Parameters

t the term

Precondition: armoise_term_get_kind (t) == ARMOISE_T_VARIABLE

Returns: the type of t

void armoise_term_get_variables	(	const armoise_term *	t,
		ccl_list *	variables
	)

Collects free and bound variables in t.

The function goes through the structure of t and collects encountered armoise_variable's. Each collected variable is added (once) to the list variables.

Parameters

t	the term
variables	the list receiving the variables

Precondition: t != NULL; variables != NULL

int armoise_term_get_vec_element_index ( const armoise_term * t )

Returns the index used by a vector element term t.

Parameters

t	the term of the form var[i]

Precondition: armoise_term_get_kind (t) == ARMOISE_T_ELEMENT

Returns: the index used by the vector element term t

const armoise_term* armoise_term_get_vec_element_variable ( const armoise_term * t )

Returns the variable referenced by a vector element term t.

Parameters

t	the term of the form var[i1]...[in]

Precondition: armoise_term_get_kind (t) == ARMOISE_T_ELEMENT

Returns: the vectorial term of the vector element term t

int armoise_term_is_constant ( const armoise_term * t )

Check if the t is constant or not.

The function returns a non-null value if t contains no variable.

Parameters

t the term

Precondition: t != NULL

Returns: a non null value if t is constant

void armoise_term_log	(	ccl_log_type	log,
		armoise_term *	t
	)

Display the term t on the log stream.

Parameters

log	the stream where the term is displayed
t	the term send on log

Precondition: t != NULL

void armoise_terminate ( void )

ARMOISE library finalizer.

This function should be call when the ARMOISE library is used any more (typically before the program exists) to release allocated ressources.

armoise_type* armoise_type_add_reference ( armoise_type * type )

Adds a new reference to type.

This function increments the counter of references to tye.

Parameters

type	the newly referenced type

Precondition: type != NULL

Returns: the pointer to type

armoise_type* armoise_type_create_product	(	int	nb_subtypes,
		armoise_type **	subtypes
	)

Creates a composite type made of nb_subtypes subtypes.

Parameters

subtypes	the sub-types
nb_subtypes	the number of subtypes

Precondition: nb_subtypes > 0

Returns: the type subtypes[0] * ... * subtypes[nb_subtypes-1]

void armoise_type_del_reference ( armoise_type * type )

Suppresses a reference to type.

This function decrements the counter of references to type. If this counter falls to 0 then the ressources allocated to type are released.

Parameters

type	the unreferenced type

Precondition: type != NULL; the number of references to type > 0

armoise_type* armoise_type_duplicate ( const armoise_type * type )

Creates a copy of type.

Parameters

type the type

Precondition: type != NULL

Returns: a copy of type

int armoise_type_equals	(	const armoise_type *	type,
		const armoise_type *	other
	)

Check whether type and other are equal.

Parameters

type	the first type
other	the second type

Precondition: type != NULL && other != NULL

Returns: a non null value if type and other are equal.

int armoise_type_get_depth_width ( const armoise_type * type )

Returns the number of leaves composing type.

This function counts the number of elementary type (i.e. scalar or unknown) composing type and its sub-types.

Parameters

type the type

Precondition: type != NULL

Returns: the number of component of type

const armoise_type* armoise_type_get_subtype	(	const armoise_type *	type,
		int	i
	)

Returns the i th subtype of type.

Parameters

type	the type
i	the index of the sub-type

Precondition: 0 <= i && i < armoise_type_get_width (type)

Returns: a non null value if type and other are equal.

armoise_type** armoise_type_get_subtype_ref	(	armoise_type *	type,
		int	i
	)

Returns the reference of the i th subtype of type.

Parameters

type	the type
i	the index of the sub-type

Precondition: 0 <= i && i < armoise_type_get_width (type)

Returns: a non null value if type and other are equal.

int armoise_type_get_width ( const armoise_type * type )

Returns the number of component of type.

Parameters

type the type

Precondition: type != NULL

Returns: the number of component of type

int armoise_type_is_scalar ( const armoise_type * type )

Returns a non-null value if type is scalar.

Parameters

type the type

Precondition: type != NULL

Returns: a non null value if the type is the scalar type

void armoise_type_log	(	ccl_log_type	log,
		const armoise_type *	type
	)

Display the type on the log stream.

Parameters

log	the stream where the type is displayed
type	the type send on log

Precondition: type != NULL

armoise_variable* armoise_variable_create	(	ccl_ustring	name,
		armoise_type *	type
	)

Constructor for a first-order variable defined by its name and its type.

Parameters

name	the identifier of the variable
type	the type of the variable

Returns: a newly create variable

void armoise_variable_del_reference ( armoise_variable * variable )

Suppresses a reference to variable.

This function decrements the counter of references to variable. If this counter falls to 0 then the ressources allocated to variable are released.

Parameters

variable the unreferenced variable

Precondition: variable != NULL; the number of references to variable > 0

const armoise_domain* armoise_variable_get_domain ( armoise_variable * variable )

Returns the domain of variable.

Parameters

variable the considered variable

Precondition: variable != NULL

Returns: the domain of variable

ccl_ustring armoise_variable_get_name ( armoise_variable * variable )

Returns the identifier of variable.

Parameters

variable the considered variable

Precondition: variable != NULL

Returns: the identifier used to create variable

armoise_type* armoise_variable_get_type ( armoise_variable * variable )

Returns the type of variable.

Parameters

variable the considered variable

Precondition: variable != NULL

Returns: a new reference to the type of variable

void armoise_variable_log	(	ccl_log_type	log,
		armoise_variable *	variable
	)

Display the variable on the log stream.

Parameters

log	the stream where the variable is displayed
variable	the variable send on log

Precondition: variable != NULL

void armoise_variable_set_domain	(	armoise_variable *	variable,
		const armoise_domain *	D
	)

Change the domain D of variable.

The current domain assigned to variable is unreferenced. D is then duplicated and assigned to variable.

Parameters

variable	the considered variable
D	the domain assigned to variable

Precondition: variable != NULL; D != NULL;

Macros

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

Enumeration Type Documentation

Function Documentation