Tests on abstract values of level 1

In abstract tests,

• true means that the predicate is certainly true;
• false means false or don't know (an exception has occurred, or the exact computation was considered too expensive to be performed, according to the options).

Function: bool ap_abstract1_is_bottom (ap_manager_t* man, ap_abstract1_t* a)

Function: bool ap_abstract1_is_top (ap_manager_t* man, ap_abstract1_t* a)

Emtpiness and universality tests.

Function: bool ap_abstract1_is_leq (ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2)

Function: bool ap_abstract1_is_eq (ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2)

Inclusion and equality tests.

Function: bool ap_abstract1_sat_interval (ap_manager_t* man, ap_abstract1_t* a, ap_var_t var, ap_interval_t* interval)

Is the variable var included in the interval interval in the abstract value a ?

Function: bool ap_abstract1_sat_lincons (ap_manager_t* man, ap_abstract1_t* a, ap_lincons1_t* cons)

Function: bool ap_abstract1_sat_tcons (ap_manager_t* man, ap_abstract1_t* a, ap_tcons1_t* cons)

Does the abstract value a satisfy the constraint cons ?

Function: bool ap_abstract1_is_variable_unconstrained (ap_manager_t* man, ap_abstract1_t* a, ap_var_t var)

Is the dimension dim unconstrained in the abstract value a ? If it is the case, we have forget(man,a,dim) == a.