We manipulate here expressions of the form
a_0.x_0 + ... + a_n.x_n + b
where the coefficients a_0, ..., a_n, b are of
ap_coeff_t type (either scalars or intervals) and the variables
x_0, ... , x_n are of type ap_var_t.
The semantics of linear expressions is exact, in the sense that the
arithmetic operations are interpreted in the real (or rational)
numbers. However, abstract domains are free to overapproximate this
exact semantics (this may occur when converting rational scalars to
double type for instance).
A special remark concerns integer variables. Abstract domains are assumed to perform the operations involving linear expressions using a real/rational semantics, and then possibly to reduce the result using the knowledge that integer variables may only take integer values.
This semantics coincides with the natural integer semantics of expressions involving only integer variables only if the involved coefficients are all integers.
A typical counter-example to this is an assignement y := 1/3 x where x and y are integer variables. If this assignement is applied to the BOX abstract domain value x in [1;1], it may lead to the bottom value, because one will first obtain y in [1/3;1/3] by real/rational computations, and this may be reduced to the empty interval because y is integer and the interval contains no integer values.
If you need expressions with a less simple semantics (mixing integer, real/rational and floating-point semantics with casts), you should use tree expressions (see Tree expressions of level 1 (ap_texpr1.h)).
(Internal) type of interval linear expressions.
Linear expressions of level 1 are created as objects of type
ap_linexpr1_t, not as pointers of type ap_linexpr1_t*.
For information:
typedef struct ap_linexpr1_t {
ap_linexpr0_t* linexpr0;
ap_environment_t* env;
} ap_linexpr1_t;
ap_linexpr1_t ap_linexpr1_make (ap_environment_t* env, ap_linexpr_discr_t lin_discr, size_t size) ¶Build a linear expressions on the environment env, with by default coefficients of type SCALAR and DOUBLE.
If lin_discr selects a dense representation, the size of the expression is the size of the environment. Otherwise, the initial size is given by size and the expression may be resized lazily.
void ap_linexpr1_minimize (ap_linexpr1_t* expr) ¶Reduce the coefficients (transform intervals into scalars when possible). In case of sparse representation, also remove zero coefficients.
ap_linexpr1_t ap_linexpr1_copy (ap_linexpr1_t* expr) ¶Duplication.
void ap_linexpr1_clear (ap_linexpr1_t expr) ¶Clear the linear expression.
void ap_linexpr1_fprint (FILE* stream, ap_linexpr1_t* expr) ¶Print the linear expression on stream stream.
bool ap_linexpr1_is_integer (ap_linexpr1_t* expr) ¶Does the expression depends only on integer variables ?
bool ap_linexpr1_is_real (ap_linexpr1_t* expr) ¶Does the expression depends only on real variables ?
bool ap_linexpr1_is_linear (ap_linexpr1_t* expr) ¶Return true iff all involved coefficients are scalars.
bool ap_linexpr1_is_quasilinear (ap_linexpr1_t* expr) ¶Return true iff all involved coefficients but the constant are scalars.
ap_environment_t* ap_linexpr1_envref (ap_linexpr1_t* expr) ¶Get a reference to the underlying environment. Do not free it.
size_t ap_linexpr1_linexpr0ref (ap_linexpr1_t* expr) ¶Get a reference to the underlying linear expression of level 0. Do not free it.
ap_coefft* ap_linexpr1_cstref (ap_linexpr1_t* e) ¶Get a reference to the constant. Do not free it.
ap_coefft* ap_linexpr1_coeffref (ap_linexpr1_t* e, ap_var_t var) ¶Get a reference to the coefficient associated to the variable var in expression e.
Do not free it. In case of sparse representation, possibly induce the addition of a new linear term.
Return NULL if var is unknown in the environment of e.
void ap_linexpr1_get_cst (ap_coefft* coeff, ap_linexpr1_t* e) ¶Assign to coeff the constant coefficient of e.
bool ap_linexpr1_get_coeff (ap_coefft* coeff, ap_linexpr1_t* e, ap_var_t var) ¶Assign to coeff the coefficient of variable var in the expression e.
Return true in case ap_linexpr1_coeffref(e,dim) returns NULL.
Iterator on the coefficients associated to variables.
ap_linexpr1_ForeachLinterm(E,I,VAR,COEFF){ body }
executes the body for each pair (coeff,var) in the
expression e. coeff is a reference to the coefficient
associated to variable var in e. i is an
auxiliary variable used internally by the macro.
bool ap_linexpr1_set_list (ap_linexpr1_t* e, ...) ¶This function assign the linear expression e from a list of tags
of type ap_coefftag_t, each followed by a number of arguments
as specified in the definition of the type ap_coefftag_t
(see Access to linear expressions of level 0). The list should end
with the tag AP_COEFF_END. The only difference with level 0 is that variables replace dimensions in the list.
Return true in case ap_linexpr1_coeffref (e,dim)
returns NULL for one of the variables involved.
Here is a typical example, in the case where ap_var_t is actually char* (the default):
ap_linexpr1_set_list(e, AP_COEFF_S_INT, 3, "x", AP_COEFF_S_FRAC, 3,2, "y", AP_COEFF_S_DOUBLE, 4.1, "z", AP_CST_I_DOUBLE, -2.4, 3.6, AP_END); /* Do not forget the last tatg ! */
which transforms an null expression into 3 x + 3/2 y + 4.1 z + [-2.4,3.6]
and is equivalent to:
ap_linexpr1_set_coeff_scalar_int(e, "x", 3); ap_linexpr1_set_coeff_scalar_frac(e, "y", 3,2); ap_linexpr1_set_coeff_scalar_double(e, "z", 4.1); ap_linexpr1_set_cst_interval_double(e, -2.4, 3.6);
void ap_linexpr1_set_cst (ap_linexpr1_t* e, ap_coefft* coeff) ¶void ap_linexpr1_set_cst_scalar (ap_linexpr1_t* e, ap_scalar_t* scalar) ¶void ap_linexpr1_set_cst_scalar_int (ap_linexpr1_t* e, int num) ¶void ap_linexpr1_set_cst_scalar_frac (ap_linexpr1_t* e, int num, unsigned int den) ¶void ap_linexpr1_set_cst_scalar_double (ap_linexpr1_t* e, double num) ¶void ap_linexpr1_set_cst_interval (ap_linexpr1_t* e, ap_interval_t* itv) ¶void ap_linexpr1_set_cst_interval_scalar (ap_linexpr1_t* e, ap_scalar_t* inf, ap_scalar_t* sup) ¶void ap_linexpr1_set_cst_interval_int (ap_linexpr1_t* e, int inf, int sup) ¶void ap_linexpr1_set_cst_interval_frac (ap_linexpr1_t* e, int numinf, unsigned int deninf, int numsup, unsigned int densup) ¶void ap_linexpr1_set_cst_interval_double (ap_linexpr1_t* e, double inf, double sup) ¶Set the constant coefficient of expression e.
bool ap_linexpr1_set_coeff (ap_linexpr1_t* e, ap_var_t var, ap_coefft* coeff) ¶bool ap_linexpr1_set_coeff_scalar (ap_linexpr1_t* e, ap_var_t var, ap_scalar_t* scalar) ¶bool ap_linexpr1_set_coeff_scalar_int (ap_linexpr1_t* e, ap_var_t var, int num) ¶bool ap_linexpr1_set_coeff_scalar_frac (ap_linexpr1_t* e, ap_var_t var, int num, unsigned int den) ¶bool ap_linexpr1_set_coeff_scalar_double (ap_linexpr1_t* e, ap_var_t var, double num) ¶bool ap_linexpr1_set_coeff_interval (ap_linexpr1_t* e, ap_var_t var, ap_interval_t* itv) ¶bool ap_linexpr1_set_coeff_interval_scalar (ap_linexpr1_t* e, ap_var_t var, ap_scalar_t* inf, ap_scalar_t* sup) ¶bool ap_linexpr1_set_coeff_interval_int (ap_linexpr1_t* e, ap_var_t var, int inf, int sup) ¶bool ap_linexpr1_set_coeff_interval_frac (ap_linexpr1_t* e, ap_var_t var,int numinf, unsigned int deninf, int numsup, unsigned int densup) ¶void ap_linexpr1_set_coeff_interval_double (ap_linexpr1_t* e, ap_var_t var, double inf, double sup) ¶Set the coefficient of the variable var of expression e.
Return true in case ap_linexpr1_coeffref(e,var) returns NULL.
bool ap_linexpr1_extend_environment (ap_linexpr1_t* nexpr, ap_linexpr1_t* expr, ap_environment_t* nenv) ¶bool ap_linexpr1_extend_environment_with (ap_linexpr1_t* expr, ap_environment_t* nenv) ¶Change the current environment of the expression expr with a
super-environment nenv. Return true if nenv is not
a superenvironment.
The first version store the result in the uninitialized *nexpr, the second one updates in-place its argument.