TaPAS  0.2
armoise.h
Go to the documentation of this file.
1 /*
2  * armoise.h -- add a comment about this file
3  *
4  * This file is a part of the ARMOISE language library.
5  *
6  * Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
7  *
8  * This program is free software; you can redistribute it and/or modify
9  * it under the terms of the AltaRica Public License that comes with this
10  * package.
11  *
12  * This program is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
15  */
16 
21 #ifndef __ARMOISE_H__
22 # define __ARMOISE_H__
23 
24 # include <limits.h>
25 # include <ccl/ccl-string.h>
26 # include <ccl/ccl-tree.h>
27 # include <ccl/ccl-hash.h>
28 # include <ccl/ccl-list.h>
29 # include <ccl/ccl-log.h>
30 
31 BEGIN_C_DECLS
32 
46 typedef struct armoise_context_st armoise_context;
47 
51 typedef struct armoise_predicate_st armoise_predicate;
52 
58 typedef enum {
59  ARMOISE_P_EMPTY,
60  ARMOISE_P_NAT,
61  ARMOISE_P_INT,
62  ARMOISE_P_POSI,
63  ARMOISE_P_REAL,
64  ARMOISE_P_UNION,
65  ARMOISE_P_INTERSECTION,
66  ARMOISE_P_DIFF,
67  ARMOISE_P_DELTA,
68  ARMOISE_P_COMPLEMENT,
69  ARMOISE_P_ADD,
70  ARMOISE_P_SUB,
71  ARMOISE_P_MUL,
72  ARMOISE_P_DIV,
73  ARMOISE_P_MOD,
74  ARMOISE_P_NEG,
75  ARMOISE_P_PRODUCT,
76  ARMOISE_P_SET,
77  ARMOISE_P_ENUM,
78  ARMOISE_P_INDIRECTION,
79  ARMOISE_P_PAREN
81 
85 typedef struct armoise_formula_st armoise_formula;
86 
91 typedef enum {
92  ARMOISE_F_CONSTANT,
93  ARMOISE_F_IN,
94  ARMOISE_F_NOT,
95  ARMOISE_F_EQ,
96  ARMOISE_F_NEQ,
97  ARMOISE_F_LEQ,
98  ARMOISE_F_GEQ,
99  ARMOISE_F_LT,
100  ARMOISE_F_GT,
101  ARMOISE_F_AND,
102  ARMOISE_F_OR,
103  ARMOISE_F_EQUIV,
104  ARMOISE_F_IMPLY,
105  ARMOISE_F_EXISTS,
106  ARMOISE_F_FORALL,
107  ARMOISE_F_PAREN
109 
113 typedef struct armoise_variable_st armoise_variable;
114 
118 typedef struct armoise_term_st armoise_term;
119 
124 typedef enum {
125  ARMOISE_T_VARIABLE,
126  ARMOISE_T_CONSTANT,
127  ARMOISE_T_VECTOR,
128  ARMOISE_T_ELEMENT,
129  ARMOISE_T_ADD,
130  ARMOISE_T_SUB,
131  ARMOISE_T_MUL,
132  ARMOISE_T_DIV,
133  ARMOISE_T_MOD,
134  ARMOISE_T_NEG
136 
143 typedef struct armoise_type_st armoise_type;
144 
148 typedef struct armoise_domain_st armoise_domain;
149 
153 typedef uint32_t armoise_domain_attr;
154 
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)
162 
170 extern int
171 armoise_init (void);
172 
179 extern void
180 armoise_terminate (void);
181 
194 extern armoise_context *
196 
206 extern armoise_context *
208 
219 extern armoise_context *
221 
232 extern void
234 
242 extern armoise_context *
244 
253 extern int
255 
266 extern int
268 
282 extern void *
284 
300 extern void
301 armoise_context_add (armoise_context *ctx, ccl_ustring id, void *object);
302 
314 extern ccl_hash *
316 
327 extern ccl_list *
329 
334 extern int
336 
342 extern ccl_tree *
344 
351 extern void
353  ccl_tree *tree);
354 
367 extern armoise_predicate *
369  int nb_indices, const int *indices);
370 
375 extern const armoise_predicate *
377  int nb_indices, const int *indices);
378 
384 extern int
386 
393 extern void
395 
401 extern armoise_variable *
403 
412 extern armoise_variable *
414 
415 /*
416  * \brief Adds a new reference to \a variable.
417  *
418  * This function increments the counter of references to \a variable.
419  *
420  * \param variable the variable newly referenced
421  * \pre variable != NULL
422  *
423  * \return the pointer to \a variable
424  */
425 extern armoise_variable *
426 armoise_variable_add_reference (armoise_variable *variable);
427 
438 extern void
440 
447 extern ccl_ustring
449 
456 extern armoise_type *
458 
466 extern const armoise_domain *
468 
480 extern void
482  const armoise_domain *D);
483 
490 extern void
492 
502 extern armoise_predicate *
504 
513 extern armoise_predicate *
515 
523 extern armoise_predicate *
525 
534 extern armoise_predicate *
536 
544 extern armoise_predicate *
546 
568 extern armoise_predicate *
570  int nb_indices, const int *indices);
571 
585 extern armoise_predicate *
587  armoise_predicate *P2);
588 
602 extern armoise_predicate *
604  armoise_predicate *P1,
605  armoise_predicate *P2);
606 
621 extern armoise_predicate *
623  armoise_predicate *P2);
624 
637 extern armoise_predicate *
639  armoise_predicate *P2);
640 
653 extern armoise_predicate *
655  armoise_predicate *P);
656 
671 extern armoise_predicate *
673  armoise_predicate *P2);
674 
689 extern armoise_predicate *
691  armoise_predicate *P2);
692 
708 extern armoise_predicate *
710  armoise_predicate *P2);
711 
726 extern armoise_predicate *
728  armoise_predicate *P2);
729 
744 extern armoise_predicate *
746  armoise_predicate *P2);
747 
759 extern armoise_predicate *
761 
774 extern armoise_predicate *
776  armoise_predicate **comps);
777 
787 extern armoise_predicate *
789 
799 extern armoise_predicate *
801 
813 extern armoise_predicate *
815  armoise_term **values);
816 
829 extern armoise_predicate *
831  armoise_predicate *P,
832  armoise_formula *def);
833 
844 extern armoise_predicate *
846 
857 extern void
859 
867 extern armoise_domain_attr
869 
880 extern int
882 
891 extern armoise_type *
893 
902 extern armoise_context *
904 
911 extern void
913 
920 extern void
922 
932 extern void
934 
947 extern void
949 
962 
978 extern const armoise_predicate *
980 
985 extern armoise_predicate *
987 
994 extern int
996 
1010 extern armoise_domain *
1012 
1024 extern int
1026 
1034 extern const armoise_term *
1036 
1044 extern const armoise_term *
1046  armoise_predicate **resultP);
1047 
1055 extern const armoise_formula *
1057 
1068 extern void
1070  ccl_ustring *p_name, int *p_nb_indices,
1071  const int **p_indices);
1072 
1083 extern armoise_formula *
1085 
1096 extern void
1098 
1105 extern armoise_formula_kind
1107 
1119 extern armoise_formula *
1121 
1132 extern armoise_formula *
1134 
1145 extern armoise_formula *
1147 
1158 extern armoise_formula *
1160 
1171 extern armoise_formula *
1173 
1184 extern armoise_formula *
1186 
1195 extern armoise_formula *
1197 
1208 extern armoise_formula *
1210 
1221 extern armoise_formula *
1223 
1234 extern armoise_formula *
1236 
1247 extern armoise_formula *
1249 
1260 extern armoise_formula *
1262 
1273 extern armoise_formula *
1275 
1284 extern armoise_formula *
1286 
1301 extern armoise_formula *
1303  armoise_formula *F);
1304 
1319 extern armoise_formula *
1321  armoise_formula *F);
1322 
1329 extern void
1331 
1344 extern void
1346 
1354 extern int
1356 
1365 extern const armoise_formula *
1367 
1375 extern int
1377 
1387 extern const armoise_formula *
1389 
1402 extern armoise_term *
1404  armoise_predicate **p_domain);
1405 
1406 
1413 extern armoise_term *
1415 
1422 extern armoise_predicate *
1424 
1431 extern armoise_term *
1433 
1440 extern armoise_term *
1442 
1453 extern armoise_term *
1455 
1466 extern void
1468 
1479 extern armoise_term_kind
1481 
1489 extern int
1491 
1501 extern int
1503 
1513 extern int
1515 
1522 extern armoise_type *
1524 
1531 extern armoise_variable *
1533 
1541 extern void
1542 armoise_term_get_value (const armoise_term *t, int *num, int *den);
1543 
1555 extern armoise_term *
1557 
1564 extern armoise_term *
1566 
1576 extern armoise_term *
1577 armoise_term_create_vector_element (armoise_term *variable, int index);
1578 
1589 extern armoise_term *
1590 armoise_term_create_constant (int num, int den);
1591 
1603 extern armoise_term *
1604 armoise_term_create_vector (int width, armoise_term **terms);
1605 
1612 extern armoise_term *
1614 
1623 extern armoise_term *
1625 
1634 extern armoise_term *
1636 
1645 extern armoise_term *
1647 
1656 extern armoise_term *
1658 
1667 extern armoise_term *
1669 
1676 extern void
1678 
1691 extern void
1692 armoise_term_get_variables (const armoise_term *t, ccl_list *variables);
1693 
1700 extern int
1702 
1716 extern const armoise_term *
1717 armoise_term_get_operand (const armoise_term *t, int i);
1718 
1725 extern const armoise_term *
1727 
1734 extern int
1736 
1740 extern armoise_type *
1742 
1750 extern armoise_type *
1751 armoise_type_create_product (int nb_subtypes, armoise_type **subtypes);
1752 
1759 extern int
1760 armoise_type_is_scalar (const armoise_type *type);
1761 
1772 extern armoise_type *
1774 
1785 extern void
1787 
1795 extern int
1796 armoise_type_get_width (const armoise_type *type);
1797 
1808 extern int
1810 
1817 extern void
1818 armoise_type_log (ccl_log_type log, const armoise_type *type);
1819 
1827 extern int
1828 armoise_type_equals (const armoise_type *type, const armoise_type *other);
1829 
1837 extern armoise_type **
1839 
1847 extern const armoise_type *
1848 armoise_type_get_subtype (const armoise_type *type, int i);
1849 
1856 extern armoise_type *
1857 armoise_type_duplicate (const armoise_type *type);
1858 
1863 
1868 
1873 
1878 
1884 extern armoise_domain *
1886 
1891 extern armoise_domain *
1892 armoise_domain_create (void);
1893 
1898 extern armoise_domain *
1900 
1910 extern armoise_domain *
1912 
1923 extern armoise_domain *
1925 
1936 extern void
1938 
1945 extern int
1947 
1954 extern int
1956 
1965 extern const armoise_domain *
1967 
1977 extern void
1979  const armoise_domain *di);
1980 
1987 extern int
1989 
1996 extern int
1998 
2006 extern void
2008 
2015 extern armoise_domain_attr
2017 
2024 extern int
2026 
2033 extern int
2035 
2042 extern void
2044 
2051 extern armoise_domain *
2053 
2062 extern int
2063 armoise_domain_equals (const armoise_domain *d1, const armoise_domain *d2);
2064 
2071 extern int
2073 
2074 END_C_DECLS
2075 
2076 #endif /* ! __ARMOISE_H__ */
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.
Definition: armoise.h:85
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.
Definition: armoise.h:148
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.
Definition: armoise.h:46
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.
Definition: armoise.h:118
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.
Definition: ccl-tree.h:40
struct armoise_predicate_st armoise_predicate
Abstract of an ARMOISE predicate.
Definition: armoise.h:51
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.
Definition: armoise.h:143
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 &lt; 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.
Definition: armoise.h:153
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.
Definition: ccl-list.h:33
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.
Definition: armoise.h:113
armoise_formula_kind
Kind of formula.
Definition: armoise.h:91
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 &lt; 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.
Definition: armoise.h:58
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 ...
Definition: ccl-string.h:34
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 &gt;= t2.
armoise_term_kind
Kind of term.
Definition: armoise.h:124
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 ...
Definition: ccl-log.h:50
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 &lt;= 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.
Definition: ccl-hash.h:57
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.
Message displayer.
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].