TaPAS  0.2
Macros | Typedefs | Enumerations | Functions | Variables
armoise.h File Reference
#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>

Go to the source code of this file.

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_contextarmoise_context_create_for_predicates (armoise_context *parent)
 Constructor for contexts storing predicate symbols. More...
 
armoise_contextarmoise_context_create_for_variables (armoise_context *parent)
 Constructor for contexts storing first order symbols. More...
 
armoise_contextarmoise_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_contextarmoise_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_hasharmoise_context_get_table (armoise_context *ctx)
 Returns the symbol table of ctx. More...
 
ccl_listarmoise_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_treearmoise_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_predicatearmoise_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_predicatearmoise_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_variablearmoise_context_get_variable (armoise_context *ctx, ccl_ustring id)
 Retrieves the variable identified by id in ctx. More...
 
armoise_variablearmoise_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_typearmoise_variable_get_type (armoise_variable *variable)
 Returns the type of variable. More...
 
const armoise_domainarmoise_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_predicatearmoise_predicate_create_empty (armoise_context *ctx, armoise_type *type)
 Constructor for an empty and untyped relation. More...
 
armoise_predicatearmoise_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_predicatearmoise_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_predicatearmoise_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_predicatearmoise_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_predicatearmoise_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_predicatearmoise_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_predicatearmoise_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_predicatearmoise_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_predicatearmoise_predicate_create_diff (armoise_context *ctx, armoise_predicate *P1, armoise_predicate *P2)
 Creates a predicate representing the difference of P1 and P2. More...
 
armoise_predicatearmoise_predicate_create_complement (armoise_context *ctx, armoise_predicate *P)
 Creates a predicate representing the complement of P. More...
 
armoise_predicatearmoise_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_predicatearmoise_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_predicatearmoise_predicate_create_mul (armoise_context *ctx, armoise_predicate *P1, armoise_predicate *P2)
 Creates a predicate representing the multiplicaton of P1 and P2. More...
 
armoise_predicatearmoise_predicate_create_div (armoise_context *ctx, armoise_predicate *P1, armoise_predicate *P2)
 Creates a predicate representing the division of P1 by P2. More...
 
armoise_predicatearmoise_predicate_create_mod (armoise_context *ctx, armoise_predicate *P1, armoise_predicate *P2)
 Creates a predicate representing the modulo of P1 by P2. More...
 
armoise_predicatearmoise_predicate_create_neg (armoise_context *ctx, armoise_predicate *P)
 Creates a predicate representing the negation of P. More...
 
armoise_predicatearmoise_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_predicatearmoise_predicate_create_integer (armoise_context *ctx, int i)
 Creates the singleton predicate $\{ i \}$. More...
 
armoise_predicatearmoise_predicate_create_paren (armoise_context *ctx, armoise_predicate *P)
 Creates a predicate enclosed by parenthesis $(P)$. More...
 
armoise_predicatearmoise_predicate_create_finite_set (armoise_context *ctx, int nb_terms, armoise_term **values)
 Creates a predicate encoding a finite set of values. More...
 
armoise_predicatearmoise_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_predicatearmoise_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_typearmoise_predicate_get_type (const armoise_predicate *P)
 Returns the type of P. More...
 
armoise_contextarmoise_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_predicatearmoise_predicate_get_operand (const armoise_predicate *P, int i)
 Returns the i th operand of P. More...
 
armoise_predicatearmoise_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_domainarmoise_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_termarmoise_predicate_get_element (const armoise_predicate *P, int i)
 Returns the i th element of a finite set P. More...
 
const armoise_termarmoise_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_formulaarmoise_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_formulaarmoise_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_formulaarmoise_formula_create_constant (int value)
 Creates a formula encoding the Boolean value. More...
 
armoise_formulaarmoise_formula_create_in (armoise_term *t, armoise_predicate *P)
 Creates a formula encoding membership checking of t in P. More...
 
armoise_formulaarmoise_formula_create_or (armoise_formula *F1, armoise_formula *F2)
 Creates a formula encoding the disjunction of F1 and F2. More...
 
armoise_formulaarmoise_formula_create_and (armoise_formula *F1, armoise_formula *F2)
 Creates a formula encoding the conjunction of F1 and F2. More...
 
armoise_formulaarmoise_formula_create_equiv (armoise_formula *F1, armoise_formula *F2)
 Creates a formula encoding the equivalence of F1 and F2. More...
 
armoise_formulaarmoise_formula_create_imply (armoise_formula *F1, armoise_formula *F2)
 Creates a formula encoding the implication of F2 by F1. More...
 
armoise_formulaarmoise_formula_create_not (armoise_formula *F)
 Creates a formula encoding the negation of F. More...
 
armoise_formulaarmoise_formula_create_eq (armoise_term *t1, armoise_term *t2)
 Creates a formula encoding the equality of t1 and t2. More...
 
armoise_formulaarmoise_formula_create_neq (armoise_term *t1, armoise_term *t2)
 Creates a formula encoding the not-equality of t1 and t2. More...
 
armoise_formulaarmoise_formula_create_leq (armoise_term *t1, armoise_term *t2)
 Creates a formula encoding the inequality of t1 <= t2. More...
 
armoise_formulaarmoise_formula_create_geq (armoise_term *t1, armoise_term *t2)
 Creates a formula encoding the inequality of t1 >= t2. More...
 
armoise_formulaarmoise_formula_create_lt (armoise_term *t1, armoise_term *t2)
 Creates a formula encoding the inequality of t1 < t2. More...
 
armoise_formulaarmoise_formula_create_gt (armoise_term *t1, armoise_term *t2)
 Creates a formula encoding the inequality of t1 < t2. More...
 
armoise_formulaarmoise_formula_create_paren (armoise_formula *F)
 Creates a formula enclosed with parenthesis (F). More...
 
armoise_formulaarmoise_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_formulaarmoise_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_formulaarmoise_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_formulaarmoise_formula_get_quantified_formula (const armoise_formula *F)
 Returns the formula part of a quantified formula F. More...
 
armoise_termarmoise_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_termarmoise_formula_get_in_term (const armoise_formula *F)
 Returns the term of a membership formula F. More...
 
armoise_predicatearmoise_formula_get_in_predicate (const armoise_formula *F)
 Returns the term of a membership checking formula F. More...
 
armoise_termarmoise_formula_get_cmp_left_term (const armoise_formula *F)
 Returns the left operand of the comparison encoded by F. More...
 
armoise_termarmoise_formula_get_cmp_right_term (const armoise_formula *F)
 Returns the righr operand of the comparison encoded by F. More...
 
armoise_termarmoise_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_typearmoise_term_get_type (const armoise_term *t)
 Returns the type of t. More...
 
armoise_variablearmoise_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_termarmoise_term_get_operand_at (armoise_term *t, int i)
 Returns a new reference to the i th operand of t. More...
 
armoise_termarmoise_term_create_variable (armoise_variable *v)
 Creates a new term encoding the variable v. More...
 
armoise_termarmoise_term_create_vector_element (armoise_term *variable, int index)
 Creates a new term encoding the index th element of the vector variable. More...
 
armoise_termarmoise_term_create_constant (int num, int den)
 Creates a new term encoding the rational number num / den. More...
 
armoise_termarmoise_term_create_vector (int width, armoise_term **terms)
 Creates a term encoding a vector of terms. More...
 
armoise_termarmoise_term_create_neg (armoise_term *t)
 Creates a term encoding the opposite of t. More...
 
armoise_termarmoise_term_create_mul (armoise_term *t1, armoise_term *t2)
 Creates a term encoding the multiplication of t1 and t2. More...
 
armoise_termarmoise_term_create_div (armoise_term *t1, armoise_term *t2)
 Creates a term encoding the division of t1 by t2. More...
 
armoise_termarmoise_term_create_mod (armoise_term *t1, armoise_term *t2)
 Creates a term encoding the modulo of t1 by t2. More...
 
armoise_termarmoise_term_create_add (armoise_term *t1, armoise_term *t2)
 Creates a term encoding the addition of t1 and t2. More...
 
armoise_termarmoise_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_termarmoise_term_get_operand (const armoise_term *t, int i)
 Returns the i th operand of P. More...
 
const armoise_termarmoise_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_typearmoise_type_create_scalar (void)
 Creates the scalar type.
 
armoise_typearmoise_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_typearmoise_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_typearmoise_type_get_subtype (const armoise_type *type, int i)
 Returns the i th subtype of type. More...
 
armoise_typearmoise_type_duplicate (const armoise_type *type)
 Creates a copy of type. More...
 
armoise_domainarmoise_domain_create_with_attr (const armoise_domain_attr attr)
 Creates a domain with given attibutes attr. More...
 
armoise_domainarmoise_domain_create (void)
 Creates a domain containing real numbers. More...
 
armoise_domainarmoise_domain_create_empty (void)
 Creates an empty domain. More...
 
armoise_domainarmoise_domain_create_compound_domain (int width, armoise_domain **domains)
 Creates a domain composed of width domains. More...
 
armoise_domainarmoise_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_domainarmoise_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_domainarmoise_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

Kind of formula.

See Also
armoise_formula_get_kind

Definition at line 91 of file armoise.h.

Kind of predicates.

See Also
armoise_predicate_get_kind

Definition at line 58 of file armoise.h.

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
ctxthe considered context
idthe defined symbol
objectthe 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
ctxthe 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
parentthe 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
parentthe 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
ctxthe 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
ctxthe considered context
idthe 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
ctxthe 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
ctxthe 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
ctxthe 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
ctxthe considered context
idthe 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
ctxthe considered context
idthe 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
dthe 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
widththe number of components
domainsthe 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
attrthe 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
dthe 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
dthe 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
d1the first domain
d2the 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
dthe 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
dthe domain
ithe 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
dthe 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
dthe 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
dthe 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
dthe 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
dthe 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
dthe 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
dthe 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
logthe stream where the domain is displayed
dthe 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
dthe domain
attrthe 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
dthe domain
ithe index of the component
dithe 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
Fthe 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
F1the first operand
F2the 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
valuethe 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
t1the first operand
t2the 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
F1the first operand
F2the 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_qvarsthe number of variables to quantify
qvarsthe variables to quantify
Fthe 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_qvarsthe number of variables to quantify
qvarsthe variables to quantify
Fthe 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
t1the first operand
t2the 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
t1the first operand
t2the second operand
Precondition
t1 != NULL
t2 != NULL
Returns
a formula of kind ARMOISE_F_GT encoding $t1 > t2$
armoise_formula* armoise_formula_create_imply ( armoise_formula F1,
armoise_formula F2 
)

Creates a formula encoding the implication of F2 by F1.

Parameters
F1the first operand
F2the 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
Pthe predicate.
tthe 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
t1the first operand
t2the 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
t1the first operand
t2the second operand
Precondition
t1 != NULL
t2 != NULL
Returns
a formula of kind ARMOISE_F_LT encoding $t1 < t2$
armoise_formula* armoise_formula_create_neq ( armoise_term t1,
armoise_term t2 
)

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

Parameters
t1the first operand
t2the 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
Fthe 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
F1the first operand
F2the 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
Fthe operand
Precondition
F != NULL
Returns
a formula of kind ARMOISE_F_PAREN encoding $ (F)$
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
Fthe 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
Fthe 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
Fthe 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
Fthe 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
Fthe 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
Fthe 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
Fthe 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
Fthe formula
ithe 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
Fthe 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
Fthe formula
p_nb_varsa 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
Fthe 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
Fthe formula
variablesthe 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
logthe stream where the formula is displayed
Fthe 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
Pthe 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
Pthe 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe context of the newly created predicate
Pthe 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe 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
ctxthe context of the newly created predicate
nb_termsthe number of values in the set
valuesthe 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
ctxthe context of the newly created predicate
namethe identifier of a predicate or ccl_tree defined in ctx.
nb_indicesdepth of search the ccl_tree referred by name
indicesarray 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
ctxthe context of the newly created predicate
ithe 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
ctxthe 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe 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
ctxthe context of the newly created predicate
Pthe 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
ctxthe context of the newly created predicate
Pthe predicate
Returns
the predicate of kind ARMOISE_P_PAREN encoding $(P)$
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
ctxthe 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
ctxthe context of the newly created predicate
nb_compthe number of components of the product
compsthe 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
ctxthe 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
ctxthe context of the newly created predicate
protoa term encoding the prototype of the encoded relation
Pa predicate that is the domain of proto
defthe 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
ctxthe context of the newly created predicate
P1first operand
P2second 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
Pthe 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
Pthe 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
Pthe 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
Pthe 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
Pthe predicate
ithe 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
Pthe predicate
p_namethe identifier of a ccl_tree definied in the context of P
p_nb_indicesthe depth of indirection
p_indicesan 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
Pthe 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
Pthe 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
Pthe 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
Pthe 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
Pthe predicate
ithe 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
Pthe 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
Pthe 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
Pthe 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
Pthe predicate
variablesthe 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
logthe stream where the predicate is displayed
Pthe 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
logthe stream where the variable is displayed
tthe 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
tthe 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
t1the first operand
t2the second operand
Precondition
t1 != NULL
t2 != NULL
Returns
a term of kind ARMOISE_T_ADD encoding the $t1 + t2$
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
numthe numerator
denthe 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
t1the first operand
t2the second operand
Precondition
t1 != NULL
t2 != NULL
Returns
a term of kind ARMOISE_T_DIV encoding the $t1 / t2$
armoise_term* armoise_term_create_mod ( armoise_term t1,
armoise_term t2 
)

Creates a term encoding the modulo of t1 by t2.

Parameters
t1the first operand
t2the 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
t1the first operand
t2the 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
tthe term
Precondition
t != NULL
Returns
a term of kind ARMOISE_T_NEG encoding the $-t$
armoise_term* armoise_term_create_sub ( armoise_term t1,
armoise_term t2 
)

Creates a term encoding the difference of t1 and t2.

Parameters
t1the first operand
t2the second operand
Precondition
t1 != NULL
t2 != NULL
Returns
a term of kind ARMOISE_T_SUB encoding the $t1 - t2$
armoise_term* armoise_term_create_variable ( armoise_variable v)

Creates a new term encoding the variable v.

Parameters
vthe 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
widththe number of components of the vector
termsthe 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
variablethe vectorial variable
indexthe 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
tthe 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
tthe 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
tthe 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
tthe 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
tthe 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
tthe term
ithe 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
tthe term
ithe 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
tthe 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
tthe term
numthe address of the integer receiving the numerator
denthe 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
tthe 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
tthe term
variablesthe 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
tthe 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
tthe 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
tthe 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
logthe stream where the term is displayed
tthe 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
typethe 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
subtypesthe sub-types
nb_subtypesthe 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
typethe 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
typethe 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
typethe first type
otherthe 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
typethe 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
typethe type
ithe 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
typethe type
ithe 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
typethe 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
typethe 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
logthe stream where the type is displayed
typethe 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
namethe identifier of the variable
typethe 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
variablethe 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
variablethe 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
variablethe 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
variablethe 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
logthe stream where the variable is displayed
variablethe 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
variablethe considered variable
Dthe domain assigned to variable
Precondition
variable != NULL
D != NULL;