|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <algorithm>#include <iosfwd>#include <util/base/threeval.h>#include <util/message/message.h>#include <sstream>#include <util/arith/ieee_float.h>#include <optional>Go to the source code of this file.
Classes | |
| class | interval_templatet< T > |
| This class is used to store intervals in the form of lower <= upper. More... | |
Functions | |
| template<class T> | |
| tvt | operator<= (const interval_templatet< T > &a, const interval_templatet< T > &b) |
| template<class T> | |
| tvt | operator>= (const interval_templatet< T > &a, const interval_templatet< T > &b) |
| template<class T> | |
| tvt | operator< (const interval_templatet< T > &a, const interval_templatet< T > &b) |
| template<class T> | |
| tvt | operator> (const interval_templatet< T > &a, const interval_templatet< T > &b) |
| template<class T> | |
| bool | operator== (const interval_templatet< T > &a, const interval_templatet< T > &b) |
| template<class T> | |
| bool | operator!= (const interval_templatet< T > &a, const interval_templatet< T > &b) |
| template<class T> | |
| interval_templatet< T > | upper_interval (const T &u) |
| template<class T> | |
| interval_templatet< T > | lower_interval (const T &l) |
| template<class T> | |
| std::ostream & | operator<< (std::ostream &out, const interval_templatet< T > &i) |
| interval_templatet< T > lower_interval | ( | const T & | l | ) |
| bool operator!= | ( | const interval_templatet< T > & | a, |
| const interval_templatet< T > & | b ) |
| tvt operator< | ( | const interval_templatet< T > & | a, |
| const interval_templatet< T > & | b ) |
| std::ostream & operator<< | ( | std::ostream & | out, |
| const interval_templatet< T > & | i ) |
| tvt operator<= | ( | const interval_templatet< T > & | a, |
| const interval_templatet< T > & | b ) |
| bool operator== | ( | const interval_templatet< T > & | a, |
| const interval_templatet< T > & | b ) |
| tvt operator> | ( | const interval_templatet< T > & | a, |
| const interval_templatet< T > & | b ) |
| tvt operator>= | ( | const interval_templatet< T > & | a, |
| const interval_templatet< T > & | b ) |
| interval_templatet< T > upper_interval | ( | const T & | u | ) |