libapron-dev 0.9.10-5.2ubuntu3 / usr / include / ap_abstract0.h

/* ************************************************************************* */
/* ap_abstract0.h: generic operations on numerical abstract values */
/* ************************************************************************* */

/* This file is part of the APRON Library, released under LGPL license.  Please
   read the COPYING file packaged in the distribution */

#ifndef _AP_ABSTRACT0_H_
#define _AP_ABSTRACT0_H_

typedef struct ap_abstract0_t ap_abstract0_t;

#include "ap_manager.h"
#include "ap_expr0.h"

#ifdef __cplusplus
extern "C" {
#endif

/* Generic abstract value at level 0 */
struct ap_abstract0_t {
  void* value;       /* Abstract value of the underlying library */
  ap_manager_t* man; /* Used to identify the effective type of value */
};

/* ********************************************************************** */
/* I. General management */
/* ********************************************************************** */

/* ============================================================ */
/* I.1 Memory */
/* ============================================================ */

ap_abstract0_t* ap_abstract0_copy(ap_manager_t* man, ap_abstract0_t* a);
  /* Return a copy of an abstract value, on
     which destructive update does not affect the initial value. */

void ap_abstract0_free(ap_manager_t* man, ap_abstract0_t* a);
  /* Free all the memory used by the abstract value */

size_t ap_abstract0_size(ap_manager_t* man, ap_abstract0_t* a);
  /* Return the abstract size of an abstract value (see ap_manager_t) */


/* ============================================================ */
/* I.2 Control of internal representation */
/* ============================================================ */


void ap_abstract0_minimize(ap_manager_t* man, ap_abstract0_t* a);
  /* Minimize the size of the representation of a.
     This may result in a later recomputation of internal information.
  */

void ap_abstract0_canonicalize(ap_manager_t* man, ap_abstract0_t* a);
  /* Put the abstract value in canonical form. (not yet clear definition) */

int ap_abstract0_hash(ap_manager_t* man, ap_abstract0_t* a);
  /* Return an hash value for the abstract value.  Two abstract values in
     canonical from (according to @code{ap_abstract1_canonicalize}) and
     considered as equal by the function ap_abstract0_is_eq should be given the
     same hash value (this implies more or less a canonical form).
  */


void ap_abstract0_approximate(ap_manager_t* man, ap_abstract0_t* a, int algorithm);
  /* Perform some transformation on the abstract value, guided by the
     field algorithm.

     The transformation may lose information.  The argument "algorithm"
     overrides the field algorithm of the structure of type ap_funopt_t
     associated to ap_abstract0_approximate (commodity feature). */

/* ============================================================ */
/* I.3 Printing */
/* ============================================================ */


void ap_abstract0_fprint(FILE* stream,
			 ap_manager_t* man, ap_abstract0_t* a, char** name_of_dim);
  /* Print the abstract value in a pretty way, using function
     name_of_dim to name dimensions */


void ap_abstract0_fprintdiff(FILE* stream,
			     ap_manager_t* man,
			     ap_abstract0_t* a1, ap_abstract0_t* a2,
			     char** name_of_dim);
  /* Print the difference between a1 (old value) and a2 (new value),
     using function name_of_dim to name dimensions.
     The meaning of difference is library dependent. */


void ap_abstract0_fdump(FILE* stream, ap_manager_t* man, ap_abstract0_t* a);
  /* Dump the internal representation of an abstract value,
     for debugging purposes */

/* ============================================================ */
/* I.4 Serialization */
/* ============================================================ */


ap_membuf_t ap_abstract0_serialize_raw(ap_manager_t* man, ap_abstract0_t* a);
  /* Allocate a memory buffer (with malloc), output the abstract value in raw
     binary format to it and return a pointer on the memory buffer and the size
     of bytes written.  It is the user responsibility to free the memory
     afterwards (with free). */


ap_abstract0_t* ap_abstract0_deserialize_raw(ap_manager_t* man, void* ptr, size_t* size);
  /* Return the abstract value read in raw binary format from the input stream
     and store in size the number of bytes read */

/* ********************************************************************** */
/* II. Constructor, accessors, tests and property extraction */
/* ********************************************************************** */

/* ============================================================ */
/* II.1 Basic constructors */
/* ============================================================ */

/* We assume that dimensions [0..intdim-1] correspond to integer variables, and
   dimensions [intdim..intdim+realdim-1] to real variables */

ap_abstract0_t* ap_abstract0_bottom(ap_manager_t* man, size_t intdim, size_t realdim);
  /* Create a bottom (empty) value */


ap_abstract0_t* ap_abstract0_top(ap_manager_t* man, size_t intdim, size_t realdim);
  /* Create a top (universe) value */

ap_abstract0_t* ap_abstract0_of_box(ap_manager_t* man,
				    size_t intdim, size_t realdim,
				    ap_interval_t** tinterval);
  /* Abstract an hypercube defined by the array of intervals
     of size intdim+realdim */

/* ============================================================ */
/* II.2 Accessors */
/* ============================================================ */

ap_dimension_t ap_abstract0_dimension(ap_manager_t* man, ap_abstract0_t* a);
  /* Return the dimensionality of the abstract values */

/* ============================================================ */
/* II.3 Tests */
/* ============================================================ */

/* In abstract tests,

   - true means that the predicate is certainly true.

   - false means by default don't know (an exception has occurred, or the exact
     computation was considered too expensive to be performed).

     However, if the flag exact in the manager is true, then false means really
     that the predicate is false.
*/

bool ap_abstract0_is_bottom(ap_manager_t* man, ap_abstract0_t* a);
bool ap_abstract0_is_top(ap_manager_t* man, ap_abstract0_t* a);


bool ap_abstract0_is_leq(ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2);
  /* inclusion check */
bool ap_abstract0_is_eq(ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2);
  /* equality check */

bool ap_abstract0_sat_lincons(ap_manager_t* man, ap_abstract0_t* a, ap_lincons0_t* lincons);
bool ap_abstract0_sat_tcons(ap_manager_t* man, ap_abstract0_t* a, ap_tcons0_t* tcons);
  /* does the abstract value satisfy the constraint ? */
bool ap_abstract0_sat_interval(ap_manager_t* man, ap_abstract0_t* a,
			      ap_dim_t dim, ap_interval_t* interval);
  /* is the dimension included in the interval in the abstract value ? */

bool ap_abstract0_is_dimension_unconstrained(ap_manager_t* man,
					     ap_abstract0_t* a, ap_dim_t dim);
  /* is the dimension unconstrained in the abstract value ?  If it is the case,
     we have forget(man,a,dim) == a */

/* ============================================================ */
/* II.4 Extraction of properties */
/* ============================================================ */

ap_interval_t* ap_abstract0_bound_linexpr(ap_manager_t* man,
					  ap_abstract0_t* a, ap_linexpr0_t* expr);
ap_interval_t* ap_abstract0_bound_texpr(ap_manager_t* man,
					ap_abstract0_t* a, ap_texpr0_t* expr);
  /* Returns the interval taken by the expression
     over the abstract value */


ap_interval_t* ap_abstract0_bound_dimension(ap_manager_t* man,
					    ap_abstract0_t* a, ap_dim_t dim);
  /* Returns the interval taken by the dimension
     over the abstract value */


ap_lincons0_array_t ap_abstract0_to_lincons_array(ap_manager_t* man, ap_abstract0_t* a);
  /* Converts an abstract value to a polyhedra
     (conjunction of linear constraints).

     The constraints are normally guaranteed to be really linear (without intervals) */

ap_tcons0_array_t ap_abstract0_to_tcons_array(ap_manager_t* man, ap_abstract0_t* a);
  /* Converts an abstract value to conjunction of tree expressions constraints.

     The constraints are normally guaranteed to be scalar (without intervals) */

ap_interval_t** ap_abstract0_to_box(ap_manager_t* man, ap_abstract0_t* a);
  /* Converts an abstract value to an interval/hypercube.
     The size of the resulting array is ap_abstract0_dimension(man,a).  This
     function can be reimplemented by using ap_abstract0_bound_linexpr */


ap_generator0_array_t ap_abstract0_to_generator_array(ap_manager_t* man, ap_abstract0_t* a);
  /* Converts an abstract value to a system of generators. */


/* ********************************************************************** */
/* III. Operations */
/* ********************************************************************** */

/* ============================================================ */
/* III.1 Meet and Join */
/* ============================================================ */


ap_abstract0_t* ap_abstract0_meet(ap_manager_t* man,
				  bool destructive, ap_abstract0_t* a1, ap_abstract0_t* a2);

ap_abstract0_t* ap_abstract0_join(ap_manager_t* man,
				  bool destructive, ap_abstract0_t* a1, ap_abstract0_t* a2);
  /* Meet and Join of 2 abstract values */


ap_abstract0_t* ap_abstract0_meet_array(ap_manager_t* man,
					ap_abstract0_t** tab, size_t size);

ap_abstract0_t* ap_abstract0_join_array(ap_manager_t* man,
					ap_abstract0_t** tab, size_t size);
  /* Meet and Join of an array of abstract values.
     Raises an [[exc_invalid_argument]] exception if [[size==0]]
     (no way to define the dimensionality of the result in such a case */


ap_abstract0_t*
ap_abstract0_meet_lincons_array(ap_manager_t* man,
				bool destructive, ap_abstract0_t* a, ap_lincons0_array_t* array);
ap_abstract0_t*
ap_abstract0_meet_tcons_array(ap_manager_t* man,
				bool destructive, ap_abstract0_t* a, ap_tcons0_array_t* array);
  /* Meet of an abstract value with a set of constraints */

ap_abstract0_t*
ap_abstract0_add_ray_array(ap_manager_t* man,
			   bool destructive, ap_abstract0_t* a, ap_generator0_array_t* array);
  /* Generalized time elapse operator */

/* ============================================================ */
/* III.2 Assignment and Substitutions */
/* ============================================================ */

ap_abstract0_t*
ap_abstract0_assign_linexpr_array(ap_manager_t* man,
				  bool destructive,
				  ap_abstract0_t* org,
				  ap_dim_t* tdim, ap_linexpr0_t** texpr, size_t size,
				  ap_abstract0_t* dest);
ap_abstract0_t*
ap_abstract0_assign_texpr_array(ap_manager_t* man,
				bool destructive,
				ap_abstract0_t* org,
				ap_dim_t* tdim, ap_texpr0_t** texpr, size_t size,
				ap_abstract0_t* dest);
ap_abstract0_t*
ap_abstract0_substitute_linexpr_array(ap_manager_t* man,
				      bool destructive,
				      ap_abstract0_t* org,
				      ap_dim_t* tdim, ap_linexpr0_t** texpr, size_t size,
				      ap_abstract0_t* dest);
ap_abstract0_t*
ap_abstract0_substitute_texpr_array(ap_manager_t* man,
				    bool destructive,
				    ap_abstract0_t* org,
				    ap_dim_t* tdim, ap_texpr0_t** texpr, size_t size,
				    ap_abstract0_t* dest);

  /* Parallel Assignment and Substitution of several dimensions by
     linear/tree expressions in abstract value org.

     dest is an optional argument. If not NULL, semantically speaking,
     the result of the transformation is intersected with dest. This is
     useful for precise backward transformations in lattices like intervals or
     octagons. */

/* ============================================================ */
/* III.3 Projections */
/* ============================================================ */

ap_abstract0_t*
ap_abstract0_forget_array(ap_manager_t* man,
			  bool destructive,
			  ap_abstract0_t* a, ap_dim_t* tdim, size_t size,
			  bool project);

/* ============================================================ */
/* III.4 Change and permutation of dimensions */
/* ============================================================ */

ap_abstract0_t*
ap_abstract0_add_dimensions(ap_manager_t* man,
			    bool destructive,
			    ap_abstract0_t* a,ap_dimchange_t* dimchange,
			    bool project);
ap_abstract0_t*
ap_abstract0_remove_dimensions(ap_manager_t* man,
			       bool destructive,
			       ap_abstract0_t* a, ap_dimchange_t* dimchange);
  /* Size of the permutation is supposed to be equal to
     the dimension of the abstract value */
ap_abstract0_t*
ap_abstract0_permute_dimensions(ap_manager_t* man,
				bool destructive,
				ap_abstract0_t* a, ap_dimperm_t* perm);

/* ============================================================ */
/* III.5 Expansion and folding of dimensions */
/* ============================================================ */


ap_abstract0_t*
ap_abstract0_expand(ap_manager_t* man,
		    bool destructive,
		    ap_abstract0_t* a, ap_dim_t dim, size_t n);
  /* Expand the dimension dim into itself + n additional dimensions.
     It results in (n+1) unrelated dimensions having same
     relations with other dimensions. The (n+1) dimensions are put as follows:

     - original dimension dim

     - if the dimension is integer, the n additional dimensions are put at the
       end of integer dimensions; if it is real, at the end of the real
       dimensions.
  */


ap_abstract0_t*
ap_abstract0_fold(ap_manager_t* man,
		  bool destructive,
		  ap_abstract0_t* a, ap_dim_t* tdim, size_t size);
  /* Fold the dimensions in the array tdim of size n>=1 and put the result
     in the first dimension in the array. The other dimensions of the array
     are then removed (using ap_abstract0_permute_remove_dimensions). */

/* ============================================================ */
/* III.6 Widening */
/* ============================================================ */

ap_abstract0_t* ap_abstract0_widening(ap_manager_t* man,
				      ap_abstract0_t* a1, ap_abstract0_t* a2);

/* ============================================================ */
/* III.7 Closure operation */
/* ============================================================ */

/* Returns the topological closure of a possibly opened abstract value */
ap_abstract0_t* ap_abstract0_closure(ap_manager_t* man, bool destructive, ap_abstract0_t* a);

/* ********************************************************************** */
/* IV. Functions offered by the APRON interface */
/* ********************************************************************** */

/* These functions do not correspond to functions in the underlying library. */

static inline
ap_manager_t* ap_abstract0_manager(ap_abstract0_t* a)
  { return a->man; }
  /* Return a reference to the manager contained in the abstract value.
     The reference should not be freed */

ap_abstract0_t* ap_abstract0_of_lincons_array(ap_manager_t* man,
					      size_t intdim, size_t realdim,
					      ap_lincons0_array_t* array);
ap_abstract0_t* ap_abstract0_of_tcons_array(ap_manager_t* man,
					    size_t intdim, size_t realdim,
					    ap_tcons0_array_t* array);
  /* Abstract a conjunction of tree constraints */

ap_abstract0_t* ap_abstract0_assign_linexpr(ap_manager_t* man,
					    bool destructive,
					    ap_abstract0_t* org,
					    ap_dim_t dim, ap_linexpr0_t* expr,
					    ap_abstract0_t* dest);
ap_abstract0_t* ap_abstract0_assign_texpr(ap_manager_t* man,
					  bool destructive,
					  ap_abstract0_t* org,
					  ap_dim_t dim, ap_texpr0_t* expr,
					  ap_abstract0_t* dest);
ap_abstract0_t* ap_abstract0_substitute_linexpr(ap_manager_t* man,
						bool destructive,
						ap_abstract0_t* org,
						ap_dim_t dim, ap_linexpr0_t* expr,
						ap_abstract0_t* dest);
ap_abstract0_t* ap_abstract0_substitute_texpr(ap_manager_t* man,
					      bool destructive,
					      ap_abstract0_t* org,
					      ap_dim_t dim, ap_texpr0_t* expr,
					      ap_abstract0_t* dest);
  /* Assignment and Substitution of a single dimension by an expression in
     abstract value org.

     dest is an optional argument. If not NULL, semantically speaking,
     the result of the transformation is intersected with dest. This is
     useful for precise backward transformations in lattices like intervals or
     octagons.
 */

/* Applying an ap_dimchange2_t transformation (dimension adding followed by
   dimension removal/projection).  If project is true, the newly added
   dimension are projected on their 0-hyperplane. */
ap_abstract0_t* ap_abstract0_apply_dimchange2(ap_manager_t* man,
					      bool destructive,
					      ap_abstract0_t* a, ap_dimchange2_t* dimchange2,
					      bool project);

/* Widening with threshold */
ap_abstract0_t*
ap_abstract0_widening_threshold(ap_manager_t* man,
				ap_abstract0_t* a1, ap_abstract0_t* a2,
				ap_lincons0_array_t* array);

/* ********************************************************************** */
/* ********************************************************************** */
/* Internal functions */
/* ********************************************************************** */
/* ********************************************************************** */

ap_abstract0_t*
ap_abstract0_meetjoin(ap_funid_t funid,
		      /* either meet or join */
		      ap_manager_t* man, bool destructive,
		      ap_abstract0_t* a1, ap_abstract0_t* a2);
ap_abstract0_t*
ap_abstract0_asssub_linexpr(ap_funid_t funid,
			    /* either assign or substitute */
			    ap_manager_t* man,
			    bool destructive,
			    ap_abstract0_t* a,
			    ap_dim_t dim, ap_linexpr0_t* expr,
			    ap_abstract0_t* dest);
ap_abstract0_t*
ap_abstract0_asssub_linexpr_array(ap_funid_t funid,
				  /* either assign or substitute */
				  ap_manager_t* man,
				  bool destructive,
				  ap_abstract0_t* a,
				  ap_dim_t* tdim, ap_linexpr0_t** texpr, size_t size,
				  ap_abstract0_t* dest);
ap_abstract0_t*
ap_abstract0_asssub_texpr(ap_funid_t funid,
			    /* either assign or substitute */
			  ap_manager_t* man,
			  bool destructive,
			  ap_abstract0_t* a,
			  ap_dim_t dim, ap_texpr0_t* expr,
			  ap_abstract0_t* dest);
ap_abstract0_t*
ap_abstract0_asssub_texpr_array(ap_funid_t funid,
				/* either assign or substitute */
				ap_manager_t* man,
				bool destructive,
				ap_abstract0_t* a,
				ap_dim_t* tdim, ap_texpr0_t** texpr, size_t size,
				ap_abstract0_t* dest);
#ifdef __cplusplus
}
#endif

#endif