How to make an existing library conformant to APRON ?

We briefly describe here how to connect an existing library to the common interface.

First, the library has to expose an interface which conforms to the level 0 of the interface (module abstract0). All the functions described in this module should be defined. If a function is not really implemented, at least it shoulld contain the code raising the exception EXC_NOT_IMPLEMENTED. The implementor may use any functions of the files ap_coeff.h, ap_linexpr0.h, ap_lincons0.h, ap_generator0.h and ap_manager.h to help the job of converting datatypes of the interface to internal datatypes used inside the library.

Second and last, the library should expose an initialization function that allocates and initializes properly an object of type manager_t. For this purpose, the module manager offers the utility functions manager_alloc. As an example, we give the definition of the function allocating a manager as implemented in the NewPolka.

1. Header of the function:

   manager_t* pk_manager_alloc(
     bool strict /* specific parameter: do we allow strict constaints ? */
   )
   

2. Allocation and initialisation of global data specific to NewPolka:

   {
     pk_internal_t* pk = pk_internal_alloc(strict); /* allocation */
     pk_set_approximate_max_coeff_size(pk, 1);
       /* initialization of specific functions
          (not offered in the common interface) */
   }
   

3. Allocation of the manager itself:

     manager_t* man = ap_manager_alloc("polka","2.0",
   				    pk, (void (*)(void*))pk_internal_free);
   

   We provide resp. name, version, internal specific manager, and the function to free it.

   The function manager_alloc sets the options of the common interface to their default value (see documentation).

4. Initialization of the “virtual” table: we need to connect the generic functions of the interface (eg, abstract_meet, \ldots) to the actual functions of the library.

     funptr = man->funptr;
   
     funptr[fun_minimize] = &poly_minimize;
     funptr[fun_canonicalize] = &poly_canonicalize;
     funptr[fun_hash] = &poly_hash;
     funptr[fun_approximate] = &poly_approximate;
     funptr[fun_fprint] = &poly_fprint;
     funptr[fun_fprintdiff] = &poly_fprintdiff;
     funptr[fun_fdump] = &poly_fdump;
     ...
   

5. Last, we return the allocated manager:

     return man;
   }
   

That’s all for the implementor side.