22 # define __ARMOISE_H__
65 ARMOISE_P_INTERSECTION,
78 ARMOISE_P_INDIRECTION,
158 # define ARMOISE_DOMAIN_HAS_POSITIVES (((uint32_t)0x1) << 0)
159 # define ARMOISE_DOMAIN_HAS_NEGATIVES (((uint32_t)0x1) << 1)
160 # define ARMOISE_DOMAIN_IS_FINITE (((uint32_t)0x1) << 2)
161 # define ARMOISE_DOMAIN_IN_INTEGERS (((uint32_t)0x1) << 3)
369 int nb_indices,
const int *indices);
377 int nb_indices,
const int *indices);
570 int nb_indices,
const int *indices);
1071 const int **p_indices);
armoise_term * armoise_term_create_vector(int width, armoise_term **terms)
Creates a term encoding a vector of terms.
int armoise_domain_is_singleton(const armoise_domain *d)
Checks if d contains only one element.
armoise_domain * armoise_predicate_get_domain(const armoise_predicate *P)
Returns the domain of P.
struct armoise_formula_st armoise_formula
Abstract type for a first-order formula.
void armoise_term_del_reference(armoise_term *t)
Suppresses a reference to the term t.
int armoise_term_is_constant(const armoise_term *t)
Check if the t is constant or not.
armoise_formula * armoise_formula_add_reference(armoise_formula *F)
Adds a new reference to the formula F.
armoise_term * armoise_term_create_neg(armoise_term *t)
Creates a term encoding the opposite of t.
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.
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.
armoise_predicate * armoise_predicate_create_neg(armoise_context *ctx, armoise_predicate *P)
Creates a predicate representing the negation of P.
armoise_context * armoise_context_get_parent(armoise_context *ctx)
Returns the parent context of ctx.
struct armoise_domain_st armoise_domain
Abstract type for domains of variables, terms and predicates.
void armoise_term_get_variables(const armoise_term *t, ccl_list *variables)
Collects free and bound variables in t.
armoise_domain * armoise_domain_add_reference(armoise_domain *d)
Adds a new reference to the domain d.
armoise_predicate * armoise_predicate_create_integers(armoise_context *ctx)
Constructor for the predicate representing integers ( ). The type of the predicate is set to scalar (...
int armoise_domain_get_width(const armoise_domain *d)
Returns the number of components of d.
Generic simple linked list.
int armoise_type_get_depth_width(const armoise_type *type)
Returns the number of leaves composing type.
int armoise_domain_equals(const armoise_domain *d1, const armoise_domain *d2)
Checks if d1 and d2 are equal.
void armoise_predicate_compute_domain(armoise_predicate *P)
Computes the domain of P.
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...
struct armoise_context_st armoise_context
Abstract type representing the context of a predicate.
const armoise_formula * armoise_formula_get_quantified_formula(const armoise_formula *F)
Returns the formula part of a quantified formula F.
const armoise_term * armoise_term_get_vec_element_variable(const armoise_term *t)
Returns the variable referenced by a vector element term t.
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.
struct armoise_term_st armoise_term
Abstract type for a (first-order) term.
armoise_variable * armoise_context_get_variable(armoise_context *ctx, ccl_ustring id)
Retrieves the variable identified by id in ctx.
armoise_context * armoise_context_create_for_variables(armoise_context *parent)
Constructor for contexts storing first order symbols.
int armoise_init(void)
ARMOISE library initializer.
void armoise_predicate_log(ccl_log_type log, const armoise_predicate *P)
Display the predicate P on the log stream.
int armoise_context_has(armoise_context *ctx, ccl_ustring id)
Checks if the symbol id exists in the context ctx.
Structure storing a node of a generic tree.
struct armoise_predicate_st armoise_predicate
Abstract of an ARMOISE predicate.
const armoise_domain_attr ARMOISE_DOMAIN_ATTR_FOR_NATURALS
Attributes for the domain .
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...
armoise_term * armoise_term_create_variable(armoise_variable *v)
Creates a new term encoding the variable v.
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.
armoise_term * armoise_formula_get_cmp_left_term(const armoise_formula *F)
Returns the left operand of the comparison encoded by F.
void armoise_predicate_log_tree(ccl_log_type log, ccl_tree *t)
Display the tree of predicates t on the log stream.
int armoise_domain_get_min(const armoise_domain *d)
Returns the lower bound of d.
armoise_predicate * armoise_predicate_create_reals(armoise_context *ctx)
Constructor for the real numbers ( ). The type of the predicate is set to scalar (cf. armoise_type_is_scalar).
ccl_list * armoise_context_get_ids(armoise_context *ctx)
Returns the list of symbol locally defined in ctx.
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.
int armoise_domain_get_max(const armoise_domain *d)
Returns the upper bound of d.
armoise_formula * armoise_formula_create_constant(int value)
Creates a formula encoding the Boolean value.
int armoise_term_get_vec_element_index(const armoise_term *t)
Returns the index used by a vector element term t.
armoise_domain * armoise_domain_duplicate(const armoise_domain *d)
Return a copy of d.
const armoise_term * armoise_term_get_operand(const armoise_term *t, int i)
Returns the i th operand of P.
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.
void armoise_domain_set_component(armoise_domain *d, int i, const armoise_domain *di)
Changes the i th component of d with di.
int armoise_context_has_locally(armoise_context *ctx, ccl_ustring id)
Checks if the symbol id is defined in the context ctx.
armoise_context * armoise_context_add_reference(armoise_context *ctx)
Adds a new reference to the context ctx.
void armoise_context_del_reference(armoise_context *ctx)
Suppresses a reference to the context ctx.
ccl_ustring armoise_variable_get_name(armoise_variable *variable)
Returns the identifier of variable.
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.
armoise_domain_attr armoise_domain_get_attr(const armoise_domain *d)
Returns attributes defining d.
armoise_predicate * armoise_predicate_create_integer(armoise_context *ctx, int i)
Creates the singleton predicate .
armoise_predicate * armoise_predicate_create_empty(armoise_context *ctx, armoise_type *type)
Constructor for an empty and untyped relation.
armoise_formula * armoise_formula_create_neq(armoise_term *t1, armoise_term *t2)
Creates a formula encoding the not-equality of t1 and t2.
int armoise_predicate_get_arity(armoise_predicate *P)
Returns the number of columns of P.
const armoise_formula * armoise_formula_get_operand(const armoise_formula *F, int i)
Returns the i th operands of F.
struct armoise_type_st armoise_type
Abstract type for variable or predicate types.
armoise_term * armoise_term_create_div(armoise_term *t1, armoise_term *t2)
Creates a term encoding the division of t1 by t2.
const armoise_type * armoise_type_get_subtype(const armoise_type *type, int i)
Returns the i th subtype of type.
int armoise_domain_is_empty(const armoise_domain *d)
Checks if d is empty.
armoise_formula * armoise_formula_create_gt(armoise_term *t1, armoise_term *t2)
Creates a formula encoding the inequality of t1 < t2.
armoise_term * armoise_term_create_mul(armoise_term *t1, armoise_term *t2)
Creates a term encoding the multiplication of t1 and t2.
int armoise_predicate_get_nb_operands(const armoise_predicate *P)
Returns the number of operands used to build P.
armoise_formula * armoise_formula_create_not(armoise_formula *F)
Creates a formula encoding the negation of F.
int armoise_context_has_predicate_tree(armoise_context *ctx, ccl_ustring id)
Checks the existences of a predicate tree id in ctx.
void armoise_variable_del_reference(armoise_variable *variable)
Suppresses a reference to variable.
void armoise_domain_del_reference(armoise_domain *d)
Suppresses a reference to the domain d.
void armoise_context_add(armoise_context *ctx, ccl_ustring id, void *object)
Defines symbol id in the context ctx.
int armoise_context_has_variable(armoise_context *ctx, ccl_ustring id)
Checks the existences of a first-order variable identified by id in ctx.
const armoise_term * armoise_predicate_get_element(const armoise_predicate *P, int i)
Returns the i th element of a finite set P.
const armoise_domain * armoise_domain_get_component(const armoise_domain *d, int i)
Returns the i th component of d.
void armoise_term_get_value(const armoise_term *t, int *num, int *den)
Retrieves the value of the constant encoded by t.
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.
armoise_type * armoise_type_create_scalar(void)
Creates the scalar type.
armoise_type * armoise_type_add_reference(armoise_type *type)
Adds a new reference to type.
armoise_predicate * armoise_predicate_create_naturals(armoise_context *ctx)
Constructor for the predicate representing natural numbers ( ). The type of the predicate is set to s...
uint32_t armoise_domain_attr
Attributes of an armoise_domain.
int armoise_term_get_dim(const armoise_term *t)
Returns the dimension of the term t.
const armoise_domain_attr ARMOISE_DOMAIN_ATTR_FOR_POSITIVES
Attributes for the domain .
armoise_term * armoise_formula_get_in_term(const armoise_formula *F)
Returns the term of a membership formula F.
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.
armoise_formula * armoise_formula_create_and(armoise_formula *F1, armoise_formula *F2)
Creates a formula encoding the conjunction of F1 and F2.
armoise_term * armoise_term_create_add(armoise_term *t1, armoise_term *t2)
Creates a term encoding the addition of t1 and t2.
struct ccl_list_st ccl_list
Type of a generic list.
armoise_predicate * armoise_predicate_add_reference(armoise_predicate *P)
Adds a new reference to the predicate P.
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.
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.
armoise_formula * armoise_formula_create_or(armoise_formula *F1, armoise_formula *F2)
Creates a formula encoding the disjunction of F1 and F2.
armoise_predicate * armoise_predicate_create_positives(armoise_context *ctx)
Constructor for the real numbers restricted to positive ( ). The type of the predicate is set to scal...
int armoise_term_get_nb_operands(const armoise_term *t)
Returns the number of operands of t.
armoise_domain * armoise_domain_create_compound_domain(int width, armoise_domain **domains)
Creates a domain composed of width domains.
const armoise_domain_attr ARMOISE_DOMAIN_ATTR_FOR_INTEGERS
Attributes for the domain .
int armoise_predicate_get_nb_elements(const armoise_predicate *P)
Returns the number of elements in a finite set P.
int armoise_domain_is_restricted_to_integers(const armoise_domain *d)
Checks if d is a subset of integers.
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...
void armoise_term_log(ccl_log_type log, armoise_term *t)
Display the term t on the log stream.
armoise_predicate * armoise_predicate_create_paren(armoise_context *ctx, armoise_predicate *P)
Creates a predicate enclosed by parenthesis .
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.
armoise_context * armoise_context_create_for_predicates(armoise_context *parent)
Constructor for contexts storing predicate symbols.
struct armoise_variable_st armoise_variable
Abstract type for a first-order variable.
armoise_formula_kind
Kind of formula.
armoise_type * armoise_type_duplicate(const armoise_type *type)
Creates a copy of type.
armoise_formula * armoise_formula_create_lt(armoise_term *t1, armoise_term *t2)
Creates a formula encoding the inequality of t1 < t2.
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...
armoise_predicate_kind
Kind of predicates.
armoise_term * armoise_term_create_sub(armoise_term *t1, armoise_term *t2)
Creates a term encoding the difference of t1 and t2.
Module gathering routines frequently used for the manipulation of string.
void armoise_formula_del_reference(armoise_formula *F)
Suppresses a reference to the formula F.
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.
char * ccl_ustring
Alias type for strings that are stored in an internal dictionary and then can be used as identifiers ...
int armoise_formula_get_nb_operands(const armoise_formula *F)
Returns the number of operands of F.
armoise_predicate * armoise_predicate_create_complement(armoise_context *ctx, armoise_predicate *P)
Creates a predicate representing the complement of P.
armoise_formula * armoise_formula_create_imply(armoise_formula *F1, armoise_formula *F2)
Creates a formula encoding the implication of F2 by F1.
armoise_predicate_kind armoise_predicate_get_kind(const armoise_predicate *P)
Returns the kind of P.
armoise_formula * armoise_formula_create_geq(armoise_term *t1, armoise_term *t2)
Creates a formula encoding the inequality of t1 >= t2.
armoise_term_kind
Kind of term.
Generic not ordered tree structure.
armoise_type * armoise_type_create_product(int nb_subtypes, armoise_type **subtypes)
Creates a composite type made of nb_subtypes subtypes.
void armoise_variable_set_domain(armoise_variable *variable, const armoise_domain *D)
Change the domain D of variable.
armoise_formula_kind armoise_formula_get_kind(const armoise_formula *F)
Returns the kind of formula is pointed by F.
void armoise_domain_log(ccl_log_type log, const armoise_domain *d)
Display the domain on the log stream.
const armoise_domain_attr ARMOISE_DOMAIN_ATTR_FOR_REALS
Attributes for the domain .
ccl_hash * armoise_context_get_table(armoise_context *ctx)
Returns the symbol table of ctx.
enum ccl_log_type_enum ccl_log_type
Enum that indicates which kind of message has to be displayed. Each kind of message can be displayed ...
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.
armoise_variable * armoise_term_get_variable(const armoise_term *t)
Returns the armoise_variable underlying t.
armoise_formula * armoise_formula_create_equiv(armoise_formula *F1, armoise_formula *F2)
Creates a formula encoding the equivalence of F1 and F2.
armoise_term * armoise_term_create_mod(armoise_term *t1, armoise_term *t2)
Creates a term encoding the modulo of t1 by t2.
armoise_term * armoise_term_add_reference(armoise_term *t)
Adds a new reference to the term t.
void armoise_formula_log(ccl_log_type log, armoise_formula *F)
Display the formula F on the log stream.
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.
armoise_term * armoise_term_get_operand_at(armoise_term *t, int i)
Returns a new reference to the i th operand of t.
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.
armoise_type * armoise_predicate_get_type(const armoise_predicate *P)
Returns the type of P.
int armoise_formula_get_value(const armoise_formula *F)
Returns the value of the Boolean constant encoded by F.
armoise_context * armoise_predicate_get_context(const armoise_predicate *P)
Returns a new reference to the context of P.
armoise_type * armoise_term_get_type(const armoise_term *t)
Returns the type of t.
int armoise_domain_is_finite(const armoise_domain *d)
Checks if d is finite.
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.
armoise_predicate * armoise_formula_get_in_predicate(const armoise_formula *F)
Returns the term of a membership checking formula F.
void * armoise_context_get(armoise_context *ctx, ccl_ustring id)
Returns the object associated with the symbol id.
void armoise_domain_set_attr(armoise_domain *d, const armoise_domain_attr attr)
Changes the attributes of d.
void armoise_predicate_del_reference(armoise_predicate *P)
Suppresses a reference to the predicate P.
int armoise_type_get_width(const armoise_type *type)
Returns the number of component of type.
armoise_domain_attr armoise_predicate_get_largest_domain(const armoise_predicate *P)
Computes the smallest reference set (i.e. , , , ) that contains all elements of P.
int armoise_type_is_scalar(const armoise_type *type)
Returns a non-null value if type is scalar.
armoise_variable * armoise_variable_create(ccl_ustring name, armoise_type *type)
Constructor for a first-order variable defined by its name and its type.
armoise_term * armoise_term_create_constant(int num, int den)
Creates a new term encoding the rational number num / den.
armoise_domain * armoise_domain_create(void)
Creates a domain containing real numbers.
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 inc...
int armoise_term_get_arity(const armoise_term *t)
Returns the number of operand of t.
A dynamic association table implemented by hashing.
void armoise_terminate(void)
ARMOISE library finalizer.
armoise_formula * armoise_formula_create_paren(armoise_formula *F)
Creates a formula enclosed with parenthesis (F).
armoise_formula * armoise_formula_create_leq(armoise_term *t1, armoise_term *t2)
Creates a formula encoding the inequality of t1 <= t2.
void armoise_formula_get_variables(const armoise_formula *F, ccl_list *variables)
Collects free and bound variables in F.
void armoise_type_del_reference(armoise_type *type)
Suppresses a reference to type.
armoise_term_kind armoise_term_get_kind(const armoise_term *t)
Returns the kind of t.
struct ccl_hash_st ccl_hash
abstract type of an hash table.
armoise_formula * armoise_formula_create_in(armoise_term *t, armoise_predicate *P)
Creates a formula encoding membership checking of t in P.
armoise_term * armoise_formula_get_cmp_right_term(const armoise_formula *F)
Returns the righr operand of the comparison encoded by F.
const armoise_predicate * armoise_predicate_get_operand(const armoise_predicate *P, int i)
Returns the i th operand of P.
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.
armoise_domain * armoise_domain_create_with_attr(const armoise_domain_attr attr)
Creates a domain with given attibutes attr.
int armoise_type_equals(const armoise_type *type, const armoise_type *other)
Check whether type and other are equal.
const armoise_domain * armoise_variable_get_domain(armoise_variable *variable)
Returns the domain of variable.
armoise_domain * armoise_domain_create_empty(void)
Creates an empty domain.
armoise_formula * armoise_formula_create_eq(armoise_term *t1, armoise_term *t2)
Creates a formula encoding the equality of t1 and t2.
void armoise_predicate_get_variables(armoise_predicate *P, ccl_list *variables)
Collects free and bound variables in P.
ccl_tree * armoise_context_get_predicate_tree(armoise_context *ctx, ccl_ustring id)
Retrieves the predicate tree identified by id in ctx.
armoise_type ** armoise_type_get_subtype_ref(armoise_type *type, int i)
Returns the reference of the i th subtype of type.
armoise_type * armoise_variable_get_type(armoise_variable *variable)
Returns the type of variable.
void armoise_variable_log(ccl_log_type log, armoise_variable *variable)
Display the variable on the log stream.
void armoise_type_log(ccl_log_type log, const armoise_type *type)
Display the type on the log stream.
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.
armoise_predicate * armoise_predicate_create_product(armoise_context *ctx, int nb_comp, armoise_predicate **comps)
Creates a predicate representing the cartesian product comps[0] comps[nb_comp-1].
