cprover
|
#include <interval_template.h>
Public Member Functions | |
interval_templatet () | |
interval_templatet (const T &x) | |
interval_templatet (const T &l, const T &u) | |
const T & | get_lower () const |
const T & | get_upper () const |
bool | empty () const |
bool | is_bottom () const |
bool | is_top () const |
bool | singleton () const |
void | make_le_than (const T &v) |
void | make_ge_than (const T &v) |
void | join (const interval_templatet< T > &i) |
void | meet (const interval_templatet< T > &i) |
void | intersect_with (const interval_templatet &i) |
void | approx_union_with (const interval_templatet &i) |
Public Attributes | |
bool | lower_set |
bool | upper_set |
T | lower |
T | upper |
Definition at line 18 of file interval_template.h.
|
inline |
Definition at line 21 of file interval_template.h.
|
inlineexplicit |
Definition at line 26 of file interval_template.h.
|
inlineexplicit |
Definition at line 34 of file interval_template.h.
|
inline |
Definition at line 145 of file interval_template.h.
References interval_templatet< T >::lower, interval_templatet< T >::lower_set, interval_templatet< T >::upper, and interval_templatet< T >::upper_set.
Referenced by interval_templatet< T >::join().
|
inline |
Definition at line 55 of file interval_template.h.
References interval_templatet< T >::upper.
Referenced by interval_templatet< T >::is_bottom().
|
inline |
Definition at line 45 of file interval_template.h.
References interval_templatet< T >::lower.
|
inline |
Definition at line 50 of file interval_template.h.
References interval_templatet< T >::upper.
|
inline |
Definition at line 116 of file interval_template.h.
References interval_templatet< T >::lower, interval_templatet< T >::lower_set, interval_templatet< T >::upper, and interval_templatet< T >::upper_set.
Referenced by interval_templatet< T >::meet().
|
inline |
Definition at line 60 of file interval_template.h.
References interval_templatet< T >::empty().
Referenced by interval_domaint::assume_rec(), and interval_domaint::make_expression().
|
inline |
Definition at line 65 of file interval_template.h.
References interval_templatet< T >::upper_set.
Referenced by interval_domaint::make_expression().
|
inline |
Definition at line 105 of file interval_template.h.
References interval_templatet< T >::approx_union_with().
Referenced by interval_domaint::join().
|
inline |
Definition at line 90 of file interval_template.h.
Referenced by interval_domaint::assume_rec().
|
inline |
Definition at line 76 of file interval_template.h.
Referenced by interval_domaint::assume_rec().
|
inline |
Definition at line 111 of file interval_template.h.
References interval_templatet< T >::intersect_with().
Referenced by interval_domaint::assume_rec().
|
inline |
Definition at line 70 of file interval_template.h.
References interval_templatet< T >::upper.
T interval_templatet< T >::lower |
Definition at line 43 of file interval_template.h.
Referenced by interval_templatet< T >::approx_union_with(), interval_templatet< T >::get_lower(), interval_templatet< T >::intersect_with(), lower_interval(), interval_domaint::make_expression(), operator<<(), and operator==().
bool interval_templatet< T >::lower_set |
Definition at line 42 of file interval_template.h.
Referenced by interval_templatet< T >::approx_union_with(), interval_templatet< T >::intersect_with(), lower_interval(), interval_domaint::make_expression(), and operator==().
T interval_templatet< T >::upper |
Definition at line 43 of file interval_template.h.
Referenced by interval_templatet< T >::approx_union_with(), interval_templatet< T >::empty(), interval_templatet< T >::get_upper(), interval_templatet< T >::intersect_with(), interval_domaint::make_expression(), operator==(), interval_templatet< T >::singleton(), and upper_interval().
bool interval_templatet< T >::upper_set |
Definition at line 42 of file interval_template.h.
Referenced by interval_templatet< T >::approx_union_with(), interval_templatet< T >::intersect_with(), interval_templatet< T >::is_top(), interval_domaint::make_expression(), operator==(), and upper_interval().