[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

Additional functions on abstract values of level 1

Function: ap_abstract1_t ap_abstract1_of_lincons_array (ap_manager_t* man, ap_environment_t* env, ap_lincons1_array_t* array)
Function: ap_abstract1_t ap_abstract1_of_tcons_array (ap_manager_t* man, ap_environment_t* env, ap_tcons1_array_t* array)
Abstract a conjunction of constraints. The environment of the array should be a subset of the environment env.

Function: ap_abstract1_t ap_abstract1_assign_linexpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_linexpr1_t* expr, ap_abstract1_t* dest)
Function: ap_abstract1_t ap_abstract1_substitute_linexpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_linexpr1_t* expr, ap_abstract1_t* dest)
Function: ap_abstract1_t ap_abstract1_assign_texpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_texpr1_t* expr, ap_abstract1_t* dest)
Function: ap_abstract1_t ap_abstract1_substitute_texpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_texpr1_t* expr, ap_abstract1_t* dest)
Assignement and Substitution of the dimension dim by the expression expr 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.

Function: ap_abstract1_t ap_abstract1_unify (ap_manager_t* man, bool destructive, ap_abstract1_t* a1, ap_abstract1_t* a2)
Unify two abstract values on their common variables, that is, embed them on the least common environment and then compute their meet. The result is defined on the least common environment.

For instance, the unification of 1<=x<=3 and x=y defined on { x, y } and 2<=z<=4 and z=y defined on {y,z } results in 2<=x<=3 and x=y=z defined on {x,y,z}.

Function: ap_linexpr1_t ap_abstract1_quasilinear_of_intlinear (ap_manager_t* man, ap_abstract1_t* a, ap_linexpr1_t* expr)
Evaluate the interval linear expression expr on the abstract value a and approximate it by a quasilinear expression.

This implies calls to ap_abstract0_bound_dimension.

Function: ap_linexpr1_t ap_abstract1_intlinear_of_tree (ap_manager_t* man, ap_abstract1_t* a, ap_texpr1_t* expr, bool quasilinear)
Evaluate the tree expression expr on the abstract value a and approximate it by an interval linear (resp. quasilinear if quasilinear is true) expression.

This implies calls to ap_abstract0_bound_dimension.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

This document was generated on September, 10 2009 using texi2html